Changeset 2272 for src/ASM


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.

Location:
src/ASM
Files:
7 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 )

  • src/ASM/AssemblyProofSplit.ma

    r2265 r2272  
    390390qed.
    391391
    392 lemma get_index_v_set_index_hit:
    393   ∀A: Type[0].
    394   ∀n: nat.
    395   ∀v: Vector A n.
    396   ∀i: nat.
    397   ∀e: A.
    398   ∀i_lt_n_proof: i < n.
    399   ∀i_lt_n_proof': i < n.
    400     get_index_v A n (set_index A n v i e i_lt_n_proof) i i_lt_n_proof' = e.
    401   #A #n #v elim v
    402   [1:
    403     #i #e #i_lt_n_proof
    404     cases (lt_to_not_zero … i_lt_n_proof)
    405   |2:
    406     #n' #hd #tl #inductive_hypothesis #i #e
    407     cases i
    408     [1:
    409       #i_lt_n_proof #i_lt_n_proof' %
    410     |2:
    411       #i' #i_lt_n_proof' #i_lt_n_proof''
    412       whd in ⊢ (??%?); @inductive_hypothesis
    413     ]
    414   ]
    415 qed.
     392axiom insert_low_internal_ram_of_pseudo_low_internal_ram':
     393  ∀M, M', sigma,cm,s,addr,v,v'.
     394    (∀addr'.
     395      ((false:::addr) = addr' →
     396        map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v =
     397        map_internal_ram_address_using_pseudo_address_map M' sigma (false:::addr) v') ∧
     398      ((false:::addr) ≠ addr' →
     399        let 〈callM, accM〉 ≝ M in
     400        let 〈callM', accM'〉 ≝ M' in
     401          accM = accM' ∧
     402            assoc_list_lookup … addr' (eq_bv 8) … callM =
     403              assoc_list_lookup … addr' (eq_bv 8) … callM')) →
     404    insert Byte 7 addr v'
     405      (low_internal_ram_of_pseudo_low_internal_ram M'
     406      (low_internal_ram pseudo_assembly_program cm s)) =
     407    low_internal_ram_of_pseudo_low_internal_ram M
     408      (insert Byte 7 addr v (low_internal_ram pseudo_assembly_program cm s)).
    416409
    417 (*
    418410lemma write_at_stack_pointer_status_of_pseudo_status:
    419411  ∀M, M'.
    … …  
    423415  ∀s, s'.
    424416  ∀new_b, new_b'.
    425     M = M' →
    426     map_internal_ram_address_using_pseudo_address_map M sigma new_b = new_b' →
     417    map_internal_ram_address_using_pseudo_address_map M sigma (get_8051_sfr pseudo_assembly_program cm s SFR_SP) new_b = new_b' →
    427418    status_of_pseudo_status M cm s sigma policy = s' →
    428419    write_at_stack_pointer ?? s' new_b' =
    429     status_of_pseudo_status M cm (write_at_stack_pointer ? cm s new_b) sigma policy.
     420    status_of_pseudo_status M' cm (write_at_stack_pointer ? cm s new_b) sigma policy.
    430421  #M #M' #cm #sigma #policy #s #s' #new_b #new_b'
    431   #Mrefl #new_b_refl #s_refl <Mrefl <new_b_refl <s_refl
     422  #new_b_refl #s_refl <new_b_refl <s_refl
    432423  whd in match write_at_stack_pointer; normalize nodelta
    433424  @pair_elim #nu #nl #nu_nl_refl normalize nodelta
    … …  
    449440    ]
    450441  |2:
    451     cases (get_index_v bool ????) normalize nodelta
    452     whd in match status_of_pseudo_status; normalize nodelta
    453     whd in match set_low_internal_ram; normalize nodelta
    454     @split_eq_status try %
    455     [1:
    456       @(insert_low_internal_ram_of_pseudo_low_internal_ram … sigma)
    457     |2:
    458       @(insert_high_internal_ram_of_pseudo_high_internal_ram … sigma)
     442    @if_then_else_status_of_pseudo_status try %
     443    [2:
     444      @sym_eq <set_low_internal_ram_status_of_pseudo_status
     445      [1:
     446        @eq_f2
     447        [2:
     448          @insert_low_internal_ram_of_pseudo_low_internal_ram'
     449    @sym_eq
     450    [2:
     451      <set_low_internal_ram_status_of_pseudo_status
     452      [1:
     453        @eq_f2
     454        [2:
     455          @sym_eq
     456          >(insert_low_internal_ram_of_pseudo_low_internal_ram … sigma … new_b')
     457          [2:
     458            >new_b_refl
     459    ]
    459460  ]
    460 *)
     461qed.
    461462
    462463lemma main_lemma_preinstruction:
    … …  
    519520            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
    520521                                                   (get_arg_8 … s false addr2) false in
    521             let cy_flag ≝ get_index' ? O  ? flags in
     522            let cy_flag ≝ get_index' ? O ? flags in
    522523            let ac_flag ≝ get_index' ? 1 ? flags in
    523524            let ov_flag ≝ get_index' ? 2 ? flags in
    … …  
    917918  try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*)
    918919  whd in match execute_1_preinstruction; normalize nodelta
    919   [1,2: (* ADD and ADDC *)
     920  [(*1,2: (* ADD and ADDC *)
    920921    (* XXX: work on the right hand side *)
    921922    (* XXX: switch to the left hand side *)
    … …  
    15351536      ]
    15361537    ]
    1537   |12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28: (* XXX: conditional jumps *)
     1538  |*)12: (* JC *)
     1539    >EQP -P normalize nodelta
     1540    whd in match expand_pseudo_instruction; normalize nodelta
     1541    whd in match expand_relative_jump; normalize nodelta
     1542    whd in match expand_relative_jump_internal; normalize nodelta
     1543    @pair_elim #sj_possible #disp #sj_possible_disp_refl
     1544    inversion sj_possible #sj_possible_refl normalize nodelta
     1545    [1:
     1546      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1547      whd in maps_assm:(??%%);
     1548      lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
     1549      whd in ⊢ (??%?); normalize nodelta
     1550      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     1551      whd in ⊢ (??%?);
     1552      @if_then_else_status_of_pseudo_status
     1553      >EQs >EQticks <instr_refl normalize nodelta
     1554      [1:
     1555        @(get_cy_flag_status_of_pseudo_status M') %
     1556      |2:
     1557        @sym_eq @set_program_counter_status_of_pseudo_status
     1558        [1:
     1559        |2:
     1560          @sym_eq @set_clock_status_of_pseudo_status try %
     1561          whd in match ticks_of0; normalize nodelta
     1562          @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
     1563          [1:
     1564            @eq_f2 try %
     1565            >sigma_increment_commutation
     1566            lapply sigma_policy_witness whd in match sigma_policy_specification; normalize nodelta
     1567            * #sigma_zero_assm #relevant cases (relevant ppc ?)
     1568            [1:
     1569              -relevant
     1570              [2:
     1571                >EQcm assumption
     1572              |1:
     1573                #relevant #_ <EQppc >relevant @eq_f @eq_f @eq_f
     1574                >EQlookup_labels >EQcm >create_label_cost_refl @eq_f2
     1575              ]
     1576            |2:
     1577            ]
     1578          |2:
     1579            >sj_possible_refl %
     1580          ]
     1581        ]
     1582      |3:
     1583      ]
     1584    ]
    15381585    cases daemon
    1539   |29,30: (* ANL and ORL *)
     1586  |13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28: (* XXX: conditional jumps *)
     1587    cases daemon
     1588  |(*29,30: (* ANL and ORL *)
    15401589    inversion addr
    15411590    [1,3:
    … …  
    22282277      @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … ps ps … b … false (refl …) addressing_mode_ok_assm_1)
    22292278    ]
    2230   |42: (* PUSH *)
     2279  |*)42: (* PUSH *)
    22312280    >EQP -P normalize nodelta lapply instr_refl
    22322281    @(subaddressing_mode_elim … addr) #w #instr_refl normalize nodelta

  • src/ASM/Interpret.ma

    r2264 r2272  
    727727                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    728728                let s ≝ set_8051_sfr … s SFR_SP new_sp in
    729                   write_at_stack_pointer … s d
     729                  write_at_stack_pointer ?? s (get_arg_8 ?? s false (DIRECT … d))
    730730              | _ ⇒ λother: False. ⊥
    731731              ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))

  • src/ASM/Status.ma

    r2270 r2272  
    700700      set_low_internal_ram … s new_low_internal_ram.
    701701     
    702 definition read_at_stack_pointer ≝
    703   λM: Type[0].
    704   λcode_memory:M.
    705   λs: PreStatus M code_memory.
    706     let 〈 nu, nl 〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_SP) in
    707     let m ≝ get_index_v ?? nu O ? in
    708     let r1 ≝ get_index_v ?? nu 1 ? in
    709     let r2 ≝ get_index_v ?? nu 2 ? in
    710     let r3 ≝ get_index_v ?? nu 3 ? in
    711     let address ≝ [[ r1 ; r2 ; r3 ]] @@ nl in
     702definition read_from_internal_ram ≝
     703  λM: Type[0].
     704  λcode_memory:M.
     705  λs: PreStatus M code_memory.
     706  λaddr: Byte.
     707    let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 addr in
    712708    let memory ≝
    713       if m then
     709      if head' … bit_one then
    714710        (low_internal_ram ?? s)
    715711      else
    716712        (high_internal_ram ?? s)
    717713    in
    718       lookup … address memory (zero 8).
    719   [1,2,3,4:
    720      normalize
    721      repeat (@ le_S_S)
    722      @ le_O_n
    723   ]
    724 qed.
     714      lookup … seven_bits memory (zero 8).
     715
     716definition read_at_stack_pointer ≝
     717  λM: Type[0].
     718  λcode_memory:M.
     719  λs: PreStatus M code_memory.
     720    read_from_internal_ram M code_memory s (get_8051_sfr ?? s SFR_SP).
    725721
    726722definition write_at_stack_pointer ≝
    … …  
    729725  λs: PreStatus M code_memory.
    730726  λv: Byte.
    731     let 〈 nu, nl 〉 ≝ vsplit … 4 4 (get_8051_sfr ?? s SFR_SP) in
    732     let bit_zero ≝ get_index_v ?? nu O ? in
    733     let bit_1 ≝ get_index_v ?? nu 1 ? in
    734     let bit_2 ≝ get_index_v ?? nu 2 ? in
    735     let bit_3 ≝ get_index_v ?? nu 3 ? in
    736       if bit_zero then
    737         let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
    738                               v (high_internal_ram ?? s) in
     727    let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr ?? s SFR_SP) in
     728      if head' … 0 bit_one then
     729        let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in
    739730          set_high_internal_ram ?? s memory
    740731      else
    741         let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
    742                               v (low_internal_ram ?? s) in
     732        let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in
    743733          set_low_internal_ram ?? s memory.
    744   [1,2,3,4:
    745      normalize
    746      repeat (@ le_S_S)
    747      @ le_O_n
    748   ]
    749 qed.
    750734
    751735definition set_arg_16': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. Word → [[ dptr ]] → Σs':PreStatus M code_memory. clock ?? s = clock ?? s' ≝
    … …  
    971955        match head' … bit_1 with
    972956        [ true ⇒
    973           let address ≝ nat_of_bitvector … seven_bits in
    974           let d ≝ address ÷ 8 in
    975           let m ≝ address mod 8 in
    976           let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
     957          let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
     958          let trans ≝ true:::four_bits @@ [[false; false; false]] in
    977959          let sfr ≝ get_bit_addressable_sfr ?? s trans l in
    978             get_index_v … sfr m ?
     960            get_index_v … sfr (nat_of_bitvector … three_bits) ?
    979961        | false ⇒
    980           let address ≝ nat_of_bitvector … seven_bits in
    981           let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
     962          let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
     963          let address' ≝ [[true; false; false]]@@four_bits in
    982964          let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
    983             get_index_v … t (modulus address 8) ?
     965            get_index_v … t (nat_of_bitvector … three_bits) ?
    984966        ]
    985967      | N_BIT_ADDR n ⇒
    … …  
    988970        match head' … bit_1 with
    989971        [ true ⇒
    990           let address ≝ nat_of_bitvector … seven_bits in
    991           let d ≝ address ÷ 8 in
    992           let m ≝ address mod 8 in
    993           let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
     972          let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
     973          let trans ≝ true:::four_bits @@ [[false; false; false]] in
    994974          let sfr ≝ get_bit_addressable_sfr ?? s trans l in
    995             ¬(get_index_v … sfr m ?)
     975            ¬(get_index_v ?? sfr (nat_of_bitvector … three_bits) ?)
    996976        | false ⇒
    997           let address ≝ nat_of_bitvector … seven_bits in
    998           let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
     977          let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
     978          let address' ≝ [[true; false; false]]@@four_bits in
    999979          let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
    1000             ¬(get_index_v … t (modulus address 8) ?)
     980            ¬(get_index_v … t (nat_of_bitvector … three_bits) ?)
    1001981        ]
    1002982      | CARRY ⇒ λcarry: True. get_cy_flag ?? s
    … …  
    1004984        match other in False with [ ]
    1005985      ] (subaddressing_modein … a).
    1006       @modulus_less_than
     986  //
    1007987qed.
    1008988     
    … …  
    1018998        match head' … bit_1 with
    1019999        [ true ⇒
    1020           let address ≝ nat_of_bitvector … seven_bits in
    1021           let d ≝ address ÷ 8 in
    1022           let m ≝ address mod 8 in
    1023           let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
    1024           let sfr ≝ get_bit_addressable_sfr … s t true in
    1025           let new_sfr ≝ set_index … sfr m v ? in
    1026             set_bit_addressable_sfr … s new_sfr t
     1000          let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
     1001          let trans ≝ true:::four_bits @@ [[false; false; false]] in
     1002          let sfr ≝ get_bit_addressable_sfr … s trans true in
     1003          let new_sfr ≝ set_index … sfr (nat_of_bitvector … three_bits) v ? in
     1004            set_bit_addressable_sfr … s new_sfr trans
    10271005        | false ⇒
    1028           let address ≝ nat_of_bitvector … seven_bits in
    1029           let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
     1006          let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
     1007          let address' ≝ [[true; false; false]]@@four_bits in
    10301008          let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in
    1031           let n_bit ≝ set_index … t (modulus address 8) v ? in
     1009          let n_bit ≝ set_index … t (nat_of_bitvector … three_bits) v ? in
    10321010          let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in
    10331011            set_low_internal_ram … s memory
    … …  
    10431021            [ ]
    10441022      ] (subaddressing_modein … a).
    1045   @modulus_less_than
     1023  //
    10461024qed.
    10471025

  • src/ASM/StatusProofs.ma

    r2172 r2272  
    2727  #m #s #v
    2828  whd in match write_at_stack_pointer; normalize nodelta
    29   cases(vsplit … 4 4 ?) #nu #nl normalize nodelta
    30   cases(get_index_v … 4 nu 0 ?) //
     29  cases(vsplit … 1 7 ?) #bit_one #seven_bits normalize nodelta
     30  cases (head' bool ??) normalize nodelta //
    3131qed.
    3232
    … …  
    236236  = special_function_registers_8051 T cm s.
    237237 #T #cm #s #x whd in ⊢ (??(???%)?);
    238  cases (vsplit ????) #nu #nl normalize nodelta;
    239  cases (get_index_v bool ????) %
     238 cases (vsplit ????) #bit_one #seven_bits normalize nodelta
     239  cases (head' bool ??) normalize nodelta %
    240240qed.
    241241
    … …  
    297297 ∀T,cm,s,x. external_ram T cm (write_at_stack_pointer T cm s x) = external_ram T cm s.
    298298 #T #cm #s #x whd in ⊢ (??(???%)?);
    299  cases (vsplit ????) #nu #nl normalize nodelta;
    300  cases (get_index_v bool ????) %
     299 cases (vsplit ????) #bit_one #seven_bits normalize nodelta
     300 cases (head' bool ??) %
    301301qed.
    302302
    … …  
    306306  = special_function_registers_8052 T cm s.
    307307 #T #cm #s #x whd in ⊢ (??(???%)?);
    308  cases (vsplit ????) #nu #nl normalize nodelta;
    309  cases (get_index_v bool ????) %
     308 cases (vsplit ????) #bit_one #seven_bits normalize nodelta
     309 cases (head' bool ??) %
    310310qed.
    311311
    … …  
    313313 ∀T,cm,s,x. p1_latch T cm (write_at_stack_pointer T cm s x) = p1_latch T cm s.
    314314 #T #cm #s #x whd in ⊢ (??(???%)?);
    315  cases (vsplit ????) #nu #nl normalize nodelta;
    316  cases (get_index_v bool ????) %
     315 cases (vsplit ????) #bit_one #seven_bits normalize nodelta
     316 cases (head' bool ??) %
    317317qed.
    318318
    … …  
    320320 ∀T,cm,s,x. p3_latch T cm (write_at_stack_pointer T cm s x) = p3_latch T cm s.
    321321 #T #cm #s #x whd in ⊢ (??(???%)?);
    322  cases (vsplit ????) #nu #nl normalize nodelta;
    323  cases (get_index_v bool ????) %
     322 cases (vsplit ????) #bit_one #seven_bits normalize nodelta
     323 cases (head' bool ??) %
    324324qed.
    325325
    … …  
    412412  #m #cm #s #v
    413413  whd in match write_at_stack_pointer; normalize nodelta
    414   cases (vsplit bool 4 4 ?) #nu #nl normalize nodelta
    415   cases (get_index_v bool 4 nu ??) normalize nodelta /demod/ %
     414 cases (vsplit ????) #bit_one #seven_bits normalize nodelta
     415 cases (head' bool ??) %
    416416qed.
    417417

  • src/ASM/StatusProofsSplit.ma

    r2172 r2272  
    8181  ∀cm: M.
    8282  ∀s: PreStatus M cm.
    83   ∀sfr: SFR8051.
    8483  ∀pc: Word.
    8584    get_8051_sfr M cm (set_program_counter M cm s pc) =
    8685      get_8051_sfr M cm s.
    87   #M #cm #s #sfr #pc %
     86  #M #cm #s #pc %
    8887qed.
    8988
    … …  
    360359  ∀sigma: Word → Word.
    361360  ∀policy: Word → bool.
    362     \snd M = data →
     361    \snd M = None … →
    363362      special_function_registers_8051 pseudo_assembly_program cm s =
    364363        special_function_registers_8051 (BitVectorTrie Byte 16)
    … …  
    457456  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
    458457  cases M #left #right cases right normalize nodelta try %
    459   -right * #address
     458  -right * * #address normalize nodelta
    460459  @pair_elim #high #low #high_low_refl normalize nodelta
    461460  whd in match sfr_8051_index; normalize nodelta
    … …  
    469468include alias "ASM/BitVectorTrie.ma".
    470469*)
    471 
    472 lemma get_8051_sfr_status_of_pseudo_status:
    473   ∀M.
    474   ∀cm, ps, sigma, policy.
    475   ∀sfr.
    476     (sfr = SFR_ACC_A → \snd M = data) →
    477     get_8051_sfr (BitVectorTrie Byte 16)
    478       (code_memory_of_pseudo_assembly_program cm sigma policy)
    479       (status_of_pseudo_status M cm ps sigma policy) sfr =
    480     get_8051_sfr pseudo_assembly_program cm ps sfr.
    481   #M #cm #ps #sigma #policy * cases M #fstM #sndM #relevant
    482   [18:
    483      >relevant %
    484   ]
    485   cases sndM try % * #address
    486   whd in match get_8051_sfr;
    487   whd in match status_of_pseudo_status; normalize nodelta
    488   whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
    489   @pair_elim #upper #lower #upper_lower_refl
    490   @get_index_v_set_index_miss @nmk #relevant
    491   normalize in relevant; destruct(relevant)
    492 qed.
    493470
    494471lemma bitvector_cases_hd_tl:
    … …  
    572549      special_function_registers_8051 M cm ps.
    573550  //
    574 qed.
    575 
    576 lemma get_arg_8_pseudo_addressing_mode_ok:
    577   ∀M: internal_pseudo_address_map.
    578   ∀cm: pseudo_assembly_program.
    579   ∀ps: PreStatus pseudo_assembly_program cm.
    580   ∀sigma: Word → Word.
    581   ∀policy: Word → bool.
    582   ∀addr1: [[registr; direct]].
    583     addressing_mode_ok pseudo_assembly_program M cm ps addr1 = true →
    584       get_arg_8 (BitVectorTrie Byte 16)
    585         (code_memory_of_pseudo_assembly_program cm sigma policy)
    586         (status_of_pseudo_status M cm ps sigma policy) true addr1 =
    587       get_arg_8 pseudo_assembly_program cm ps true addr1.
    588   [2,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
    589   #M #cm #ps #sigma #policy #addr1
    590   @(subaddressing_mode_elim … addr1) #arg whd in ⊢ (? → ???%);
    591   [1:
    592     whd in ⊢ (??%? → ??%?);
    593     whd in match bit_address_of_register; normalize nodelta
    594     @pair_elim #un #ln #un_ln_refl
    595     lapply (refl_to_jmrefl ??? un_ln_refl) -un_ln_refl #un_ln_refl
    596     @(pair_replace ?????????? un_ln_refl)
    597     [1:
    598       whd in match get_8051_sfr; normalize nodelta
    599       whd in match sfr_8051_index; normalize nodelta
    600       @eq_f <get_index_v_special_function_registers_8051_not_acc_a
    601       try % #absurd destruct(absurd)
    602     |2:
    603       #assembly_mode_ok_refl
    604       >low_internal_ram_of_pseudo_internal_ram_miss
    605       [1:
    606         %
    607       |2:
    608         cases (assoc_list_exists ?????) in assembly_mode_ok_refl; normalize nodelta
    609         #absurd try % @sym_eq assumption
    610       ]
    611     ]
    612   |2:
    613     #addressing_mode_ok_refl whd in ⊢ (??%?);
    614     @pair_elim #nu #nl #nu_nl_refl normalize nodelta cases daemon (*
    615     @pair_elim #ignore #three_bits #ignore_three_bits_refl normalize nodelta
    616     inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta
    617     [1:
    618       whd in ⊢ (??%%); normalize nodelta
    619       cases (eqb ??) normalize nodelta [1: % ]
    620       cases (eqb ??) normalize nodelta [1: % ]
    621       cases (eqb ??) normalize nodelta [1: % ]
    622       cases (eqb ??) normalize nodelta [1: % ]
    623       cases (eqb ??) normalize nodelta [1:
    624         @get_8051_sfr_status_of_pseudo_status
    625         #absurd destruct(absurd)
    626       ]
    627       cases (eqb ??) normalize nodelta [1:
    628         @get_8051_sfr_status_of_pseudo_status
    629         #absurd destruct(absurd)
    630       ]
    631       cases (eqb ??) normalize nodelta [1:
    632         @get_8051_sfr_status_of_pseudo_status
    633         #absurd destruct(absurd)
    634       ]
    635       cases (eqb ??) normalize nodelta [1:
    636         @get_8051_sfr_status_of_pseudo_status
    637         #absurd destruct(absurd)
    638       ]
    639       cases (eqb ??) normalize nodelta [1:
    640         @get_8051_sfr_status_of_pseudo_status
    641         #absurd destruct(absurd)
    642       ]
    643       cases (eqb ??) normalize nodelta [1: % ]
    644       cases (eqb ??) normalize nodelta [1: % ]
    645       cases (eqb ??) normalize nodelta [1: % ]
    646       cases (eqb ??) normalize nodelta [1: % ]
    647       cases (eqb ??) normalize nodelta [1: % ]
    648       cases (eqb ??) normalize nodelta [1:
    649         @get_8051_sfr_status_of_pseudo_status
    650         #absurd destruct(absurd)
    651       ]
    652       cases (eqb ??) normalize nodelta [1:
    653         @get_8051_sfr_status_of_pseudo_status
    654         #absurd destruct(absurd)
    655       ]
    656       cases (eqb ??) normalize nodelta [1:
    657         @get_8051_sfr_status_of_pseudo_status
    658         #absurd destruct(absurd)
    659       ]
    660       cases (eqb ??) normalize nodelta [1:
    661         @get_8051_sfr_status_of_pseudo_status
    662         #absurd destruct(absurd)
    663       ]
    664       cases (eqb ??) normalize nodelta [1:
    665         @get_8051_sfr_status_of_pseudo_status
    666         #absurd destruct(absurd)
    667       ]
    668       cases (eqb ??) normalize nodelta [1:
    669         @get_8051_sfr_status_of_pseudo_status
    670         #absurd destruct(absurd)
    671       ]
    672       cases (eqb ??) normalize nodelta [1:
    673         @get_8051_sfr_status_of_pseudo_status
    674         #absurd destruct(absurd)
    675       ]
    676       cases (eqb ??) normalize nodelta [1:
    677         @get_8051_sfr_status_of_pseudo_status
    678         #absurd destruct(absurd)
    679       ]
    680       cases (eqb ??) normalize nodelta [1:
    681         @get_8051_sfr_status_of_pseudo_status
    682         #absurd destruct(absurd)
    683       ]
    684       cases (eqb ??) normalize nodelta [1:
    685         @get_8051_sfr_status_of_pseudo_status
    686         #absurd destruct(absurd)
    687       ]
    688       inversion (eqb ??) #eqb_refl normalize nodelta [1:
    689         @get_8051_sfr_status_of_pseudo_status lapply addressing_mode_ok_refl
    690         whd in ⊢ (??%? → ?); <(eqb_true_to_eq … eqb_refl)
    691         >bitvector_of_nat_inverse_nat_of_bitvector >eq_bv_refl normalize nodelta
    692         #assoc_list_assm cases (conjunction_true … assoc_list_assm) #_
    693         #relevant #_ cases (eq_accumulator_address_map_entry_true_to_eq … relevant) %
    694       ]
    695       cases (eqb ??) normalize nodelta [1:
    696         @get_8051_sfr_status_of_pseudo_status
    697         #absurd destruct(absurd)
    698       ] %
    699     |2:
    700       lapply addressing_mode_ok_refl whd in ⊢ (??%? → ?); #relevant
    701       whd in match status_of_pseudo_status; normalize nodelta
    702       >low_internal_ram_of_pseudo_internal_ram_miss try %
    703       cut(arg = false:::(three_bits@@nl))
    704       [1:
    705         <get_index_v_refl
    706         cut(nu=get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3)):::three_bits)
    707         [1:
    708           cut(ignore = [[get_index_v bool 4 nu 0 ?]])
    709           [1:
    710             @le_S_S @le_O_n
    711           |2:
    712             cut(ignore = \fst (vsplit bool 1 3 nu))
    713             [1:
    714               >ignore_three_bits_refl %
    715             |2:
    716               #ignore_refl >ignore_refl
    717               cases (bitvector_cases_hd_tl … nu) #hd * #tl #nu_refl
    718               >nu_refl %
    719             ]
    720           |3:
    721             #ignore_refl >ignore_refl in ignore_three_bits_refl;
    722             #relevant lapply (vsplit_ok ?????? (sym_eq … relevant))
    723             #nu_refl <nu_refl %
    724           ]
    725         |2:
    726           #nu_refl change with (? = (?:::three_bits)@@?) <nu_refl
    727           @sym_eq @vsplit_ok >nu_nl_refl %
    728         ]
    729       |2:
    730         #arg_refl <arg_refl cases (assoc_list_exists ?????) in relevant;
    731         normalize nodelta
    732         [1:
    733           cases (eq_bv ???) normalize #absurd destruct(absurd)
    734         |2:
    735           #_ %
    736         ]
    737       ]
    738     ]
    739   ] *)
    740551qed.
    741552
    … …  
    811622  #M #cm #ps #sigma #policy #sfr #result #sfr_neq_assm
    812623  whd in match (set_8051_sfr ?????);
    813   cases M #callM * try % #upper_lower #address
     624  cases M * #low #high * try % * *
    814625  whd in match (special_function_registers_8051 ???);
    815   whd in match (sfr_8051_of_pseudo_sfr_8051 ???);
     626  whd in match (sfr_8051_of_pseudo_sfr_8051 ???); normalize nodelta
    816627  @pair_elim #high #low #high_low_refl normalize nodelta
    817628  cases (eq_upper_lower ??) normalize nodelta

  • src/ASM/Test.ma

    r2258 r2272  
    9696  λM, sigma, v.
    9797  match \snd M with
    98   [ data ⇒ v
    99   | address upper_lower word ⇒
    100     let mapped ≝ sigma word in
    101     let 〈high, low〉 ≝ vsplit bool 8 8 mapped in
     98  [ None ⇒ v
     99  | Some upper_lower_addr ⇒
     100    let 〈upper_lower, addr〉 ≝ upper_lower_addr in
    102101      if eq_upper_lower upper_lower upper then
    103         high
     102        let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (v@@addr)) in
     103          high
    104104      else
    105         low
     105        let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (addr@@v)) in
     106          low
    106107  ].
    107108
    … …  
    113114  λaddress: Byte.
    114115  λvalue: Byte.
    115   match assoc_list_lookup ?? address (eq_bv …) (\fst M) with
     116  match lookup_from_internal_ram … address M with
    116117  [ None ⇒ value
    117118  | Some upper_lower_word ⇒
    118119    let 〈upper_lower, word〉 ≝ upper_lower_word in
    119     let 〈high, low〉 ≝ vsplit bool 8 8 (sigma word) in
    120120      if eq_upper_lower upper_lower upper then
    121         high
     121        let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (value@@word)) in
     122          high
    122123      else
    123         low
     124        let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (word@@value)) in
     125          low
    124126  ].
    125127
    … …  
    216218qed.
    217219
     220lemma get_index_v_set_index_hit:
     221  ∀A: Type[0].
     222  ∀n: nat.
     223  ∀v: Vector A n.
     224  ∀i: nat.
     225  ∀e: A.
     226  ∀i_lt_n_proof: i < n.
     227  ∀i_lt_n_proof': i < n.
     228    get_index_v A n (set_index A n v i e i_lt_n_proof) i i_lt_n_proof' = e.
     229  #A #n #v elim v
     230  [1:
     231    #i #e #i_lt_n_proof
     232    cases (lt_to_not_zero … i_lt_n_proof)
     233  |2:
     234    #n' #hd #tl #inductive_hypothesis #i #e
     235    cases i
     236    [1:
     237      #i_lt_n_proof #i_lt_n_proof' %
     238    |2:
     239      #i' #i_lt_n_proof' #i_lt_n_proof''
     240      whd in ⊢ (??%?); @inductive_hypothesis
     241    ]
     242  ]
     243qed.
     244
    218245lemma set_index_status_of_pseudo_status:
    219246  ∀M, code_memory, sigma, policy, s, sfr, v, v'.
    … …  
    230257  whd in match status_of_pseudo_status; normalize nodelta
    231258  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
    232   inversion (\snd M) try (#upper_lower #address) #sndM_refl normalize nodelta
     259  inversion (\snd M) try ( * #upper_lower #address) #sndM_refl normalize nodelta
    233260  [1:
    234261    <sfr_neq_acc_a_assm cases sfr
    … …  
    240267    %
    241268  |2:
     269    inversion (eq_upper_lower upper_lower upper) #eq_upper_lower_refl normalize nodelta
    242270    @pair_elim #high #low #high_low_refl normalize nodelta
    243     inversion (eq_upper_lower upper_lower upper) #eq_upper_lower_refl normalize nodelta
    244     <sfr_neq_acc_a_assm cases sfr
     271    whd in match set_8051_sfr; normalize nodelta
     272    <sfr_neq_acc_a_assm
     273    cases sfr in high_low_refl sfr_neq_acc_a_assm;
    245274    [18,37:
     275      @pair_elim #high' #low' #high_low_refl'
     276      #high_low_refl
    246277      whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
    247278      whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
    248       >sndM_refl normalize nodelta >high_low_refl normalize nodelta
     279      >sndM_refl normalize nodelta
    249280      >eq_upper_lower_refl normalize nodelta
    250       whd in match (set_8051_sfr ?????);
    251281      [1:
     282        #relevant >relevant
    252283        <set_index_set_index_overwrite in ⊢ (??%?);
    253         <set_index_set_index_overwrite in ⊢ (???%); %
     284        <set_index_set_index_overwrite in ⊢ (???%);
     285        >get_index_v_set_index_hit in high_low_refl';
     286        #assm >assm in relevant; normalize nodelta * %
    254287      |2:
     288        #relevant >relevant
    255289        <set_index_set_index_overwrite in ⊢ (??%?);
    256         <set_index_set_index_overwrite in ⊢ (???%); %
     290        <set_index_set_index_overwrite in ⊢ (???%);
     291        >get_index_v_set_index_hit in high_low_refl';
     292        #assm >assm in relevant; normalize nodelta * %
    257293      ]
    258294    ]
    259295    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
    260     whd in match (set_8051_sfr ?????); @set_index_set_index_commutation normalize
    261     @nmk #absurd destruct(absurd)
     296    #relevant * >get_index_v_set_index_miss
     297    try (% #absurd normalize in absurd; destruct(absurd))
     298    >relevant normalize nodelta
     299    @set_index_set_index_commutation % #absurd normalize in absurd; destruct(absurd)
    262300  ]
    263301qed.
    264302
     303(*
    265304lemma get_index_v_status_of_pseudo_status:
    266305  ∀M, code_memory, sigma, policy, s, s', sfr.
    … …  
    301340  ]
    302341qed.
     342*)
    303343
    304344lemma set_8051_sfr_status_of_pseudo_status:
    … …  
    313353qed.
    314354
     355(*
    315356lemma get_8051_sfr_status_of_pseudo_status:
    316357  ∀M, code_memory, sigma, policy, s, s', s'', sfr.
    … …  
    324365  whd in match get_8051_sfr; normalize nodelta
    325366  @get_index_v_status_of_pseudo_status %
    326 qed.
     367qed.*)
    327368
    328369lemma get_8052_sfr_status_of_pseudo_status:
    … …  
    424465  (code_memory_of_pseudo_assembly_program cm sigma policy)
    425466  s'
    426   (low_internal_ram_of_pseudo_low_internal_ram M ram)
     467  (low_internal_ram_of_pseudo_low_internal_ram M sigma ram)
    427468  = status_of_pseudo_status M cm
    428469    (set_low_internal_ram pseudo_assembly_program cm s ram) sigma policy.
    … …  
    435476 map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v = v' →
    436477  insert Byte 7 addr v'
    437   (low_internal_ram_of_pseudo_low_internal_ram M
     478  (low_internal_ram_of_pseudo_low_internal_ram M sigma
    438479   (low_internal_ram pseudo_assembly_program cm s))
    439   =low_internal_ram_of_pseudo_low_internal_ram M
     480  =low_internal_ram_of_pseudo_low_internal_ram M sigma
    440481   (insert Byte 7 addr v (low_internal_ram pseudo_assembly_program cm s)).
    441482               
    … …  
    447488    (code_memory_of_pseudo_assembly_program cm sigma policy)
    448489    (status_of_pseudo_status M cm s sigma policy))
    449   = low_internal_ram_of_pseudo_low_internal_ram M
     490  = low_internal_ram_of_pseudo_low_internal_ram M sigma
    450491     (insert Byte 7 addr v
    451492      (low_internal_ram pseudo_assembly_program cm s)).
    … …  
    458499 map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr) v = v' →
    459500  insert Byte 7 addr v'
    460   (high_internal_ram_of_pseudo_high_internal_ram M
     501  (high_internal_ram_of_pseudo_high_internal_ram M sigma
    461502   (high_internal_ram pseudo_assembly_program cm s))
    462   =high_internal_ram_of_pseudo_high_internal_ram M
     503  =high_internal_ram_of_pseudo_high_internal_ram M sigma
    463504   (insert Byte 7 addr v (high_internal_ram pseudo_assembly_program cm s)).
    464505
    … …  
    470511    (code_memory_of_pseudo_assembly_program cm sigma policy)
    471512    (status_of_pseudo_status M cm s sigma policy))
    472   = high_internal_ram_of_pseudo_high_internal_ram M
     513  = high_internal_ram_of_pseudo_high_internal_ram M sigma
    473514     (insert Byte 7 addr v
    474515      (high_internal_ram pseudo_assembly_program cm s)).
    … …  
    13741415  >get_index_v_set_index_miss [2,4: /2/] %
    13751416qed.
     1417
     1418lemma get_8051_sfr_status_of_pseudo_status:
     1419  ∀M.
     1420  ∀cm, ps, sigma, policy.
     1421  ∀sfr.
     1422    (sfr = SFR_ACC_A → \snd M = None …) →
     1423    get_8051_sfr (BitVectorTrie Byte 16)
     1424      (code_memory_of_pseudo_assembly_program cm sigma policy)
     1425      (status_of_pseudo_status M cm ps sigma policy) sfr =
     1426    get_8051_sfr pseudo_assembly_program cm ps sfr.
     1427  #M #cm #ps #sigma #policy * cases M #fstM #sndM #relevant
     1428  [18:
     1429     >relevant %
     1430  ]
     1431  cases sndM try % * #address
     1432  whd in match get_8051_sfr;
     1433  whd in match status_of_pseudo_status; normalize nodelta
     1434  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta #address
     1435  cases (eq_upper_lower ??) normalize nodelta
     1436  @pair_elim #upper #lower #upper_lower_refl
     1437  @get_index_v_set_index_miss @nmk #relevant
     1438  normalize in relevant; destruct(relevant)
     1439qed.
     1440
     1441lemma get_arg_8_pseudo_addressing_mode_ok:
     1442  ∀M: internal_pseudo_address_map.
     1443  ∀cm: pseudo_assembly_program.
     1444  ∀ps: PreStatus pseudo_assembly_program cm.
     1445  ∀sigma: Word → Word.
     1446  ∀policy: Word → bool.
     1447  ∀addr1: [[registr; direct]].
     1448    assert_data pseudo_assembly_program M cm ps addr1 = true →
     1449      get_arg_8 (BitVectorTrie Byte 16)
     1450        (code_memory_of_pseudo_assembly_program cm sigma policy)
     1451        (status_of_pseudo_status M cm ps sigma policy) true addr1 =
     1452      get_arg_8 pseudo_assembly_program cm ps true addr1.
     1453  [2,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1454  #M #cm #ps #sigma #policy #addr1
     1455  @(subaddressing_mode_elim … addr1) #arg whd in ⊢ (? → ???%);
     1456  [1:
     1457    whd in ⊢ (??%? → ??%?);
     1458    whd in match bit_address_of_register; normalize nodelta
     1459    @pair_elim #un #ln #un_ln_refl
     1460    lapply (refl_to_jmrefl ??? un_ln_refl) -un_ln_refl #un_ln_refl
     1461    @(pair_replace ?????????? un_ln_refl)
     1462    [1:
     1463      whd in match get_8051_sfr; normalize nodelta
     1464      whd in match sfr_8051_index; normalize nodelta
     1465      @eq_f <get_index_v_special_function_registers_8051_not_acc_a
     1466      try % #absurd destruct(absurd)
     1467    |2:
     1468      #assembly_mode_ok_refl
     1469      >low_internal_ram_of_pseudo_internal_ram_miss
     1470      [1:
     1471        %
     1472      |2:
     1473        cases (data_or_address ?????) in assembly_mode_ok_refl; normalize nodelta
     1474        [1:
     1475          #absurd destruct(absurd)
     1476        |2:
     1477          * normalize nodelta
     1478          [1:
     1479          |2:
     1480            #_ #absurd destruct(absurd)
     1481          ]
     1482        #absurd try % @sym_eq assumption
     1483      ]
     1484    ]
     1485  |2:
     1486    #addressing_mode_ok_refl whd in ⊢ (??%?);
     1487    @pair_elim #nu #nl #nu_nl_refl normalize nodelta cases daemon (*
     1488    @pair_elim #ignore #three_bits #ignore_three_bits_refl normalize nodelta
     1489    inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta
     1490    [1:
     1491      whd in ⊢ (??%%); normalize nodelta
     1492      cases (eqb ??) normalize nodelta [1: % ]
     1493      cases (eqb ??) normalize nodelta [1: % ]
     1494      cases (eqb ??) normalize nodelta [1: % ]
     1495      cases (eqb ??) normalize nodelta [1: % ]
     1496      cases (eqb ??) normalize nodelta [1:
     1497        @get_8051_sfr_status_of_pseudo_status
     1498        #absurd destruct(absurd)
     1499      ]
     1500      cases (eqb ??) normalize nodelta [1:
     1501        @get_8051_sfr_status_of_pseudo_status
     1502        #absurd destruct(absurd)
     1503      ]
     1504      cases (eqb ??) normalize nodelta [1:
     1505        @get_8051_sfr_status_of_pseudo_status
     1506        #absurd destruct(absurd)
     1507      ]
     1508      cases (eqb ??) normalize nodelta [1:
     1509        @get_8051_sfr_status_of_pseudo_status
     1510        #absurd destruct(absurd)
     1511      ]
     1512      cases (eqb ??) normalize nodelta [1:
     1513        @get_8051_sfr_status_of_pseudo_status
     1514        #absurd destruct(absurd)
     1515      ]
     1516      cases (eqb ??) normalize nodelta [1: % ]
     1517      cases (eqb ??) normalize nodelta [1: % ]
     1518      cases (eqb ??) normalize nodelta [1: % ]
     1519      cases (eqb ??) normalize nodelta [1: % ]
     1520      cases (eqb ??) normalize nodelta [1: % ]
     1521      cases (eqb ??) normalize nodelta [1:
     1522        @get_8051_sfr_status_of_pseudo_status
     1523        #absurd destruct(absurd)
     1524      ]
     1525      cases (eqb ??) normalize nodelta [1:
     1526        @get_8051_sfr_status_of_pseudo_status
     1527        #absurd destruct(absurd)
     1528      ]
     1529      cases (eqb ??) normalize nodelta [1:
     1530        @get_8051_sfr_status_of_pseudo_status
     1531        #absurd destruct(absurd)
     1532      ]
     1533      cases (eqb ??) normalize nodelta [1:
     1534        @get_8051_sfr_status_of_pseudo_status
     1535        #absurd destruct(absurd)
     1536      ]
     1537      cases (eqb ??) normalize nodelta [1:
     1538        @get_8051_sfr_status_of_pseudo_status
     1539        #absurd destruct(absurd)
     1540      ]
     1541      cases (eqb ??) normalize nodelta [1:
     1542        @get_8051_sfr_status_of_pseudo_status
     1543        #absurd destruct(absurd)
     1544      ]
     1545      cases (eqb ??) normalize nodelta [1:
     1546        @get_8051_sfr_status_of_pseudo_status
     1547        #absurd destruct(absurd)
     1548      ]
     1549      cases (eqb ??) normalize nodelta [1:
     1550        @get_8051_sfr_status_of_pseudo_status
     1551        #absurd destruct(absurd)
     1552      ]
     1553      cases (eqb ??) normalize nodelta [1:
     1554        @get_8051_sfr_status_of_pseudo_status
     1555        #absurd destruct(absurd)
     1556      ]
     1557      cases (eqb ??) normalize nodelta [1:
     1558        @get_8051_sfr_status_of_pseudo_status
     1559        #absurd destruct(absurd)
     1560      ]
     1561      inversion (eqb ??) #eqb_refl normalize nodelta [1:
     1562        @get_8051_sfr_status_of_pseudo_status lapply addressing_mode_ok_refl
     1563        whd in ⊢ (??%? → ?); <(eqb_true_to_eq … eqb_refl)
     1564        >bitvector_of_nat_inverse_nat_of_bitvector >eq_bv_refl normalize nodelta
     1565        #assoc_list_assm cases (conjunction_true … assoc_list_assm) #_
     1566        #relevant #_ cases (eq_accumulator_address_map_entry_true_to_eq … relevant) %
     1567      ]
     1568      cases (eqb ??) normalize nodelta [1:
     1569        @get_8051_sfr_status_of_pseudo_status
     1570        #absurd destruct(absurd)
     1571      ] %
     1572    |2:
     1573      lapply addressing_mode_ok_refl whd in ⊢ (??%? → ?); #relevant
     1574      whd in match status_of_pseudo_status; normalize nodelta
     1575      >low_internal_ram_of_pseudo_internal_ram_miss try %
     1576      cut(arg = false:::(three_bits@@nl))
     1577      [1:
     1578        <get_index_v_refl
     1579        cut(nu=get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3)):::three_bits)
     1580        [1:
     1581          cut(ignore = [[get_index_v bool 4 nu 0 ?]])
     1582          [1:
     1583            @le_S_S @le_O_n
     1584          |2:
     1585            cut(ignore = \fst (vsplit bool 1 3 nu))
     1586            [1:
     1587              >ignore_three_bits_refl %
     1588            |2:
     1589              #ignore_refl >ignore_refl
     1590              cases (bitvector_cases_hd_tl … nu) #hd * #tl #nu_refl
     1591              >nu_refl %
     1592            ]
     1593          |3:
     1594            #ignore_refl >ignore_refl in ignore_three_bits_refl;
     1595            #relevant lapply (vsplit_ok ?????? (sym_eq … relevant))
     1596            #nu_refl <nu_refl %
     1597          ]
     1598        |2:
     1599          #nu_refl change with (? = (?:::three_bits)@@?) <nu_refl
     1600          @sym_eq @vsplit_ok >nu_nl_refl %
     1601        ]
     1602      |2:
     1603        #arg_refl <arg_refl cases (assoc_list_exists ?????) in relevant;
     1604        normalize nodelta
     1605        [1:
     1606          cases (eq_bv ???) normalize #absurd destruct(absurd)
     1607        |2:
     1608          #_ %
     1609        ]
     1610      ]
     1611    ]
     1612  ] *)
     1613qed.
Note: See TracChangeset for help on using the changeset viewer.