Ignore:
Timestamp:
Jan 18, 2012, 6:17:37 PM (8 years ago)
Author:
boender
Message:
  • changes to Assembly for integration with Policy and easier use of _safe functions (with CSC)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r1616 r1649  
    12881288 #H >H * #H1 try (whd in ⊢ (% → ?); * #H2)
    12891289 try (whd in ⊢ (% → ?); * #H3) whd in ⊢ (% → ?); #H4
    1290  [ whd in match fetch; normalize nodelta <H1 (*XXX
     1290 [ whd in match fetch; normalize nodelta <H1 ] cases daemon
     1291 (*XXX
    12911292   
    12921293 whd in ⊢ (let fetched ≝ ??% in ?) <H1 whd in ⊢ (let fetched ≝ % in ?)
     
    13171318               
    13181319lemma fetch_assembly_pseudo':
    1319  ∀program.∀pol:policy program.∀ppc,lookup_labels,lookup_datalabels.
     1320 ∀lookup_labels.∀pol:policy_type lookup_labels.∀ppc,lookup_datalabels.
    13201321  ∀pi,code_memory,len,assembled,instructions,pc.
    13211322   let expansion ≝ pol ppc in
    1322    Some ? instructions = expand_pseudo_instruction_safe lookup_labels lookup_datalabels (bitvector_of_nat ? pc) expansion pi →
    1323     Some … 〈len,assembled〉 = assembly_1_pseudoinstruction_safe program pol ppc (bitvector_of_nat ? pc) lookup_labels lookup_datalabels pi →
     1323   instructions = expand_pseudo_instruction lookup_labels ppc expansion lookup_datalabels pi →
     1324    〈len,assembled〉 = assembly_1_pseudoinstruction lookup_labels pol ppc lookup_datalabels pi →
    13241325     encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →
    13251326      fetch_many code_memory (bitvector_of_nat … (pc + len)) (bitvector_of_nat … pc) instructions.
    1326  #program #pol #ppc #lookup_labels #lookup_datalabels #pi #code_memory #len #assembled #instructions #pc
    1327  #EQ1 whd in ⊢ (???% → ?) <EQ1 whd in ⊢ (???% → ?) #EQ2
    1328  cases (pair_destruct ?????? (option_destruct_Some … EQ2)) -EQ2; #EQ2a #EQ2b
    1329  >EQ2a >EQ2b -EQ2a EQ2b;
     1327 #lookup_labels #pol #ppc #lookup_datalabels #pi #code_memory #len #assembled #instructions #pc
     1328 #EQ1 whd in ⊢ (???% → ?); <EQ1 whd in ⊢ (???% → ?); #EQ2
     1329 cases (pair_destruct ?????? EQ2) -EQ2; #EQ2a #EQ2b
     1330 >EQ2a >EQ2b -EQ2a -EQ2b;
    13301331  generalize in match (pc + |flatten … (map … assembly1 instructions)|); #final_pc
    1331   generalize in match pc elim instructions
    1332   [ #pc whd in ⊢ (% → %) #H >H @eq_bv_refl
     1332  generalize in match pc; elim instructions
     1333  [ #pc whd in ⊢ (% → %); #H >H @eq_bv_refl
    13331334  | #i #tl #IH #pc #H whd cases (encoding_check_append … H); -H; #H1 #H2 whd
    1334     generalize in match (fetch_assembly pc i code_memory … (refl …) H1)
    1335     cases (fetch code_memory (bitvector_of_nat … pc)) #newi_pc #ticks whd in ⊢ (% → %)
    1336     cases newi_pc #newi #newpc whd in ⊢ (% → %) #K cases (conjunction_true … K) -K; #K1
     1335    generalize in match (fetch_assembly pc i code_memory … (refl …) H1);
     1336    cases (fetch code_memory (bitvector_of_nat … pc)) #newi_pc #ticks whd in ⊢ (% → %);
     1337    cases newi_pc #newi #newpc whd in ⊢ (% → %); #K cases (conjunction_true … K) -K; #K1
    13371338    cases (conjunction_true … K1) -K1; #K1 #K2 #K3 % try %
    13381339    [ @K1 | @eqb_true_to_eq <(eq_instruction_to_eq … K1) @K2 | >(eq_bv_eq … K3) @IH @H2 ]
     
    13451346(* CSC: soo long next one; can we merge with previous one now? *)
    13461347lemma fetch_assembly_pseudo:
    1347  ∀program.∀pol:policy program.∀ppc.
    1348   ∀code_memory.
    1349    let lookup_labels ≝ ? in
    1350    let lookup_datalabels ≝ ? in
    1351    let pc ≝ ? in
    1352    let pi ≝  \fst  (fetch_pseudo_instruction (\snd  program) ppc) in
    1353    let instructions ≝ expand_pseudo_instruction program pol ppc lookup_labels lookup_datalabels pc (refl …) (refl …) (refl …) in
    1354    let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels pi (refl …) (refl …) (refl …) in
    1355      encoding_check code_memory pc (bitvector_of_nat … (nat_of_bitvector ? pc + len)) assembled →
    1356       fetch_many code_memory (bitvector_of_nat … (nat_of_bitvector ? pc + len)) pc instructions.
    1357  #program #pol #ppc #code_memory
    1358  letin lookup_labels ≝ (λx:Identifier
    1359     .sigma program pol (address_of_word_labels_code_mem (\snd  program) x))
    1360  letin lookup_datalabels ≝
    1361   (λx:BitVector 16
    1362     .lookup Identifier 16 x (construct_datalabels (\fst  program)) (zero 16))
    1363  letin pc ≝ (sigma program pol ppc)
    1364  letin pi ≝ (\fst  (fetch_pseudo_instruction (\snd  program) ppc))
    1365  letin instructions ≝ (expand_pseudo_instruction program pol ppc lookup_labels lookup_datalabels pc (refl …) (refl …) (refl …))
    1366  @pair_elim' #len #assembled #EQ1 #H
     1348  ∀program:pseudo_assembly_program.
     1349  let lookup_labels ≝ λx:Identifier.(address_of_word_labels_code_mem (\snd  program) x) in
     1350  ∀pol:(policy program).∀ppc.∀code_memory.
     1351  let lookup_datalabels ≝ λx:Identifier.lookup_def … (construct_datalabels (\fst  program)) x (zero 16) in
     1352  let pc ≝ sigma program pol ppc in
     1353  let pi ≝  \fst  (fetch_pseudo_instruction (\snd program) ppc) in
     1354  let instructions ≝ expand_pseudo_instruction lookup_labels ppc (pol lookup_labels ppc) lookup_datalabels pi in
     1355  let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels (pol lookup_labels) ppc lookup_datalabels pi in
     1356    encoding_check code_memory pc (bitvector_of_nat … (nat_of_bitvector ? pc + len)) assembled →
     1357     fetch_many code_memory (bitvector_of_nat … (nat_of_bitvector ? pc + len)) pc instructions.
     1358 #program letin lookup_labels ≝ (λx.?) #pol #ppc #code_memory
     1359 letin lookup_datalabels ≝ (λx.?)
     1360 letin pc ≝ (sigma ???) letin pi ≝ (fst ???) 
     1361 letin instructions ≝ (expand_pseudo_instruction ?????)
     1362 @pair_elim #len #assembled #EQ1 #H
    13671363 generalize in match
    1368   (fetch_assembly_pseudo' program pol ppc lookup_labels lookup_datalabels pi
    1369   code_memory len assembled instructions (nat_of_bitvector ? pc) ???) in ⊢ ?;
    1370  [ >bitvector_of_nat_nat_of_bitvector //
    1371  | >bitvector_of_nat_nat_of_bitvector normalize nodelta >(sig2 ?? (expand_pseudo_instruction …)) %
    1372  | >bitvector_of_nat_nat_of_bitvector <EQ1 @assembly_1_pseudoinstruction_ok1
    1373  | //]
     1364  (fetch_assembly_pseudo' lookup_labels ((pi1 ?? pol) lookup_labels) ppc lookup_datalabels pi code_memory len
     1365   assembled instructions (nat_of_bitvector ? pc)) in ⊢ ?;
     1366  >bitvector_of_nat_nat_of_bitvector >EQ1 normalize nodelta
     1367  #X @X //
    13741368qed.
    13751369
     
    13861380  let preamble ≝ \fst program in
    13871381  let datalabels ≝ construct_datalabels preamble in
    1388   let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in
    1389   let lookup_datalabels ≝ λx. lookup ?? x datalabels (zero ?) in
     1382  let lookup_labels ≝ λx. address_of_word_labels_code_mem (\snd program) x in
     1383  let lookup_datalabels ≝ λx. lookup_def ?? datalabels x (zero ?) in
    13901384  ∀ppc.
    13911385  let pi_newppc ≝ fetch_pseudo_instruction (\snd program) ppc in
    13921386   ∀len,assembledi.
    1393      〈len,assembledi〉 = assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels (\fst pi_newppc) (refl …) (refl …) (refl …) →
     1387     〈len,assembledi〉 = assembly_1_pseudoinstruction lookup_labels (pol lookup_labels) ppc lookup_datalabels (\fst pi_newppc) →
    13941388      encoding_check code_memory (sigma program pol ppc) (bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len)) assembledi ∧
    13951389       sigma program pol (\snd pi_newppc) = bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len).
     
    14011395  let code_memory ≝ load_code_memory assembled in
    14021396  let data_labels ≝ construct_datalabels (\fst program) in
    1403   let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in
    1404   let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in
     1397  let lookup_labels ≝ λx.address_of_word_labels_code_mem (\snd program) x in
     1398  let lookup_datalabels ≝ λx. lookup_def ? ? data_labels x (zero ?) in
    14051399  let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
    1406   let instructions ≝ expand_pseudo_instruction program pol ppc lookup_labels lookup_datalabels (sigma program pol ppc) (refl …) (refl …) (refl …) in
     1400  let instructions ≝ expand_pseudo_instruction lookup_labels ppc (pol lookup_labels ppc) lookup_datalabels pi in
    14071401   fetch_many code_memory (sigma program pol newppc) (sigma program pol ppc) instructions.
    14081402 * #preamble #instr_list #pol #ppc
     
    14101404 letin code_memory ≝ (load_code_memory assembled)
    14111405 letin data_labels ≝ (construct_datalabels preamble)
    1412  letin lookup_labels ≝ (λx. sigma … pol (address_of_word_labels_code_mem instr_list x))
    1413  letin lookup_datalabels ≝ (λx. lookup ? ? x data_labels (zero ?))
    1414  @pair_elim' #pi #newppc #EQ1 change in EQ1 with (fetch_pseudo_instruction instr_list ? = ?)
    1415  generalize in match (assembly_ok ? pol assembled (\snd (assembly 〈preamble,instr_list〉 pol)))
    1416  @pair_elim' #labels #costs #EQ2 <eq_pair_fst_snd
     1406 letin lookup_labels ≝ (λx. address_of_word_labels_code_mem instr_list x)
     1407 letin lookup_datalabels ≝ (λx. lookup_def ? ? data_labels x (zero ?))
     1408 @pair_elim #pi #newppc #EQ1 change with (fetch_pseudo_instruction instr_list ? = ?) in EQ1;
     1409 generalize in match (assembly_ok ? pol assembled (\snd (assembly 〈preamble,instr_list〉 pol)));
     1410 @pair_elim #labels #costs #EQ2 <eq_pair_fst_snd
    14171411 #H cases (H (refl \ldots)) -H; #EQ3
    1418  generalize in match (refl … (assembly_1_pseudoinstruction … pol ppc lookup_labels lookup_datalabels ? (refl …) (refl …) (refl …)))
    1419  cases (assembly_1_pseudoinstruction ?????????) in ⊢ (???% → ?) #len #assembledi #EQ4
    1420  #H cases (H ppc len assembledi ?) [2: <EQ4 %] -H; #H1 #H2
    1421  generalize in match (fetch_assembly_pseudo … pol ppc (load_code_memory assembled)) in ⊢ ?
    1422  >EQ4 #H generalize in match (H H1) in ⊢ ? -H; >(pair_destruct_2 ????? (sym_eq … EQ1))
    1423  >H2 #K @K
     1412 generalize in match (refl … (assembly_1_pseudoinstruction lookup_labels (pol lookup_labels) ppc lookup_datalabels ?));
     1413 [ cases (assembly_1_pseudoinstruction ?????) in ⊢ (???% → ?); #len #assembledi #EQ4
     1414   #H cases (H ppc len assembledi ?) [2: <EQ4 %] -H; #H1 #H2
     1415   (* XXX JPB: attention to lookup_labels *)
     1416   generalize in match (fetch_assembly_pseudo 〈preamble,instr_list〉 pol ppc (load_code_memory assembled)) in ⊢ ?;
     1417   >EQ4; #H generalize in match (H H1) in ⊢ ?; -H >(pair_destruct_2 ????? (sym_eq … EQ1))
     1418   >H2 >EQ1 #K @K
    14241419qed.
    14251420
     
    17071702*)
    17081703
    1709 definition ticks_of0: ∀p:pseudo_assembly_program. policy p → Word → ? → nat × nat ≝
    1710   λprogram: pseudo_assembly_program.λpol.
     1704definition ticks_of0: ∀p:pseudo_assembly_program. policy p → (Identifier→Word) → Word → ? → nat × nat ≝
     1705  λprogram: pseudo_assembly_program.λpol.λlookup_labels.
    17111706  λppc: Word.
    17121707  λfetched.
     
    17151710      match instr with
    17161711      [ JC lbl ⇒
    1717         match pol ppc with
     1712        match pol lookup_labels ppc with
    17181713        [ short_jump ⇒ 〈2, 2〉
    17191714        | medium_jump ⇒ ?
     
    17211716        ]
    17221717      | JNC lbl ⇒
    1723         match pol ppc with
     1718        match pol lookup_labels ppc with
    17241719        [ short_jump ⇒ 〈2, 2〉
    17251720        | medium_jump ⇒ ?
     
    17271722        ]
    17281723      | JB bit lbl ⇒
    1729         match pol ppc with
     1724        match pol lookup_labels ppc with
    17301725        [ short_jump ⇒ 〈2, 2〉
    17311726        | medium_jump ⇒ ?
     
    17331728        ]
    17341729      | JNB bit lbl ⇒
    1735         match pol ppc with
     1730        match pol lookup_labels ppc with
    17361731        [ short_jump ⇒ 〈2, 2〉
    17371732        | medium_jump ⇒ ?
     
    17391734        ]
    17401735      | JBC bit lbl ⇒
    1741         match pol ppc with
     1736        match pol lookup_labels ppc with
    17421737        [ short_jump ⇒ 〈2, 2〉
    17431738        | medium_jump ⇒ ?
     
    17451740        ]
    17461741      | JZ lbl ⇒
    1747         match pol ppc with
     1742        match pol lookup_labels ppc with
    17481743        [ short_jump ⇒ 〈2, 2〉
    17491744        | medium_jump ⇒ ?
     
    17511746        ]
    17521747      | JNZ lbl ⇒
    1753         match pol ppc with
     1748        match pol lookup_labels  ppc with
    17541749        [ short_jump ⇒ 〈2, 2〉
    17551750        | medium_jump ⇒ ?
     
    17571752        ]
    17581753      | CJNE arg lbl ⇒
    1759         match pol ppc with
     1754        match pol lookup_labels ppc with
    17601755        [ short_jump ⇒ 〈2, 2〉
    17611756        | medium_jump ⇒ ?
     
    17631758        ]
    17641759      | DJNZ arg lbl ⇒
    1765         match pol ppc with
     1760        match pol lookup_labels ppc with
    17661761        [ short_jump ⇒ 〈2, 2〉
    17671762        | medium_jump ⇒ ?
     
    18621857qed.
    18631858
    1864 definition ticks_of: ∀p:pseudo_assembly_program. policy p → Word → nat × nat ≝
    1865   λprogram: pseudo_assembly_program.λpol.
     1859definition ticks_of: ∀p:pseudo_assembly_program. policy p → (Identifier→Word) → Word → nat × nat ≝
     1860  λprogram: pseudo_assembly_program.λpol.λlookup_labels.
    18661861  λppc: Word.
    18671862    let 〈preamble, pseudo〉 ≝ program in
    18681863    let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc in
    1869      ticks_of0 program pol ppc fetched.
     1864     ticks_of0 program pol lookup_labels ppc fetched.
    18701865
    18711866lemma eq_rect_Type1_r:
     
    18741869  ∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
    18751870  #A #a #P #H #x #p
    1876   generalize in match H
    1877   generalize in match P
     1871  generalize in match H;
     1872  generalize in match P;
    18781873  cases p
    18791874  //
     
    20342029
    20352030theorem main_thm:
    2036  ∀M,M',ps,pol.
     2031 ∀M,M',ps,pol,lookup_labels.
    20372032  next_internal_pseudo_address_map M ps = Some … M' →
    20382033   ∃n.
    20392034      execute n (status_of_pseudo_status M ps pol)
    2040     = status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol) ps) ?.
     2035    = status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol lookup_labels) ps) ?.
    20412036 [2: >execute_1_pseudo_instruction_preserves_code_memory @pol]
    2042  #M #M' #ps #pol #SAFE
     2037 #M #M' #ps #pol #lookup_labels #SAFE
    20432038 cut
    20442039  (∀ps'.
    2045     ∀prf:ps'=execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol) ps.
     2040    ∀prf:ps'=execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol lookup_labels) ps.
    20462041    ∃n. execute n (status_of_pseudo_status M ps pol) = status_of_pseudo_status M' ps' ?)
    20472042 [ >prf >execute_1_pseudo_instruction_preserves_code_memory @pol |3: #K @(K ? (refl …))]
    20482043 #ps' #EQ
    2049  whd in ⊢ (??(λ_.??(??%)?))
     2044 whd in ⊢ (??(λ_.??(??%)?));
    20502045 change with
    20512046  (∃n.
     
    20622057        (set_program_counter ?
    20632058          (set_code_memory ?? ? (load_code_memory ?))
    2064          (sigma ???)) ?) ?)
    2065  >EQ whd in match eq_rect_Type0_r normalize nodelta
     2059         (sigma ???)) ?) ?);
     2060 >EQ whd in match eq_rect_Type0_r; normalize nodelta
    20662061 >execute_1_pseudo_instruction_preserves_code_memory normalize nodelta
    2067  generalize in match EQ -EQ;
    2068  generalize in match (refl … (code_memory pseudo_assembly_program ps))
    2069  generalize in match pol -pol; generalize in ⊢ (∀_.??%? → ?)
    2070  * #preamble #instr_list #pol #EQ1 generalize in match pol -pol <EQ1 #pol #EQps' <EQps'
     2062 generalize in match EQ; -EQ;
     2063 generalize in match (refl … (code_memory pseudo_assembly_program ps));
     2064 generalize in match pol; -pol; generalize in ⊢ (∀_.??%? → ?);
     2065 * #preamble #instr_list #pol #EQ1 generalize in match pol; -pol <EQ1 #pol #EQps' <EQps'
    20712066 (* Dependent types madness ends here *)
    20722067 letin ppc ≝ (program_counter … ps)
    2073  generalize in match (fetch_assembly_pseudo2 ? pol ppc) in ⊢ ?
     2068 generalize in match (fetch_assembly_pseudo2 ? pol ppc) in ⊢ ?;
    20742069 letin assembled ≝ (\fst (assembly ? pol))
    2075  letin lookup_labels ≝ (λx. sigma ? pol (address_of_word_labels_code_mem instr_list x))
    2076  letin lookup_datalabels ≝ (λx. lookup … x (construct_datalabels preamble) (zero 16))
    2077  @pair_elim' #pi #newppc #EQ2
     2070 letin lookup_labels ≝ (λx.(address_of_word_labels_code_mem instr_list x))
     2071 letin lookup_datalabels ≝ (λx. lookup_def … (construct_datalabels preamble) x (zero 16))
     2072 @pair_elim #pi #newppc #EQ2
    20782073 letin instructions ≝
    2079   (expand_pseudo_instruction ? pol ppc lookup_labels lookup_datalabels
    2080     (sigma ? pol ppc) (refl …) (refl …) (refl …))
    2081  change with (fetch_many ???? → ?) #H1
    2082  change in EQ2 with (fetch_pseudo_instruction instr_list ppc = ?)
    2083  change in SAFE with (next_internal_pseudo_address_map0 ???? = ?) <EQ1 in SAFE;
    2084  >EQ2 whd in ⊢ (??(??%??)? → ?) #SAFE
     2074  (expand_pseudo_instruction lookup_labels ppc ((pi1 ?? pol) lookup_labels ppc) lookup_datalabels
     2075    pi)
     2076 change with (fetch_many ???? → ?); #H1
     2077 change with (fetch_pseudo_instruction instr_list ppc = ?) in EQ2;
     2078 change with (next_internal_pseudo_address_map0 ???? = ?) in SAFE; <EQ1 in SAFE;
     2079 >EQ2 whd in ⊢ (??(??%??)? → ?); #SAFE
    20852080 whd in EQps':(???%); <EQ1 in EQps'; >EQ2 normalize nodelta
    2086  generalize in match H1; -H1; generalize in match instructions -instructions
    2087  * #instructions >EQ2 change in match (\fst 〈pi,newppc〉) with pi
    2088  whd in match ticks_of normalize nodelta <EQ1 >EQ2
    2089  cases pi in SAFE
    2090   [2,3: (* Comment, Cost *) #ARG whd in ⊢ (??%? → ???% → ?)
     2081 generalize in match H1; -H1; generalize in match instructions; -instructions
     2082 * #instructions >EQ2 change with pi in match (\fst 〈pi,newppc〉);
     2083 whd in match ticks_of; normalize nodelta <EQ1 >EQ2
     2084 cases pi in SAFE;
     2085  [2,3: (* Comment, Cost *) #ARG whd in ⊢ (??%? → ???% → ?);
    20912086   @Some_Some_elim #MAP #EQ3 @(Some_Some_elim ????? EQ3) #EQ3'
    20922087   whd in match eject normalize nodelta >EQ3' in ⊢ (% → ?) whd in ⊢ (% → ?)
Note: See TracChangeset for help on using the changeset viewer.