Changeset 2999 for src/ASM/Fetch.ma


Ignore:
Timestamp:
Mar 28, 2013, 12:47:55 PM (8 years ago)
Author:
sacerdot
Message:

code_memory added to labelled_object_code to avoid recomputing it every time.
This gives a major speed up in the semantics of the extracted code.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Fetch.ma

    r2770 r2999  
    173173definition code_memory_size ≝ bitvector_max_nat 16.
    174174
    175 include alias "ASM/BitVectorTrie.ma".
    176 include alias "ASM/Arithmetic.ma".
    177 
    178 definition next: BitVectorTrie Byte 16 → ∀program_counter: Word. Word × Byte ≝
    179   λpmem: BitVectorTrie Byte 16.
    180   λpc: Word.
    181     〈add … pc (bitvector_of_nat 16 1), lookup … pc pmem (zero …)〉.
    182 
    183 definition load_code_memory0:
    184  ∀program: object_code. Σres: BitVectorTrie Byte 16.
    185   let program_size ≝ |program| in
    186    program_size ≤ 2^16 →
    187     ∀pc. ∀pc_ok: pc < program_size.
    188      nth_safe ? pc program pc_ok = \snd (next res (bitvector_of_nat … pc))
    189 
    190  λprogram. \snd
    191   (foldl_strong ?
    192    (λprefix.
    193      Σres: nat × (BitVectorTrie Byte 16).
    194       let 〈i,mem〉 ≝ res in
    195       i = |prefix| ∧
    196       (i ≤ 2^16 →
    197         ∀pc. ∀pc_ok: pc < |prefix|.
    198          nth_safe ? pc prefix pc_ok = \snd (next mem (bitvector_of_nat … pc))))
    199    program
    200    (λprefix,v,tl,prf,i_mem.
    201      let 〈i,mem〉 ≝ i_mem in
    202       〈S i,insert … (bitvector_of_nat … i) v mem〉)
    203   〈0,Stub Byte 16〉).
    204 [3: cases (foldl_strong ? (λprefix.Σres.?) ???) * #i #mem * #H1 >H1 #H2 @H2
    205 | % // #_ #pc #abs @⊥ @(absurd … abs (not_le_Sn_O …))
    206 | cases i_mem in p; * #i' #mem' #H #EQ destruct(EQ) cases H -H #H1 #H2 %
    207   [ >length_append >H1 normalize //
    208   | #LE #pc #pc_ok
    209     cases (le_to_or_lt_eq … pc_ok)
    210     [2: #EQ_Spc >(?: pc = |prefix| + 0) in pc_ok;
    211       [2: >length_append in EQ_Spc; normalize #EQ @injective_S >EQ //]
    212       #pc_ok <nth_safe_prepend [2: //] whd in ⊢ (??%?);
    213       <H1 <plus_n_O whd in ⊢ (???%); //
    214     | >length_append <plus_n_Sm <plus_n_O #LT <shift_nth_prefix [2: /2/]
    215       >H2 [2: @(transitive_le … LE) //]
    216       cut (pc ≠ i) [ >H1 @lt_to_not_eq @lt_S_S_to_lt //] #NEQ
    217       whd in ⊢ (??%%); @sym_eq @lookup_insert_miss >eq_bv_false %
    218       #EQ @(absurd ?? NEQ) @(eq_bitvector_of_nat_to_eq … EQ) try assumption
    219       @(transitive_lt … LE) >H1 @lt_S_S_to_lt //]]
    220 qed.
    221 
    222 definition load_code_memory: object_code → BitVectorTrie Byte 16 ≝
    223  λprogram.load_code_memory0 program.
    224 
    225 lemma load_code_memory_ok:
    226  ∀program: object_code.
    227   let program_size ≝ |program| in
    228    program_size ≤ 2^16 →
    229     ∀pc. ∀pc_ok: pc < program_size.
    230      nth_safe ? pc program pc_ok = \snd (next (load_code_memory program) (bitvector_of_nat … pc)).
    231 whd in match load_code_memory; normalize nodelta #program @pi2
    232 qed.
    233 
    234175lemma Prod_inv_rect_Type0:
    235176 ∀A,B. ∀P: A × B → Type[0].∀ab.
Note: See TracChangeset for help on using the changeset viewer.