Changeset 2279


Ignore:
Timestamp:
Jul 30, 2012, 11:44:50 PM (7 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
Location:
src/ASM
Files:
4 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 ≝
  • src/ASM/AssemblyProofSplit.ma

    r2278 r2279  
    1818include alias "ASM/Vector.ma".
    1919include "ASM/Test.ma".
     20include "ASM/Test2.ma".
    2021
    2122(*CSC: move elsewhere*)
     
    365366              set_8051_sfr … s SFR_ACC_A new_acc
    366367        | PUSH addr ⇒ λinstr_refl.
    367             match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → x = addr → ? with
    368               [ DIRECT d ⇒ λdirect: True. λEQaddr.
    369                 let s ≝ add_ticks1 s in
    370                 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    371                 let s ≝ set_8051_sfr … s SFR_SP new_sp in
    372                   write_at_stack_pointer … s d
    373               | _ ⇒ λother: False. ⊥
    374               ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
     368            let s ≝ add_ticks1 s in
     369            let new_sp ≝ add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
     370            let s ≝ set_8051_sfr … s SFR_SP new_sp in
     371             write_at_stack_pointer … s (get_arg_8 … s false addr)
    375372        | POP addr ⇒ λinstr_refl.
    376373            let s ≝ add_ticks1 s in
     
    19411938    |*:
    19421939      >EQs >EQticks <instr_refl
    1943       cases daemon (* XXX: write_at_stack_pointer_status_of_pseudo_status *)
     1940      @(write_at_stack_pointer_status_of_pseudo_status 〈low,high,accA〉)
     1941      [2,4,6,8: @set_8051_sfr_status_of_pseudo_status try %
     1942      | >get_8051_sfr_set_8051_sfr
     1943        cut (new_sp = (add … (get_8051_sfr … ps SFR_SP) (bitvector_of_nat … 1)))
     1944        [ >(pair_destruct_2 ????? (sym_eq … carry_new_sp_refl))
     1945          change with (add ??? = ?); @eq_f2 try %
     1946          cases daemon (*CSC: use @get_8051_sfr_status_of_pseudo_status*) ] #EQnew_sp
     1947        >EQnew_sp
     1948        @internal_pseudo_address_map_equal_up_to_address_overwrite_or_delete_from_internal_ram
     1949       
     1950     
     1951         XXX
     1952        (*CSC: lemma here*)
     1953        cases accA
     1954        whd in match overwrite_or_delete_from_internal_ram; normalize nodelta
     1955        [ whd whd in match delete_from_internal_ram; normalize nodelta
     1956          @pair_elim #bit_one
     1957        |
     1958        ]
     1959      |
     1960      |
     1961      ]
    19441962    ]
    19451963  |43: (* POP *)
  • src/ASM/Interpret.ma

    r2272 r2279  
    298298              set_8051_sfr … s SFR_ACC_A new_acc
    299299        | PUSH addr ⇒ λinstr_refl.
    300             match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → ? with
    301               [ DIRECT d ⇒ λdirect: True.
    302                 let s ≝ add_ticks1 s in
    303                 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    304                 let s ≝ set_8051_sfr … s SFR_SP new_sp in
    305                   write_at_stack_pointer … s d
    306               | _ ⇒ λother: False. ⊥
    307               ] (subaddressing_modein … addr)
     300            let s ≝ add_ticks1 s in
     301            let new_sp ≝ add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
     302            let s ≝ set_8051_sfr … s SFR_SP new_sp in
     303             write_at_stack_pointer … s (get_arg_8 … s false addr)
    308304        | POP addr ⇒ λinstr_refl.
    309305            let s ≝ add_ticks1 s in
  • src/ASM/Test.ma

    r2276 r2279  
    19451945*)
    19461946
    1947 (*
     1947definition internal_pseudo_address_map_equal_up_to_low ≝
     1948 λM,M': internal_pseudo_address_map. \snd M = \snd M' ∧ \snd (\fst M) = \snd (\fst M').
     1949
     1950lemma set_low_internal_ram_status_of_pseudo_status:
     1951 ∀cm,sigma,policy,M,M',s,s',ram,ram'.
     1952  internal_pseudo_address_map_equal_up_to_low M M' →
     1953  s' = status_of_pseudo_status M' cm s sigma policy →
     1954  ram'=internal_ram_of_pseudo_internal_ram sigma ram (\fst (\fst M)) →
     1955  set_low_internal_ram (BitVectorTrie Byte 16)
     1956  (code_memory_of_pseudo_assembly_program cm sigma policy)
     1957  s'
     1958  ram'
     1959  = status_of_pseudo_status M cm
     1960    (set_low_internal_ram pseudo_assembly_program cm s ram) sigma policy.
     1961  #cm #sigma #policy #M #M' #s #s' #ram #ram' #M_refl #s_refl >s_refl #ram_refl >ram_refl
     1962  cases M' in M_refl; * #low' #high' #accA' cases M * #low #high #accA #H cases H
     1963  #accA_refl #high_refl destruct whd in ⊢ (??%%); @split_eq_status %
     1964qed.
     1965
     1966definition internal_pseudo_address_map_equal_up_to_high ≝
     1967 λM,M': internal_pseudo_address_map. \snd M = \snd M' ∧ \fst (\fst M) = \fst (\fst M').
     1968
     1969lemma set_high_internal_ram_status_of_pseudo_status:
     1970 ∀cm,sigma,policy,M,M',s,s',ram,ram'.
     1971  internal_pseudo_address_map_equal_up_to_high M M' →
     1972  s' = status_of_pseudo_status M' cm s sigma policy →
     1973  ram'=internal_ram_of_pseudo_internal_ram sigma ram (\snd (\fst M)) →
     1974  set_high_internal_ram (BitVectorTrie Byte 16)
     1975  (code_memory_of_pseudo_assembly_program cm sigma policy)
     1976  s'
     1977  ram'
     1978  = status_of_pseudo_status M cm
     1979    (set_high_internal_ram pseudo_assembly_program cm s ram) sigma policy.
     1980  #cm #sigma #policy #M #M' #s #s' #ram #ram' #M_refl #s_refl >s_refl #ram_refl >ram_refl
     1981  cases M' in M_refl; * #low' #high' #accA' cases M * #low #high #accA #H cases H
     1982  #accA_refl #high_refl destruct whd in ⊢ (??%%); @split_eq_status %
     1983qed.
     1984
     1985definition internal_pseudo_address_map_equal_up_to_address ≝
     1986 λM,M',sigma,addr,v,v'.
     1987  let 〈low,high,accA〉 ≝ M in
     1988  let 〈low',high',accA'〉 ≝ M' in
     1989  let 〈bit_one,seven_bits〉 ≝ vsplit bool 1 7 addr in
     1990   if head' … 0 bit_one then
     1991    (internal_pseudo_address_map_equal_up_to_high M' M ∧
     1992     internal_half_pseudo_address_map_equal_up_to_address high high' sigma
     1993      seven_bits v v')
     1994   else
     1995    (internal_pseudo_address_map_equal_up_to_low M' M ∧
     1996      internal_half_pseudo_address_map_equal_up_to_address low low' sigma
     1997       seven_bits v v').
     1998 
    19481999lemma write_at_stack_pointer_status_of_pseudo_status:
    19492000  ∀M, M'.
     
    19522003  ∀policy.
    19532004  ∀s, s'.
    1954   ∀new_b, new_b'.
    1955     map_internal_ram_address_using_pseudo_address_map M sigma (get_8051_sfr pseudo_assembly_program cm s SFR_SP) new_b = new_b' →
    1956     status_of_pseudo_status M cm s sigma policy = s' →
    1957     write_at_stack_pointer ?? s' new_b' =
    1958     status_of_pseudo_status M' cm (write_at_stack_pointer ? cm s new_b) sigma policy.
    1959   #M #M' #cm #sigma #policy #s #s' #new_b #new_b'
    1960   #new_b_refl #s_refl <new_b_refl <s_refl
     2005  ∀v, v'.
     2006    internal_pseudo_address_map_equal_up_to_address M M' sigma
     2007     (get_8051_sfr ?? s SFR_SP) v v' →
     2008    s' = status_of_pseudo_status M cm s sigma policy →
     2009    write_at_stack_pointer ?? s' v' =
     2010    status_of_pseudo_status M' cm (write_at_stack_pointer ? cm s v) sigma policy.
     2011  ** #low #high #accA ** #low' #high' #accA'
     2012  #cm #sigma #policy #s #s' #v #v' #H whd in H; #s_refl >s_refl
    19612013  whd in match write_at_stack_pointer; normalize nodelta
    1962   @pair_elim #nu #nl #nu_nl_refl normalize nodelta
    1963   @(pair_replace ?????????? (eq_to_jmeq … nu_nl_refl))
    1964   [1:
    1965     @eq_f
    1966     whd in match get_8051_sfr; normalize nodelta
    1967     whd in match sfr_8051_index; normalize nodelta
     2014  >(get_8051_sfr_status_of_pseudo_status … (refl …) … (refl …)) lapply H; -H
     2015  @vsplit_elim #bit_one #seven_bits cases (Vector_Sn … bit_one) #bitone * #tl
     2016  >(Vector_O … tl) #EQbit_one >EQbit_one -bit_one normalize nodelta cases bitone
     2017  #bit_one_seven_bits_refl normalize nodelta * #H1 #H2
     2018  [ @(set_high_internal_ram_status_of_pseudo_status … 〈low',high',accA'〉 〈low,high,accA〉)
     2019    try @refl try assumption
    19682020    whd in match status_of_pseudo_status; normalize nodelta
    1969     whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
    1970     cases (\snd M) [2: * #address ] normalize nodelta
    1971     [1,2:
    1972       cases (vsplit bool ???) #high #low normalize nodelta
    1973       whd in match sfr_8051_index; normalize nodelta
    1974       >get_index_v_set_index_miss %
    1975       #absurd destruct(absurd)
    1976     |3:
    1977       %
    1978     ]
    1979   |2:
    1980     @if_then_else_status_of_pseudo_status try %
    1981     [2:
    1982       @sym_eq <set_low_internal_ram_status_of_pseudo_status
    1983       [1:
    1984         @eq_f2
    1985         [2:
    1986           @insert_low_internal_ram_of_pseudo_low_internal_ram'
    1987     @sym_eq
    1988     [2:
    1989       <set_low_internal_ram_status_of_pseudo_status
    1990       [1:
    1991         @eq_f2
    1992         [2:
    1993           @sym_eq
    1994           >(insert_low_internal_ram_of_pseudo_low_internal_ram … sigma … new_b')
    1995           [2:
    1996             >new_b_refl
    1997     ]
     2021    whd in match high_internal_ram_of_pseudo_high_internal_ram; normalize nodelta
     2022    @insert_internal_ram_of_pseudo_internal_ram assumption
     2023  | @(set_low_internal_ram_status_of_pseudo_status … 〈low',high',accA'〉 〈low,high,accA〉)
     2024    try @refl try assumption
     2025    whd in match status_of_pseudo_status; normalize nodelta
     2026    whd in match low_internal_ram_of_pseudo_low_internal_ram; normalize nodelta
     2027    @insert_internal_ram_of_pseudo_internal_ram assumption
    19982028  ]
    1999 qed.*)
     2029qed.
     2030
     2031(*CSC: move elsewhere and generalize*)
     2032axiom lookup_opt_delete_miss:
     2033 ∀n.∀M:BitVectorTrie address_entry n.∀addr,addr': BitVector n.
     2034  addr' ≠ addr →
     2035     lookup_opt address_entry n addr' (delete address_entry n addr M)
     2036   = lookup_opt address_entry n addr' M.
     2037
     2038(*CSC: move elsewhere and generalize*)
     2039axiom lookup_opt_delete_hit:
     2040 ∀n.∀M:BitVectorTrie address_entry n.∀addr: BitVector n.
     2041  lookup_opt address_entry n addr (delete address_entry n addr M) = None ….
     2042
     2043lemma internal_pseudo_address_map_equal_up_to_address_delete_from_internal_ram:
     2044 ∀M,sigma,addr,v1,v2.
     2045  v2=v1 →
     2046  internal_pseudo_address_map_equal_up_to_address M
     2047   (delete_from_internal_ram addr M) sigma addr v1 v2.
     2048 ** #low #high #accA #sigma #addr #v1 #v2 * whd in match delete_from_internal_ram;
     2049 normalize nodelta @vsplit_elim #bit_one #seven_bits
     2050 cases (Vector_Sn … bit_one) ** #tl >(Vector_O … tl) #EQ >EQ #EQ2 normalize nodelta
     2051 >EQ2 whd whd in match (tail ???); % % try %
     2052 [2,4: #addr #addr' >lookup_opt_delete_miss try assumption %
     2053 |1,3: >lookup_opt_delete_hit % ]
     2054qed.
     2055
     2056lemma internal_pseudo_address_map_equal_up_to_address_insert_into_internal_ram:
     2057 ∀M,sigma,addr,entry,v1,v2.
     2058  v2=map_value_using_opt_address_entry sigma v1 (Some address_entry entry) →
     2059  internal_pseudo_address_map_equal_up_to_address M
     2060   (insert_into_internal_ram addr entry M) sigma addr v1 v2.
     2061 ** #low #high #accA #sigma #addr #entry #v1 #v2 #H whd in match insert_into_internal_ram;
     2062 normalize nodelta whd in match internal_pseudo_address_map_equal_up_to_address;
     2063 normalize nodelta @vsplit_elim #bit_one cases (Vector_Sn … bit_one) ** #tl
     2064 >(Vector_O … tl) #EQ >EQ #seven_bits #EQ2 normalize nodelta >EQ2 % % try %
     2065 [2,4: #addr' #NEQ >lookup_opt_insert_miss try % >eq_bv_false try % #EQ @(absurd … EQ NEQ)
     2066 |1,3: >lookup_opt_insert_hit assumption ]
     2067qed.
     2068
     2069lemma internal_pseudo_address_map_equal_up_to_address_overwrite_or_delete_from_internal_ram:
     2070 ∀M,sigma,addr,v1,v2,entry.
     2071  v2=map_value_using_opt_address_entry sigma v1 entry →
     2072  internal_pseudo_address_map_equal_up_to_address M
     2073  (overwrite_or_delete_from_internal_ram addr entry M) sigma addr v1 v2.
     2074 ** #low #high #accA #sigma #addr #v1 #v2 #entry
     2075 whd in match overwrite_or_delete_from_internal_ram; normalize nodelta
     2076 cases entry normalize nodelta
     2077 [ @internal_pseudo_address_map_equal_up_to_address_delete_from_internal_ram
     2078 | #addr_entry @internal_pseudo_address_map_equal_up_to_address_insert_into_internal_ram ]
     2079qed.
Note: See TracChangeset for help on using the changeset viewer.