Ignore:
Timestamp:
Jul 27, 2012, 5:53:25 PM (8 years ago)
Author:
mulligan
Message:

Changed proof strategy for main lemma after noticed that the current approach would not work with POP, RET, etc. Ported throughout the assembly proof and all the way up to Test.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/AssemblyProof.ma

    r2256 r2272  
    335335qed.
    336336
    337 inductive accumulator_address_map_entry: Type[0] ≝
    338   | data: accumulator_address_map_entry
    339   | address: upper_lower → Word → accumulator_address_map_entry.
     337(* XXX: if upper then the byte in the entry is the least significant byte of the address and
     338        the byte in the status is the most significant, otherwise if lower then the
     339        other way around
     340*)
     341definition address_entry ≝ upper_lower × Byte.
    340342
    341343definition eq_accumulator_address_map_entry:
    342     accumulator_address_map_entry → accumulator_address_map_entry → bool ≝
    343   λleft: accumulator_address_map_entry.
    344   λright: accumulator_address_map_entry.
     344    option address_entry → option address_entry → bool ≝
     345  λleft.
     346  λright.
    345347    match left with
    346     [ data                     ⇒
     348    [ None                   ⇒
    347349      match right with
    348       [ data ⇒ true
     350      [ None ⇒ true
    349351      | _    ⇒ false
    350352      ]
    351     | address upper_lower word ⇒
     353    | Some upper_lower_addr ⇒
     354      let 〈upper_lower, addr〉 ≝ upper_lower_addr in
    352355      match right with
    353       [ address upper_lower' word' ⇒
    354           eq_upper_lower upper_lower upper_lower' ∧ eq_bv … word word'
     356      [ Some upper_lower_addr' ⇒
     357        let 〈upper_lower', addr'〉 ≝ upper_lower_addr' in
     358          eq_upper_lower upper_lower upper_lower' ∧ eq_bv … addr addr'
    355359      | _                          ⇒ false
    356360      ]
    … …  
    358362
    359363lemma eq_accumulator_address_map_entry_true_to_eq:
    360   ∀left: accumulator_address_map_entry.
    361   ∀right: accumulator_address_map_entry.
     364  ∀left: option address_entry.
     365  ∀right: option address_entry.
    362366    eq_accumulator_address_map_entry left right = true → left = right.
    363367  #left #right cases left cases right
    … …  
    365369    #_ %
    366370  |2,3:
    367     #upper_lower #word normalize #absurd destruct(absurd)
     371    * * #word normalize #absurd destruct(absurd)
    368372  |4:
    369     #upper_lower #word #upper_lower' #word' normalize
    370     cases upper_lower' normalize nodelta
    371     cases upper_lower normalize
     373    * * #word * * #word'
    372374    [2,3:
    373       #absurd destruct(absurd)
     375      #absurd normalize in absurd; destruct(absurd)
    374376    ]
    375     change with (eq_bv 16 ?? = true → ?)
    376     #relevant lapply (eq_bv_eq … relevant)
    377     #word_refl >word_refl %
     377    normalize change with (eq_bv 8 ?? = true → ?)
     378    #relevant >(eq_bv_eq … relevant) %
    378379  ]
    379380qed.
    … …  
    403404   
    404405lemma eq_accumulator_address_map_entry_false_to_neq:
    405   ∀left: accumulator_address_map_entry.
    406   ∀right: accumulator_address_map_entry.
     406  ∀left: option address_entry.
     407  ∀right: option address_entry.
    407408    eq_accumulator_address_map_entry left right = false → left ≠ right.
    408409  #left #right cases left cases right
    … …  
    410411    normalize #absurd destruct(absurd)
    411412  |2,3:
    412     #upper_lower #word normalize #_
    413     @nmk #absurd destruct(absurd)
     413    * * #word normalize #_ % #absurd destruct(absurd)
    414414  |4:
    415     #upper_lower #word #upper_lower' #word' normalize
    416     cases upper_lower' normalize nodelta
    417     cases upper_lower normalize nodelta
     415    * * #word * * #word' normalize
    418416    [2,3:
    419       #_ @nmk #absurd destruct(absurd)
     417      #_ % #absurd destruct(absurd)
    420418    ]
    421419    change with (eq_bv ??? = false → ?)
    422     #eq_bv_false_assm lapply(eq_bv_false_to_neq … eq_bv_false_assm)
    423     #word_neq_assm @nmk #address_eq_assm cases word_neq_assm
     420    #eq_bv_false_assm lapply (eq_bv_false_to_neq … eq_bv_false_assm)
     421    #word_neq_assm % @Some_Some_elim #address_eq_assm cases word_neq_assm
    424422    #word_eq_assm @word_eq_assm destruct(address_eq_assm) %
    425423  ]
    426 qed. 
     424qed.
    427425
    428426(* XXX: changed this type.  Bool specifies whether byte is first or second
    … …  
    431429        A.
    432430*)
    433 definition internal_pseudo_address_map ≝ list (Byte × (upper_lower × Word)) × accumulator_address_map_entry.
     431definition internal_pseudo_address_map ≝
     432  (* low, high, acc *)
     433  (BitVectorTrie address_entry 7) × (BitVectorTrie address_entry 7) × (option address_entry).
    434434
    435435include alias "ASM/BitVectorTrie.ma".
    … …  
    437437include "common/AssocList.ma".
    438438
    439 axiom low_internal_ram_of_pseudo_low_internal_ram:
    440  ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
    441 
    442 axiom high_internal_ram_of_pseudo_high_internal_ram:
    443  ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
    444 
     439axiom bvt_map2:
     440  ∀A, B, C: Type[0].
     441  ∀n: nat.
     442  ∀bvt_1: BitVectorTrie A n.
     443  ∀bvt_2: BitVectorTrie B n.
     444  ∀f: ∀a: option A. ∀b: option B. option C.
     445    BitVectorTrie C n.
     446
     447axiom is_in_domain:
     448  ∀A: Type[0].
     449  ∀n: nat.
     450  ∀bvt: BitVectorTrie A n.
     451  ∀b: BitVector n.
     452    Prop.
     453
     454axiom bvt_map2_function_extensionality:
     455  ∀A, B, C: Type[0].
     456  ∀n: nat.
     457  ∀bvt_1: BitVectorTrie A n.
     458  ∀bvt_2, bvt_2': BitVectorTrie B n.
     459  ∀f: ∀a: option A. ∀b: option B. option C.
     460    (∀addr.
     461      is_in_domain … bvt_1 addr ∨ is_in_domain … bvt_2 addr ∨ is_in_domain … bvt_2' addr →
     462        f (lookup_opt … addr bvt_1) (lookup_opt … addr bvt_2) = f (lookup_opt … addr bvt_1) (lookup_opt … addr bvt_2')) →
     463          bvt_map2 … bvt_1 bvt_2 f = bvt_map2 … bvt_1 bvt_2' f.
     464
     465definition internal_ram_of_pseudo_internal_ram:
     466    ∀sigma: Word → Word.
     467    ∀ram: BitVectorTrie Byte 7.
     468    ∀map: BitVectorTrie address_entry 7.
     469      BitVectorTrie Byte 7 ≝
     470  λsigma, ram, map.
     471      bvt_map2 ??? ? ram map (λv. λul_addr.
     472        match
     473        match ul_addr with
     474        [ None ⇒ v
     475        | Some ul_addr' ⇒
     476          let 〈ul, addr〉 ≝ ul_addr' in
     477          let v ≝ match v with [ None ⇒ zero … | Some v ⇒ v ] in
     478          match ul with
     479          [ upper ⇒
     480            let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (v@@addr)) in
     481              Some … high
     482          | lower ⇒
     483            let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (addr@@v)) in
     484              Some … low
     485          ]
     486        ] with
     487        [ None ⇒ None …
     488        | Some v ⇒
     489          if eq_bv … v (zero …) then
     490            None …
     491          else
     492            Some … v
     493        ]).
     494
     495definition low_internal_ram_of_pseudo_low_internal_ram:
     496    ∀M: internal_pseudo_address_map.
     497    ∀sigma: Word → Word.
     498    ∀ram: BitVectorTrie Byte 7.
     499      BitVectorTrie Byte 7 ≝
     500  λM, sigma, ram.
     501    let 〈low, high, accA〉 ≝ M in
     502      internal_ram_of_pseudo_internal_ram sigma ram low.
     503
     504definition high_internal_ram_of_pseudo_high_internal_ram:
     505    ∀M: internal_pseudo_address_map.
     506    ∀sigma: Word → Word.
     507    ∀ram: BitVectorTrie Byte 7.
     508      BitVectorTrie Byte 7 ≝
     509  λM, sigma, ram.
     510    let 〈low, high, accA〉 ≝ M in
     511      internal_ram_of_pseudo_internal_ram sigma ram high.
     512
     513(*
    445514axiom low_internal_ram_of_pseudo_internal_ram_hit:
    446  ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word × bool.∀upper_lower: upper_lower. ∀points_to: Word. ∀addr:BitVector 7.
    447   assoc_list_lookup ?? (false:::addr) (eq_bv 8) (\fst M) = Some … 〈upper_lower, points_to〉  →
    448    let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
     515 ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word.∀upper_lower: upper_lower. ∀points_to: Word. ∀addr:BitVector 7.
     516  lookup_opt ?? (false:::addr) (eq_bv 8) (\fst M) = Some … 〈upper_lower, points_to〉  →
     517   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M sigma (low_internal_ram … s) in
    449518   let pbl ≝ lookup ? 7 addr (low_internal_ram … s) (zero 8) in
    450519   let bl ≝ lookup ? 7 addr ram (zero 8) in
    451520   let 〈lower, higher〉 ≝ vsplit ? 8 8 points_to in
    452    let 〈plower, phigher〉 ≝ vsplit ? 8 8 (\fst (sigma points_to)) in
     521   let 〈plower, phigher〉 ≝ vsplit ? 8 8 (sigma points_to) in
    453522     if eq_upper_lower upper_lower upper then
    454523       (pbl = higher) ∧ (bl = phigher)
    455524     else
    456525       (pbl = lower) ∧ (bl = plower).
     526*)
    457527
    458528(* changed from add to sub *)
    459529axiom low_internal_ram_of_pseudo_internal_ram_miss:
    460  ∀T.∀M:internal_pseudo_address_map.∀cm.∀s:PreStatus T cm.∀addr:BitVector 7.
    461   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
    462     assoc_list_exists ?? (false:::addr) (eq_bv 8) (\fst M) = false →
    463       lookup ? 7 addr ram (zero ?) = lookup ? 7 addr (low_internal_ram … s) (zero ?).
    464 
    465 definition addressing_mode_ok ≝
     530 ∀T.∀M:internal_pseudo_address_map.∀sigma. ∀cm.∀s:PreStatus T cm.∀addr:BitVector 7.
     531  let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M sigma (low_internal_ram … s) in
     532    lookup_opt … addr (\fst (\fst M)) = None … →
     533      lookup … addr ram (zero …) = lookup … addr (low_internal_ram … s) (zero ?).
     534
     535definition exists:
     536    ∀A: Type[0].
     537    ∀n: nat.
     538    ∀v: BitVector n.
     539    ∀bvt: BitVectorTrie A n.
     540      bool ≝
     541  λA, n, v, bvt.
     542    match lookup_opt … v bvt with
     543    [ None ⇒ false
     544    | _    ⇒ true
     545    ].
     546
     547definition data_or_address ≝
    466548  λT.
    467549  λM: internal_pseudo_address_map.
    … …  
    469551  λs: PreStatus T cm.
    470552  λaddr: addressing_mode.
    471   match addr with
     553  let 〈low, high, accA〉 ≝ M in
     554  match addr return λx. option (option address_entry) with
    472555    [ DIRECT d ⇒
    473         if eq_bv … d (bitvector_of_nat … 224) then
    474           ¬assoc_list_exists ?? d (eq_bv 8) (\fst M) ∧ eq_accumulator_address_map_entry (\snd M) data
    475         else
    476          ¬assoc_list_exists ?? d (eq_bv 8) (\fst M)
     556       let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 d in
     557         match head' … hd with
     558         [ true ⇒
     559             if eq_bv … d (bitvector_of_nat … 224) then
     560               Some … accA
     561             else
     562               Some … (None …)
     563         | false ⇒ Some … (lookup_opt … seven_bits low)
     564         ]
    477565    | INDIRECT i ⇒
    478566        let d ≝ get_register … s [[false;false;i]] in
    479567        let address ≝ bit_address_of_register … s [[false;false;i]] in
    480           ¬assoc_list_exists … (false:::address) (eq_bv 8) (\fst M) ∧
    481             ¬assoc_list_exists ?? d (eq_bv 8) (\fst M)
     568          if ¬exists … address low then
     569            let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 d in
     570              if head' … 0 bit_one then
     571                Some … (lookup_opt … seven_bits high)
     572              else
     573                Some … (lookup_opt … seven_bits low)
     574          else
     575            None ?
    482576    | EXT_INDIRECT e ⇒
    483577        let address ≝ bit_address_of_register … s [[false;false;e]] in
    484           ¬assoc_list_exists … (false:::address) (eq_bv 8) (\fst M)
     578          if ¬exists … address low then
     579            Some … (None …)
     580          else
     581            None ?
    485582    | REGISTER r ⇒
    486583        let address ≝ bit_address_of_register … s r in
    487           ¬assoc_list_exists … (false:::address) (eq_bv 8) (\fst M)
    488     | ACC_A ⇒
    489       match \snd M with
    490       [ data ⇒ true
    491       | _ ⇒ false
    492       ]
    493     | ACC_B ⇒ true
    494     | DPTR ⇒ true
    495     | DATA _ ⇒ true
    496     | DATA16 _ ⇒ true
    497     | ACC_DPTR ⇒ true
    498     | ACC_PC ⇒ true
    499     | EXT_INDIRECT_DPTR ⇒ true
    500     | INDIRECT_DPTR ⇒ true
    501     | CARRY ⇒ true
     584          Some … (lookup_opt … address low)
     585    | ACC_A ⇒ Some … accA
     586    | ACC_B ⇒ Some … (None …)
     587    | DPTR ⇒ Some … (None …)
     588    | DATA _ ⇒ Some … (None …)
     589    | DATA16 _ ⇒ Some … (None …)
     590    | ACC_DPTR ⇒ Some … (None …)
     591    | ACC_PC ⇒ Some … (None …)
     592    | EXT_INDIRECT_DPTR ⇒ Some … (None …)
     593    | INDIRECT_DPTR ⇒ Some … (None …)
     594    | CARRY ⇒ Some … (None …)
    502595    | BIT_ADDR b ⇒
    503596      let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 b in
     597      let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
    504598        if head' bool 0 bit_one then
    505           eq_accumulator_address_map_entry (\snd M) data
     599            if eq_bv … four_bits [[true; true; false; false]] then (* XXX: this is the accumulator apparently. *)
     600              Some … accA
     601            else
     602              Some … (None …)
    506603        else
    507           let address ≝ nat_of_bitvector 7 seven_bits in 
    508           let address' ≝ bitvector_of_nat 7 ((address÷8)+32) in
    509             ¬assoc_list_exists ?? (false:::address') (eq_bv 8) (\fst M)
    510     | N_BIT_ADDR b ⇒ ¬true (* TO BE COMPLETED *)
    511     | RELATIVE _ ⇒ true
    512     | ADDR11 _ ⇒ true
    513     | ADDR16 _ ⇒ true
     604          let address' ≝ [[true; false; false]]@@four_bits in
     605            Some … (lookup_opt … address' low)
     606    | N_BIT_ADDR b ⇒
     607      let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 b in
     608      let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
     609        if head' bool 0 bit_one then
     610            if eq_bv … four_bits [[true; true; false; false]] then (* XXX: this is the accumulator apparently. *)
     611              Some … accA
     612            else
     613              Some … (None …)
     614        else
     615          let address' ≝ [[true; false; false]]@@four_bits in
     616            Some … (lookup_opt … address' low)
     617    | RELATIVE _ ⇒ Some … (None …)
     618    | ADDR11 _ ⇒ Some … (None …)
     619    | ADDR16 _ ⇒ Some … (None …)
    514620    ].
     621
     622definition assert_data ≝
     623  λT.
     624  λM: internal_pseudo_address_map.
     625  λcm.
     626  λs: PreStatus T cm.
     627  λaddr: addressing_mode.
     628    match data_or_address T M cm s addr with
     629    [ None   ⇒ false
     630    | Some s ⇒
     631      match s with
     632      [ None ⇒ true
     633      | _    ⇒ false
     634      ]
     635    ].
     636   
     637definition insert_into_internal_ram:
     638  ∀addr: Byte.
     639  ∀v: address_entry.
     640  ∀M: internal_pseudo_address_map.
     641    internal_pseudo_address_map ≝
     642  λaddr, v, M.
     643    let 〈low, high, accA〉 ≝ M in
     644    let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 addr in
     645      if head' … bit_one then
     646        〈insert … seven_bits v low, high, accA〉
     647      else
     648        〈low, insert … seven_bits v high, accA〉.
     649   
     650axiom delete:
     651  ∀A: Type[0].
     652  ∀n: nat.
     653  ∀b: BitVector n.
     654    BitVectorTrie A n → BitVectorTrie A n.
     655
     656definition delete_from_internal_ram:
     657    ∀addr: Byte.
     658    ∀M: internal_pseudo_address_map.
     659      internal_pseudo_address_map ≝
     660  λaddr, M.
     661    let 〈low, high, accA〉 ≝ M in
     662    let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 addr in
     663      if head' … bit_one then
     664        〈delete … seven_bits low, high, accA〉
     665      else
     666        〈low, delete … seven_bits high, accA〉.
     667
     668definition overwrite_or_delete_from_internal_ram:
     669    ∀addr: Byte.
     670    ∀v: option address_entry.
     671    ∀M: internal_pseudo_address_map.
     672      internal_pseudo_address_map ≝
     673  λaddr, v, M.
     674    let 〈low, high, accA〉 ≝ M in
     675      match v with
     676      [ None ⇒ delete_from_internal_ram addr M
     677      | Some v' ⇒ insert_into_internal_ram addr v' M
     678      ].
     679
     680definition lookup_from_internal_ram:
     681    ∀addr: Byte.
     682    ∀M: internal_pseudo_address_map.
     683      option address_entry ≝
     684  λaddr, M.
     685    let 〈low, high, accA〉 ≝ M in
     686    let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 addr in
     687      if head' … bit_one then
     688        lookup_opt … seven_bits high
     689      else
     690        lookup_opt … seven_bits low.
    515691   
    516692definition next_internal_pseudo_address_map0 ≝
    … …  
    521697  λM: internal_pseudo_address_map.
    522698  λs: PreStatus T cm.
     699  let 〈low, high, accA〉 ≝ M in
    523700   match fetched with
    524701    [ Comment _ ⇒ Some ? M
    … …  
    527704    | Call a ⇒
    528705      let a' ≝ addr_of a s in
    529       let 〈callM, accM〉 ≝ M in
    530          Some … 〈〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)), 〈lower, a'〉〉::
    531                  〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)), 〈upper, a'〉〉::callM, accM〉
     706      let 〈upA, lowA〉 ≝ vsplit bool 8 8 a' in
     707        Some … (insert_into_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) 〈lower, upA〉
     708                (insert_into_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) 〈upper, lowA〉 M))
    532709    | Mov _ _ ⇒ Some … M
    533710    | Instruction instr ⇒
    534711      match instr return λx. option internal_pseudo_address_map with
    535712       [ ADD addr1 addr2 ⇒
    536          if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
     713         if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
    537714           Some ? M
    538715         else
    539716           None ?
    540717       | ADDC addr1 addr2 ⇒
    541          if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
     718         if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
    542719           Some ? M
    543720         else
    544721           None ?
    545722       | SUBB addr1 addr2 ⇒
    546          if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
     723         if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
    547724           Some ? M
    548725         else
    549726           None ?
    550727       | INC addr1 ⇒
    551          if addressing_mode_ok T M ? s addr1 then
     728         if assert_data T M ? s addr1 then
    552729           Some ? M
    553730         else
    554731           None ?
    555732       | DEC addr1 ⇒
    556          if addressing_mode_ok T M … s addr1 then
     733         if assert_data T M … s addr1 then
    557734           Some ? M
    558735         else
    559736           None ?
    560737       | MUL addr1 addr2 ⇒
    561          if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
     738         if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
    562739           Some ? M
    563740         else
    564741           None ?
    565742       | DIV addr1 addr2 ⇒
    566          if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
     743         if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
    567744           Some ? M
    568745         else
    569746           None ?
    570747       | DA addr1 ⇒
    571          if addressing_mode_ok T M … s addr1 then
     748         if assert_data T M … s addr1 then
    572749           Some ? M
    573750         else
    … …  
    584761         [ inl l ⇒
    585762           let 〈left, right〉 ≝ l in
    586              if addressing_mode_ok T M … s left ∧ addressing_mode_ok T M … s right then
     763             if assert_data T M … s left ∧ assert_data T M … s right then
    587764               Some ? M
    588              else if ¬(addressing_mode_ok T M … s left) ∧ ¬(addressing_mode_ok T M … s right) then
     765             else if ¬(assert_data T M … s left) ∧ ¬(assert_data T M … s right) then
    589766               Some ? M
    590767             else
    … …  
    592769         | inr r ⇒
    593770           let 〈left, right〉 ≝ r in
    594              if addressing_mode_ok T M … s left ∧ addressing_mode_ok T M … s right then
     771             if assert_data T M … s left ∧ assert_data T M … s right then
    595772               Some ? M
    596              else if ¬(addressing_mode_ok T M … s left) ∧ ¬(addressing_mode_ok T M … s right) then
     773             else if ¬(assert_data T M … s left) ∧ ¬(assert_data T M … s right) then
    597774               Some ? M
    598775             else
    … …  
    600777         ]
    601778       | DJNZ addr1 addr2 ⇒
    602          if addressing_mode_ok T M … s addr1 then
     779         if assert_data T M … s addr1 then
    603780           Some ? M
    604781         else
    605782           None ?
    606783       | CLR addr1 ⇒
    607          if addressing_mode_ok T M … s addr1 then
     784         if assert_data T M … s addr1 then
    608785           Some ? M
    609786         else
    610787           None ?
    611788       | CPL addr1 ⇒
    612          if addressing_mode_ok T M … s addr1 then
     789         if assert_data T M … s addr1 then
    613790           Some ? M
    614791         else
    615792           None ?
    616793       | RL addr1 ⇒
    617          if addressing_mode_ok T M … s addr1 then
     794         if assert_data T M … s addr1 then
    618795           Some ? M
    619796         else
    620797           None ?
    621798       | RLC addr1 ⇒
    622          if addressing_mode_ok T M … s addr1 then
     799         if assert_data T M … s addr1 then
    623800           Some ? M
    624801         else
    625802           None ?
    626803       | RR addr1 ⇒
    627          if addressing_mode_ok T M … s addr1 then
     804         if assert_data T M … s addr1 then
    628805           Some ? M
    629806         else
    630807           None ?
    631808       | RRC addr1 ⇒
    632          if addressing_mode_ok T M … s addr1 then
     809         if assert_data T M … s addr1 then
    633810           Some ? M
    634811         else
    635812           None ?
    636813       | SWAP addr1 ⇒
    637          if addressing_mode_ok T M … s addr1 then
     814         if assert_data T M … s addr1 then
    638815           Some ? M
    639816         else
    640817           None ?
    641818       | SETB addr1 ⇒
    642          if addressing_mode_ok T M … s addr1 then
     819         if assert_data T M … s addr1 then
    643820           Some ? M
    644821         else
    … …  
    646823       (* XXX: need to track addresses pushed and popped off the stack? *)
    647824       | PUSH addr1 ⇒
    648          let 〈callM, accM〉 ≝ M in
    649825         match addr1 return λx. bool_to_Prop (is_in … [[direct]] x) → ? with
    650826         [ DIRECT d ⇒ λproof.
    651            let extended ≝ pad 8 8 d in
    652              Some … 〈〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)), 〈lower, extended〉〉::callM, accM〉
     827           let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 d in
     828             if head' … bit_one then
     829               if eq_bv … seven_bits (bitvector_of_nat … 224) then
     830                 Some … (overwrite_or_delete_from_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) accA M)
     831               else
     832                 Some … (delete_from_internal_ram … (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) M)
     833             else
     834               match lookup_from_internal_ram … d M with
     835               [ None ⇒
     836                   Some … (delete_from_internal_ram … (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) M)
     837               | Some ul_addr ⇒
     838                   Some … (insert_into_internal_ram (add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) ul_addr M)
     839               ]
    653840         | _ ⇒ λother: False. ⊥
    654841         ] (subaddressing_modein … addr1)
    655        | POP addr1 ⇒ Some … M
     842       | POP addr1 ⇒
     843         let sp ≝ get_8051_sfr ?? s SFR_SP in
     844         match addr1 return λx. bool_to_Prop (is_in … [[direct]] x) → ? with
     845         [ DIRECT d ⇒ λproof.
     846           let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 d in
     847             if head' … bit_one then
     848               if eq_bv … d (bitvector_of_nat … 224) then
     849                 Some … 〈low, high, lookup_from_internal_ram … sp M〉
     850               else
     851                 match lookup_from_internal_ram sp M with
     852                 [ None ⇒ Some ? M
     853                 | _    ⇒ None ?
     854                 ]
     855             else
     856               Some … (overwrite_or_delete_from_internal_ram d (lookup_from_internal_ram … sp M) M)
     857         | _ ⇒ λother: False. ⊥
     858         ] (subaddressing_modein … addr1)
    656859       | XCH addr1 addr2 ⇒
    657          if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
     860         if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
    658861           Some ? M
    659862         else
    660863           None ?
    661864       | XCHD addr1 addr2 ⇒
    662          if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then
     865         if assert_data T M … s addr1 ∧ assert_data T M … s addr2 then
    663866           Some ? M
    664867         else
    665868           None ?
    666869      | RET ⇒
    667         let 〈callM, accM〉 ≝ M in
    668         let sp_plus_1 ≝ assoc_list_exists ?? (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (eq_bv 8) callM in
    669         let sp_plus_2 ≝ assoc_list_exists ?? (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) (eq_bv 8) callM in
    670           if sp_plus_1 ∧ sp_plus_2 then
    671             Some … M
    672           else
    673             None ?
     870        let sp_minus_1 ≝ subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1) in
     871        let sp_minus_2 ≝ subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2) in
     872        match lookup_from_internal_ram sp_minus_1 M with
     873        [ None ⇒ None …
     874        | Some low_addr_high ⇒
     875            match lookup_from_internal_ram sp_minus_2 M with
     876            [ None ⇒ None …
     877            | Some high_addr_low ⇒
     878              let 〈low, addr_high〉 ≝ low_addr_high in
     879              let 〈high, addr_low〉 ≝ high_addr_low in
     880              let addr_low' ≝ read_from_internal_ram … s sp_minus_1 in
     881              let addr_high' ≝ read_from_internal_ram … s sp_minus_2 in
     882                if eq_upper_lower low lower ∧ eq_upper_lower high upper ∧ eq_bv … addr_low addr_low' ∧ eq_bv … addr_high addr_high' then
     883                  Some ? M
     884                else
     885                  None ?
     886            ]
     887        ]
    674888      | RETI ⇒
    675         let 〈callM, accM〉 ≝ M in
    676         let sp_plus_1 ≝ assoc_list_exists ?? (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) (eq_bv 8) callM in
    677         let sp_plus_2 ≝ assoc_list_exists ?? (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) (eq_bv 8) callM in
    678           if sp_plus_1 ∧ sp_plus_2 then
    679             Some … M
    680           else
    681             None ?
     889        let sp_minus_1 ≝ subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1) in
     890        let sp_minus_2 ≝ subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2) in
     891        match lookup_from_internal_ram (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)) M with
     892        [ None ⇒ None …
     893        | Some low_addr_high ⇒
     894            match lookup_from_internal_ram (subtraction 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)) M with
     895            [ None ⇒ None …
     896            | Some high_addr_low ⇒
     897              let 〈low, addr_high〉 ≝ low_addr_high in
     898              let 〈high, addr_low〉 ≝ high_addr_low in
     899              let addr_low' ≝ read_from_internal_ram … s sp_minus_1 in
     900              let addr_high' ≝ read_from_internal_ram … s sp_minus_2 in
     901                if eq_upper_lower low lower ∧ eq_upper_lower high upper ∧ eq_bv … addr_low addr_low' ∧ eq_bv … addr_high addr_high' then
     902                  Some ? M
     903                else
     904                  None ?
     905            ]
     906        ]
    682907      | NOP ⇒ Some … M
    683908      | MOVX addr1 ⇒
    684909        match addr1 with
    685910        [ inl l ⇒
    686           let 〈acc_a, others〉 ≝ l in
    687           let acc_a_ok ≝ addressing_mode_ok T M … s acc_a in
    688           let others_ok ≝ addressing_mode_ok T M … s others in
    689             if acc_a_ok ∧ others_ok then
    690               Some ? M
    691             else
    692               None ?
     911            Some ? 〈low, high, None …〉
    693912        | inr r ⇒
    694913          let 〈others, acc_a〉 ≝ r in
    695           let acc_a_ok ≝ addressing_mode_ok T M … s acc_a in
    696           let others_ok ≝ addressing_mode_ok T M … s others in
    697             if others_ok ∧ acc_a_ok then
     914            if assert_data T M … s acc_a then
    698915              Some ? M
    699916            else
    … …  
    704921        [ inl l ⇒
    705922          let 〈acc_a, others〉 ≝ l in
    706           let acc_a_ok ≝ addressing_mode_ok T M … s acc_a in
    707           let others_ok ≝ addressing_mode_ok T M … s others in
     923          let acc_a_ok ≝ assert_data T M … s acc_a in
     924          let others_ok ≝ assert_data T M … s others in
    708925          if acc_a_ok ∧ others_ok then
    709926            Some ? M
    … …  
    712929        | inr r ⇒
    713930          let 〈direct, others〉 ≝ r in
    714           let direct_ok ≝ addressing_mode_ok T M … s direct in
    715           let others_ok ≝ addressing_mode_ok T M … s others in
     931          let direct_ok ≝ assert_data T M … s direct in
     932          let others_ok ≝ assert_data T M … s others in
    716933          if direct_ok ∧ others_ok then
    717934            Some ? M
    … …  
    725942          [ inl l ⇒
    726943            let 〈acc_a, others〉 ≝ l in
    727             let acc_a_ok ≝ addressing_mode_ok T M … s acc_a in
    728             let others_ok ≝ addressing_mode_ok T M … s others in
     944            let acc_a_ok ≝ assert_data T M … s acc_a in
     945            let others_ok ≝ assert_data T M … s others in
    729946            if acc_a_ok ∧ others_ok then
    730947              Some ? M
    … …  
    733950          | inr r ⇒
    734951            let 〈direct, others〉 ≝ r in
    735             let direct_ok ≝ addressing_mode_ok T M … s direct in
    736             let others_ok ≝ addressing_mode_ok T M … s others in
     952            let direct_ok ≝ assert_data T M … s direct in
     953            let others_ok ≝ assert_data T M … s others in
    737954            if direct_ok ∧ others_ok then
    738955              Some ? M
    … …  
    742959        | inr r ⇒
    743960          let 〈carry, others〉 ≝ r in
    744           let carry_ok ≝ addressing_mode_ok T M … s carry in
    745           let others_ok ≝ addressing_mode_ok T M … s others in
     961          let carry_ok ≝ assert_data T M … s carry in
     962          let others_ok ≝ assert_data T M … s others in
    746963          if carry_ok ∧ others_ok then
    747964            Some ? M
    … …  
    755972          [ inl l ⇒
    756973            let 〈acc_a, others〉 ≝ l in
    757             let acc_a_ok ≝ addressing_mode_ok T M … s acc_a in
    758             let others_ok ≝ addressing_mode_ok T M … s others in
     974            let acc_a_ok ≝ assert_data T M … s acc_a in
     975            let others_ok ≝ assert_data T M … s others in
    759976            if acc_a_ok ∧ others_ok then
    760977              Some ? M
    … …  
    763980          | inr r ⇒
    764981            let 〈direct, others〉 ≝ r in
    765             let direct_ok ≝ addressing_mode_ok T M … s direct in
    766             let others_ok ≝ addressing_mode_ok T M … s others in
     982            let direct_ok ≝ assert_data T M … s direct in
     983            let others_ok ≝ assert_data T M … s others in
    767984            if direct_ok ∧ others_ok then
    768985              Some ? M
    … …  
    772989        | inr r ⇒
    773990          let 〈carry, others〉 ≝ r in
    774           let carry_ok ≝ addressing_mode_ok T M … s carry in
    775           let others_ok ≝ addressing_mode_ok T M … s others in
     991          let carry_ok ≝ assert_data T M … s carry in
     992          let others_ok ≝ assert_data T M … s others in
    776993          if carry_ok ∧ others_ok then
    777994            Some ? M
    … …  
    780997        ]
    781998      | MOV addr1 ⇒
     999        (* XXX: wrong *)
    7821000        match addr1 with
    7831001        [ inl l ⇒
    … …  
    7911009                [ inl l'''' ⇒
    7921010                  let 〈acc_a, others〉 ≝ l'''' in
    793                   if addressing_mode_ok T M … s acc_a ∧ addressing_mode_ok T M … s others then
    794                     Some ? M
    795                   else
    796                     None ?
     1011                    match data_or_address T M … s others with
     1012                    [ None ⇒ None ?
     1013                    | Some s ⇒
     1014                        Some … 〈low, high, s〉
     1015                    ]
    7971016                | inr r ⇒
    7981017                  let 〈others, others'〉 ≝ r in
    799                   if addressing_mode_ok T M … s others ∧ addressing_mode_ok T M … s others' then
    800                     Some ? M
    801                   else
    802                     None ?
     1018                  let address ≝
     1019                    match others return λx. bool_to_Prop (is_in … [[ registr; indirect ]] x) → ? with
     1020                    [ REGISTER r ⇒ λproof. false:::bit_address_of_register … s r
     1021                    | INDIRECT i ⇒ λproof. get_register … s [[false; false; i]]
     1022                    | _ ⇒ λother: False. ⊥
     1023                    ] (subaddressing_modein … others)
     1024                  in
     1025                    match data_or_address T M … s others' with
     1026                    [ None ⇒ None ?
     1027                    | Some s ⇒
     1028                        Some … (overwrite_or_delete_from_internal_ram address s M)
     1029                    ]
    8031030                ]
    8041031              | inr r ⇒
    805                 let 〈direct, others〉 ≝ r in
    806                 if addressing_mode_ok T M … s direct ∧ addressing_mode_ok T M … s others then
    807                   Some ? M
    808                 else
    809                   None ?
     1032                let 〈direct', others〉 ≝ r in
     1033                  match direct' return λx. bool_to_Prop (is_in … [[direct]] x) → ? with
     1034                  [ DIRECT d ⇒ λproof.
     1035                    match data_or_address T M … s others with
     1036                    [ None ⇒ None ?
     1037                    | Some s' ⇒
     1038                        let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 d in
     1039                          if head' … bit_one then
     1040                            if eq_bv … d (bitvector_of_nat … 224) then
     1041                              Some … 〈low, high, s'〉
     1042                            else
     1043                              match s' with
     1044                              [ None ⇒ Some ? M
     1045                              | Some s'' ⇒ None ?
     1046                              ]
     1047                          else
     1048                            Some … (overwrite_or_delete_from_internal_ram d s' M)
     1049                    ]
     1050                  | _ ⇒ λother: False. ⊥
     1051                  ] (subaddressing_modein … direct')
    8101052              ]
    811             | inr r ⇒
    812               let 〈dptr, data_16〉 ≝ r in
    813               if addressing_mode_ok T M … s dptr ∧ addressing_mode_ok T M … s data_16 then
    814                 Some ? M
    815               else
    816                 None ?
     1053            | inr r ⇒ Some … M
    8171054            ]
    8181055          | inr r ⇒
    8191056            let 〈carry, bit_addr〉 ≝ r in
    820             if addressing_mode_ok T M … s carry ∧ addressing_mode_ok T M … s bit_addr then
     1057            if assert_data T M … s bit_addr then
    8211058              Some ? M
    8221059            else
    … …  
    8251062        | inr r ⇒
    8261063          let 〈bit_addr, carry〉 ≝ r in
    827           if addressing_mode_ok T M … s bit_addr ∧ addressing_mode_ok T M … s carry then
     1064          if assert_data T M … s bit_addr then
    8281065            Some ? M
    8291066          else
    … …  
    8581095  λsigma: Word → Word.
    8591096    match \snd M with
    860     [ data ⇒ sfrs
    861     | address upper_lower address ⇒
     1097    [ None ⇒ sfrs
     1098    | Some upper_lower_address ⇒
    8621099      let index ≝ sfr_8051_index SFR_ACC_A in
    863       let 〈high, low〉 ≝ vsplit ? 8 8 (sigma address) in
     1100      let acc_a ≝ get_index_v … sfrs index ? in
     1101      let 〈upper_lower, address〉 ≝ upper_lower_address in
    8641102        if eq_upper_lower upper_lower upper then
    865           set_index Byte 19 sfrs index high ?
     1103          let 〈high, low〉 ≝ vsplit ? 8 8 (sigma (acc_a@@address)) in
     1104            set_index Byte 19 sfrs index high ?
    8661105        else
    867           set_index Byte 19 sfrs index low ?
     1106          let 〈high, low〉 ≝ vsplit ? 8 8 (sigma (address@@acc_a)) in
     1107            set_index Byte 19 sfrs index low ?
    8681108    ].
    8691109  //
    … …  
    8811121  let cm ≝ code_memory_of_pseudo_assembly_program … sigma policy in
    8821122  let pc ≝ sigma (program_counter … ps) in
    883   let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in
    884   let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in
     1123  let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M sigma (low_internal_ram … ps) in
     1124  let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M sigma (high_internal_ram … ps) in
    8851125     mk_PreStatus (BitVectorTrie Byte 16)
    8861126      cm
    … …  
    12061446  ∀arg: Byte.
    12071447  ∀b: bool.
    1208     addressing_mode_ok m s (DIRECT arg) = true →
     1448    assert_data m s (DIRECT arg) = true →
    12091449      get_arg_8 ? (set_low_internal_ram ? s (low_internal_ram_of_pseudo_low_internal_ram m (low_internal_ram ? s))) b (DIRECT arg) =
    12101450      get_arg_8 ? s b (DIRECT arg).
    … …  
    12651505  get_arg_8 (internal_ram ...) (DIRECT arg)
    12661506
    1267 ((if addressing_mode_ok M ps ACC_A∧addressing_mode_ok M ps (DIRECT ARG2) 
     1507((if assert_data M ps ACC_A∧assert_data M ps (DIRECT ARG2) 
    12681508                     then Some internal_pseudo_address_map M 
    12691509                     else None internal_pseudo_address_map )
Note: See TracChangeset for help on using the changeset viewer.