Ignore:
Timestamp:
Jul 30, 2012, 2:36:41 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2272 r2276  
    463463          bvt_map2 … bvt_1 bvt_2 f = bvt_map2 … bvt_1 bvt_2' f.
    464464
     465definition lookup_from_internal_ram:
     466    ∀addr: Byte.
     467    ∀M: internal_pseudo_address_map.
     468      option address_entry ≝
     469  λaddr, M.
     470    let 〈low, high, accA〉 ≝ M in
     471    let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 addr in
     472      if head' … bit_one then
     473        lookup_opt … seven_bits high
     474      else
     475        lookup_opt … seven_bits low.
     476
     477definition map_value_using_opt_address_entry:
     478  (Word → Word) → Byte → option address_entry → Byte ≝
     479  λsigma: Word → Word.
     480  λvalue: Byte.
     481  λul_addr: option address_entry.
     482  match ul_addr with
     483  [ None ⇒ value
     484  | Some upper_lower_word ⇒
     485    let 〈upper_lower, word〉 ≝ upper_lower_word in
     486      if eq_upper_lower upper_lower upper then
     487        let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (value@@word)) in
     488          high
     489      else
     490        let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (word@@value)) in
     491          low
     492  ].
     493
     494definition map_acc_a_using_internal_pseudo_address_map:
     495 ∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte ≝
     496   λM, sigma, v. map_value_using_opt_address_entry sigma v (\snd M).
     497
     498definition map_internal_ram_address_using_pseudo_address_map:
     499  ∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte → Byte ≝
     500  λM: internal_pseudo_address_map.
     501  λsigma: Word → Word.
     502  λaddress: Byte.
     503  λvalue: Byte.
     504   map_value_using_opt_address_entry sigma value
     505    (lookup_from_internal_ram … address M ).
     506
     507definition map_opt_value_using_opt_address_entry:
     508 (Word → Word) → option Byte → option address_entry → option Byte ≝
     509 λsigma,v,ul_addr.
     510  let v ≝ match v with [ None ⇒ zero … | Some v ⇒ v ] in
     511  let v' ≝ map_value_using_opt_address_entry sigma v ul_addr in
     512    if eq_bv … v' (zero …) then
     513      None …
     514    else
     515      Some … v'.
     516
    465517definition internal_ram_of_pseudo_internal_ram:
    466518    ∀sigma: Word → Word.
     
    469521      BitVectorTrie Byte 7 ≝
    470522  λ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         ]).
     523      bvt_map2 ??? ? ram map (map_opt_value_using_opt_address_entry sigma).
     524
     525axiom insert_internal_ram_of_pseudo_internal_ram:
     526 ∀M,M',sigma,addr,v,v',ram.
     527  v' = map_value_using_opt_address_entry sigma v (lookup_opt … addr M) →
     528  (∀addr'. addr' ≠ addr → lookup_opt … addr' M = lookup_opt … addr' M') →
     529  insert Byte … addr v' (internal_ram_of_pseudo_internal_ram sigma ram M)
     530  = internal_ram_of_pseudo_internal_ram sigma (insert ?? addr v ram) M'.
    494531
    495532definition low_internal_ram_of_pseudo_low_internal_ram:
     
    677714      | Some v' ⇒ insert_into_internal_ram addr v' M
    678715      ].
    679 
    680 definition 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.
    691716   
    692717definition next_internal_pseudo_address_map0 ≝
Note: See TracChangeset for help on using the changeset viewer.