 Timestamp:
 May 26, 2011, 6:26:57 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r847 r848 18 18 qed. 19 19 20 (*coercion bigbang nocomposites: ∀A:Type[0].False → ∀v:VOID.A ≝ bigbang on _v:VOID to ?.*) 20 coercion bigbang nocomposites: ∀A:Type[0].False → ∀v:VOID.A ≝ bigbang on _v:VOID to ?. 21 21 22 22 lemma sig2: ∀A.∀P:A → Prop. ∀p:Σx:A.P x. P (eject … p). … … 55 55 Some … pc ]. 56 56 57 definition sigma : pseudo_assembly_program → option (Word → Word) ≝57 definition sigma_safe: pseudo_assembly_program → option (Word → Word) ≝ 58 58 λinstr_list. 59 59 match sigma0 instr_list with … … 67 67 Some ? (λx.lookup ?? x sigma_map (zero …)) ]. 68 68 69 axiom policy_ok: ∀p. sigma p ≠ None …. 69 axiom policy_ok: ∀p. sigma_safe p ≠ None …. 70 71 definition sigma: pseudo_assembly_program → Word → Word ≝ 72 λp. 73 match sigma_safe p return λr:option (Word → Word). r ≠ None … → Word → Word with 74 [ None ⇒ λabs. ⊥ 75  Some r ⇒ λ_.r] (policy_ok p). 76 cases abs // 77 qed. 78 79 (* 80 definition build_maps' ≝ 81 λpseudo_program. 82 let 〈preamble,instr_list〉 ≝ pseudo_program in 83 let result ≝ 84 foldl 85 ((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))) 86 (option Identifier × pseudo_instruction) 87 (λt,i. 88 let 〈labels, pc_costs〉 ≝ t in 89 let 〈program_counter, costs〉 ≝ pc_costs in 90 let 〈label, i'〉 ≝ i in 91 let labels ≝ 92 match label with 93 [ None ⇒ labels 94  Some label ⇒ 95 let program_counter_bv ≝ bitvector_of_nat ? program_counter in 96 insert ? ? label program_counter_bv labels 97 ] 98 in 99 match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with 100 [ None ⇒ 101 let dummy ≝ 〈labels,pc_costs〉 in 102 dummy 103  Some construct ⇒ 〈labels, construct〉 104 ] 105 ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 instr_list 106 in 107 let 〈labels, pc_costs〉 ≝ result in 108 let 〈pc, costs〉 ≝ pc_costs in 109 〈labels, costs〉. 110 111 (* 112 notation < "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)" 113 with precedence 10 114 for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }. 115 *) 116 117 lemma build_maps_ok: 118 ∀p:pseudo_assembly_program. 119 let 〈labels,costs〉 ≝ build_maps' p in 120 ∀pc. 121 (nat_of_bitvector … pc) < length … (\snd p) → 122 lookup ?? pc labels (zero …) = sigma p (\snd (fetch_pseudo_instruction (\snd p) pc)). 123 #p cases p #preamble #instr_list 124 elim instr_list 125 [ whd #pc #abs normalize in abs; cases (not_le_Sn_O ?) [#H cases (H abs) ] 126  #hd #tl #IH 127 whd in ⊢ (match % with [ _ ⇒ ?]) 128 ] 129 qed. 130 *) 131 132 (* 133 lemma list_elim_rev: 134 ∀A:Type[0].∀P:list A → Prop. 135 P [ ] → (∀n,l. length l = n → P l → 136 P [ ] → (∀l,a. P l → P (l@[a])) → 137 ∀l. P l. 138 #A #P 139 qed.*) 140 141 lemma length_append: 142 ∀A.∀l1,l2:list A. 143 l1 @ l2 = l1 + l2. 144 #A #l1 elim l1 145 [ // 146  #hd #tl #IH #l2 normalize <IH //] 147 qed. 148 149 lemma rev_preserves_length: 150 ∀A.∀l. length … (rev A l) = length … l. 151 #A #l elim l 152 [ % 153  #hd #tl #IH normalize >length_append normalize /2/ ] 154 qed. 155 156 lemma rev_append: 157 ∀A.∀l1,l2. 158 rev A (l1@l2) = rev A l2 @ rev A l1. 159 #A #l1 elim l1 normalize // 160 qed. 161 162 lemma rev_rev: ∀A.∀l. rev … (rev A l) = l. 163 #A #l elim l 164 [ // 165  #hd #tl #IH normalize >rev_append normalize // ] 166 qed. 167 168 lemma split_len_Sn: 169 ∀A:Type[0].∀l:list A.∀len. 170 length … l = S len → 171 Σl'.Σa. l = l'@[a] ∧ length … l' = len. 172 #A #l elim l 173 [ normalize #len #abs destruct 174  #hd #tl #IH #len 175 generalize in match (rev_rev … tl) 176 cases (rev A tl) in ⊢ (??%? → ?) 177 [ #H <H normalize #EQ % [@[ ]] % [@hd] normalize /2/ 178  #a #l' #H <H normalize #EQ 179 %[@(hd::rev … l')] %[@a] % // 180 >length_append in EQ #EQ normalize in EQ; normalize; 181 generalize in match (injective_S … EQ) #EQ2 /2/ ]] 182 qed. 183 184 lemma list_elim_rev: 185 ∀A:Type[0].∀P:list A → Type[0]. 186 P [ ] → (∀l,a. P l → P (l@[a])) → 187 ∀l. P l. 188 #A #P #H1 #H2 #l 189 generalize in match (refl … (length … l)) 190 generalize in ⊢ (???% → ?) #n generalize in match l 191 elim n 192 [ #L cases L [ //  #x #w #abs (normalize in abs) @⊥ // ] 193  #m #IH #L #EQ 194 cases (split_len_Sn … EQ) #l' * #a * /3/ ] 195 qed. 70 196 71 197 axiom is_prefix: ∀A:Type[0]. list A → list A → Prop. 72 73 (* 198 axiom prefix_of_append: 199 ∀A:Type[0].∀l,l1,l2:list A. 200 is_prefix … l l1 → is_prefix … l (l1@l2). 201 74 202 definition build_maps' ≝ 75 203 λpseudo_program. … … 82 210 (Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix. 83 211 let instr_list_prefix' ≝ instr_list_prefix @ [i] in 84 is_prefix ? instr_list_prefix' instr_list ∧212 is_prefix ? instr_list_prefix' instr_list → 85 213 tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ?) 86 214 (λt: Σt:((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16))). … … 89 217 λi: Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix. 90 218 let instr_list_prefix' ≝ instr_list_prefix @ [i] in 91 is_prefix ? instr_list_prefix' instr_list ∧219 is_prefix ? instr_list_prefix' instr_list → 92 220 tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ? . 93 221 let 〈labels, pc_costs〉 ≝ t in … … 103 231 in 104 232 match construct_costs pseudo_program program_counter (λx. zero ?) (λx. zero ?) costs i' with 105 [ None ⇒ 〈labels,pc_costs〉 (*assert_false*) 233 [ None ⇒ 234 let dummy ≝ 〈labels,pc_costs〉 in 235 dummy 106 236  Some construct ⇒ 〈labels, construct〉 107 237 ] 108 ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 (\snd ?(*instr_list*))238 ) 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉 ?(*instr_list*) 109 239 in 110 240 let 〈labels, pc_costs〉 ≝ result in 111 241 let 〈pc, costs〉 ≝ pc_costs in 112 242 〈labels, costs〉. 113 [ cases t in c2 ⊢ % #t' * #LIST_PREFIX * #H1t' #H2t' #HJMt' 243 [4: @(list_elim_rev ? 244 (λinstr_list. list ( 245 (Σi:option Identifier × pseudo_instruction. ∀instr_list_prefix. 246 let instr_list_prefix' ≝ instr_list_prefix @ [i] in 247 is_prefix ? instr_list_prefix' instr_list → 248 tech_pc_sigma0 〈preamble,instr_list_prefix'〉 ≠ None ?))) 249 ?? instr_list) (* CSC: BAD ORDER FOR CODE EXTRACTION *) 250 [ @[ ] 251  #l' #a #limage %2 252 [ %[@a] #PREFIX #PREFIX_OK 253  (* CSC: EVEN WORST CODE FOR EXTRACTION: WE SHOULD STRENGTHEN 254 THE INDUCTION HYPOTHESIS INSTEAD *) 255 elim limage 256 [ %1 257  #HD #TL #IH @(?::IH) cases HD #ELEM #K1 %[@ELEM] #K2 #K3 258 @K1 @(prefix_of_append ???? K3) 259 ] 260 ] 261 262 263 264 265 cases t in c2 ⊢ % #t' * #LIST_PREFIX * #H1t' #H2t' #HJMt' 114 266 % [@ (LIST_PREFIX @ [i])] % 115 267 [ cases (sig2 … i LIST_PREFIX) #K1 #K2 @K1 … … 118 270  (* assert false case *) 119 271 3: % [@ ([ ])] % [2: %  (* DOABLE *)] 120  121 *) 272  122 273 123 274 let rec encoding_check (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
Note: See TracChangeset
for help on using the changeset viewer.