- Timestamp:
- Jul 26, 2012, 12:38:42 AM (9 years ago)
- Location:
- src/ASM
- Files:
-
- 8 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Assembly.ma
r2221 r2264 582 582 583 583 584 (* label_map: identifier ↦ pseudo program counter *)585 definition label_map ≝ identifier_map ASMTag ℕ.586 587 584 (* Labels *) 588 585 definition is_label ≝ … … 617 614 ] 618 615 ] 619 qed.620 621 (* The function that creates the label-to-address map *)622 definition create_label_cost_map0: ∀program:list labelled_instruction.623 (Σlabels_costs:label_map × (BitVectorTrie costlabel 16). (* Both on ppcs *)624 let 〈labels,costs〉 ≝ labels_costs in625 ∀l.occurs_exactly_once ?? l program →626 And (bitvector_of_nat ? (lookup_def ?? labels l 0) =627 address_of_word_labels_code_mem program l)628 (lookup_def ?? labels l 0 < |program|)629 ) ≝630 λprogram.631 \fst (pi1 ?? (foldl_strong (option Identifier × pseudo_instruction)632 (λprefix.Σlabels_costs_ppc:label_map × (BitVectorTrie costlabel 16) × ℕ.633 let 〈labels,costs,ppc〉 ≝ labels_costs_ppc in634 ppc = |prefix| ∧635 ∀l.occurs_exactly_once ?? l prefix →636 And (bitvector_of_nat ? (lookup_def ?? labels l 0) =637 address_of_word_labels_code_mem prefix l)638 (lookup_def ?? labels l 0 < |program|))639 program640 (λprefix.λx.λtl.λprf.λlabels_costs_ppc.641 let 〈labels,costs,ppc〉 ≝ pi1 ?? labels_costs_ppc in642 let 〈label,instr〉 ≝ x in643 let labels ≝644 match label with645 [ None ⇒ labels646 | Some l ⇒ add … labels l ppc647 ] in648 let costs ≝649 match instr with650 [ Cost cost ⇒ insert … (bitvector_of_nat ? ppc) cost costs651 | _ ⇒ costs ] in652 〈labels,costs,S ppc〉653 ) 〈(empty_map …),(Stub ??),0〉)).654 [ normalize nodelta lapply (pi2 … labels_costs_ppc) >p >p1 normalize nodelta * #IH1 #IH2655 -labels_costs_ppc % [>IH1 >length_append <plus_n_Sm <plus_n_O %]656 inversion label [#EQ | #l #EQ]657 [ #lbl #Hocc <address_of_word_labels_code_mem_None [2: @Hocc] normalize nodelta658 >occurs_exactly_once_None in Hocc; @(IH2 lbl)659 | #lbl normalize nodelta inversion (eq_identifier ? lbl l)660 [ #Heq #Hocc >(eq_identifier_eq … Heq) @conj661 [ >address_of_word_labels_code_mem_Some_hit662 [ >IH1 >lookup_def_add_hit %663 | <(eq_identifier_eq … Heq) in Hocc; //664 ]665 | >lookup_def_add_hit >IH1 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r666 ]667 | #Hneq #Hocc lapply (IH2 lbl ?)668 [ >occurs_exactly_once_Some_eq in Hocc; >eq_identifier_sym >Hneq //669 | #IH3 @conj670 [ <address_of_word_labels_code_mem_Some_miss671 [ >lookup_def_add_miss672 [ @(proj1 ?? IH3)673 | % @neq_identifier_neq @Hneq674 ]675 | @Hocc676 | >eq_identifier_sym @Hneq677 ]678 | >lookup_def_add_miss679 [ @(proj2 ?? IH3)680 | % @neq_identifier_neq @Hneq681 ]682 ]683 ]684 ]685 ]686 | @pair_elim * #labels #costs #ppc #EQ destruct normalize nodelta % try %687 #l #abs cases (abs)688 | cases (foldl_strong ? (λ_.Σx.?) ???) * * #labels #costs #ppc normalize nodelta *689 #_ #H @H690 ]691 qed.692 693 (* The function that creates the label-to-address map *)694 definition create_label_cost_map: ∀program:list labelled_instruction.695 label_map × (BitVectorTrie costlabel 16) ≝696 λprogram.697 pi1 … (create_label_cost_map0 program).698 699 theorem create_label_cost_map_ok:700 ∀pseudo_program: pseudo_assembly_program.701 let 〈labels, costs〉 ≝ create_label_cost_map (\snd pseudo_program) in702 ∀id. occurs_exactly_once ?? id (\snd pseudo_program) → And703 (bitvector_of_nat ? (lookup_def ?? labels id 0) = address_of_word_labels_code_mem (\snd pseudo_program) id)704 (lookup_def ?? labels id 0 < |\snd pseudo_program|).705 #p change with (pi1 … (create_label_cost_map0 ?)) in match (create_label_cost_map ?); @pi2706 616 qed. 707 617 -
src/ASM/AssemblyProofSplitSplit.ma
r2140 r2264 38 38 >(eq_bv_eq … relevant) % 39 39 qed. 40 40 41 41 theorem main_thm: 42 42 ∀M, M': internal_pseudo_address_map. 43 43 ∀program: pseudo_assembly_program. 44 44 ∀program_in_bounds: |\snd program| ≤ 2^16. 45 ∀addr_of: Identifier → PreStatus pseudo_assembly_program program → BitVector 16. 45 let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in 46 let addr_of ≝ λid.λ_.bitvector_of_nat 16 (lookup_def ASMTag ℕ labels id O) in 46 47 ∀is_well_labelled: is_well_labelled_p (\snd program). 47 48 ∀sigma: Word → Word. … … 53 54 ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) = 54 55 status_of_pseudo_status M' … 55 (execute_1_pseudo_instruction program (ticks_of program sigma policy) ps program_counter_in_bounds) sigma policy. 56 #M #M' * #preamble #instr_list #program_in_bounds #addr_of 56 (execute_1_pseudo_instruction program (ticks_of program (λid. addr_of id ps) sigma policy) ps program_counter_in_bounds) sigma policy. 57 #M #M' * #preamble #instr_list #program_in_bounds 58 @pair_elim #labels #cost #create_label_cost_refl 57 59 #is_well_labelled_witness #sigma #policy #sigma_policy_witness #ps 58 60 letin ppc ≝ (program_counter pseudo_assembly_program ? ps) #ppc_in_bounds 59 61 change with (next_internal_pseudo_address_map0 ?????? = ? → ?) 60 62 generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 program_in_bounds sigma policy sigma_policy_witness ppc ppc_in_bounds) in ⊢ ?; 61 @pair_elim #labels #costs #create_label_cost_refl normalize nodelta63 >create_label_cost_refl normalize nodelta 62 64 @pair_elim #assembled #costs' #assembly_refl normalize nodelta 63 65 lapply (pair_destruct_1 ????? (sym_eq ??? assembly_refl)) #EQassembled … … 87 89 (* XXX: we give the existential *) 88 90 %{0} 91 whd in match execute_1_pseudo_instruction0; normalize nodelta 92 change with (status_of_pseudo_status ????? = ?) cases daemon (*CSC: ??? 89 93 whd in match (execute_1_pseudo_instruction0 ?????); 90 94 (* XXX: work on the left hand side of the equality *) 91 95 whd in ⊢ (??%?); 92 96 @split_eq_status try % 93 /demod/ >add_commutative <add_zero % (*CSC: auto not working, why? *) 97 /demod/ >add_commutative <add_zero % (*CSC: auto not working, why? *) *) 94 98 |6: (* Mov *) 95 99 #arg1 #arg2 #_ … … 114 118 #fetch_many_assm whd in fetch_many_assm; 115 119 lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc 116 destruct whd in ⊢ (??%?);120 destruct 117 121 (* XXX: now we start to work on the mk_PreStatus equality *) 118 122 (* XXX: lhs *) 119 123 change with (set_arg_16 ????? = ?) 120 >set_program_counter_mk_Status_commutation 121 >set_clock_mk_Status_commutation 122 >set_arg_16_mk_Status_commutation 123 (* XXX: rhs *) 124 change with (status_of_pseudo_status ?? (set_arg_16 pseudo_assembly_program 〈preamble, instr_list〉 ?? arg1) ??) in ⊢ (???%); 125 >set_program_counter_mk_Status_commutation 126 >set_clock_mk_Status_commutation 127 >set_arg_16_mk_Status_commutation in ⊢ (???%); 128 (* here we are *) 129 @split_eq_status try % 130 [1: 131 assumption 132 |2: 133 @special_function_registers_8051_set_arg_16 % 134 ] 124 @set_arg_16_status_of_pseudo_status 125 [3: @(subaddressing_mode_elim … arg1) % 126 |2: % 127 | @sym_eq @set_clock_status_of_pseudo_status 128 [ @sym_eq @set_program_counter_status_of_pseudo_status [<EQnewpc % | %] 129 | % ]] 135 130 |1: (* Instruction *) 136 #instr #pi_refl #EQP #EQnext #fetch_many_assm 137 @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) ? sigma policy sigma_policy_witness 138 ps ppc ? ? labels costs create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels 139 EQnewppc instr ? (ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr)) (refl …) 140 (λx:Identifier. λy:PreStatus pseudo_assembly_program 〈preamble, instr_list〉. address_of_word_labels 〈preamble, instr_list〉 x) (refl …) (set_program_counter pseudo_assembly_program 〈preamble, instr_list〉 ps (add 16 ppc (bitvector_of_nat 16 1))) 141 (refl …) ? (refl …)) 142 [1,2: 143 assumption 144 |3: 145 % 146 |4: 147 >fetch_pseudo_refl @pi_refl 148 |5: 149 <EQP % 150 |6: 151 >assembly_refl assumption 152 |7: 153 <EQassembled assumption 154 ] 131 #instr #pi_refl 132 change with (execute_1_preinstruction ???????) in match (execute_1_pseudo_instruction0 ?????); 133 >EQassembled whd in match address_of_word_labels; normalize nodelta 134 >create_label_cost_refl in ⊢ (? → ? → ? → %); 135 @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) ? sigma policy sigma_policy_witness 136 ps ppc ? ? labels cost create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels 137 EQnewppc instr ? ? (refl …) ? (refl …) 138 (set_program_counter pseudo_assembly_program 〈preamble, instr_list〉 ps (add 16 ppc (bitvector_of_nat 16 1))) 139 (refl …) ? (refl …)) 140 try % try assumption >fetch_pseudo_refl assumption 155 141 |4: (* Jmp *) 156 142 #arg1 #pi_refl -
src/ASM/Fetch.ma
r2124 r2264 3 3 include "ASM/ASM.ma". 4 4 include "basics/russell.ma". 5 6 (***** Pseudo-code ******) 7 8 definition inefficient_address_of_word_labels_code_mem ≝ 9 λcode_mem : list labelled_instruction. 10 λid: Identifier. 11 bitvector_of_nat 16 (index_of ? (instruction_matches_identifier ?? id) code_mem). 12 13 lemma inefficient_address_of_word_labels_None: ∀i,id,instr_list. 14 occurs_exactly_once ?? id (instr_list@[〈None …,i〉]) → 15 inefficient_address_of_word_labels_code_mem instr_list id = 16 inefficient_address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id. 17 #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?)); 18 >(index_of_internal_None ?????? H) % 19 qed. 20 21 lemma inefficient_address_of_word_labels_Some_miss: ∀i,id,id',instr_list. 22 eq_identifier ? id' id = false → 23 occurs_exactly_once ?? id (instr_list@[〈Some ? id',i〉]) → 24 inefficient_address_of_word_labels_code_mem instr_list id = 25 inefficient_address_of_word_labels_code_mem (instr_list@[〈Some … id',i〉]) id. 26 #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?)); 27 >(index_of_internal_Some_miss ???????? H) [ @refl | // ] 28 qed. 29 30 lemma inefficient_address_of_word_labels_Some_hit: ∀i,id,instr_list. 31 occurs_exactly_once ?? id (instr_list@[〈Some ? id,i〉]) → 32 inefficient_address_of_word_labels_code_mem (instr_list@[〈Some … id,i〉]) id 33 = bitvector_of_nat … (|instr_list|). 34 #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)?); 35 >(index_of_internal_Some_hit ?????? H) <plus_n_O @refl 36 qed. 37 38 (* label_map: identifier ↦ pseudo program counter *) 39 definition label_map ≝ identifier_map ASMTag ℕ. 40 41 (* The function that creates the label-to-address map *) 42 definition create_label_cost_map0: ∀program:list labelled_instruction. 43 (Σlabels_costs:label_map × (BitVectorTrie costlabel 16). (* Both on ppcs *) 44 let labels ≝ \fst labels_costs in 45 (∀l.occurs_exactly_once ?? l program → 46 bitvector_of_nat ? (lookup_def ?? labels l 0) = 47 inefficient_address_of_word_labels_code_mem program l) ∧ 48 (∀l.occurs_exactly_once ?? l program →lookup_def ?? labels l 0 < |program|) 49 ) ≝ 50 λprogram. 51 \fst (pi1 ?? (foldl_strong (option Identifier × pseudo_instruction) 52 (λprefix.Σlabels_costs_ppc:label_map × (BitVectorTrie costlabel 16) × ℕ. 53 let 〈labels,costs,ppc〉 ≝ labels_costs_ppc in 54 ppc = |prefix| ∧ 55 ((∀l.occurs_exactly_once ?? l prefix → 56 bitvector_of_nat ? (lookup_def ?? labels l 0) = 57 inefficient_address_of_word_labels_code_mem prefix l) ∧ 58 (∀l.occurs_exactly_once ?? l prefix → lookup_def ?? labels l 0 < |program|))) 59 program 60 (λprefix.λx.λtl.λprf.λlabels_costs_ppc. 61 let 〈labels,costs,ppc〉 ≝ pi1 ?? labels_costs_ppc in 62 let 〈label,instr〉 ≝ x in 63 let labels ≝ 64 match label with 65 [ None ⇒ labels 66 | Some l ⇒ add … labels l ppc 67 ] in 68 let costs ≝ 69 match instr with 70 [ Cost cost ⇒ insert … (bitvector_of_nat ? ppc) cost costs 71 | _ ⇒ costs ] in 72 〈labels,costs,S ppc〉 73 ) 〈(empty_map …),(Stub ??),0〉)). 74 [ normalize nodelta lapply (pi2 … labels_costs_ppc) >p >p1 normalize nodelta * 75 #IH1 * #IH2 #IH3 -labels_costs_ppc % [>IH1 >length_append <plus_n_Sm <plus_n_O %] 76 inversion label [#EQ | #l #EQ] 77 [ % #lbl 78 [ #Hocc <inefficient_address_of_word_labels_None [2: @Hocc] normalize nodelta 79 >occurs_exactly_once_None in Hocc; @IH2 80 | #Hocc normalize nodelta >occurs_exactly_once_None in Hocc; @IH3 ] 81 | % 82 #lbl normalize nodelta inversion (eq_identifier ? lbl l) 83 [1,3: #Heq #Hocc >(eq_identifier_eq … Heq) 84 [ >inefficient_address_of_word_labels_Some_hit 85 [ >IH1 >lookup_def_add_hit % 86 | <(eq_identifier_eq … Heq) in Hocc; // 87 ] 88 | >lookup_def_add_hit >IH1 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 89 ] 90 |*: #Hneq #Hocc 91 cut (occurs_exactly_once … lbl prefix) 92 [1,3: >occurs_exactly_once_Some_eq in Hocc; >eq_identifier_sym >Hneq // ] 93 #Hocc' lapply (IH2 lbl ?) try assumption 94 [ <inefficient_address_of_word_labels_Some_miss // 95 >lookup_def_add_miss // % @neq_identifier_neq @Hneq 96 | >lookup_def_add_miss /2/ 97 ] 98 ] 99 ] 100 | @pair_elim * #labels #costs #ppc #EQ destruct normalize nodelta % try % 101 #l #abs cases (abs) 102 | cases (foldl_strong ? (λ_.Σx.?) ???) * * #labels #costs #ppc normalize nodelta * 103 #_ #H @H 104 ] 105 qed. 106 107 (* The function that creates the label-to-address map *) 108 definition create_label_cost_map: ∀program:list labelled_instruction. 109 label_map × (BitVectorTrie costlabel 16) ≝ 110 λprogram. 111 pi1 … (create_label_cost_map0 program). 112 113 theorem create_label_cost_map_ok: 114 ∀instr_list. 115 let labels ≝ \fst (create_label_cost_map instr_list) in 116 ((∀id. occurs_exactly_once ?? id instr_list → 117 (bitvector_of_nat ? (lookup_def ?? labels id 0) = inefficient_address_of_word_labels_code_mem instr_list id)) 118 ∧ 119 (∀id. occurs_exactly_once ?? id instr_list → lookup_def ?? labels id 0 < |instr_list|)). 120 #p change with (pi1 … (create_label_cost_map0 ?)) in match (create_label_cost_map ?); 121 @pi2 122 qed. 123 124 definition address_of_word_labels : 125 list labelled_instruction → Identifier → Word 126 ≝ 127 λcode_mem : list labelled_instruction. 128 λid: Identifier. 129 let labels ≝ \fst (create_label_cost_map code_mem) in 130 bitvector_of_nat 16 (lookup_def ASMTag ℕ labels id O). 131 132 lemma address_of_word_labels_None: ∀i,id,instr_list. 133 occurs_exactly_once ?? id (instr_list@[〈None …,i〉]) → 134 address_of_word_labels instr_list id = 135 address_of_word_labels (instr_list@[〈None …,i〉]) id. 136 #i #id #instr_list #H 137 whd in match address_of_word_labels; normalize nodelta 138 lapply (create_label_cost_map_ok (instr_list@[〈None …,i〉])) * #K' #_ 139 lapply (create_label_cost_map_ok instr_list) * #K #_ 140 >K' // >K // <inefficient_address_of_word_labels_None // 141 qed. 142 143 lemma address_of_word_labels_Some_miss: ∀i,id,id',instr_list. 144 eq_identifier ? id' id = false → 145 occurs_exactly_once ?? id (instr_list@[〈Some ? id',i〉]) → 146 address_of_word_labels instr_list id = 147 address_of_word_labels (instr_list@[〈Some … id',i〉]) id. 148 #i #id #id' #instr_list #H1 #H2 149 whd in match address_of_word_labels; normalize nodelta 150 lapply (create_label_cost_map_ok (instr_list@[〈Some … id',i〉])) * #K' #_ 151 lapply (create_label_cost_map_ok instr_list) * #K #_ 152 >K' // >K 153 [2: lapply (occurs_exactly_once_Some ?????? H2) >H1 #H @H ] 154 @inefficient_address_of_word_labels_Some_miss // 155 qed. 156 157 lemma address_of_word_labels_Some_hit: ∀i,id,instr_list. 158 occurs_exactly_once ?? id (instr_list@[〈Some ? id,i〉]) → 159 address_of_word_labels (instr_list@[〈Some … id,i〉]) id 160 = bitvector_of_nat … (|instr_list|). 161 #i #id #instr_list #H 162 whd in match address_of_word_labels; normalize nodelta 163 lapply (create_label_cost_map_ok (instr_list@[〈Some … id,i〉])) * #K #_ 164 >K // @inefficient_address_of_word_labels_Some_hit // 165 qed. 166 167 (***** Object-code *******) 5 168 6 169 definition bitvector_max_nat ≝ -
src/ASM/Interpret.ma
r2212 r2264 1190 1190 let s ≝ 1191 1191 match instr with 1192 [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels cmx) instr s1192 [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels (\snd cm) x) instr s 1193 1193 | Comment cmt ⇒ set_clock … s (\fst ticks + clock … s) 1194 1194 | Cost cst ⇒ s 1195 1195 | Jmp jmp ⇒ 1196 1196 let s ≝ set_clock … s (\fst ticks + clock … s) in 1197 set_program_counter … s (address_of_word_labels cmjmp)1197 set_program_counter … s (address_of_word_labels (\snd cm) jmp) 1198 1198 | Call call ⇒ 1199 1199 let s ≝ set_clock ?? s (\fst ticks + clock … s) in 1200 let a ≝ address_of_word_labels cmcall in1200 let a ≝ address_of_word_labels (\snd cm) call in 1201 1201 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in 1202 1202 let s ≝ set_8051_sfr … s SFR_SP new_sp in -
src/ASM/Policy.ma
r2230 r2264 30 30 ] (refl … z) 31 31 ] (refl … n). 32 [5: cases labels #label_map #spec #id #id_ok cases (spec … id_ok) //32 [5: #l #_ % 33 33 | normalize nodelta cases (jump_expansion_start program (create_label_map program)) 34 34 #x cases x -x … … 262 262 | Some p ⇒ measure_int l policy acc ≤ measure_int l p acc 263 263 ]. 264 [2: cases (create_label_map ?) #label_map #H #id #id_ok cases (H … id_ok) //]264 [2: #l #_ %] 265 265 #program #policy #l elim l -l; 266 266 [ #Hp #acc cases (jump_expansion_step ???) #pi1 cases pi1 #p #q -pi1; cases q [ // | #x #_ @le_n ] … … 332 332 [ None ⇒ True 333 333 | Some p ⇒ measure_int program policy 0 = measure_int program p 0 → sigma_jump_equal program policy p ]. 334 [2: cases (create_label_map ?) #label_map #H #id #id_ok cases (H … id_ok) //]334 [2: #l #_ %] 335 335 #program #policy inversion (jump_expansion_step ???) 336 336 #p cases p -p #ch #pol normalize nodelta cases pol -
src/ASM/PolicyFront.ma
r2235 r2264 315 315 (Σlabels:label_map. 316 316 ∀l.occurs_exactly_once ?? l program → 317 And (bitvector_of_nat ? (lookup_def ?? labels l 0) =318 address_of_word_labels _code_memprogram l)319 ( lookup_def ?? labels l 0 < |program|)317 (*And (bitvector_of_nat ? (lookup_def ?? labels l 0) = 318 address_of_word_labels program l) 319 ( *)lookup_def ?? labels l 0 < |program|(*)*) 320 320 ) ≝ 321 321 λprogram. 322 322 \fst (create_label_cost_map program). 323 #l #Hl lapply (pi2 ?? (create_label_cost_map0 program)) @pair_elim 324 #labels #costs #EQ normalize nodelta #H whd in match create_label_cost_map; 325 normalize nodelta >EQ @(H l Hl) 323 #l #Hl cases (create_label_cost_map_ok program) #_ #X @(X … Hl) 326 324 qed. 327 325 … … 667 665 cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|)) 668 666 [1,3: cases (create_label_map program) #clm #Hclm 669 @le_S_to_le @( proj2 ?? (Hclm x ?))667 @le_S_to_le @(Hclm x ?) 670 668 [1: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Jmp x) ??) 671 669 |2: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Call x) ??)] … … 696 694 cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|)) 697 695 [1,3,5,7: cases (create_label_map program) #clm #Hclm 698 @le_S_to_le @( proj2 ?? (Hclm x ?))696 @le_S_to_le @(Hclm x ?) 699 697 [1,2: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Jmp x) ??) 700 698 |3,4: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Call x) ??)] … … 728 726 lookup_def ?? (create_label_map program) x 0 ≤ (|program|)) 729 727 [#x #Heq cases (create_label_map program) #clm #Hclm 730 @le_S_to_le @( proj2 ?? (Hclm x ?))728 @le_S_to_le @(Hclm x ?) 731 729 @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (\snd (nth i ? program 〈None ?, Comment []〉)) ??) 732 730 [ >nat_of_bitvector_bitvector_of_nat_inverse -
src/ASM/PolicyStep.ma
r2248 r2264 1067 1067 occurs_exactly_once ?? l program → 1068 1068 bitvector_of_nat ? (lookup_def … lm l 0) = 1069 address_of_word_labels _code_memprogram l).1069 address_of_word_labels program l). 1070 1070 ∀old_policy:(Σpolicy:ppc_pc_map. 1071 1071 (* out_of_program_none program policy *) -
src/ASM/Status.ma
r2247 r2264 1101 1101 occurs_exactly_once ASMTag pseudo_instruction id instr_list. 1102 1102 1103 definition address_of_word_labels_code_mem ≝1104 λcode_mem : list labelled_instruction.1105 λid: Identifier.1106 bitvector_of_nat 16 (index_of ? (instruction_matches_identifier ?? id) code_mem).1107 1108 lemma address_of_word_labels_code_mem_None: ∀i,id,instr_list.1109 occurs_exactly_once ?? id (instr_list@[〈None …,i〉]) →1110 address_of_word_labels_code_mem instr_list id =1111 address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id.1112 #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?));1113 >(index_of_internal_None ?????? H) %1114 qed.1115 1116 lemma address_of_word_labels_code_mem_Some_miss: ∀i,id,id',instr_list.1117 eq_identifier ? id' id = false →1118 occurs_exactly_once ?? id (instr_list@[〈Some ? id',i〉]) →1119 address_of_word_labels_code_mem instr_list id =1120 address_of_word_labels_code_mem (instr_list@[〈Some … id',i〉]) id.1121 #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)(??%?));1122 >(index_of_internal_Some_miss ???????? H) [ @refl | // ]1123 qed.1124 1125 lemma address_of_word_labels_code_mem_Some_hit: ∀i,id,instr_list.1126 occurs_exactly_once ?? id (instr_list@[〈Some ? id,i〉]) →1127 address_of_word_labels_code_mem (instr_list@[〈Some … id,i〉]) id1128 = bitvector_of_nat … (|instr_list|).1129 #i #id #instr_list #H whd in ⊢ (??%%); whd in ⊢ (??(??%?)?);1130 >(index_of_internal_Some_hit ?????? H) <plus_n_O @refl1131 qed.1132 1133 definition address_of_word_labels ≝1134 λpr: pseudo_assembly_program.1135 λid: Identifier.1136 address_of_word_labels_code_mem (\snd pr) id.1137 1138 1103 definition construct_datalabels: preamble → ? ≝ 1139 1104 λthe_preamble: preamble.
Note: See TracChangeset
for help on using the changeset viewer.