Ignore:
Timestamp:
May 15, 2012, 12:01:30 AM (8 years ago)
Author:
sacerdot
Message:

\snd half_add => add everywhere

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r1945 r1946  
    12511251qed.
    12521252
    1253 (* XXX: this looks almost certainly wrong *)
    1254 example half_add_SO:
    1255  ∀pc.
    1256  \snd (half_add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1)) = bitvector_of_nat … (S pc).
    1257  cases daemon.
    1258 qed.
    1259 
    12601253(*
    12611254axiom not_eqvb_S:
     
    13181311  |2:
    13191312    #hd #tl #IH #pc #l2 * #H1 #H2
    1320 (*    >half_add_SO in H2; #H2 *)
     1313(*    >add_SO in H2; #H2 *)
    13211314    cases (IH … H2) #E1 #E2 %
    13221315    [1:
     
    16141607   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
    16151608   let pbl ≝ lookup ? 7 addr (low_internal_ram … s) (zero 8) in
    1616    let pbu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) (low_internal_ram … s) (zero 8) in
     1609   let pbu ≝ lookup ? 7 (add ? addr (bitvector_of_nat 7 1)) (low_internal_ram … s) (zero 8) in
    16171610   let bl ≝ lookup ? 7 addr ram (zero 8) in
    1618    let bu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) ram (zero 8) in
     1611   let bu ≝ lookup ? 7 (add ? addr (bitvector_of_nat 7 1)) ram (zero 8) in
    16191612    bu@@bl = \fst (sigma (pbu@@pbl)).
    16201613
     
    16721665    | Jmp _ ⇒ Some … M
    16731666    | Call _ ⇒
    1674        Some … (\snd (half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1))::M)
     1667       Some … (add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1)::M)
    16751668    | Mov _ _ ⇒ Some … M
    16761669    | Instruction instr ⇒
     
    21142107  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
    21152108  low_internal_ram ? cm2 s2 = low_internal_ram T2 cm3 s3 →
    2116   sp1 = \snd (half_add ? (get_8051_sfr … cm1 s1 SFR_SP) (bitvector_of_nat 8 1)) →
    2117   sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) →
     2109  sp1 = add ? (get_8051_sfr … cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
     2110  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
    21182111  bu@@bl = \fst (sigma (pbu@@pbl)) →
    21192112   low_internal_ram T1 cm1
     
    21402133  get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →
    21412134  high_internal_ram ?? s2 = high_internal_ram T2 cm3 s3 →
    2142   sp1 = \snd (half_add ? (get_8051_sfr ? cm1 s1 SFR_SP) (bitvector_of_nat 8 1)) →
    2143   sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) →
     2135  sp1 = add ? (get_8051_sfr ? cm1 s1 SFR_SP) (bitvector_of_nat 8 1) →
     2136  sp2 = add ? sp1 (bitvector_of_nat 8 1) →
    21442137  bu@@bl = \fst (sigma (pbu@@pbl)) →
    21452138   high_internal_ram T1 cm1
Note: See TracChangeset for help on using the changeset viewer.