Changeset 1984 for src


Ignore:
Timestamp:
May 22, 2012, 5:37:09 PM (8 years ago)
Author:
mulligan
Message:

Most proof obligations closed in main_lemma apart from those of the `false' cases in conditional jumps.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/AssemblyProof.ma

    r1983 r1984  
    14351435  [ nil ⇒ eq_bv … pc final_pc = true
    14361436  | cons i tl ⇒
    1437       (∃pc': Word. 〈i, pc', ticks_of_instruction i〉 = fetch code_memory pc ∧
     1437    let pc' ≝ add 16 pc (bitvector_of_nat 16 (|assembly1 … i|)) in
     1438      (〈i, pc', ticks_of_instruction i〉 = fetch code_memory pc ∧
    14381439        fetch_many code_memory final_pc pc' tl)
    14391440  ].
    … …  
    15071508    lapply (conjunction_true ?? H3) * #H4 #H5
    15081509    lapply (conjunction_true … H4) * #B1 #B2
    1509     %{pc'} <(eq_instruction_to_eq … B1) >(eq_bv_eq … H5)
    1510     >(eqb_true_to_refl … B2) % try % @IH @H2
     1510    >(eq_instruction_to_eq … B1) >(eq_bv_eq … H5) %
     1511    >(eqb_true_to_refl … B2) >(eq_instruction_to_eq … B1) try % @IH @H2
    15111512  ]
    15121513qed.
    … …  
    23642365  //
    23652366qed.
     2367
     2368(* XXX: easy but tedious *)
     2369axiom assembly1_lt_128:
     2370  ∀i: instruction.
     2371    |(assembly1 i)| < 128.
     2372
     2373axiom most_significant_bit_zero:
     2374  ∀size, m: nat.
     2375  ∀size_proof: 0 < size.
     2376    m < 2^size → get_index_v bool (S size) (bitvector_of_nat (S size) m) 1 ? = false.
     2377  normalize in size_proof; /2/
     2378qed.
     2379
     2380lemma bitvector_of_nat_sign_extension_equivalence:
     2381  ∀m: nat.
     2382  ∀size_proof: m < 128.
     2383    sign_extension … (bitvector_of_nat 8 m) = bitvector_of_nat 16 m.
     2384  #m #size_proof whd in ⊢ (??%?);
     2385  >most_significant_bit_zero
     2386  [1:
     2387    cases daemon
     2388  |2:
     2389    assumption
     2390  |3:
     2391    //
     2392  ]
     2393qed.

  • src/ASM/AssemblyProofSplit.ma

    r1983 r1984  
    9595qed.
    9696
     97lemma program_counter_set_arg_1:
     98  ∀M: Type[0].
     99  ∀cm: M.
     100  ∀s: PreStatus M cm.
     101  ∀addr: [[bit_addr; carry]].
     102  ∀b: Bit.
     103    program_counter M cm (set_arg_1 M cm s addr b) = program_counter M cm s.
     104  #M #cm #s whd in match set_arg_1; whd in match set_arg_1'; normalize nodelta
     105  #addr #b
     106  @(subaddressing_mode_elim … [[bit_addr; carry]] … [[bit_addr; carry]]) [1: // ]
     107  [1:
     108    #byte cases (split ????) #nu #nl normalize nodelta
     109    cases (split ????) #ignore #three_bits normalize nodelta
     110    cases (get_index_v bool ????) normalize nodelta
     111    [1:
     112      @program_counter_set_bit_addressable_sfr
     113    |2:
     114      @program_counter_set_low_internal_ram
     115    ]
     116  |2:
     117    cases (split ????) //
     118  ]
     119qed.
     120
    97121lemma None_Some_elim: ∀P:Prop. ∀A,a. None A = Some A a → P.
    98122 #P #A #a #abs destruct
    … …  
    166190    fetch_many code_memory final_pc start_pc [i] →
    167191      〈i, final_pc, ticks_of_instruction i〉 = fetch code_memory start_pc.
    168   #code_memory #final_pc #start_pc #i * #new_pc *
    169   #fetch_refl #fetch_many_assm whd in fetch_many_assm;
     192  #code_memory #final_pc #start_pc #i * #new_pc
     193  #fetch_many_assm whd in fetch_many_assm;
    170194  cases (eq_bv_eq … fetch_many_assm) assumption
    171195qed.
    … …  
    184208 ∀costs : BitVectorTrie costlabel 16.
    185209 ∀create_label_cost_refl : create_label_cost_map instr_list=〈labels,costs〉.
    186  ∀assembled : list Byte.
    187  ∀costs' : BitVectorTrie costlabel 16.
    188  ∀assembly_refl : assembly 〈preamble,instr_list〉 sigma policy=〈assembled,costs'〉.
    189  ∀EQassembled : assembled=\fst  (assembly cm sigma policy).
    190210 ∀newppc : Word.
    191211 ∀lookup_labels : Identifier→Word.
    192  ∀EQlookup_labels : lookup_labels = (λx:Identifier.sigma (address_of_word_labels_code_mem instr_list x)).
     212 ∀EQlookup_labels : lookup_labels = (λx:Identifier. address_of_word_labels_code_mem instr_list x).
    193213 ∀lookup_datalabels : identifier ASMTag→Word.
    194214 ∀EQlookup_datalabels : lookup_datalabels = (λx.lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)).
    … …  
    205225         (add 16 ppc (bitvector_of_nat 16 1))).
    206226 ∀P.
    207  ∀EQP:
    208   P = (λs.
    209         execute (|expand_relative_jump lookup_labels sigma ppc instr|)
    210        (code_memory_of_pseudo_assembly_program cm sigma
    211         policy)
    212        (status_of_pseudo_status M cm ps sigma policy)
    213       =status_of_pseudo_status M' cm s sigma policy).
     227 ∀EQP: P = (λinstr, s.
    214228  sigma (add 16 ppc (bitvector_of_nat 16 1))
    215229   =add 16 (sigma ppc)
    … …  
    224238     (expand_pseudo_instruction lookup_labels sigma policy (program_counter pseudo_assembly_program cm ps) lookup_datalabels
    225239      (Instruction instr))
    226      →P (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm
     240     → ∃n. execute n
     241       (code_memory_of_pseudo_assembly_program cm sigma
     242        policy)
     243       (status_of_pseudo_status M cm ps sigma policy)
     244      =status_of_pseudo_status M' cm s sigma policy).
     245     P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm
    227246         addr_of instr s).
    228247 #M #M' #preamble #instr_list #cm #EQcm #sigma #policy #sigma_policy_witness #ps #ppc #EQppc #labels
    229  #costs #create_label_cost_refl #assembled #costs' #assembly_refl #EQassembled #newppc
     248 #costs #create_label_cost_refl #newppc
    230249 #lookup_labels #EQlookup_labels #lookup_datalabels #EQlookup_datalabels #EQnewppc #instr
    231250 #ticks #EQticks #addr_of #EQaddr_of #s #EQs #P #EQP
    232  #sigma_increment_commutation #maps_assm #fetch_many_assm
     251 (*#sigma_increment_commutation #maps_assm #fetch_many_assm *)
    233252 letin a ≝ Identifier letin m ≝ pseudo_assembly_program
    234  cut (Σxxx:PseudoStatus cm. P (execute_1_preinstruction ticks a m cm addr_of instr s))
     253 cut (Σxxx:PseudoStatus cm. P instr (execute_1_preinstruction ticks a m cm addr_of instr s))
    235254 [2: * // ]
    236255 @(
    … …  
    644663whd in match execute_1_preinstruction; normalize nodelta
    645664[4,5,6,7,8,36,37,38,39,40,41,50: (* INC, CLR, CPL, PUSH *)
     665  (* XXX: work on the right hand side *)
    646666  lapply (subaddressing_modein ???)
    647667  <EQaddr normalize nodelta #irrelevant
    648668  try (>p normalize nodelta)
    649669  try (>p1 normalize nodelta)
    650   (* XXX: start work on the left hand side *)
    651   >EQP <instr_refl normalize nodelta whd in ⊢ (??%?);
    652   (* XXX: work on fetch_many *)
    653   <instr_refl in fetch_many_assm; #fetch_many_assm
    654   <(fetch_many_singleton … fetch_many_assm) whd in ⊢ (??%?);
    655   (* XXX: work on sigma commutation *)
    656   <instr_refl in sigma_increment_commutation; #sigma_increment_commutation
    657   (* XXX: work on both sides *)
     670  (* XXX: switch to the left hand side *)
     671  -instr_refl >EQP -P normalize nodelta
     672  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     673  whd in ⊢ (??%?);
     674  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
     675  (* XXX: work on the left hand side *)
    658676  [1,2,3,4,5:
    659677    generalize in ⊢ (??(???(?%))?);
    … …  
    666684  try @(jmpair_as_replace ?????????? p)
    667685  [10: normalize nodelta try @(jmpair_as_replace ?????????? p1) ]
    668   normalize nodelta
    669   (* XXX: work on ticks (of all kinds) *)
    670   <instr_refl in EQticks; #EQticks >EQticks
    671   (* XXX: removes status 's' *)
    672   normalize nodelta >EQs -s -ticks
     686  (* XXX: switch to the right hand side *)
     687  normalize nodelta >EQs -s >EQticks -ticks
    673688  whd in ⊢ (??%%);
    674   (* XXX: simplify the left hand side *)
     689  (* XXX: finally, prove the equality using sigma commutation *)
    675690  cases daemon
    676691  (* XXX: work on both sides *)
    677692|1,2,3,9,46,51,53,54,55: (* ADD, ADDC, SUBB, DEC, SWAP, POP, XCHD, RET, RETI  *)
    678   (* XXX: simplify the right hand side *)
     693  (* XXX: work on the right hand side *)
    679694  >p normalize nodelta
    680695  try (>p1 normalize nodelta)
    681   (* XXX: start work on the left hand side *)
    682   >EQP <instr_refl normalize nodelta whd in ⊢ (??%?);
    683   (* XXX: work on fetch_many *)
    684   <instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled
    685   whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
    686   whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy));
    687   <EQppc cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * *
    688   #eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm;
    689   >(eq_bv_eq … fetch_many_assm) -newpc
    690   >(eq_instruction_to_eq … eq_instr) -instr' whd in ⊢ (??%?);
    691   (* XXX: work on sigma commutation *)
    692   <instr_refl in sigma_increment_commutation; #sigma_increment_commutation
    693   (* XXX: work on ticks (of all kinds) *)
    694   >EQticks' -ticks' <instr_refl in EQticks; #EQticks >EQticks
    695   (* XXX: simplify the left hand side *)
     696  (* XXX: switch to the left hand side *)
     697  -instr_refl >EQP -P normalize nodelta
     698  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     699  whd in ⊢ (??%?);
     700  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
     701  (* XXX: work on the left hand side *)
    696702  @(pair_replace ?????????? p)
    697703  [1,3,5,7,9,11,13,15,17:
    … …  
    704710       ]
    705711  ]
    706   (* XXX: removes status 's' *)
    707   normalize nodelta >EQs -s -ticks
     712  (* XXX: switch to the right hand side *)
     713  normalize nodelta >EQs -s >EQticks -ticks
    708714  whd in ⊢ (??%%);
    709   (* XXX: work on both sides *)
     715  (* XXX: finally, prove the equality using sigma commutation *)
    710716  cases daemon (*
    711717       @split_eq_status try %
    … …  
    715721       ] *)
    716722|10,42,43,44,45,49,52,56: (* MUL *)
    717   (* XXX: simplify the right hand side *)
    718   (* XXX: start work on the left hand side *)
    719   >EQP <instr_refl normalize nodelta whd in ⊢ (??%?);
    720   (* XXX: work on fetch_many *)
    721   <instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled
    722   whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
    723   whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy));
    724   <EQppc cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * *
    725   #eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm;
    726   >(eq_bv_eq … fetch_many_assm) -newpc
    727   >(eq_instruction_to_eq … eq_instr) -instr' whd in ⊢ (??%?);
    728   (* XXX: work on sigma commutation *)
    729   <instr_refl in sigma_increment_commutation; #sigma_increment_commutation
    730   (* XXX: work on ticks (of all kinds) *)
    731   >EQticks' -ticks' <instr_refl in EQticks; #EQticks >EQticks
    732   (* XXX: removes status 's' *)
    733   normalize nodelta >EQs -s -ticks
     723  (* XXX: work on the right hand side *)
     724  (* XXX: switch to the left hand side *)
     725  -instr_refl >EQP -P normalize nodelta
     726  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     727  whd in ⊢ (??%?);
     728  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
     729  (* XXX: work on the left hand side *)
     730  (* XXX: switch to the right hand side *)
     731  normalize nodelta >EQs -s >EQticks -ticks
    734732  whd in ⊢ (??%%);
    735   (* XXX: work on both sides *)
    736   (* @split_eq_status try % *)
     733  (* XXX: finally, prove the equality using sigma commutation *)
    737734  cases daemon
    738735|11,12: (* DIV *)
     736  (* XXX: work on the right hand side *)
    739737  normalize nodelta in p;
    740738  >p normalize nodelta
    741   >EQP <instr_refl normalize nodelta whd in ⊢ (??%?);
    742   (* XXX: work on fetch_many *)
    743   <instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled
    744   whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
    745   whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy));
    746   <EQppc cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * *
    747   #eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm;
    748   >(eq_bv_eq … fetch_many_assm) -newpc
    749   >(eq_instruction_to_eq … eq_instr) -instr' whd in ⊢ (??%?);
    750   (* XXX: work on sigma commutation *)
    751   <instr_refl in sigma_increment_commutation; #sigma_increment_commutation
    752   (* XXX: work on ticks (of all kinds) *)
    753   >EQticks' -ticks' <instr_refl in EQticks; #EQticks >EQticks
    754   (* XXX: work on both sides *)
     739  (* XXX: switch to the left hand side *)
     740  -instr_refl >EQP -P normalize nodelta
     741  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     742  whd in ⊢ (??%?);
     743  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
    755744  @(pose … (nat_of_bitvector 8 ?)) #pose_assm #pose_refl
    756   >(?: pose_assm = 0)
     745  >(?: pose_assm = 0) normalize nodelta
    757746  [2,4:
    758747    <p >pose_refl
    759748    cases daemon
    760749  |1,3:
    761     (* XXX: removes status 's' *)
    762     normalize nodelta >EQs -s -ticks
     750    (* XXX: switch to the right hand side *)
     751    >EQs -s >EQticks -ticks
    763752    whd in ⊢ (??%%);
    764     (* XXX: work on both sides *)
     753    (* XXX: finally, prove the equality using sigma commutation *)
    765754    @split_eq_status try %
    766755    cases daemon
    767756  ]
    768757|13,14,15: (* DA *)
     758  (* XXX: work on the right hand side *)
    769759  >p normalize nodelta
    770760  >p1 normalize nodelta
    … …  
    773763  try (>p4 normalize nodelta
    774764  try (>p5 normalize nodelta))))
    775   >EQP <instr_refl normalize nodelta whd in ⊢ (??%?);
    776   (* XXX: work on fetch_many *)
    777   <instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled
    778   whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
    779   whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy));
    780   <EQppc cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * *
    781   #eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm;
    782   >(eq_bv_eq … fetch_many_assm) -newpc
    783   >(eq_instruction_to_eq … eq_instr) -instr' whd in ⊢ (??%?);
    784   (* XXX: work on sigma commutation *)
    785   <instr_refl in sigma_increment_commutation; #sigma_increment_commutation
    786   (* XXX: work on ticks (of all kinds) *)
    787   >EQticks' -ticks' <instr_refl in EQticks; #EQticks >EQticks
    788   (* XXX: work on both sides *)
     765  (* XXX: switch to the left hand side *)
     766  -instr_refl >EQP -P normalize nodelta
     767  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     768  whd in ⊢ (??%?);
     769  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
     770  (* XXX: work on the left hand side *)
    789771  @(pair_replace ?????????? p)
    790772  [1,3,5:
    … …  
    804786      ]
    805787    ]
    806     (* XXX: removes status 's' *)
    807     normalize nodelta >EQs -s -ticks
     788  (* XXX: switch to the right hand side *)
     789  normalize nodelta >EQs -s >EQticks -ticks
     790  whd in ⊢ (??%%);
     791  (* XXX: finally, prove the equality using sigma commutation *)
     792  @split_eq_status try %
     793  cases daemon
     794  ]
     795|33,34,35,48: (* ANL, ORL, XRL, MOVX *)
     796  (* XXX: work on the right hand side *)
     797  cases addr #addr' normalize nodelta
     798  [1,3:
     799    cases addr' #addr'' normalize nodelta
     800  ]
     801  @pair_elim #lft #rgt #lft_rgt_refl >lft_rgt_refl normalize nodelta
     802  (* XXX: switch to the left hand side *)
     803  -instr_refl >EQP -P normalize nodelta
     804  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     805  whd in ⊢ (??%?);
     806  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
     807  (* XXX: work on the left hand side *)
     808  (* XXX: switch to the right hand side *)
     809  normalize nodelta >EQs -s >EQticks -ticks
     810  whd in ⊢ (??%%);
     811  (* XXX: finally, prove the equality using sigma commutation *)
     812  cases daemon
     813|47: (* MOV *)
     814  (* XXX: work on the right hand side *)
     815  cases addr -addr #addr normalize nodelta
     816  [1:
     817    cases addr #addr normalize nodelta
     818    [1:
     819      cases addr #addr normalize nodelta
     820      [1:
     821        cases addr #addr normalize nodelta
     822        [1:
     823          cases addr #addr normalize nodelta
     824        ]
     825      ]
     826    ]
     827  ]
     828  cases addr #lft #rgt normalize nodelta
     829  (* XXX: switch to the left hand side *)
     830  >EQP -P normalize nodelta
     831  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     832  whd in ⊢ (??%?);
     833  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
     834  (* XXX: work on the left hand side *)
     835  (* XXX: switch to the right hand side *)
     836  normalize nodelta >EQs -s >EQticks -ticks
     837  whd in ⊢ (??%%);
     838  (* XXX: finally, prove the equality using sigma commutation *)
     839  cases daemon
     840|16,18,20,22,24,26,28: (* JC, JNC, JB, JNB, JBC, JZ, JNZ (true cases) *)
     841  (* XXX: work on the right hand side *)
     842  >p normalize nodelta
     843  (* XXX: switch to the left hand side *)
     844  -instr_refl >EQP -P normalize nodelta
     845  #sigma_increment_commutation #maps_assm #fetch_many_assm
     846 
     847  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
     848  whd in match (expand_relative_jump ????);
     849  <EQppc in fetch_many_assm;
     850  @pair_elim #result #flags #sub16_refl
     851  @pair_elim #upper #lower #split_refl
     852  cases (eq_bv ???) normalize nodelta
     853  [1,3,5,7,9,11,13:
     854    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
     855    whd in ⊢ (??%?);
     856    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
     857    (* XXX: work on the left hand side *)
     858    @(if_then_else_replace ???????? p) normalize nodelta
     859    [1,3,5,7,9,11,13:
     860      cases daemon
     861    ]
     862    (* XXX: switch to the right hand side *)
     863    normalize nodelta >EQs -s >EQticks -ticks
    808864    whd in ⊢ (??%%);
    809     (* XXX: work on both sides *)
     865    (* XXX: finally, prove the equality using sigma commutation *)
    810866    @split_eq_status try %
    811867    cases daemon
    812   ]
    813 |33,34,35,48: (* ANL, ORL, XRL, MOVX *)
    814   (* XXX: simplify the right hand side *)
    815   inversion addr #addr' #EQaddr normalize nodelta
    816   [1,3:
    817     inversion addr' #addr'' #EQaddr' normalize nodelta
    818   ]
    819   @pair_elim #lft #rgt #lft_rgt_refl normalize nodelta
    820   (* XXX: start work on the left hand side *)
    821   >EQP <instr_refl normalize nodelta whd in ⊢ (??%?);
    822   (* XXX: work on fetch_many *)
    823   <instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled
    824   whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
    825   whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy));
    826   <EQppc cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * *
    827   #eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm;
    828   >(eq_bv_eq … fetch_many_assm) -newpc
    829   >(eq_instruction_to_eq … eq_instr) -instr' whd in ⊢ (??%?);
    830   (* XXX: work on sigma commutation *)
    831   <instr_refl in sigma_increment_commutation; #sigma_increment_commutation
    832   (* XXX: work on ticks (of all kinds) *)
    833   >EQticks' -ticks' <instr_refl in EQticks; #EQticks >EQticks
    834   (* XXX: simplify the left hand side *)
    835   >EQaddr normalize nodelta try (>EQaddr' normalize nodelta)
    836   >lft_rgt_refl normalize nodelta
    837   (* XXX: removes status 's' *)
    838   normalize nodelta >EQs -s -ticks
    839   whd in ⊢ (??%%);
    840   (* XXX: work on both sides *)
    841   cases daemon
    842 |47: (* MOV *)
    843 |* (* JUMPS!!! *)
     868  |2,4,6,8,10,12,14:
     869    >EQppc
     870    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
     871    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
     872    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
     873    #fetch_many_assm whd in fetch_many_assm; %{2}
     874    change with (execute_1 ?? = ?)
     875    @(pose … (execute_1 ? (status_of_pseudo_status …)))
     876    #status_after_1 #EQstatus_after_1
     877    <(?: ? = status_after_1)
     878    [3,6,9,12,15,18,21:
     879      >EQstatus_after_1 in ⊢ (???%);
     880      whd in ⊢ (???%);
     881      [1: <fetch_refl in ⊢ (???%);
     882      |2: <fetch_refl in ⊢ (???%);
     883      |3: <fetch_refl in ⊢ (???%);
     884      |4: <fetch_refl in ⊢ (???%);
     885      |5: <fetch_refl in ⊢ (???%);
     886      |6: <fetch_refl in ⊢ (???%);
     887      |7: <fetch_refl in ⊢ (???%);
     888      ]
     889      whd in ⊢ (???%);
     890      @(if_then_else_replace ???????? p)
     891      [1,3,5,7,9,11,13:
     892        cases daemon
     893      |2,4,6,8,10,12,14:
     894        normalize nodelta
     895        whd in match (addr_of_relative ????);
     896        >set_clock_mk_Status_commutation
     897        [5:
     898          (* XXX: demodulation not working in this case *)
     899          >program_counter_set_arg_1 in ⊢ (???%);
     900          >program_counter_set_program_counter in ⊢ (???%);
     901        |*:
     902          /demod/
     903        ]
     904        whd in ⊢ (???%);
     905        change with (add ???) in match (\snd (half_add ???));
     906        >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
     907        [2,4,6,8,10,12,14:
     908          >bitvector_of_nat_sign_extension_equivalence
     909          [1,3,5,7,9,11,13:
     910            >EQintermediate_pc' %
     911          |*:
     912            repeat @le_S_S @le_O_n
     913          ]
     914        ]
     915        %
     916      ]
     917    |1,4,7,10,13,16,19:
     918      skip
     919    ]
     920    -status_after_1
     921    @(pose … (execute_1 ? (mk_PreStatus …)))
     922    #status_after_1 #EQstatus_after_1
     923    <(?: ? = status_after_1)
     924    [3,6,9,12,15,18,21:
     925      >EQstatus_after_1 in ⊢ (???%);
     926      whd in ⊢ (???%);
     927      (* XXX: matita bug with patterns across multiple goals *)
     928      [1: <fetch_refl'' in ⊢ (???%);
     929      |2: <fetch_refl'' in ⊢ (???%);
     930      |3: <fetch_refl'' in ⊢ (???%);
     931      |4: <fetch_refl'' in ⊢ (???%);
     932      |5: <fetch_refl'' in ⊢ (???%);
     933      |6: <fetch_refl'' in ⊢ (???%);
     934      |7: <fetch_refl'' in ⊢ (???%);
     935      ]
     936      whd in ⊢ (???%);
     937      [5:
     938      |*:
     939        /demod/
     940      ] %
     941    |1,4,7,10,13,16,19:
     942      skip
     943    ]
     944    -status_after_1 whd in ⊢ (??%?);
     945    (* XXX: switch to the right hand side *)
     946    normalize nodelta >EQs -s >EQticks -ticks
     947    whd in ⊢ (??%%);
     948    (* XXX: finally, prove the equality using sigma commutation *)
     949    @split_eq_status try %
     950    [3,7,11,15,20,28,32:
     951      >program_counter_set_program_counter >set_clock_mk_Status_commutation
     952      [5: >program_counter_set_program_counter ]
     953      >EQaddr_of normalize nodelta
     954      whd in ⊢ (??%?); >EQlookup_labels normalize nodelta
     955      >EQcm %
     956    |*:
     957      cases daemon
     958    ]
    844959]
    845960qed.
Note: See TracChangeset for help on using the changeset viewer.