Changeset 2119 for src/ASM/Fetch.ma


Ignore:
Timestamp:
Jun 27, 2012, 12:09:25 PM (7 years ago)
Author:
sacerdot
Message:

load_code_memory moved to Fetch.ma and proved correct w.r.t. next
(fetching) using Russell

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Fetch.ma

    r1961 r2119  
    1717  λpc: Word.
    1818    〈add … pc (bitvector_of_nat 16 1), lookup … pc pmem (zero …)〉.
     19
     20(*CSC: move elsewhere *)
     21axiom eq_bitvector_of_nat_to_eq:
     22 ∀n,n1,n2.
     23  n1 < 2^n → n2 < 2^n →
     24   bitvector_of_nat n n1 = bitvector_of_nat n n2 → n1=n2.
     25
     26discriminator Prod.
     27
     28definition load_code_memory0:
     29 ∀program: list Byte. Σres: BitVectorTrie Byte 16.
     30  let program_size ≝ |program| in
     31   program_size ≤ 2^16 →
     32    ∀pc. ∀pc_ok: pc < program_size.
     33     nth_safe ? pc program pc_ok = \snd (next res (bitvector_of_nat … pc))
     34
     35 λprogram. \snd
     36  (foldl_strong ?
     37   (λprefix.
     38     Σres: nat × (BitVectorTrie Byte 16).
     39      let 〈i,mem〉 ≝ res in
     40      i = |prefix| ∧
     41      (i ≤ 2^16 →
     42        ∀pc. ∀pc_ok: pc < |prefix|.
     43         nth_safe ? pc prefix pc_ok = \snd (next mem (bitvector_of_nat … pc))))
     44   program
     45   (λprefix,v,tl,prf,i_mem.
     46     let 〈i,mem〉 ≝ i_mem in
     47      〈S i,insert … (bitvector_of_nat … i) v mem〉)
     48  〈0,Stub Byte 16〉).
     49[3: cases (foldl_strong ? (λprefix.Σres.?) ???) * #i #mem * #H1 >H1 #H2 @H2
     50| % // #_ #pc #abs @⊥ @(absurd … abs (not_le_Sn_O …))
     51| cases i_mem in p; * #i' #mem' #H #EQ destruct(EQ) cases H -H #H1 #H2 %
     52  [ >length_append >H1 normalize //
     53  | #LE #pc #pc_ok
     54    cases (le_to_or_lt_eq … pc_ok)
     55    [2: #EQ_Spc >(?: pc = |prefix| + 0) in pc_ok;
     56      [2: >length_append in EQ_Spc; normalize #EQ @injective_S >EQ //]
     57      #pc_ok <nth_safe_prepend [2: //] whd in ⊢ (??%?);
     58      <H1 <plus_n_O whd in ⊢ (???%); //
     59    | >length_append <plus_n_Sm <plus_n_O #LT <shift_nth_prefix [2: /2/]
     60      >H2 [2: @(transitive_le … LE) //]
     61      cut (pc ≠ i) [ >H1 @lt_to_not_eq @lt_S_S_to_lt //] #NEQ
     62      whd in ⊢ (??%%); @sym_eq @lookup_insert_miss >eq_bv_false %
     63      #EQ @(absurd ?? NEQ) @(eq_bitvector_of_nat_to_eq … EQ) try assumption
     64      @(transitive_lt … LE) >H1 @lt_S_S_to_lt //]]
     65qed.
     66
     67definition load_code_memory: list Byte → BitVectorTrie Byte 16 ≝
     68 λprogram.load_code_memory0 program.
     69
     70lemma load_code_memory_ok:
     71 ∀program: list Byte.
     72  let program_size ≝ |program| in
     73   program_size ≤ 2^16 →
     74    ∀pc. ∀pc_ok: pc < program_size.
     75     nth_safe ? pc program pc_ok = \snd (next (load_code_memory program) (bitvector_of_nat … pc)).
     76whd in match load_code_memory; normalize nodelta #program @pi2
     77qed.
    1978
    2079lemma Prod_inv_rect_Type0:
Note: See TracChangeset for help on using the changeset viewer.