Changeset 2119 for src/ASM/Fetch.ma
 Timestamp:
 Jun 27, 2012, 12:09:25 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Fetch.ma
r1961 r2119 17 17 λpc: Word. 18 18 〈add … pc (bitvector_of_nat 16 1), lookup … pc pmem (zero …)〉. 19 20 (*CSC: move elsewhere *) 21 axiom 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 26 discriminator Prod. 27 28 definition 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 //]] 65 qed. 66 67 definition load_code_memory: list Byte → BitVectorTrie Byte 16 ≝ 68 λprogram.load_code_memory0 program. 69 70 lemma 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)). 76 whd in match load_code_memory; normalize nodelta #program @pi2 77 qed. 19 78 20 79 lemma Prod_inv_rect_Type0:
Note: See TracChangeset
for help on using the changeset viewer.