 Timestamp:
 Jun 28, 2012, 4:47:42 PM (9 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r2137 r2138 721 721 let 〈assembled,costs〉 ≝ res in 722 722 assembled ≤ 2^16 ∧ 723 nat_of_bitvector … (sigma (bitvector_of_nat … (instr_list))) = assembled ∧ 723 724 let 〈labels_to_ppc,ppc_to_costs〉 ≝ create_label_cost_map instr_list in 724 725 let datalabels ≝ construct_datalabels preamble in … … 742 743 let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def … labels_to_ppc x 0) in 743 744 let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero ?) in 744 let 〈 ignore,revcode〉 ≝ pi1 … (745 let 〈next_pc,revcode〉 ≝ pi1 … ( 745 746 foldl_strong 746 747 (option Identifier × pseudo_instruction) … … 776 777  #nlimit %1 >nat_of_bitvector_bitvector_of_nat_inverse try assumption 777 778 @not_eq_to_le_to_lt assumption ] 778  >length_reverse <Hfold3 779 @(transitive_le … (S (nat_of_bitvector … (sigma ignore)))) 780 [ //  change with (? < ?); @lt_nat_of_bitvector ]] 779  >length_reverse <Hfold3 % 780 [ @(transitive_le … (S (nat_of_bitvector … (sigma next_pc)))) 781 [ //  change with (? < ?); @lt_nat_of_bitvector ] 782  >Hfold1 % ]] 781 783  * #sigma_pol_ok1 #_ #instr_list_ok % 782 784 [ % // >sigma_pol_ok1 % ] 
src/ASM/AssemblyProof.ma
r2136 r2138 377 377 #H lapply (H sigma_policy_witness instr_list_ok) H whd in ⊢ (% → ?); 378 378 @pair_elim #labels #costs #create_label_cost_refl whd in ⊢ (% → %); 379 * #assembly_ok1#assembly_ok2 #Pair_eq destruct(Pair_eq) whd379 * * #assembly_ok1 #assembly_ok3 #assembly_ok2 #Pair_eq destruct(Pair_eq) whd 380 380 #ppc #ppc_ok @pair_elim #pi #newppc #eq_fetch_pseudo_instruction 381 381 @pair_elim #len #assembled #eq_assembly_1_pseudoinstruction whd … … 1051 1051 *) 1052 1052 1053 (*CSC: ???*)1054 (* XXX: we need a precondition here stating that the PPC is within the1055 bounds of the instruction list in order for Jaap's specification to1056 apply.1057 *)1058 1053 lemma snd_assembly_1_pseudoinstruction_ok: 1059 1054 ∀program: pseudo_assembly_program.
Note: See TracChangeset
for help on using the changeset viewer.