Changeset 3253


Ignore:
Timestamp:
May 6, 2013, 4:08:52 PM (4 years ago)
Author:
piccolo
Message:

some proof obbligation closed of ERTL to LTL proof

Location:
src/ERTL
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTLProof.ma

    r3252 r3253  
    44include "common/AssocList.ma".
    55include "joint/StatusSimulationHelper.ma".
     6include "ERTL/MoveCorrectness.ma".
    67
    78(* Inefficient, replace with Trie lookup *)
     
    227228].
    228229
    229 definition write_decision :
    230 ℕ →  decision → beval → state LTL_LIN_state → res (state LTL_LIN_state) ≝
    231 λlocalss,d,bv,st.
    232 match d with
    233 [ decision_spill n ⇒
    234   ! addrl ← hw_reg_retrieve (regs … st) RegisterSPL;
    235   ! addrh ← hw_reg_retrieve (regs … st) RegisterSPH;
    236   ! 〈newaddrl,new_carry〉 ←
    237      be_op2 (carry … st) Add (BVByte (bitvector_of_nat 8 (localss + n))) addrl;
    238   ! 〈newaddrh,new_carry'〉← be_op2 new_carry Addc zero_byte addrh;
    239   ! ptr ← pointer_of_address 〈newaddrl,newaddrh〉;
    240   ! new_mem ← opt_to_res ? [MSG FailedStore] (bestorev (m … st) ptr bv);
    241   return
    242    set_m ? new_mem
    243    (set_regs LTL_semantics
    244     (hwreg_store RegisterDPL newaddrl (hwreg_store RegisterDPH newaddrh (regs … st)))
    245      (set_carry ? new_carry' st))
    246 | decision_colour r ⇒
    247    !rgs  ← hw_reg_store r bv (regs … st);
    248     return set_regs LTL_LIN_state rgs st
    249 ].
    250 
    251 definition read_arg_decision : ℕ  → state LTL_LIN_state → arg_decision →
    252 res (beval × (state LTL_LIN_state)) ≝
    253 λlocalss,st,d.
    254 match d with
    255 [ arg_decision_colour r ⇒
    256     return 〈hwreg_retrieve (regs … st) r,st〉
    257 | arg_decision_spill n ⇒
    258   ! addrl ← hw_reg_retrieve (regs … st) RegisterSPL;
    259   ! addrh ← hw_reg_retrieve (regs … st) RegisterSPH;
    260   ! 〈newaddrl,new_carry〉 ←
    261      be_op2 (carry … st) Add (BVByte (bitvector_of_nat 8 (localss + n))) addrl;
    262   ! 〈newaddrh,new_carry'〉← be_op2 new_carry Addc zero_byte addrh;
    263   ! ptr ← pointer_of_address 〈newaddrl,newaddrh〉;
    264   ! bv ← opt_to_res ? [MSG FailedLoad] (beloadv (m … st) ptr);
    265   return 〈bv,set_regs LTL_semantics (hwreg_store RegisterDPL newaddrl
    266                                      (hwreg_store RegisterDPH newaddrh
    267                                        (regs … st))) (set_carry ? new_carry' st)〉
    268 | arg_decision_imm b ⇒
    269    return 〈BVByte b,st〉
    270 ].
    271 
    272230axiom insensitive_to_be_cleared_sb :
    273231 ∀prog. ∀tb : local_clear_sb_type. ∀st : state LTL_LIN_state.
     
    288246@lookup_insert_hit
    289247qed.
    290 
    291 include alias "arithmetics/nat.ma".
    292 
    293 definition is_zero: nat → Prop ≝
    294  λn. match n with [ O ⇒ True | S _ ⇒ False ].
    295 
    296 lemma furbo: ∀r,s. eqb (nat_of_register r) (nat_of_register s) → r = s.
    297 * normalize in ⊢ (∀_. ?(?%?) → ?);
    298 try ( #x cases x normalize * %) (* 24s *)
    299 qed.
    300 
    301 (* it is true but there are 1296 cases *)
    302 lemma nat_of_register_inj : ∀r,s.nat_of_register r = nat_of_register s →  r = s.
    303 #r #s #H @furbo @eqb_elim #H2 try % @(absurd … H H2)
    304 qed.
    305  
    306 lemma eq_Register_elim : ∀P : bool → Prop.
    307 ∀r,s: Register.(r=s → P true) → (r ≠s → P false) →
    308 P (eq_Register r s).
    309 #P #r #s #H1 #H2 whd in match eq_Register; normalize nodelta
    310 @eqb_elim
    311 [ #H @H1 @(nat_of_register_inj … H)
    312 | * #H @H2 % #EQ @H >EQ %
    313 ]
    314 qed.
    315 
    316 lemma hwreg_retrieve_hwregstore_hit :
    317 ∀regs,r,bv.
    318 hwreg_retrieve (hwreg_store r bv regs) r = bv.
    319 #regs #r #bv whd in match hwreg_retrieve; whd in match hwreg_store;
    320 normalize nodelta @lookup_insert_hit
    321 qed.
    322 
    323 axiom bitvector_of_register_inj : ∀r,s.
    324 bitvector_of_register r = bitvector_of_register s → r =s.
    325 
    326 lemma hwreg_retrieve_hwregstore_miss :
    327 ∀regs,r,s,bv.
    328 r ≠ s →
    329 hwreg_retrieve (hwreg_store s bv regs) r = hwreg_retrieve regs r.
    330 #regs #r #s #bv * #H whd in match hwreg_retrieve; whd in match hwreg_store;
    331 normalize nodelta @lookup_insert_miss @eq_bv_elim
    332 [ #H1 @H @(bitvector_of_register_inj … H1) ] #_ @I
    333 qed.
    334 
    335 lemma hwreg_retrieve_insensitive_to_set_other :
    336 ∀regs,r,b.
    337 hwreg_retrieve (hwreg_set_other b regs) r = hwreg_retrieve regs r.
    338 #regs #r #b %
    339 qed.
    340 
    341 axiom hwreg_store_idempotent : ∀r,bv1,bv2,regs.
    342 hwreg_store r bv1 (hwreg_store r bv2 regs) =
    343 hwreg_store r bv1 regs.
    344 
    345 axiom hwreg_store_commute : ∀r1,r2,bv1,bv2,regs.
    346 r1 ≠r2 →
    347 hwreg_store r1 bv1 (hwreg_store r2 bv2 regs) =
    348 hwreg_store r2 bv2 (hwreg_store r1 bv1 regs).
    349 
    350 axiom other_bit_insensitive_to_reg_store : ∀r,bv,regs.
    351 other_bit (hwreg_store r bv regs) = other_bit regs.
    352 
    353 axiom hwreg_store_retrieve_eq : ∀r,regs.
    354 hwreg_store r (hwreg_retrieve regs r) regs = regs.
    355 
    356 definition invariant_for_move :  arg_decision → Prop ≝
    357 λsrc.match src with
    358 [ arg_decision_colour r ⇒ r ≠ RegisterDPL ∧ r ≠ RegisterDPH
    359 | _ ⇒ True
    360 ].
    361 
    362 lemma hwreg_store_set_other_commut : ∀regs,r,bv,b.
    363 hwreg_store r bv (hwreg_set_other b regs) =
    364 hwreg_set_other b (hwreg_store r bv regs).
    365 * #reg_env #other #r #bv #b %
    366 qed.
    367 
    368 lemma move_spec : ∀prog.∀stack_size.∀localss : nat.
    369 ∀ carry_lives_after : bool.∀dest : decision.∀src : arg_decision.
    370 ∀f : ident.
    371 ∀s : state LTL_LIN_state.
    372 invariant_for_move src →
    373 repeat_eval_seq_no_pc LTL_semantics (mk_prog_params LTL_semantics prog stack_size) f
    374    (move (prog_names … prog) localss carry_lives_after dest src) s =
    375 match src with
    376 [ arg_decision_spill n ⇒
    377   match dest with
    378   [ decision_spill n1 ⇒
    379      if eqb n n1 then return s
    380      else ! 〈bv,s'〉 ← (read_arg_decision localss s src);
    381           let news ≝ set_regs LTL_semantics (hwreg_store RegisterA bv (regs … s')) s' in
    382           ! s'' ← write_decision localss dest bv news;
    383           let regSt1 ≝ (hwreg_store RegisterST1 bv (regs … s'')) in
    384           if carry_lives_after then
    385             return set_regs LTL_semantics (hwreg_set_other (carry … s) regSt1)
    386                     (set_carry ? (carry … s) s'')
    387           else
    388             return set_regs LTL_semantics regSt1 s''
    389    | decision_colour r ⇒
    390         if eq_Register r RegisterA then
    391          ! 〈bv,s'〉 ← (read_arg_decision localss s src);
    392          ! s'' ← write_decision localss dest bv s';
    393          if carry_lives_after then
    394            return set_regs LTL_semantics (hwreg_set_other (carry … s) (regs … s''))
    395                    (set_carry ? (carry … s) s'')
    396          else
    397            return s''
    398         else
    399          ! 〈bv,s'〉 ← (read_arg_decision localss s src);
    400          let news ≝ set_regs LTL_semantics (hwreg_store RegisterA bv (regs … s')) s' in
    401          ! s'' ← write_decision localss dest bv news;
    402          if carry_lives_after then
    403            return set_regs LTL_semantics (hwreg_set_other (carry … s) (regs … s''))
    404                    (set_carry ? (carry … s) s'')
    405          else
    406            return s''
    407    ]
    408 | arg_decision_colour r ⇒
    409       match dest with
    410       [ decision_spill _ ⇒
    411         ! 〈bv,s'〉 ← (read_arg_decision localss s src);
    412         let rgs ≝ if eq_Register r RegisterA then
    413                hwreg_store RegisterST1 (hwreg_retrieve (regs … s') RegisterA)
    414                 (regs … s')
    415               else
    416                hwreg_store RegisterA (hwreg_retrieve (regs … s') r) (regs … s') in
    417         ! s'' ← write_decision localss dest bv (set_regs LTL_semantics rgs s');
    418         if carry_lives_after then
    419            return set_regs LTL_semantics (hwreg_set_other (carry … s) (regs … s''))
    420                    (set_carry ? (carry … s) s'')
    421          else
    422            return s''
    423       | decision_colour r1 ⇒
    424          if eq_Register r1 r then return s
    425          else if eq_Register r1 RegisterA then
    426                ! 〈bv,s'〉 ← (read_arg_decision localss s src);
    427                write_decision localss dest bv s'
    428          else ! 〈bv,s'〉 ← (read_arg_decision localss s src);
    429                let rgs ≝ (hwreg_store RegisterA (hwreg_retrieve (regs … s) r) (regs … s')) in
    430                write_decision localss dest bv (set_regs LTL_semantics rgs s')
    431       ]     
    432 | arg_decision_imm b ⇒
    433    match dest with
    434    [ decision_spill _ ⇒
    435       ! 〈bv,s'〉 ← (read_arg_decision localss s src);
    436       let rgs ≝ hwreg_store RegisterA (BVByte b) (regs … s') in
    437       ! s'' ← write_decision localss dest bv (set_regs LTL_semantics rgs s');
    438       if carry_lives_after then
    439            return set_regs LTL_semantics (hwreg_set_other (carry … s) (regs … s''))
    440                    (set_carry ? (carry … s) s'')
    441          else
    442            return s''
    443    | decision_colour r ⇒
    444       ! 〈bv,s'〉 ← (read_arg_decision localss s src);
    445       if eq_Register r RegisterA then 
    446        write_decision localss dest bv s'
    447       else
    448        write_decision localss dest bv
    449         (set_regs LTL_semantics
    450          (hwreg_store RegisterA (BVByte b) (regs … s')) s')
    451   ]
    452 ].
    453 (*
    454 #prog #stack_size #localss #cl #dest #src #f #st #good
    455 inversion(repeat_eval_seq_no_pc ?????)
    456 [ #st' whd in match move; normalize nodelta
    457   cases dest in good; -dest normalize nodelta
    458   [ #off cases src -src normalize nodelta
    459     [ #r whd in match invariant_for_move; normalize nodelta
    460       whd in match preserve_carry_bit; normalize nodelta * #H1 #H2
    461       cases cl -cl normalize nodelta
    462       whd in match set_stack; normalize nodelta whd in match read_arg_decision;
    463       normalize nodelta @eq_Register_elim
    464       [1,3: #EQ destruct(EQ) normalize nodelta whd in match set_stack_a;
    465             normalize nodelta
    466       |*:   * #Hr normalize nodelta
    467       ]
    468       whd in match set_stack_not_a; whd in match set_dp_by_offset;
    469       whd in match repeat_eval_seq_no_pc; normalize nodelta
    470       whd in match (m_fold ??????) in ⊢ (??%?? → ?);
    471       inversion (eval_seq_no_pc ??????) [2,4,6,8: #e #_ normalize nodelta #EQ destruct]
    472       #st1 whd in match eval_seq_no_pc in ⊢ (% → ?); whd in match acca_arg_retrieve;
    473       normalize nodelta
    474       change with (hw_reg_retrieve ??) in match (acca_arg_retrieve_ ?????);
    475       whd in match hw_reg_retrieve; normalize nodelta whd in match set_regs;
    476       normalize nodelta >hwreg_retrieve_hwregstore_hit >m_return_bind
    477       whd in match snd_arg_retrieve; normalize nodelta
    478       whd in match (snd_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_miss
    479       [2,4,6,8: % #ABS whd in ABS : (??%%); destruct(ABS)]
    480       [1,2: >hwreg_retrieve_hwregstore_miss
    481             [2,4: % #ABS whd in ABS : (??%%); destruct(ABS)] ]
    482       [1,3: >hwreg_retrieve_insensitive_to_set_other ] >m_return_bind
    483       #H @('bind_inversion H) -H * #x1 #x2 #EQx1x2 whd in match acca_store;
    484       normalize nodelta change with (hw_reg_store ???) in match (acca_store_ ??????);
    485       whd in match hw_reg_store; normalize nodelta >hwreg_store_idempotent
    486       [ >hwreg_retrieve_insensitive_to_set_other ] >m_return_bind
    487       whd in match set_carry; whd in match set_regs; normalize nodelta
    488       whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match (m_fold ??????) in ⊢ (??%?? → ?);
    489       inversion (eval_seq_no_pc ??????) [2,4,6,8: #e #_ whd in ⊢ (??%%% → ?); #EQ destruct(EQ)]
    490       #st'' whd in match set_regs; normalize nodelta >hwreg_retrieve_hwregstore_hit in ⊢ (% → ?);
    491       >(hwreg_store_commute RegisterDPL RegisterA) [2,4,6,8: % normalize #EQ destruct]
    492       >hwreg_store_idempotent whd in match eval_seq_no_pc in ⊢ (% → ?);
    493       whd in match acca_arg_retrieve; normalize nodelta
    494       change with (hw_reg_retrieve ??) in match (acca_arg_retrieve_ ?????) in ⊢ (% → ?);
    495       whd in match hw_reg_retrieve; normalize nodelta >hwreg_retrieve_hwregstore_hit
    496       >m_return_bind whd in match snd_arg_retrieve; normalize nodelta
    497       whd in match (snd_arg_retrieve_ ?????);
    498       >hwreg_retrieve_hwregstore_miss [2,4,6,8: % normalize #EQ destruct(EQ)]
    499       >hwreg_retrieve_hwregstore_miss [2,4,6,8: % normalize #EQ destruct(EQ)]
    500       [1,3: >hwreg_retrieve_hwregstore_miss [2,4: % normalize #EQ destruct(EQ)] ]
    501       [1,3: >hwreg_retrieve_insensitive_to_set_other ] >m_return_bind
    502       #H @('bind_inversion H) -H * #y1 #y2 #EQy1y2 whd in match acca_store;
    503       normalize nodelta whd in match (acca_store_ ??????);
    504       >hwreg_store_idempotent >m_return_bind whd in match set_carry;
    505       whd in match set_regs; normalize nodelta whd in ⊢ (??%% → ?); #EQ
    506       destruct(EQ) whd in match (m_fold ??????) in ⊢ (??%?? → ?);
    507       inversion (eval_seq_no_pc ??????)
    508       [2,4,6,8: #e #_ whd in ⊢ (??%%% → ?); #EQ destruct(EQ)] #st''
    509       whd in match set_regs; normalize nodelta
    510       [ >hwreg_retrieve_hwregstore_miss in ⊢ (??(??????(?????(??%?)??))?? → ?);
    511         [2: normalize % #EQ destruct]
    512         >hwreg_retrieve_hwregstore_miss in ⊢ (??(??????(?????(??%?)??))?? → ?);
    513         [2: normalize % #EQ destruct]
    514         >hwreg_retrieve_hwregstore_miss in ⊢ (??(??????(?????(??%?)??))?? → ?);
    515         [2: normalize % #EQ destruct]
    516         >hwreg_retrieve_hwregstore_hit in ⊢ (??(??????(?????(??%?)??))?? → ?);
    517         >hwreg_retrieve_hwregstore_hit in ⊢ (??(??????(?????(???%)??))?? → ?);
    518       | >hwreg_retrieve_hwregstore_hit
    519       | >hwreg_retrieve_hwregstore_miss in ⊢ (??(??????(?????(??%?)??))?? → ?);
    520         [2: normalize % #EQ destruct]
    521         >hwreg_retrieve_hwregstore_miss in ⊢ (??(??????(?????(??%?)??))?? → ?);
    522         [2: normalize % #EQ destruct]
    523         >hwreg_retrieve_hwregstore_miss in ⊢ (??(??????(?????(??%?)??))?? → ?
    524         );
    525         [2: normalize % #EQ destruct]
    526         >hwreg_retrieve_hwregstore_hit in ⊢ (??(??????(?????(??%?)??))?? → ?);
    527         >hwreg_retrieve_hwregstore_hit in ⊢ (??(??????(?????(???%)??))?? → ?);
    528       | >hwreg_retrieve_hwregstore_hit
    529       ] 
    530       whd in match eval_seq_no_pc in ⊢ (% → ?); whd in match dph_arg_retrieve;
    531       normalize nodelta whd in ⊢ (??%?? → ?); inversion(pointer_of_address ?)
    532       [2,4,6,8: #e #_ whd in ⊢ (??%?? → ?); #EQ destruct(EQ)] #ptr
    533       [ >hwreg_retrieve_hwregstore_miss in ⊢ (% → ?); [2: normalize % #EQ destruct]
    534         >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
    535         [2: normalize % #EQ destruct]
    536         >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
    537         [2: normalize % #EQ destruct]
    538         >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
    539         >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(????%))?? → ?);
    540         [2: normalize % #EQ destruct]
    541         >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(????%))?? → ?);
    542       | >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
    543         [2: normalize % #EQ destruct]
    544         >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
    545         [2: normalize % #EQ destruct]
    546         >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
    547         [2: normalize % #EQ destruct]
    548         >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
    549         >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(????%))?? → ?);
    550         [2: normalize % #EQ destruct]
    551         >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(????%))?? → ?);
    552       | >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
    553         [2: normalize % #EQ destruct]
    554         >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
    555         [2: normalize % #EQ destruct]
    556         >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
    557         [2: normalize % #EQ destruct]
    558         >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
    559         >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(????%))?? → ?);
    560         [2: normalize % #EQ destruct]
    561         >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(????%))?? → ?);
    562       | >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
    563         [2: normalize % #EQ destruct]
    564         >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
    565         [2: normalize % #EQ destruct]
    566         >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
    567         [2: normalize % #EQ destruct]
    568         >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
    569         >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(????%))?? → ?);
    570         [2: normalize % #EQ destruct]
    571         >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(????%))?? → ?);
    572       ]
    573       #EQptr normalize nodelta whd in match acca_arg_retrieve; normalize nodelta
    574       whd in match (acca_arg_retrieve_ ?????);
    575       [1,3: >hwreg_retrieve_hwregstore_hit >m_return_bind #H @('bind_inversion H) -H
    576             #m1 #H lapply(opt_eq_from_res ???? H) -H #EQm1
    577       |*: whd in ⊢ (??%?? → ?); inversion (opt_to_res ???)
    578           [2,4: #e #_ normalize nodelta #EQ destruct] #m1 #H lapply(opt_eq_from_res ???? H)
    579           -H
    580           [ >hwreg_retrieve_hwregstore_hit in ⊢ (??(???%)? → ?);
    581           | >hwreg_retrieve_hwregstore_hit in ⊢ (??(???%)? → ?);
    582           ]
    583           >hwreg_retrieve_hwregstore_miss [2,4: assumption]
    584           >hwreg_retrieve_hwregstore_miss [2,4: % assumption]
    585           >hwreg_retrieve_hwregstore_miss [2,4: assumption]
    586           [ >hwreg_retrieve_insensitive_to_set_other ] #EQm1 normalize nodelta
    587       ]
    588       whd in match set_m; normalize nodelta
    589       [1,2: whd in ⊢ (??%% → ?); |*: whd in ⊢ (??%%% → ?);] #EQ destruct(EQ)
    590       whd in match (m_fold ??????) in ⊢ (??%?? → ?);
    591       [1,3: whd in match set_carry; normalize nodelta
    592             >other_bit_insensitive_to_reg_store >other_bit_insensitive_to_reg_store
    593             >other_bit_insensitive_to_reg_store >other_bit_insensitive_to_reg_store
    594             [ >other_bit_insensitive_to_reg_store ]
    595             whd in match hwreg_set_other; normalize nodelta
    596       ]
    597       #EQ destruct(EQ) @sym_eq >m_return_bind whd in match write_decision;
    598       normalize nodelta
    599       whd in match hw_reg_retrieve; whd in match set_regs; normalize nodelta
    600       >hwreg_retrieve_hwregstore_miss [2,4,6,8: normalize % #EQ destruct]
    601       >m_return_bind
    602       >hwreg_retrieve_hwregstore_miss [2,4,6,8: normalize % #EQ destruct]
    603       >m_return_bind
    604       >EQx1x2 >m_return_bind >EQy1y2 >m_return_bind >EQptr
    605       >m_return_bind >EQm1 >m_return_bind @eq_f whd in match set_m;
    606       normalize nodelta @eq_f3 [2,3,5,6,8,9,11,12: %]
    607       >(hwreg_store_commute RegisterDPH RegisterA) in ⊢ (???(???%));
    608       [2,4,6,8: % #EQ destruct]
    609       [1,3: >(hwreg_store_idempotent RegisterA)
    610               >(hwreg_store_commute RegisterA RegisterDPH) [2,4,6: % #EQ destruct]
    611               >(hwreg_store_commute RegisterA RegisterDPL) [2,4,6: % #EQ destruct]
    612       |*: >(hwreg_store_commute RegisterDPH RegisterA) [2,4: % #EQ destruct]
    613         [ >(hwreg_store_idempotent RegisterA) in ⊢ (???%);
    614         | >(hwreg_store_idempotent RegisterA) in ⊢ (???%);
    615         ]
    616         [2:  >(hwreg_store_commute RegisterA RegisterDPH) [2: % #EQ destruct]
    617              >(hwreg_store_commute RegisterA RegisterDPH) [2: % #EQ destruct]
    618              >(hwreg_store_commute RegisterA RegisterDPL) [2,4: % #EQ destruct]
    619              >(hwreg_store_commute RegisterDPL RegisterDPH) in ⊢ (??%?); [%| % #EQ destruct]
    620          |  >(hwreg_store_commute RegisterDPL RegisterA) [2: % #EQ destruct]
    621             >(hwreg_store_commute RegisterDPL RegisterDPH) [2: % #EQ destruct]
    622             %
    623          ]
    624       ]
    625       [ >(hwreg_store_commute RegisterDPL RegisterDPH) in ⊢ (??%?);
    626       | >(hwreg_store_commute RegisterDPL RegisterDPH) in ⊢ (??%?);
    627       ]  [2,4: % #EQ destruct]
    628       >(hwreg_store_commute RegisterA RegisterST1) [2,4: normalize % #EQ destruct]
    629       [ <(hwreg_retrieve_insensitive_to_set_other … RegisterA (carry … st)) ]
    630       >(hwreg_store_retrieve_eq RegisterA) %
    631     | #off1 #_ @eqb_elim
    632       [ #EQ destruct(EQ) normalize nodelta whd in ⊢ (??%?? → ?); #EQ destruct(EQ) % ]
    633       #_ normalize nodelta whd in match get_stack; whd in match set_stack;
    634       normalize nodelta whd in match set_dp_by_offset; whd in match set_stack_a;
    635       normalize nodelta whd in match set_stack_not_a; normalize nodelta
    636       whd in match repeat_eval_seq_no_pc; normalize nodelta
    637       whd in match preserve_carry_bit; normalize nodelta cases cl -cl
    638       normalize nodelta whd in match (m_fold ??????) in ⊢ (??%?? → ?);
    639       inversion (eval_seq_no_pc ??????) [2,4: #e #_ normalize nodelta #EQ destruct(EQ)]
    640       #st'' whd in match set_regs; whd in match eval_seq_no_pc in ⊢ (% → ?);
    641       normalize nodelta whd in match acca_arg_retrieve; normalize nodelta
    642       whd in match (acca_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_hit
    643       >m_return_bind whd in match snd_arg_retrieve; normalize nodelta
    644       whd in match (snd_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_miss
    645       [2,4: % normalize #EQ destruct] [ >hwreg_retrieve_insensitive_to_set_other]
    646       >m_return_bind #H @('bind_inversion H) -H * #x1 #x2 #EQx1x2
    647       whd in match acca_store; normalize nodelta whd in match (acca_store_ ??????);
    648       >hwreg_store_idempotent >m_return_bind whd in match set_carry;
    649       whd in match set_regs; normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
    650       whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
    651       normalize nodelta inversion (eval_seq_no_pc ??????)
    652       [2,4: #e #_ normalize nodelta #EQ destruct(EQ)] #st''
    653       >hwreg_retrieve_hwregstore_hit whd in match eval_seq_no_pc in ⊢ (% → ?);
    654       normalize nodelta whd in match acca_arg_retrieve; normalize nodelta
    655       whd in match (acca_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_hit
    656       >m_return_bind whd in match snd_arg_retrieve; normalize nodelta
    657       whd in match (snd_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_miss
    658       [2,4: normalize % #EQ destruct] >hwreg_retrieve_hwregstore_miss
    659       [2,4: normalize % #EQ destruct] >hwreg_retrieve_hwregstore_miss
    660       [2,4: normalize % #EQ destruct]  [ >hwreg_retrieve_insensitive_to_set_other]
    661       >m_return_bind #H @('bind_inversion H) -H * #y1 #y2 #EQy1y2
    662       whd in match acca_store; normalize nodelta whd in match (acca_store_ ??????);
    663       >hwreg_store_idempotent >(hwreg_store_commute RegisterDPL RegisterA)
    664       [2,4: normalize % #EQ destruct] >hwreg_store_idempotent >m_return_bind
    665       whd in match set_carry; whd in match set_regs; normalize nodelta
    666       whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
    667       normalize nodelta inversion (eval_seq_no_pc ??????)
    668       [2,4: #e #_ normalize nodelta #EQ destruct(EQ)] #st'' >hwreg_retrieve_hwregstore_hit
    669       whd in match eval_seq_no_pc in ⊢ (% → ?); normalize nodelta whd in match dph_arg_retrieve;
    670       whd in match dpl_arg_retrieve; normalize nodelta whd in ⊢ (??%?% → ?);
    671       inversion (pointer_of_address ?) [2,4: #e #_ whd in ⊢ (??%?% → ?); #EQ destruct]
    672       #ptr >hwreg_retrieve_hwregstore_miss [2,4: normalize % #EQ destruct]
    673       [ >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?); [2: normalize % #EQ destruct]
    674       | >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?); [2: normalize % #EQ destruct]
    675       ]
    676       [ >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
    677       | >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
    678       ]
    679       >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(????%))?? → ?); #EQptr normalize nodelta
    680       #H @('bind_inversion H) -H #bv #H lapply(opt_eq_from_res ???? H) -H #EQbv
    681       whd in match acca_store; normalize nodelta whd in match (acca_store_ ??????);
    682       >(hwreg_store_commute RegisterDPH RegisterA) [2,4: normalize % #EQ destruct]
    683       >hwreg_store_idempotent >m_return_bind whd in match set_regs; normalize nodelta
    684       whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
    685       normalize nodelta inversion (eval_seq_no_pc ??????)
    686       [2,4: #e #_ normalize nodelta #EQ destruct(EQ)] #st'' >hwreg_retrieve_hwregstore_hit
    687       >(hwreg_store_commute RegisterST1 RegisterA) [2,4: normalize % #EQ destruct]
    688       >hwreg_store_idempotent whd in match eval_seq_no_pc in ⊢ (% → ?);
    689       normalize nodelta whd in match acca_arg_retrieve; normalize nodelta
    690       whd in match (acca_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_hit
    691       >m_return_bind whd in match snd_arg_retrieve; normalize nodelta
    692       whd in match (snd_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_miss
    693       [2,4: normalize % #EQ destruct(EQ)] >hwreg_retrieve_hwregstore_miss
    694       [2,4: normalize % #EQ destruct(EQ)] >hwreg_retrieve_hwregstore_miss
    695       [2,4: normalize % #EQ destruct(EQ)] >hwreg_retrieve_hwregstore_miss
    696       [2,4: normalize % #EQ destruct(EQ)]  [ >hwreg_retrieve_insensitive_to_set_other]
    697       >m_return_bind #H @('bind_inversion H) -H * #z1 #z2 #EQz1z2
    698       whd in match acca_store; normalize nodelta whd in match (acca_store_ ??????);
    699       >hwreg_store_idempotent >m_return_bind whd in match set_carry; whd in match set_regs;
    700       normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
    701       whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
    702       normalize nodelta inversion (eval_seq_no_pc ??????)
    703       [2,4: #e #_ normalize nodelta #EQ destruct(EQ)] #st'' >hwreg_retrieve_hwregstore_hit
    704       >(hwreg_store_commute RegisterDPL RegisterA) [2,4: normalize % #EQ destruct]
    705       >hwreg_store_idempotent whd in match eval_seq_no_pc in ⊢ (% → ?);
    706       normalize nodelta whd in match acca_arg_retrieve; normalize nodelta
    707       whd in match (acca_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_hit
    708       >m_return_bind whd in match snd_arg_retrieve; normalize nodelta
    709       whd in match (snd_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_miss
    710       [2,4: normalize % #EQ destruct(EQ)] >hwreg_retrieve_hwregstore_miss
    711       [2,4: normalize % #EQ destruct(EQ)] >hwreg_retrieve_hwregstore_miss
    712       [2,4: normalize % #EQ destruct(EQ)] >hwreg_retrieve_hwregstore_miss
    713       [2,4: normalize % #EQ destruct(EQ)] >hwreg_retrieve_hwregstore_miss
    714       [2,4: normalize % #EQ destruct(EQ)] [ >hwreg_retrieve_insensitive_to_set_other]
    715       >m_return_bind #H @('bind_inversion H) -H * #w1 #w2 #EQw1w2 whd in match acca_store;
    716       normalize nodelta whd in match (acca_store_ ??????); >hwreg_store_idempotent
    717       >m_return_bind whd in match set_regs; whd in match set_carry; normalize nodelta
    718       whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
    719       normalize nodelta inversion (eval_seq_no_pc ??????)
    720       [2,4: #e #_ normalize nodelta #EQ destruct(EQ)] #st''
    721       [ >hwreg_retrieve_hwregstore_miss in ⊢ (??(??????(?????(??%?)??))?? → ?);
    722         [2: normalize % #EQ destruct]
    723         >hwreg_retrieve_hwregstore_miss in ⊢ (??(??????(?????(??%?)??))?? → ?);
    724         [2: normalize % #EQ destruct]
    725         >hwreg_retrieve_hwregstore_miss in ⊢ (??(??????(?????(??%?)??))?? → ?);
    726         [2: normalize % #EQ destruct]
    727          >hwreg_retrieve_hwregstore_hit in ⊢ (??(??????(?????(??%?)??))?? → ?);
    728       | >hwreg_retrieve_hwregstore_miss in ⊢ (??(??????(?????(??%?)??))?? → ?);
    729         [2: normalize % #EQ destruct]
    730         >hwreg_retrieve_hwregstore_miss in ⊢ (??(??????(?????(??%?)??))?? → ?);
    731         [2: normalize % #EQ destruct]
    732         >hwreg_retrieve_hwregstore_miss in ⊢ (??(??????(?????(??%?)??))?? → ?);
    733         [2: normalize % #EQ destruct]
    734          >hwreg_retrieve_hwregstore_hit in ⊢ (??(??????(?????(??%?)??))?? → ?);
    735       ]
    736       >hwreg_retrieve_hwregstore_hit >(hwreg_store_commute RegisterDPH RegisterA)
    737       [2,4: normalize % #EQ destruct]  >hwreg_store_idempotent
    738       whd in match eval_seq_no_pc in ⊢ (% → ?); normalize nodelta
    739       whd in match dph_arg_retrieve; whd in match dpl_arg_retrieve; normalize nodelta;
    740       whd in ⊢ (??%?% → ?); inversion (pointer_of_address ?); [2,4: #e #_ whd in ⊢ (??%?% → ?); #EQ destruct]
    741       #ptr1 >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?); [2,4: normalize % #EQ destruct]
    742       [ >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?); [2: normalize % #EQ destruct]
    743         >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
    744         >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(????%))?? → ?); [2: normalize % #EQ destruct]
    745         >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(????%))?? → ?);     
    746       | >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?); [2: normalize % #EQ destruct]
    747         >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
    748         >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(????%))?? → ?); [2: normalize % #EQ destruct]
    749         >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(????%))?? → ?);
    750       ]
    751       #EQptr1 normalize nodelta whd in match acca_arg_retrieve; normalize nodelta
    752       whd in match (acca_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_hit
    753       >m_return_bind #H @('bind_inversion H) -H #m1 #H lapply(opt_eq_from_res ???? H)
    754       -H #EQm1 whd in match set_m; normalize nodelta whd in ⊢ (??%% → ?);
    755       #EQ destruct(EQ) whd in match (m_fold ??????) in ⊢ (??%?? → ?);
    756       [ >other_bit_insensitive_to_reg_store >other_bit_insensitive_to_reg_store
    757         >other_bit_insensitive_to_reg_store >other_bit_insensitive_to_reg_store
    758         >other_bit_insensitive_to_reg_store >other_bit_insensitive_to_reg_store
    759         whd in match set_carry; normalize nodelta ]
    760       #EQ destruct(EQ) @sym_eq whd in match read_arg_decision; normalize nodelta
    761       >m_return_bind >m_return_bind >EQx1x2 >m_return_bind >EQy1y2
    762       >m_return_bind >EQptr >m_return_bind >EQbv >m_return_bind
    763       whd in match set_regs; whd in match write_decision; normalize nodelta
    764       whd in match hw_reg_retrieve; normalize nodelta
    765       >hwreg_retrieve_hwregstore_miss [2,4: normalize % #EQ destruct]
    766       [ >hwreg_retrieve_hwregstore_miss in ⊢ (??(????(????%?)?)?);
    767          [2: normalize % #EQ destruct]
    768         >hwreg_retrieve_hwregstore_miss in ⊢ (??(????(????%?)?)?);
    769         [2: normalize % #EQ destruct]
    770       | >hwreg_retrieve_hwregstore_miss in ⊢ (??(????(????%?)?)?);
    771         [2: normalize % #EQ destruct]
    772         >hwreg_retrieve_hwregstore_miss in ⊢ (??(????(????%?)?)?);
    773         [2: normalize % #EQ destruct]
    774       ]
    775       >m_return_bind >hwreg_retrieve_hwregstore_miss [2,4: normalize % #EQ destruct]
    776       >hwreg_retrieve_hwregstore_miss [2,4: normalize % #EQ destruct]
    777       >hwreg_retrieve_hwregstore_miss [2,4: normalize % #EQ destruct]
    778       >m_return_bind >EQz1z2 >m_return_bind
    779       >EQw1w2 >m_return_bind >EQptr1 >m_return_bind >EQm1 >m_return_bind
    780        whd in match set_m; whd in match set_carry; whd in match set_regs;
    781        normalize nodelta
    782        @eq_f whd in match (other_bit ?); whd in match set_carry; normalize nodelta
    783        @eq_f3 [2,3,5,6: %]
    784        [ >(hwreg_store_commute RegisterDPH RegisterDPL) in ⊢ (???%); [2: normalize % #EQ destruct]
    785          >(hwreg_store_commute RegisterA RegisterDPL) in ⊢ (???%); [2: normalize % #EQ destruct]
    786          >(hwreg_store_commute RegisterST1 RegisterDPL) in ⊢ (??%?); [2: normalize % #EQ destruct]
    787        | >(hwreg_store_commute RegisterDPH RegisterDPL) in ⊢ (???%); [2: normalize % #EQ destruct]
    788          >(hwreg_store_commute RegisterA RegisterDPL) in ⊢ (???%); [2: normalize % #EQ destruct]
    789          >(hwreg_store_commute RegisterST1 RegisterDPL) in ⊢ (??%?); [2: normalize % #EQ destruct]           
    790        ] [<hwreg_store_set_other_commut] @eq_f3 [1,2,4,5: %]
    791        [ >(hwreg_store_commute RegisterA RegisterDPH) in ⊢ (???%); [2: normalize % #EQ destruct]
    792          >(hwreg_store_commute RegisterST1 RegisterDPH) in ⊢ (??%?); [2: normalize % #EQ destruct]
    793        | >(hwreg_store_commute RegisterA RegisterDPH) in ⊢ (???%); [2: normalize % #EQ destruct]
    794          >(hwreg_store_commute RegisterST1 RegisterDPH) in ⊢ (??%?); [2: normalize % #EQ destruct]
    795        ] [<hwreg_store_set_other_commut] @eq_f3 [1,2,4,5: %]
    796        [ <hwreg_store_set_other_commut <hwreg_store_set_other_commut
    797          <hwreg_store_set_other_commut ]
    798          >(hwreg_store_commute RegisterA RegisterST1) in ⊢ (???%); [2,4: normalize % #EQ destruct]         
    799           @eq_f3 [1,2,4,5: %] @eq_f3 [1,2,4,5: %]
    800          [<hwreg_store_set_other_commut ]
    801          >(hwreg_store_commute RegisterDPL RegisterDPH) in ⊢ (??%?);
    802          [2,4: normalize % #EQ destruct] %
    803     | #by #_ whd in match preserve_carry_bit; whd in match set_stack_int; normalize nodelta
    804       cases cl -cl normalize nodelta whd in match repeat_eval_seq_no_pc; normalize nodelta     
    805       whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
    806       normalize nodelta inversion (eval_seq_no_pc ??????)
    807       [2,4: #e #_ normalize nodelta #EQ destruct(EQ)] #st'' whd in match eval_seq_no_pc in ⊢ (% → ?);
    808       normalize nodelta whd in match acca_arg_retrieve; normalize nodelta
    809       whd in match (acca_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_hit
    810       >m_return_bind whd in match snd_arg_retrieve; normalize nodelta
    811       whd in match (snd_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_miss
    812       [2,4: normalize % #EQ destruct] [ >hwreg_retrieve_insensitive_to_set_other]
    813       >m_return_bind #H @('bind_inversion H) -H * #x1 #x2 #EQx1x2
    814       whd in match acca_store; normalize nodelta whd in match (acca_store_ ??????);
    815       >hwreg_store_idempotent >m_return_bind whd in match set_carry; whd in match set_regs;
    816       normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
    817       whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
    818       normalize nodelta inversion (eval_seq_no_pc ??????)
    819       [2,4: #e #_ normalize nodelta #EQ destruct(EQ)] #st'' >hwreg_retrieve_hwregstore_hit
    820       >(hwreg_store_commute RegisterDPL RegisterA) [2,4: normalize % #EQ destruct]
    821       >hwreg_store_idempotent whd in match eval_seq_no_pc in ⊢ (% → ?);
    822       normalize nodelta whd in match acca_arg_retrieve; normalize nodelta
    823       whd in match (acca_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_hit
    824       >m_return_bind whd in match snd_arg_retrieve; normalize nodelta
    825       whd in match (snd_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_miss
    826       [2,4: normalize % #EQ destruct] >hwreg_retrieve_hwregstore_miss
    827       [2,4: normalize % #EQ destruct]  [ >hwreg_retrieve_insensitive_to_set_other]
    828       >m_return_bind #H @('bind_inversion H) -H * #y1 #y2 #EQy1y2
    829       whd in match acca_store; normalize nodelta whd in match (acca_store_ ??????);
    830       >hwreg_store_idempotent >m_return_bind whd in match set_regs; whd in match set_carry;
    831       normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
    832       whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
    833       normalize nodelta inversion (eval_seq_no_pc ??????)
    834       [2,4: #e #_ normalize nodelta #EQ destruct(EQ)] #st'' >hwreg_retrieve_hwregstore_hit
    835       >(hwreg_store_commute RegisterDPH RegisterA) [2,4: normalize % #EQ destruct]
    836       >hwreg_store_idempotent whd in match eval_seq_no_pc in ⊢ (% → ?);
    837       normalize nodelta whd in match dph_arg_retrieve; normalize nodelta
    838       whd in ⊢ (??%?% → ?); inversion (pointer_of_address ?) [2,4: #e #_ whd in ⊢ (??%?% → ?); #EQ destruct]
    839       #ptr >hwreg_retrieve_hwregstore_miss [2,4: normalize % #EQ destruct]
    840       [ >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?); [2: normalize % #EQ destruct]
    841         >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
    842         >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(????%))?? → ?); [2: normalize % #EQ destruct]
    843         >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(????%))?? → ?);
    844       | >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?); [2: normalize % #EQ destruct]
    845         >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
    846         >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(????%))?? → ?); [2: normalize % #EQ destruct]
    847         >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(????%))?? → ?);
    848       ]
    849       #EQptr normalize nodelta whd in match acca_arg_retrieve; normalize nodelta
    850       whd in match (acca_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_hit
    851       >m_return_bind #H @('bind_inversion H) -H #m #H lapply(opt_eq_from_res ???? H) -H
    852       #EQm whd in match set_m; normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
    853       whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
    854       normalize nodelta whd in match set_carry; normalize nodelta
    855       [ >other_bit_insensitive_to_reg_store >other_bit_insensitive_to_reg_store
    856         >other_bit_insensitive_to_reg_store whd in match hwreg_set_other; normalize nodelta ]
    857       #EQ destruct(EQ) @sym_eq whd in match read_arg_decision; normalize nodelta
    858       >m_return_bind whd in match write_decision; normalize nodelta whd in match set_regs;
    859       whd in match hw_reg_retrieve; normalize nodelta >hwreg_retrieve_hwregstore_miss
    860       [2,4: % normalize #EQ destruct] >m_return_bind  >hwreg_retrieve_hwregstore_miss
    861       [2,4: % normalize #EQ destruct] >m_return_bind >EQx1x2 >m_return_bind >EQy1y2
    862       >m_return_bind >EQptr >m_return_bind >EQm >m_return_bind whd in match set_m;
    863       whd in match set_regs; normalize nodelta @eq_f whd in match set_carry;
    864       normalize nodelta @eq_f3 [2,3,5,6: %]
    865       [ >(hwreg_store_commute RegisterDPH RegisterA) in ⊢ (??%?); [2: % normalize #EQ destruct]
    866         >(hwreg_store_commute RegisterDPL RegisterA) in ⊢ (??%?); [2: % normalize #EQ destruct]
    867       | >(hwreg_store_commute RegisterDPH RegisterA) in ⊢ (??%?); [2: % normalize #EQ destruct]
    868         >(hwreg_store_commute RegisterDPL RegisterA) in ⊢ (??%?); [2: % normalize #EQ destruct]
    869       ]
    870       [2: @eq_f3 [1,2: %] >(hwreg_store_commute RegisterDPL RegisterDPH) in ⊢ (??%?);
    871          [2: % normalize #EQ destruct]
    872       |  >(hwreg_store_commute RegisterDPL RegisterDPH) in ⊢ (??%?); [2: % normalize #EQ destruct]
    873       ]
    874       %   
    875     ] 
    876   | #r cases src -src
    877     [ #r1 * #H1 #H2 normalize nodelta @eq_Register_elim
    878       [ #EQ destruct(EQ) normalize nodelta whd in ⊢ (??%?% → ?); #EQ destruct(EQ) % ]
    879       #H3 normalize nodelta @eq_Register_elim normalize nodelta
    880       [ #EQ destruct(EQ) whd in match repeat_eval_seq_no_pc; normalize nodelta
    881         whd in match (m_fold ??????) in ⊢ (??%?? → ?); #EQ destruct(EQ)
    882         @sym_eq whd in match read_arg_decision; normalize nodelta >m_return_bind
    883         whd in match write_decision; normalize nodelta >m_return_bind
    884         whd in match set_regs; normalize nodelta @eq_f % ]
    885       #H4 normalize nodelta @eq_Register_elim
    886       [ #EQ destruct(EQ) | #H5] normalize nodelta whd in ⊢ (??%?% → ?);
    887       whd in match set_regs; normalize nodelta [2: >hwreg_retrieve_hwregstore_hit ]
    888       #EQ destruct(EQ) @sym_eq whd in match read_arg_decision; normalize nodelta
    889       >m_return_bind whd in match write_decision; normalize nodelta >m_return_bind
    890       @eq_f whd in match set_regs; normalize nodelta cases cl normalize nodelta
    891       @eq_f3 try % @eq_f3 [1,2,4,5: %] >hwreg_store_retrieve_eq %
    892     | #n #_ normalize nodelta whd in match preserve_carry_bit; whd in match get_stack;
    893       normalize nodelta whd in match set_dp_by_offset; normalize nodelta
    894       cases cl -cl [ letin CL_TRUE ≝ it | letin CL_FALSE ≝ it ]
    895       normalize nodelta whd in match repeat_eval_seq_no_pc;
    896       normalize nodelta  whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
    897       normalize nodelta inversion (eval_seq_no_pc ??????)
    898       [2,4: #e #_ normalize nodelta #EQ destruct(EQ)] #st''
    899       whd in match eval_seq_no_pc in ⊢ (% → ?); normalize nodelta
    900       whd in match acca_arg_retrieve; normalize nodelta
    901       whd in match (acca_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_hit
    902       >m_return_bind whd in match snd_arg_retrieve; normalize nodelta
    903       whd in match (snd_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_miss
    904       [2,4: normalize % #EQ destruct(EQ)] [ >hwreg_retrieve_insensitive_to_set_other]
    905       >m_return_bind #H @('bind_inversion H) -H * #x1 #x2 #EQx1x2
    906       whd in match acca_store; normalize nodelta whd in match (acca_store_ ??????);
    907       >hwreg_store_idempotent >m_return_bind whd in match set_regs;     
    908       whd in match set_carry; normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
    909       whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
    910       normalize nodelta inversion (eval_seq_no_pc ??????)
    911       [2,4: #e #_ normalize nodelta #EQ destruct(EQ)] #st'' >hwreg_retrieve_hwregstore_hit
    912       whd in match eval_seq_no_pc in ⊢ (% → ?); normalize nodelta
    913       whd in match acca_arg_retrieve; normalize nodelta
    914       whd in match (acca_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_hit
    915       >m_return_bind whd in match snd_arg_retrieve; normalize nodelta
    916       whd in match (snd_arg_retrieve_ ?????); >hwreg_retrieve_hwregstore_miss
    917       [2,4: normalize % #EQ destruct(EQ)] >hwreg_retrieve_hwregstore_miss
    918       [2,4: normalize % #EQ destruct(EQ)] >hwreg_retrieve_hwregstore_miss
    919       [2,4: normalize % #EQ destruct(EQ)] [ >hwreg_retrieve_insensitive_to_set_other]
    920       >m_return_bind #H @('bind_inversion H) -H * #y1 #y2 #EQy1y2
    921       whd in match acca_store; normalize nodelta whd in match (acca_store_ ??????);
    922       >hwreg_store_idempotent >(hwreg_store_commute RegisterDPL RegisterA)
    923       [2,4: normalize % #EQ destruct(EQ)] >hwreg_store_idempotent
    924       >m_return_bind whd in match set_carry; whd in match set_regs; normalize nodelta
    925       whd in ⊢ (??%% → ?); #EQ destruct(EQ)
    926       whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
    927       normalize nodelta inversion (eval_seq_no_pc ??????)
    928       [2,4: #e #_ normalize nodelta #EQ destruct(EQ)] #st'' >hwreg_retrieve_hwregstore_hit
    929       whd in match eval_seq_no_pc in ⊢ (% → ?); normalize nodelta
    930       whd in ⊢ (??%?? → ?); inversion (pointer_of_address ?)
    931       [2,4: #e #_ whd in ⊢ (??%?% → ?); #EQ destruct(EQ)] #ptr >hwreg_retrieve_hwregstore_miss
    932       [2,4: normalize % #EQ destruct(EQ)]
    933       [ >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
    934         [2,4: normalize % #EQ destruct(EQ)]
    935         >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
    936         >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(????%))?? → ?);
    937       | >hwreg_retrieve_hwregstore_miss in ⊢ (??(?(???%?))?? → ?);
    938         [2,4: normalize % #EQ destruct(EQ)]
    939         >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(???%?))?? → ?);
    940         >hwreg_retrieve_hwregstore_hit in ⊢ (??(?(????%))?? → ?);
    941       ]
    942       #EQptr normalize nodelta #H @('bind_inversion H) -H #bv #H
    943       lapply(opt_eq_from_res ???? H) -H #EQbv whd in match acca_store;
    944       normalize nodelta whd in match (acca_store_ ??????);
    945       >(hwreg_store_commute RegisterDPH RegisterA)
    946       [2,4: normalize % #EQ destruct(EQ)] >hwreg_store_idempotent
    947       >m_return_bind whd in match set_regs; normalize nodelta whd in ⊢ (??%% → ?);
    948       #EQ destruct(EQ) @eq_Register_elim [1,3: #EQ destruct(EQ) |*: #H1 ]
    949       normalize nodelta whd in match (m_fold ??????) in ⊢ (??%?? → ?); whd in match set_regs;
    950       normalize nodelta whd in match set_carry; whd in match set_regs;
    951       normalize nodelta
    952       [1,3: >other_bit_insensitive_to_reg_store >other_bit_insensitive_to_reg_store
    953             >other_bit_insensitive_to_reg_store
    954             [2: >other_bit_insensitive_to_reg_store ] ]
    955       [1,4: >hwreg_retrieve_hwregstore_hit ] #EQ destruct(EQ) @sym_eq
    956       whd in match read_arg_decision; normalize nodelta >m_return_bind
    957       >m_return_bind >EQx1x2 >m_return_bind >EQy1y2 >m_return_bind
    958       >EQptr >m_return_bind >EQbv >m_return_bind whd in match write_decision;
    959       normalize nodelta whd in match set_regs; normalize nodelta
    960       whd in match hw_reg_store; normalize nodelta >m_return_bind
    961       @eq_f whd in match set_carry; whd in match (other_bit ?); normalize nodelta @eq_f3 [2,3,5,6,8,9,11,12: %]
    962       [1,3: <hwreg_store_set_other_commut <hwreg_store_set_other_commut
    963             <hwreg_store_set_other_commut [ <hwreg_store_set_other_commut]]
    964       @eq_f3 [1,2,4,5,7,8,10,11: %]
    965       >(hwreg_store_commute RegisterDPL RegisterDPH) in ⊢ (??%?);
    966       [2,4,6,8: % normalize #EQ destruct] %
    967     | #by #_ normalize nodelta @eq_Register_elim [#EQ destruct(EQ) | #H1 ]
    968       whd in ⊢ (??%?? → ?); whd in match set_regs; normalize nodelta #EQ destruct(EQ)
    969       @sym_eq whd in match read_arg_decision; normalize nodelta >m_return_bind
    970       whd in match write_decision; normalize nodelta >m_return_bind
    971       @eq_f whd in match set_regs; normalize nodelta [%] @eq_f3 [2,3: %]
    972       >hwreg_retrieve_hwregstore_hit %
    973     ]
    974   ] 
    975 | cases daemon (*TODO*)
    976 ] *)
    977 cases daemon qed.
    978248
    979249definition sigma_beval : fixpoint_computer → coloured_graph_computer → 
Note: See TracChangeset for help on using the changeset viewer.