Changeset 2279 for src/ASM/Test.ma


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/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.