Changeset 2119
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r2115 r2119 616 616 qed. 617 617 618 definition load_code_memory_aux ≝619 fold_left_i_aux … (620 λi, mem, v.621 insert … (bitvector_of_nat … i) v mem) (Stub Byte 16).622 623 618 lemma vsplit_zero: 624 619 ∀A,m. … … 1060 1055 ]. 1061 1056 1062 (* This is a trivial consequence of fetch_assembly_pseudo + the proof that the 1063 function that load the code in memory is correct. The latter is based 1064 on missing properties from the standard library on the BitVectorTrie 1065 data structrure. 1066 1067 Wrong at the moment, requires Jaap's precondition to ensure that the program 1068 does not overflow when put into code memory (i.e. shorter than 2^16 bytes). 1069 *) 1070 1071 lemma load_code_memory_ok: 1072 ∀program. 1073 let program_size ≝ program in 1074 program_size ≤ 2^16 → 1075 ∀pc. ∀pc_ok: pc < program_size. 1076 nth_safe ? pc program pc_ok = \snd (next (load_code_memory program) (bitvector_of_nat … pc)). 1077 #program elim program 1078 [ #_ #pc #abs normalize in abs; @⊥ /2/ 1079  #hd #tl #IH #size_ok * 1080 [ #pc_ok whd in ⊢ (??%?); whd in match (load_code_memory ?); 1081 whd in match next; normalize nodelta 1082  #pc' #pc_ok' whd in ⊢ (??%?); whd in match (load_code_memory ?); 1083 whd in match next; normalize nodelta 1084 ] 1085 cases daemon (*CSC: complete! *) 1086 qed. 1087 (*NO! Prima dimostrare tipo Russell di assembly in Assembly.ma 1088 Poi dimostrare che per ogni i, se fetcho l'iesimo bit di program 1089 e' come fetchare l'iesimo bit dalla memoria. 1090 Concludere assembly_ok come semplice corollario. 1091 *) 1057 (* This is a trivial consequence of fetch_assembly_pseudo + load_code_memory_ok. *) 1092 1058 lemma assembly_ok: 1093 1059 ∀program. 
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: 
src/ASM/Status.ma
r2111 r2119 1104 1104 qed. 1105 1105 1106 definition load_code_memory ≝1107 fold_left_i … (1108 λi, mem, v.1109 insert … (bitvector_of_nat … i) v mem) (Stub Byte 16).1110 1111 definition load ≝1112 λl,cm.1113 λstatus.1114 set_code_memory (BitVectorTrie Word 16) ? cm status (load_code_memory l).1115 1116 1106 definition fetch_pseudo_instruction: 1117 1107 ∀code_mem:list labelled_instruction. ∀pc:Word.
Note: See TracChangeset
for help on using the changeset viewer.