Changeset 1966


Ignore:
Timestamp:
May 17, 2012, 5:45:21 PM (7 years ago)
Author:
mulligan
Message:

Progress made on main_thm proof: trying to find a pattern to use across all ~150 goals

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r1957 r1966  
    13121312
    13131313lemma destruct_bug_fix:
    1314   3 = 0 → False.
    1315   #absurd destruct(absurd)
     1314  ∀n: nat.
     1315    S n = 0 → False.
     1316  #n #absurd destruct(absurd)
    13161317qed.
    13171318
     
    13191320  ∀b: BitVector 3.
    13201321    ∃l, c, r: bool.
    1321       b ≃ [[l; c; r]] ≝ ?.
     1322      b ≃ [[l; c; r]].
    13221323  #b
    13231324  @(Vector_inv_ind bool 3 b (λn: nat. λv: Vector bool n. ∃l:bool.∃c:bool.∃r:bool. v ≃ [[l; c; r]]))
    13241325  [1:
    1325     #absurd @⊥ @destruct_bug_fix
     1326    #absurd @⊥ -b @(destruct_bug_fix 2)
    13261327    >absurd %
    13271328  |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;
    13291334    cases daemon
    13301335  ]
     1336  cases daemon
    13311337qed.
    13321338
     
    14771483    encoding_check code_memory pc pc_plus_len assembled →
    14781484      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
     1495qed.
     1496
     1497definition 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
     1505definition 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 …))).
    14901522
    14911523(* This is a trivial consequence of fetch_assembly_pseudo + the proof that the
     
    15011533  ∀sigma: Word → Word.
    15021534  ∀policy: Word → bool.
     1535  ∀sigma_policy_witness: sigma_policy_specification program sigma policy.
    15031536  ∀assembled.
    15041537  ∀costs'.
    15051538  let 〈preamble, instr_list〉 ≝ program in
    15061539  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 in
    1510   let datalabels ≝ construct_datalabels (\fst program) in
    1511   let lookup_labels ≝ λx. sigma (address_of_word_labels_code_mem (\snd program) x) in 
    1512   let lookup_datalabels ≝ λx. lookup_def ?? datalabels x (zero ?) in
    1513   ∀ppc.
    1514   let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
    1515   let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
    1516   let pc ≝ sigma ppc in
    1517   let pc_plus_len ≝ add … pc (bitvector_of_nat … len) in
    1518    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'
    15211554  @pair_elim #preamble #instr_list #program_refl
    15221555  @pair_elim #labels #costs #create_label_cost_refl
    1523   #assembly_refl %
     1556  #assembly_refl % cases daemon (*
    15241557  [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 %
    15281570      [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
    15341572      |2:
    1535         <assembly_refl %
    15361573      ]
    1537     |2:
    1538       >create_label_cost_refl %
    1539     ]
    1540   |2:
     1574    ]
    15411575  ]
    1542   cases daemon (* XXX: !!! *)
     1576  cases daemon (* XXX: !!! *) *)
    15431577qed.
    15441578
     
    15481582  ∀sigma.
    15491583  ∀policy.
     1584  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
    15501585  ∀ppc.
    15511586  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
     
    15581593  let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
    15591594    fetch_many code_memory (sigma newppc) (sigma ppc) instructions.
    1560   * #preamble #instr_list #sigma #policy #ppc
     1595  * #preamble #instr_list #sigma #policy #sigma_policy_specification_witness #ppc
    15611596  @pair_elim #labels #costs #create_label_map_refl
    15621597  @pair_elim #assembled #costs' #assembled_refl
     
    15661601  letin lookup_datalabels ≝ (λx. ?)
    15671602  @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')
    15691604  normalize nodelta
    15701605  @pair_elim #labels' #costs' #create_label_map_refl' #H
     
    15761611  lapply (H ppc) >fetch_pseudo_refl #H
    15771612  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
    15791615  >fetch_pseudo_refl in H1; #assm @assm assumption
    15801616qed.
     
    22182254qed.
    22192255
    2220 definition is_present_in_machine_code_image_p: ∀pseudo_instruction. Prop ≝
    2221   λpseudo_instruction.
    2222     match pseudo_instruction with
    2223     [ Comment c ⇒ False
    2224     | Cost c ⇒ False
    2225     | _ ⇒ True
    2226     ].
    2227 
    22282256lemma pair_destruct_right:
    22292257  ∀A: Type[0].
     
    22402268  ∀sigma: Word → Word.
    22412269  ∀policy: Word → bool.
     2270  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
    22422271  ∀ppc: Word.
    22432272  ∀pi.
    2244   ∀present_in_machine_code_image_witness: is_present_in_machine_code_image_p pi.
    22452273  ∀lookup_labels.
    22462274  ∀lookup_datalabels.
     
    22502278    let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) ppc lookup_datalabels  pi) in
    22512279      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_witness
    2253   #lookup_labels #lookup_datalabels #lookup_labels_refl #lookup_datalabels_refl
    2254   #fetch_pseudo_refl
     2280  #program #sigma #policy #sigma_policy_specification_witness #ppc #pi
     2281  #lookup_labels #lookup_datalabels
     2282  #lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl
    22552283  normalize nodelta
    22562284  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_witness
    2258   cases pi
    2259   [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 absurd
    2264   |4,5:
    2265     #identifier #_
    2266   |6:
    2267     #dptr #identifier #_
    2268   ]
    22692285  #fetch_pseudo_refl
    22702286  letin assembled ≝ (\fst (assembly program sigma policy))
    22712287  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)
    22732289  @pair_elim #preamble #instr_list #program_refl
    22742290  @pair_elim #labels #costs' #create_label_cost_map_refl
     
    22762292  lapply (H ppc) -H
    22772293  @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
    22792296  #encoding_check_assm #sigma_newppc_refl
    22802297  >fetch_pseudo_refl' in fetch_pseudo_refl; #pi_refl'
    22812298  >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
    22832302  <sigma_newppc_refl
    22842303  generalize in match fetch_pseudo_refl';
  • src/ASM/AssemblyProofSplit.ma

    r1963 r1966  
    33include alias "basics/logic.ma".
    44
    5 axiom add_commutative:
    6   ∀n: nat.
    7   ∀l, r: BitVector n.
    8     add … l r = add … r l.
     5lemma 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 %
     28qed.
     29
     30lemma 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  //
     47qed.       
     48
     49lemma 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  //
     66qed.
     67
     68
     69lemma 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
     85qed.
     86
    987
    1088theorem main_thm:
    1189  ∀M.
    1290  ∀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' →
    1897      ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) =
    1998        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 #policy
     99          (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
    22101  change with (next_internal_pseudo_address_map0 ????? = ? → ?)
    23102  @(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
    28108  @(pose … (λx. sigma (address_of_word_labels_code_mem instr_list x))) #lookup_labels #EQlookup_labels
    29109  @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
    30110  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
    37118  cases pi
    38119  [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}
    43130    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   
    47200      #H3 normalize nodelta in H3; normalize in match (assembly_1_pseudoinstruction ??????) in H3;
    48201      #H2
     
    70223       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
    71224
    72 
     225*)
    73226
    74227  |4: (* Jmp *) #label whd in ⊢ (??%? → ???% → ?);
     
    130283              @low_internal_ram_write_at_stack_pointer
    131284               [ >EQ0 @pol | % | %
    132                | @(pair_destruct_2 … EQ1)
     285               | @(  … EQ1)
    133286               | @(pair_destruct_2 … EQ2)
    134287               | >(pair_destruct_1 ????? EQpc)
Note: See TracChangeset for help on using the changeset viewer.