Ignore:
Timestamp:
Jun 13, 2011, 1:14:38 AM (9 years ago)
Author:
sacerdot
Message:

New invariant for the main theorem.
The new invariant is much more complex since it needs to take care of
memory locations that hold pseudo addresses.

ATM, only the Comment and Cost cases are accepted, but the proof for
ADD/ADDC/SUBB is almost there and the one for Jump should pass almost untouched.
The Call proof should pass for the first time. All the others are still to
be done.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r941 r942  
    14811481*)
    14821482
    1483 definition status_of_pseudo_status: PseudoStatus → option Status ≝
    1484  λps.
     1483definition internal_pseudo_address_map ≝ list (BitVector 8).
     1484
     1485axiom low_internal_ram_of_pseudo_low_internal_ram:
     1486 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
     1487
     1488axiom high_internal_ram_of_pseudo_high_internal_ram:
     1489 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
     1490
     1491axiom low_internal_ram_of_pseudo_internal_ram_hit:
     1492 ∀M:internal_pseudo_address_map.∀s:PseudoStatus.∀addr:BitVector 7.
     1493  member ? (eq_bv 8) (false:::addr) M = true →
     1494   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
     1495   let pbl ≝ lookup ? 7 addr (low_internal_ram ? s) (zero 8) in
     1496   let pbu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) (low_internal_ram ? s) (zero 8) in
     1497   let bl ≝ lookup ? 7 addr ram (zero 8) in
     1498   let bu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) ram (zero 8) in
     1499    bu@@bl = sigma (code_memory … s) (pbu@@pbl).
     1500
     1501axiom low_internal_ram_of_pseudo_internal_ram_miss:
     1502 ∀M:internal_pseudo_address_map.∀s:PseudoStatus.∀addr:BitVector 7.
     1503  let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
     1504  let 〈carr,Saddr〉 ≝ half_add ? addr (bitvector_of_nat 7 1) in
     1505  carr = false →
     1506  member ? (eq_bv 8) (false:::addr) M = false →
     1507   member ? (eq_bv 8) (false:::Saddr) M = false →
     1508    lookup ? 7 Saddr ram = lookup ? 7 Saddr (low_internal_ram … s).
     1509
     1510definition addressing_mode_ok ≝
     1511 λM:internal_pseudo_address_map.λs:PseudoStatus.
     1512  λaddr:addressing_mode.
     1513   match addr with
     1514    [ DIRECT d ⇒
     1515       ¬(member ? (eq_bv 8) d M) ∧
     1516       ¬(member ? (eq_bv 8) (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) M)
     1517    | INDIRECT i ⇒
     1518       let d ≝ get_register ? s [[false;false;i]] in
     1519       ¬(member ? (eq_bv 8) d M) ∧
     1520       ¬(member ? (eq_bv 8) (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) M)
     1521    | EXT_INDIRECT _ ⇒ true
     1522    | REGISTER _ ⇒ true
     1523    | ACC_A ⇒ true
     1524    | ACC_B ⇒ true
     1525    | DPTR ⇒ true
     1526    | DATA _ ⇒ true
     1527    | DATA16 _ ⇒ true
     1528    | ACC_DPTR ⇒ true
     1529    | ACC_PC ⇒ true
     1530    | EXT_INDIRECT_DPTR ⇒ true
     1531    | INDIRECT_DPTR ⇒ true
     1532    | CARRY ⇒ true
     1533    | BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
     1534    | N_BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *)
     1535    | RELATIVE _ ⇒ true
     1536    | ADDR11 _ ⇒ true
     1537    | ADDR16 _ ⇒ true ].
     1538
     1539definition next_internal_pseudo_address_map ≝
     1540 λM:internal_pseudo_address_map.
     1541  λs:PseudoStatus.
     1542   match \fst (fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s)) with
     1543    [ Comment _ ⇒ Some ? M
     1544    | Cost _ ⇒ Some … M
     1545    | Jmp _ ⇒ Some … M
     1546    | Call _ ⇒
     1547       Some … (\snd (half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1))::M)
     1548    | Mov _ _ ⇒ Some … M
     1549    | Instruction instr ⇒
     1550       match instr with
     1551        [ ADD addr1 addr2 ⇒
     1552           if addressing_mode_ok M s addr1 ∧ addressing_mode_ok M s addr2 then
     1553            Some ? M
     1554           else
     1555            None ?
     1556        | ADDC addr1 addr2 ⇒
     1557           if addressing_mode_ok M s addr1 ∧ addressing_mode_ok M s addr2 then
     1558            Some ? M
     1559           else
     1560            None ?
     1561        | SUBB addr1 addr2 ⇒
     1562           if addressing_mode_ok M s addr1 ∧ addressing_mode_ok M s addr2 then
     1563            Some ? M
     1564           else
     1565            None ?       
     1566        | _ ⇒ (* TO BE COMPLETED *) Some ? M ]].
     1567   
     1568definition status_of_pseudo_status:
     1569 internal_pseudo_address_map → PseudoStatus → option Status ≝
     1570 λM,ps.
    14851571  let pap ≝ code_memory … ps in
    14861572   match assembly pap with
     
    14891575       let cm ≝ load_code_memory (\fst p) in
    14901576       let pc ≝ sigma pap (program_counter ? ps) in
     1577       let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in
     1578       let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (low_internal_ram … ps) in
    14911579        Some …
    14921580         (mk_PreStatus (BitVectorTrie Byte 16)
    14931581           cm
    1494            (low_internal_ram … ps)
    1495            (high_internal_ram … ps)
     1582           lir
     1583           hir
    14961584           (external_ram … ps)
    14971585           pc
     
    16001688
    16011689lemma status_of_pseudo_status_failure_depends_only_on_code_memory:
     1690 ∀M:internal_pseudo_address_map.
    16021691 ∀ps,ps': PseudoStatus.
    16031692  code_memory … ps = code_memory … ps' →
    1604    match status_of_pseudo_status ps with
    1605     [ None ⇒ status_of_pseudo_status ps' = None …
    1606     | Some _ ⇒ ∃w. status_of_pseudo_status ps' = Some … w
     1693   match status_of_pseudo_status M ps with
     1694    [ None ⇒ status_of_pseudo_status M ps' = None …
     1695    | Some _ ⇒ ∃w. status_of_pseudo_status M ps' = Some … w
    16071696    ].
    1608  #ps #ps' #H whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
     1697 #M #ps #ps' #H whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
    16091698 generalize in match (refl … (assembly (code_memory … ps)))
    16101699 cases (assembly ?) in ⊢ (???% → %)
     
    19732062
    19742063lemma main_thm:
    1975  ∀ps,s,s''.
    1976   status_of_pseudo_status ps = Some … s →
    1977   status_of_pseudo_status (execute_1_pseudo_instruction (ticks_of (code_memory … ps)) ps) = Some … s'' →
     2064 ∀M,M',ps,s,s''.
     2065  next_internal_pseudo_address_map M ps = Some … M' →
     2066  status_of_pseudo_status M ps = Some … s →
     2067  status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory … ps)) ps) = Some … s'' →
    19782068   ∃n. execute n s = s''.
    1979  #ps #s #s''
     2069 #M #M' #ps #s #s''
    19802070 generalize in match (fetch_assembly_pseudo2 (code_memory … ps))
    1981  whd in ⊢ (? → ??%? → ??%? → ?)
     2071 whd in ⊢ (? → ? → ??%? → ??%? → ?)
    19822072 >execute_1_pseudo_instruction_preserves_code_memory
    19832073 generalize in match (refl … (assembly (code_memory … ps)))
    19842074 generalize in match (assembly (code_memory … ps)) in ⊢ (??%? → %) #ASS whd in ⊢ (???% → ?)
    19852075 cases (build_maps (code_memory … ps))
    1986   [ cases (code_memory … ps) #preamble #instr_list whd in ⊢ (???% → ?) #EQ >EQ #H
     2076  [ cases (code_memory … ps) #preamble #instr_list whd in ⊢ (???% → ?) #EQ >EQ #H #MAP
    19872077    #abs @⊥ normalize in abs; destruct (abs) ]
    1988  * #labels #costs generalize in match (refl … (code_memory … ps))
     2078 * #labels #costs whd in ⊢ (? → ? → ??%? → ?) generalize in match (refl … (code_memory … ps))
    19892079 cases (code_memory … ps) in ⊢ (???% → %) #preamble #instr_list #EQ0 normalize nodelta;
    19902080 generalize in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?]) → ?) *; normalize nodelta;
    1991   [ #EQ >EQ #_ #abs @⊥ normalize in abs; destruct (abs) ]
     2081  [ #EQ >EQ #_ #_ #abs @⊥ normalize in abs; destruct (abs) ]
    19922082 * #final_ppc * #final_pc #assembled #EQ >EQ -EQ ASS; normalize nodelta;
    19932083 #H generalize in match (H ??? (refl …) (refl …)) -H; #H;
     2084 #MAP
    19942085 #H1 generalize in match (option_destruct_Some ??? H1) -H1; #H1 <H1 -H1;
    19952086 #H2 generalize in match (option_destruct_Some ??? H2) -H2; #H2 <H2 -H2;
    19962087 change with
    19972088  (∃n.
    1998     execute n (set_program_counter ? (set_code_memory ?? ps (load_code_memory assembled)) ?)
    1999    = set_program_counter ? (set_code_memory ?? (execute_1_pseudo_instruction ? ps) (load_code_memory assembled)) ?)
     2089    execute n
     2090     (set_low_internal_ram ?
     2091       (set_high_internal_ram ?
     2092         (set_program_counter ?
     2093           (set_code_memory ?? ps (load_code_memory assembled))
     2094          (sigma 〈preamble,instr_list〉 (program_counter ? ps)))
     2095        (high_internal_ram_of_pseudo_high_internal_ram M ?))
     2096      (low_internal_ram_of_pseudo_low_internal_ram M ?))
     2097   = set_low_internal_ram ?
     2098      (set_high_internal_ram ?
     2099        (set_program_counter ?
     2100          (set_code_memory ?? (execute_1_pseudo_instruction ? ps) (load_code_memory assembled))
     2101         (sigma ??))
     2102       ?)
     2103     ?)
    20002104 whd in match (\snd 〈preamble,instr_list〉) in H;
    20012105 whd in match (\fst 〈preamble,instr_list〉) in H;
    20022106 whd in match (\snd 〈final_pc,assembled〉) in H;
     2107 whd in match (\snd 〈preamble,instr_list〉) in MAP;
    20032108 -s s'' labels costs final_ppc final_pc;
    20042109 letin ps' ≝ (execute_1_pseudo_instruction (ticks_of 〈preamble,instr_list〉) ps)
     
    20092114 whd in ⊢ (???(?%?) → ?)
    20102115 whd in ⊢ (???% → ?) generalize in match (H (program_counter … ps)) -H; >EQ0 normalize nodelta;
    2011  cases (fetch_pseudo_instruction instr_list (program_counter … ps))
    2012  #pi #newppc normalize nodelta; * #instructions *;
    2013  cases pi normalize nodelta;
    2014   [2,3: (* Comment, Cost *) #ARG #H1 #H2 #EQ %[1,3:@0]
     2116 cases (fetch_pseudo_instruction instr_list (program_counter … ps)) in MAP ⊢ %
     2117 #pi #newppc normalize nodelta; #MAP * #instructions *;
     2118 cases pi in MAP; normalize nodelta;
     2119  [2,3: (* Comment, Cost *) #ARG #MAP #H1 #H2 #EQ %[1,3:@0]
     2120    generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP M';
    20152121    normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
    20162122    #H2 >(eq_bv_to_eq … H2) >EQ %
    2017   |4: (* Jmp *) #label
     2123(*  |6: (* Mov *) #arg1 #arg2
     2124       #H1 #H2 #EQ %[@1]
     2125       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
     2126       change in ⊢ (? → ??%?) with (execute_1_0 ??)
     2127       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
     2128       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
     2129       >H2b >(eq_instruction_to_eq … H2a)
     2130       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
     2131       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; whd in ⊢ (???% → ??%?)
     2132       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
     2133       normalize nodelta;
     2134       [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
     2135       #result #flags
     2136       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c) % *)
     2137(*  |4,5: (* Jmp, Call *) #label
    20182138      whd in ⊢ (???% → ?) cases (jump_expansion ??) normalize nodelta;
    2019        [3: (* long *) #H1 #H2 #EQ %[@1]
     2139       [3,6: (* long *) #H1 #H2 #EQ %[1,3:@1]
    20202140           (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
    20212141           change in ⊢ (? → ??%?) with (execute_1_0 ??)
     
    20242144           >H2b >(eq_instruction_to_eq … H2a)
    20252145           generalize in match EQ; -EQ;
    2026            (*whd in ⊢ (???% → ??%?);*)
     2146           [2: whd in ⊢ (???% → ??%?);
     2147               cases (half_add ???) #carry #new_sp normalize nodelta;
     2148               >(eq_bv_to_eq … H2c)
     2149               change with
     2150                ((?=let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 newppc in ?) →
     2151                    (let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
     2152               (* MISMATCH ON WHAT IS ON THE STACK!!!! *)
     2153               (* HOW TO PROVE THIS?? *)
     2154           ]
    20272155           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2c)
    2028            cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
    2029        | (* short *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
     2156           cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX
     2157            [2: % | ]
     2158       |4: (* short Call *) #abs @⊥ destruct (abs)
     2159       |1: (* short Jmp *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
    20302160           generalize in match
    20312161            (refl ?
     
    20882218            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
    20892219              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]]
    2090   |5: (* Call *)
    2091   |6: (* Mov *)
    2092   | (* Instruction *) -pi; *
    2093     [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #H1 #H2 #EQ %[1,3,5:@1]
     2220  (*|5: (* Call *)*) *)
     2221  | (* Instruction *) -pi; *; normalize nodelta;
     2222    [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #MAP #H1 #H2 #EQ %[1,3,5:@1]
    20942223       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
    20952224       change in ⊢ (? → ??%?) with (execute_1_0 ??)
     
    20972226       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
    20982227       >H2b >(eq_instruction_to_eq … H2a)
    2099        generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
     2228       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?); generalize in match MAP; -MAP;
    21002229       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1;
    21012230       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
    2102        normalize nodelta;
     2231       normalize nodelta; #MAP;(* [1,2:whd in MAP:(??(match % with [ _ ⇒ ?])?)]*)
    21032232       [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
    21042233       #result #flags
Note: See TracChangeset for help on using the changeset viewer.