Changeset 906
 Timestamp:
 Jun 8, 2011, 6:12:15 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r905 r906 828 828 qed. 829 829 830 axiom eq_bv_refl: ∀n,v. eq_bv n v v = true.831 832 830 axiom bitvector_3_elim_prop: 833 831 ∀P: BitVector 3 → Prop. … … 1103 1101 *) 1104 1102 1105 axiom assembly_ok: 1106 ∀program,assembled,costs,labels,datalabels. 1107 Some … 〈labels,datalabels〉 = build_maps program → 1108 Some … 〈assembled,costs〉 = assembly program → 1109 let code_memory ≝ load_code_memory assembled in 1110 let lookup_labels ≝ λx. lookup ?? x labels (zero ?) in 1111 let lookup_datalabels ≝ λx. lookup ?? x datalabels (zero ?) in 1112 ∀ppc,len,assembledi. 1113 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in 1114 Some … 〈len,assembledi〉 = assembly_1_pseudoinstruction program ppc lookup_labels lookup_datalabels pi → 1115 encoding_check code_memory (sigma program ppc) (bitvector_of_nat … (nat_of_bitvector … (sigma program ppc) + len)) assembledi ∧ 1116 sigma program newppc = bitvector_of_nat … (nat_of_bitvector … (sigma program ppc) + len). 1117 1103 (* 1118 1104 lemma rev_preserves_length: 1119 1105 ∀A.∀l. length … (rev A l) = length … l. … … 1362 1348 3: % [@ ([ ])] % [2: %  (* DOABLE *)] 1363 1349  1364 1350 *) 1351 1352 axiom assembly_ok: 1353 ∀program,assembled,costs,labels,datalabels. 1354 Some … 〈labels,datalabels〉 = build_maps program → 1355 Some … 〈assembled,costs〉 = assembly program → 1356 let code_memory ≝ load_code_memory assembled in 1357 let lookup_labels ≝ λx. lookup ?? x labels (zero ?) in 1358 let lookup_datalabels ≝ λx. lookup ?? x datalabels (zero ?) in 1359 ∀ppc,len,assembledi. 1360 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in 1361 (* BUG HERE: WE SHOULD PASS BOTH ppc (FOR THE POLICY) AND (sigma program ppc) FOR THE OFFSETS *) 1362 Some … 〈len,assembledi〉 = assembly_1_pseudoinstruction program ppc lookup_labels lookup_datalabels pi → 1363 encoding_check code_memory (sigma program ppc) (bitvector_of_nat … (nat_of_bitvector … (sigma program ppc) + len)) assembledi ∧ 1364 sigma program newppc = bitvector_of_nat … (nat_of_bitvector … (sigma program ppc) + len). 1365 1366 (* OLD? 1365 1367 definition assembly_specification: 1366 1368 ∀assembly_program: pseudo_assembly_program. … … 1407 1409  cases not_implemented 1408 1410 ] *) 1411 *) 1409 1412 1410 1413 definition status_of_pseudo_status: PseudoStatus → option Status ≝
Note: See TracChangeset
for help on using the changeset viewer.