Changeset 1966
 Timestamp:
 May 17, 2012, 5:45:21 PM (7 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r1957 r1966 1312 1312 1313 1313 lemma destruct_bug_fix: 1314 3 = 0 → False. 1315 #absurd destruct(absurd) 1314 ∀n: nat. 1315 S n = 0 → False. 1316 #n #absurd destruct(absurd) 1316 1317 qed. 1317 1318 … … 1319 1320 ∀b: BitVector 3. 1320 1321 ∃l, c, r: bool. 1321 b ≃ [[l; c; r]] ≝ ?.1322 b ≃ [[l; c; r]]. 1322 1323 #b 1323 1324 @(Vector_inv_ind bool 3 b (λn: nat. λv: Vector bool n. ∃l:bool.∃c:bool.∃r:bool. v ≃ [[l; c; r]])) 1324 1325 [1: 1325 #absurd @⊥ @destruct_bug_fix1326 #absurd @⊥ b @(destruct_bug_fix 2) 1326 1327 >absurd % 1327 1328 2: 1328 #n #hd #tl #_ #_ #_ %{hd} 1329 #n #hd #tl #_ #size_refl #hd_tl_refl %{hd} 1330 cut (n = 2) 1331 [1: 1332 2: 1333 #n_refl >n_refl in tl; 1329 1334 cases daemon 1330 1335 ] 1336 cases daemon 1331 1337 qed. 1332 1338 … … 1477 1483 encoding_check code_memory pc pc_plus_len assembled → 1478 1484 fetch_many code_memory pc_plus_len pc instructions. 1479 #program #sigma #policy letin lookup_labels ≝ (λx.?) #ppc #code_memory 1480 letin lookup_datalabels ≝ (λx.?) 1481 letin pi ≝ (fst ???) 1482 letin pc ≝ (sigma ?) 1483 letin instructions ≝ (expand_pseudo_instruction ??????) 1484 @pair_elim #len #assembled #assembled_refl normalize nodelta 1485 #H 1486 generalize in match 1487 (fetch_assembly_pseudo' lookup_labels sigma policy ppc lookup_datalabels pi code_memory len assembled instructions) in ⊢ ?; 1488 #X destruct normalize nodelta @X try % <assembled_refl try % assumption 1489 qed. 1485 #program #sigma #policy letin lookup_labels ≝ (λx.?) #ppc #code_memory 1486 letin lookup_datalabels ≝ (λx.?) 1487 letin pi ≝ (fst ???) 1488 letin pc ≝ (sigma ?) 1489 letin instructions ≝ (expand_pseudo_instruction ??????) 1490 @pair_elim #len #assembled #assembled_refl normalize nodelta 1491 #H 1492 generalize in match 1493 (fetch_assembly_pseudo' lookup_labels sigma policy ppc lookup_datalabels pi code_memory len assembled instructions) in ⊢ ?; 1494 #X destruct normalize nodelta @X try % <assembled_refl try % assumption 1495 qed. 1496 1497 definition is_present_in_machine_code_image_p: ∀pseudo_instruction. Prop ≝ 1498 λpseudo_instruction. 1499 match pseudo_instruction with 1500 [ Comment c ⇒ False 1501  Cost c ⇒ False 1502  _ ⇒ True 1503 ]. 1504 1505 definition sigma_policy_specification ≝ 1506 λprogram: pseudo_assembly_program. 1507 λsigma: Word → Word. 1508 λpolicy: Word → bool. 1509 ∀ppc: Word. 1510 let 〈preamble, instr_list〉 ≝ program in 1511 let pc ≝ sigma ppc in 1512 let labels ≝ \fst (create_label_cost_map instr_list) in 1513 let lookup_labels ≝ λx. bitvector_of_nat 16 (lookup_def … labels x 0) in 1514 let instruction ≝ \fst (fetch_pseudo_instruction instr_list ppc) in 1515 let next_pc ≝ sigma (add 16 ppc (bitvector_of_nat 16 1)) in 1516 And (nat_of_bitvector … ppc ≤ instr_list → 1517 next_pc = add 16 pc (bitvector_of_nat … 1518 (instruction_size lookup_labels sigma policy ppc instruction))) 1519 (Or (nat_of_bitvector … ppc < instr_list → 1520 nat_of_bitvector … pc < nat_of_bitvector … next_pc) 1521 (nat_of_bitvector … ppc = instr_list → next_pc = (zero …))). 1490 1522 1491 1523 (* This is a trivial consequence of fetch_assembly_pseudo + the proof that the … … 1501 1533 ∀sigma: Word → Word. 1502 1534 ∀policy: Word → bool. 1535 ∀sigma_policy_witness: sigma_policy_specification program sigma policy. 1503 1536 ∀assembled. 1504 1537 ∀costs'. 1505 1538 let 〈preamble, instr_list〉 ≝ program in 1506 1539 let 〈labels, costs〉 ≝ create_label_cost_map instr_list in 1507 〈assembled,costs'〉 = assembly program sigma policy →1508 costs = costs' ∧1509 let code_memory ≝ load_code_memory assembled in1510 let datalabels ≝ construct_datalabels (\fst program) in1511 let lookup_labels ≝ λx. sigma (address_of_word_labels_code_mem (\snd program) x) in1512 let lookup_datalabels ≝ λx. lookup_def ?? datalabels x (zero ?) in1513 ∀ppc.1514 let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in1515 let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in1516 let pc ≝ sigma ppc in1517 let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in1518 encoding_check code_memory pc pc_plus_len assembled ∧1519 sigma newppc = add … pc (bitvector_of_nat … len).1520 #program #sigma #policy # assembled #costs'1540 let datalabels ≝ construct_datalabels preamble in 1541 let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero …) in 1542 〈assembled,costs'〉 = assembly program sigma policy → 1543 costs = costs' ∧ 1544 let code_memory ≝ load_code_memory assembled in 1545 let lookup_labels ≝ λx. sigma (address_of_word_labels_code_mem instr_list x) in 1546 ∀ppc. 1547 let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in 1548 let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in 1549 let pc ≝ sigma ppc in 1550 let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in 1551 encoding_check code_memory pc pc_plus_len assembled ∧ 1552 sigma newppc = add … pc (bitvector_of_nat … len). 1553 #program #sigma #policy #sigma_policy_witness #assembled #costs' 1521 1554 @pair_elim #preamble #instr_list #program_refl 1522 1555 @pair_elim #labels #costs #create_label_cost_refl 1523 #assembly_refl % 1556 #assembly_refl % cases daemon (* 1524 1557 [1: 1525 >(?: costs = \snd (create_label_cost_map instr_list)) 1526 [1: 1527 >(?: costs' = \snd (assembly program sigma policy)) 1558 (* XXX: lemma on BitVectorTries *) 1559 cases daemon 1560 2: 1561 #ppc #sigma_policy_specification_witness 1562 @pair_elim #pi #newppc #fetch_pseudo_refl 1563 cases pi 1564 [2,3: (* Cost and Comment cases *) 1565 #comment_or_cost normalize in ⊢ (% → ?); #absurd cases absurd 1566 1: (* PreInstruction cases *) 1567 #preinstruction #_ 1568 @pair_elim #len #assembled' #assembly_1_pseudo_refl 1569 normalize nodelta % 1528 1570 [1: 1529 whd in match assembly; normalize nodelta 1530 >program_refl normalize nodelta 1531 >create_label_cost_refl in ⊢ (???%); normalize nodelta 1532 whd in match create_label_cost_map; normalize nodelta 1533 whd in match create_label_cost_map0; normalize nodelta 1571 cases assembled' normalize 1534 1572 2: 1535 <assembly_refl %1536 1573 ] 1537 2: 1538 >create_label_cost_refl % 1539 ] 1540 2: 1574 ] 1541 1575 ] 1542 cases daemon (* XXX: !!! *) 1576 cases daemon (* XXX: !!! *) *) 1543 1577 qed. 1544 1578 … … 1548 1582 ∀sigma. 1549 1583 ∀policy. 1584 ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy. 1550 1585 ∀ppc. 1551 1586 let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in … … 1558 1593 let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in 1559 1594 fetch_many code_memory (sigma newppc) (sigma ppc) instructions. 1560 * #preamble #instr_list #sigma #policy # ppc1595 * #preamble #instr_list #sigma #policy #sigma_policy_specification_witness #ppc 1561 1596 @pair_elim #labels #costs #create_label_map_refl 1562 1597 @pair_elim #assembled #costs' #assembled_refl … … 1566 1601 letin lookup_datalabels ≝ (λx. ?) 1567 1602 @pair_elim #pi #newppc #fetch_pseudo_refl 1568 lapply (assembly_ok 〈preamble, instr_list〉 sigma policy assembled costs')1603 lapply (assembly_ok 〈preamble, instr_list〉 sigma policy sigma_policy_specification_witness assembled costs') 1569 1604 normalize nodelta 1570 1605 @pair_elim #labels' #costs' #create_label_map_refl' #H … … 1576 1611 lapply (H ppc) >fetch_pseudo_refl #H 1577 1612 lapply (fetch_assembly_pseudo 〈preamble,instr_list〉 sigma policy ppc (load_code_memory assembled)) 1578 >EQ4 #H1 cases H #H2 #H3 >H3 normalize nodelta in H1; normalize nodelta 1613 >EQ4 #H1 cases H 1614 #H2 #H3 >H3 normalize nodelta in H1; normalize nodelta 1579 1615 >fetch_pseudo_refl in H1; #assm @assm assumption 1580 1616 qed. … … 2218 2254 qed. 2219 2255 2220 definition is_present_in_machine_code_image_p: ∀pseudo_instruction. Prop ≝2221 λpseudo_instruction.2222 match pseudo_instruction with2223 [ Comment c ⇒ False2224  Cost c ⇒ False2225  _ ⇒ True2226 ].2227 2228 2256 lemma pair_destruct_right: 2229 2257 ∀A: Type[0]. … … 2240 2268 ∀sigma: Word → Word. 2241 2269 ∀policy: Word → bool. 2270 ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy. 2242 2271 ∀ppc: Word. 2243 2272 ∀pi. 2244 ∀present_in_machine_code_image_witness: is_present_in_machine_code_image_p pi.2245 2273 ∀lookup_labels. 2246 2274 ∀lookup_datalabels. … … 2250 2278 let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) ppc lookup_datalabels pi) in 2251 2279 sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len). 2252 #program #sigma #policy # ppc #pi #is_present_in_machine_code_image_witness2253 #lookup_labels #lookup_datalabels #lookup_labels_refl #lookup_datalabels_refl2254 # fetch_pseudo_refl2280 #program #sigma #policy #sigma_policy_specification_witness #ppc #pi 2281 #lookup_labels #lookup_datalabels 2282 #lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl 2255 2283 normalize nodelta 2256 2284 generalize in match fetch_pseudo_refl; fetch_pseudo_refl 2257 generalize in match is_present_in_machine_code_image_witness; is_present_in_machine_code_image_witness2258 cases pi2259 [1:2260 #preinstruction #_2261 2,3:2262 (* XXX: bug in original statement here, to prove: sigma (ppc + 1) = sigma ppc *)2263 #cost_or_comment normalize in ⊢ (% → ?); #absurd cases absurd2264 4,5:2265 #identifier #_2266 6:2267 #dptr #identifier #_2268 ]2269 2285 #fetch_pseudo_refl 2270 2286 letin assembled ≝ (\fst (assembly program sigma policy)) 2271 2287 letin costs ≝ (\snd (assembly program sigma policy)) 2272 lapply (assembly_ok program sigma policy assembled costs)2288 lapply (assembly_ok program sigma policy sigma_policy_specification_witness assembled costs) 2273 2289 @pair_elim #preamble #instr_list #program_refl 2274 2290 @pair_elim #labels #costs' #create_label_cost_map_refl … … 2276 2292 lapply (H ppc) H 2277 2293 @pair_elim #pi' #newppc #fetch_pseudo_refl' 2278 @pair_elim #len #assembled #assembly1_refl #H cases H 2294 @pair_elim #len #assembled #assembly1_refl #H 2295 cases H 2279 2296 #encoding_check_assm #sigma_newppc_refl 2280 2297 >fetch_pseudo_refl' in fetch_pseudo_refl; #pi_refl' 2281 2298 >pi_refl' in assembly1_refl; #assembly1_refl 2282 >lookup_labels_refl >lookup_datalabels_refl >assembly1_refl 2299 >lookup_labels_refl >lookup_datalabels_refl 2300 >program_refl normalize nodelta 2301 >assembly1_refl 2283 2302 <sigma_newppc_refl 2284 2303 generalize in match fetch_pseudo_refl'; 
src/ASM/AssemblyProofSplit.ma
r1963 r1966 3 3 include alias "basics/logic.ma". 4 4 5 axiom add_commutative: 6 ∀n: nat. 7 ∀l, r: BitVector n. 8 add … l r = add … r l. 5 lemma set_arg_16_mk_Status_commutation: 6 ∀M: Type[0]. 7 ∀cm: M. 8 ∀s: PreStatus M cm. 9 ∀w: Word. 10 ∀d: [[dptr]]. 11 set_arg_16 M cm s w d = 12 mk_PreStatus M cm 13 (low_internal_ram … s) 14 (high_internal_ram … s) 15 (external_ram … s) 16 (program_counter … s) 17 (special_function_registers_8051 … (set_arg_16 M cm s w d)) 18 (special_function_registers_8052 … s) 19 (p1_latch … s) 20 (p3_latch … s) 21 (clock … s). 22 #M #cm #s #w #d 23 whd in match set_arg_16; normalize nodelta 24 whd in match set_arg_16'; normalize nodelta 25 @(subaddressing_mode_elim … [[dptr]] … [[dptr]]) [1: // ] 26 cases (split bool 8 8 w) #bu #bl normalize nodelta 27 whd in match set_8051_sfr; normalize nodelta % 28 qed. 29 30 lemma set_program_counter_mk_Status_commutation: 31 ∀M: Type[0]. 32 ∀cm: M. 33 ∀s: PreStatus M cm. 34 ∀w: Word. 35 set_program_counter M cm s w = 36 mk_PreStatus M cm 37 (low_internal_ram … s) 38 (high_internal_ram … s) 39 (external_ram … s) 40 w 41 (special_function_registers_8051 … s) 42 (special_function_registers_8052 … s) 43 (p1_latch … s) 44 (p3_latch … s) 45 (clock … s). 46 // 47 qed. 48 49 lemma set_clock_mk_Status_commutation: 50 ∀M: Type[0]. 51 ∀cm: M. 52 ∀s: PreStatus M cm. 53 ∀c: nat. 54 set_clock M cm s c = 55 mk_PreStatus M cm 56 (low_internal_ram … s) 57 (high_internal_ram … s) 58 (external_ram … s) 59 (program_counter … s) 60 (special_function_registers_8051 … s) 61 (special_function_registers_8052 … s) 62 (p1_latch … s) 63 (p3_latch … s) 64 c. 65 // 66 qed. 67 68 69 lemma special_function_registers_8051_set_arg_16: 70 ∀M, M': Type[0]. 71 ∀cm: M. 72 ∀cm': M'. 73 ∀s: PreStatus M cm. 74 ∀s': PreStatus M' cm'. 75 ∀w, w': Word. 76 ∀d, d': [[dptr]]. 77 (∀sfr: SFR8051. 78 sfr ≠ SFR_DPH → sfr ≠ SFR_DPL → 79 get_8051_sfr M cm s sfr = get_8051_sfr M' cm' s' sfr) → 80 w = w' → 81 special_function_registers_8051 ?? (set_arg_16 … s w d) = 82 special_function_registers_8051 ?? (set_arg_16 M' cm' s' w' d'). 83 #M #M' #cm #cm' #s #s' #w #w' #d 84 cases daemon 85 qed. 86 9 87 10 88 theorem main_thm: 11 89 ∀M. 12 90 ∀M'. 13 ∀cm. 14 ∀ps. 15 ∀sigma. 16 ∀policy. 17 next_internal_pseudo_address_map M cm ps = Some … M' → 91 ∀program: pseudo_assembly_program. 92 ∀sigma: Word → Word. 93 ∀policy: Word → bool. 94 ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy. 95 ∀ps: PseudoStatus program. 96 next_internal_pseudo_address_map M program ps = Some … M' → 18 97 ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) = 19 98 status_of_pseudo_status M' … 20 (execute_1_pseudo_instruction (ticks_of cm sigma policy) cm ps) sigma policy.21 #M #M' * #preamble #instr_list # ps #sigma #policy99 (execute_1_pseudo_instruction (ticks_of program sigma policy) program ps) sigma policy. 100 #M #M' * #preamble #instr_list #sigma #policy #sigma_policy_witness #ps 22 101 change with (next_internal_pseudo_address_map0 ????? = ? → ?) 23 102 @(pose … (program_counter ?? ps)) #ppc #EQppc 24 generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma policy ppc) in ⊢ ?; 25 @pair_elim #labels #costs #H0 normalize nodelta 26 @pair_elim #assembled #costs' #EQ1 normalize nodelta 27 @pair_elim #pi #newppc #EQ2 normalize nodelta 103 generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma policy sigma_policy_witness ppc) in ⊢ ?; 104 @pair_elim #labels #costs #create_label_cost_refl normalize nodelta 105 @pair_elim #assembled #costs' #assembly_refl normalize nodelta 106 lapply (pair_destruct_1 ????? (sym_eq ??? assembly_refl)) #EQassembled 107 @pair_elim #pi #newppc #fetch_pseudo_refl normalize nodelta 28 108 @(pose … (λx. sigma (address_of_word_labels_code_mem instr_list x))) #lookup_labels #EQlookup_labels 29 109 @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels 30 110 whd in match execute_1_pseudo_instruction; normalize nodelta 31 whd in match ticks_of; normalize nodelta <EQppc >EQ2 normalize nodelta 32 lapply (snd_fetch_pseudo_instruction instr_list ppc) >EQ2 #EQnewppc >EQnewppc 33 lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … policy … ppc pi … EQlookup_labels EQlookup_datalabels ?) 34 [1: >EQ2 % 35 2: 36 3: normalize nodelta 111 whd in match ticks_of; normalize nodelta <EQppc >fetch_pseudo_refl normalize nodelta 112 lapply (snd_fetch_pseudo_instruction instr_list ppc) >fetch_pseudo_refl #EQnewppc >EQnewppc 113 lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … sigma policy sigma_policy_witness … ppc pi … EQlookup_labels EQlookup_datalabels ?) 114 [1: >fetch_pseudo_refl % ] 115 #assm1 #assm2 #assm3 generalize in match assm2; generalize in match assm3; 116 generalize in match assm1; assm1 assm2 assm3 117 normalize nodelta 37 118 cases pi 38 119 [2,3: 39 #ARG 40 #H3 normalize nodelta in H3; normalize in match (assembly_1_pseudoinstruction ??????) in H3; 41 #H2 42 whd in ⊢ (??%? → ?); @Some_Some_elim #MAP <MAP 120 #arg 121 (* XXX: we first work on sigma_increment_commutation *) 122 #sigma_increment_commutation 123 normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation; 124 (* XXX: we work on the maps *) 125 whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm 126 (* XXX: we assume the fetch_many hypothesis *) 127 #fetch_many_assm 128 (* XXX: we give the existential *) 129 %{0} 43 130 whd in match (execute_1_pseudo_instruction0 ?????); 44 %{0} @split_eq_status // 45 [1,2: /demod/ >EQnewppc >H3 <add_zero % (*CSC: auto not working, why? *) ] 46 6: (* Mov *) #arg1 #arg2 131 (* XXX: work on the left hand side of the equality *) 132 whd in ⊢ (??%?); 133 @split_eq_status // 134 [1,2: /demod/ >EQnewppc >sigma_increment_commutation <add_zero % (*CSC: auto not working, why? *) ] 135 6: (* Mov *) 136 #arg1 #arg2 137 (* XXX: we first work on sigma_increment_commutation *) 138 #sigma_increment_commutation 139 normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation; 140 (* XXX: we work on the maps *) 141 whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm 142 (* XXX: we assume the fetch_many hypothesis *) 143 #fetch_many_assm 144 (* XXX: we give the existential *) 145 %{1} 146 whd in match (execute_1_pseudo_instruction0 ?????); 147 (* XXX: work on the left hand side of the equality *) 148 whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc 149 (* XXX: execute fetches some more *) 150 whd in match code_memory_of_pseudo_assembly_program; normalize nodelta 151 whd in fetch_many_assm; 152 >EQassembled in fetch_many_assm; 153 cases (fetch ??) * #instr #newpc #ticks normalize nodelta * * 154 #eq_instr #EQticks whd in EQticks:(???%); >EQticks 155 #fetch_many_assm whd in fetch_many_assm; 156 lapply (eq_bv_eq … fetch_many_assm) fetch_many_assm #EQnewpc 157 >(eq_instruction_to_eq … eq_instr) instr whd in ⊢ (??%?); 158 (* XXX: now we start to work on the mk_PreStatus equality *) 159 change with (set_arg_16 ????? = ?) 160 >set_program_counter_mk_Status_commutation 161 >set_clock_mk_Status_commutation 162 >set_arg_16_mk_Status_commutation 163 164 change with (? = status_of_pseudo_status ?? (set_arg_16 ?????) ??) 165 >set_program_counter_mk_Status_commutation 166 >set_clock_mk_Status_commutation 167 >set_arg_16_mk_Status_commutation in ⊢ (???%); 168 169 170 @split_eq_status // 171 [1: 172 assumption 173 2: 174 @special_function_registers_8051_set_arg_16 175 [2: 176 >EQlookup_datalabels % 177 1: 178 * 179 #absurd1 #absurd2 180 try (@⊥ cases absurd1 absurd #absurd1 @absurd1 %) 181 try (@⊥ cases absurd2 absurd #absurd2 @absurd2 %) 182 whd in ⊢ (??%%); cases daemon (* XXX: not nice! manipulation of vectors; true though *) 183 ] 184 ] 185 186 (* 187 @(list_addressing_mode_tags_elim_prop … arg1) whd try % arg1 whd in ⊢ (??%?); 188 whd in match (get_arg_16 ????); whd in match (set_arg_16' ?????); 189 190 @split_eq_status 191 192 193 #fetch_many_assm 194 >assembly_refl in fetch_many_assm; 195 196 cases (fetch ??) * #instr #newppc' #ticks normalize nodelta 197 whd in ⊢ (??%?); 198 199 47 200 #H3 normalize nodelta in H3; normalize in match (assembly_1_pseudoinstruction ??????) in H3; 48 201 #H2 … … 70 223 #EQ >EQ EQ; normalize nodelta; >(eq_bv_eq … H2c) % 71 224 72 225 *) 73 226 74 227 4: (* Jmp *) #label whd in ⊢ (??%? → ???% → ?); … … 130 283 @low_internal_ram_write_at_stack_pointer 131 284 [ >EQ0 @pol  %  % 132  @( pair_destruct_2… EQ1)285  @( … EQ1) 133 286  @(pair_destruct_2 … EQ2) 134 287  >(pair_destruct_1 ????? EQpc)
Note: See TracChangeset
for help on using the changeset viewer.