Ignore:
Timestamp:
Jul 30, 2012, 11:44:50 PM (8 years ago)
Author:
sacerdot
Message:
  1. Bug fixed in the semantics of PUSH (no indirection performed)
  2. Proved write_at_stack_pointer_status_of_pseudo_status
  3. PUSH case of main lemma almost done
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2276 r2279  
    523523      bvt_map2 ??? ? ram map (map_opt_value_using_opt_address_entry sigma).
    524524
     525definition internal_half_pseudo_address_map_equal_up_to_address:
     526 BitVectorTrie address_entry 7 → BitVectorTrie address_entry 7 → (Word → Word) →
     527  BitVector 7 → Byte → Byte → Prop
     528 ≝
     529 λM,M',sigma,addr,v,v'.
     530  v' = map_value_using_opt_address_entry sigma v (lookup_opt … addr M') ∧
     531   ∀addr'. addr' ≠ addr → lookup_opt … addr' M = lookup_opt … addr' M'. 
     532
    525533axiom insert_internal_ram_of_pseudo_internal_ram:
    526534 ∀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') →
     535  internal_half_pseudo_address_map_equal_up_to_address M M' sigma addr v v' →
    529536  insert Byte … addr v' (internal_ram_of_pseudo_internal_ram sigma ram M)
    530537  = internal_ram_of_pseudo_internal_ram sigma (insert ?? addr v ram) M'.
     
    681688    let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 addr in
    682689      if head' … bit_one then
    683         〈insert … seven_bits v low, high, accA〉
     690        〈low, insert … seven_bits v high, accA〉
    684691      else
    685         〈low, insert … seven_bits v high, accA〉.
     692        〈insert … seven_bits v low, high, accA〉.
    686693   
    687694axiom delete:
     
    699706    let 〈bit_one, seven_bits〉 ≝ vsplit bool 1 7 addr in
    700707      if head' … bit_one then
    701         〈delete … seven_bits low, high, accA〉
     708        〈low,delete … seven_bits high, accA〉
    702709      else
    703         〈low, delete … seven_bits high, accA〉.
     710        〈delete … seven_bits low, high, accA〉.
    704711
    705712definition overwrite_or_delete_from_internal_ram:
     
    709716      internal_pseudo_address_map ≝
    710717  λaddr, v, M.
    711     let 〈low, high, accA〉 ≝ M in
    712       match v with
    713       [ None ⇒ delete_from_internal_ram addr M
    714       | Some v' ⇒ insert_into_internal_ram addr v' M
    715       ].
     718    match v with
     719    [ None ⇒ delete_from_internal_ram addr M
     720    | Some v' ⇒ insert_into_internal_ram addr v' M
     721    ].
    716722   
    717723definition next_internal_pseudo_address_map0 ≝
Note: See TracChangeset for help on using the changeset viewer.