Ignore:
Timestamp:
Jun 20, 2011, 5:05:23 PM (9 years ago)
Author:
sacerdot
Message:

Half repaired, half broken. Most functions no longer return option types,
taking in input dependent types.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r994 r998  
    11891189               
    11901190
    1191 lemma fetch_assembly_pseudo:
     1191notation < "❰ x ❱" with precedence 90 for @{'dp $x $y }.
     1192interpretation "dp" 'dp x y = (dp x y).
     1193
     1194lemma fetch_assembly_pseudo':
    11921195 ∀program.∀pol:policy program.∀ppc,lookup_labels,lookup_datalabels.
    11931196  ∀pi,code_memory,len,assembled,instructions,pc.
    11941197   let expansion ≝ pol ppc in
    1195    Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (bitvector_of_nat ? pc) expansion pi →
    1196     Some … 〈len,assembled〉 = assembly_1_pseudoinstruction program pol ppc (bitvector_of_nat ? pc) lookup_labels lookup_datalabels pi →
     1198   Some ? instructions = expand_pseudo_instruction_safe lookup_labels lookup_datalabels (bitvector_of_nat ? pc) expansion pi →
     1199    Some … 〈len,assembled〉 = assembly_1_pseudoinstruction_safe program pol ppc (bitvector_of_nat ? pc) lookup_labels lookup_datalabels pi →
    11971200     encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →
    11981201      fetch_many code_memory (bitvector_of_nat … (pc + len)) (bitvector_of_nat … pc) instructions.
     
    12121215qed.
    12131216
    1214 (*
    1215 lemma rev_preserves_length:
    1216  ∀A.∀l. length … (rev A l) = length … l.
    1217   #A #l elim l
    1218    [ %
    1219    | #hd #tl #IH normalize >length_append normalize /2/ ]
    1220 qed.
    1221 
    1222 lemma rev_append:
    1223  ∀A.∀l1,l2.
    1224   rev A (l1@l2) = rev A l2 @ rev A l1.
    1225  #A #l1 elim l1 normalize //
    1226 qed.
    1227  
    1228 lemma rev_rev: ∀A.∀l. rev … (rev A l) = l.
    1229  #A #l elim l
    1230   [ //
    1231   | #hd #tl #IH normalize >rev_append normalize // ]
    1232 qed.
    1233 
    1234 lemma split_len_Sn:
    1235  ∀A:Type[0].∀l:list A.∀len.
    1236   length … l = S len →
    1237    Σl'.Σa. l = l'@[a] ∧ length … l' = len.
    1238  #A #l elim l
    1239   [ normalize #len #abs destruct
    1240   | #hd #tl #IH #len
    1241     generalize in match (rev_rev … tl)
    1242     cases (rev A tl) in ⊢ (??%? → ?)
    1243      [ #H <H normalize #EQ % [@[ ]] % [@hd] normalize /2/ 
    1244      | #a #l' #H <H normalize #EQ
    1245       %[@(hd::rev … l')] %[@a] % //
    1246       >length_append in EQ #EQ normalize in EQ; normalize;
    1247       generalize in match (injective_S … EQ) #EQ2 /2/ ]]
    1248 qed.
    1249 
    1250 lemma list_elim_rev:
    1251  ∀A:Type[0].∀P:list A → Type[0].
    1252   P [ ] → (∀l,a. P l → P (l@[a])) →
    1253    ∀l. P l.
    1254  #A #P #H1 #H2 #l
    1255  generalize in match (refl … (length … l))
    1256  generalize in ⊢ (???% → ?) #n generalize in match l
    1257  elim n
    1258   [ #L cases L [ // | #x #w #abs (normalize in abs) @⊥ // ]
    1259   | #m #IH #L #EQ
    1260     cases (split_len_Sn … EQ) #l' * #a * /3/ ]
    1261 qed.
    1262 
    1263 axiom is_prefix: ∀A:Type[0]. list A → list A → Prop.
    1264 axiom prefix_of_append:
    1265  ∀A:Type[0].∀l,l1,l2:list A.
    1266   is_prefix … l l1 → is_prefix … l (l1@l2).
    1267 axiom prefix_reflexive: ∀A,l. is_prefix A l l.
    1268 axiom nil_prefix: ∀A,l. is_prefix A [ ] l.
    1269 
    1270 record Propify (A:Type[0]) : Type[0] (*Prop*) ≝ { in_propify: A }.
    1271 
    1272 definition Propify_elim: ∀A. ∀P:Prop. (A → P) → (Propify A → P) ≝
    1273  λA,P,H,x. match x with [ mk_Propify p ⇒ H p ].
    1274 
    1275 definition app ≝
    1276  λA:Type[0].λl1:Propify (list A).λl2:list A.
    1277   match l1 with
    1278    [ mk_Propify l1 ⇒ mk_Propify … (l1@l2) ].
    1279 
    1280 lemma app_nil: ∀A,l1. app A l1 [ ] = l1.
    1281  #A * /3/
    1282 qed.
    1283 
    1284 lemma app_assoc: ∀A,l1,l2,l3. app A (app A l1 l2) l3 = app A l1 (l2@l3).
    1285  #A * #l1 normalize //
    1286 qed.
    1287 *)
     1217axiom bitvector_of_nat_nat_of_bitvector:
     1218  ∀n,v.
     1219    bitvector_of_nat n (nat_of_bitvector n v) = v.
     1220
     1221(* CSC: soo long next one; can we merge with previous one now? *)
     1222lemma fetch_assembly_pseudo:
     1223 ∀program.∀pol:policy program.∀ppc.
     1224  ∀code_memory.
     1225   let lookup_labels ≝ ? in
     1226   let lookup_datalabels ≝ ? in
     1227   let pc ≝ ? in
     1228   let pi ≝  \fst  (fetch_pseudo_instruction (\snd  program) ppc) in
     1229   let instructions ≝ expand_pseudo_instruction program pol ppc lookup_labels lookup_datalabels pc pi (refl …) (refl …) (refl …) (refl …) in
     1230   let 〈len,assembled〉 ≝ assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels pi (refl …) (refl …) (refl …) in
     1231     encoding_check code_memory pc (bitvector_of_nat … (nat_of_bitvector ? pc + len)) assembled →
     1232      fetch_many code_memory (bitvector_of_nat … (nat_of_bitvector ? pc + len)) pc instructions.
     1233 #program #pol #ppc #code_memory
     1234 letin lookup_labels ≝ (λx:Identifier
     1235    .sigma program pol (address_of_word_labels_code_mem (\snd  program) x))
     1236 letin lookup_datalabels ≝
     1237  (λx:BitVector 16
     1238    .lookup Identifier 16 x (construct_datalabels (\fst  program)) (zero 16))
     1239 letin pc ≝ (sigma program pol ppc)
     1240 letin pi ≝ (\fst  (fetch_pseudo_instruction (\snd  program) ppc))
     1241 letin instructions ≝ (expand_pseudo_instruction program pol ppc lookup_labels lookup_datalabels pc pi (refl …) (refl …) (refl …) (refl …))
     1242 @pair_elim' #len #assembled #EQ1 #H
     1243 generalize in match
     1244  (fetch_assembly_pseudo' program pol ppc lookup_labels lookup_datalabels pi
     1245  code_memory len assembled instructions (nat_of_bitvector ? pc) ???) in ⊢ ?;
     1246 [ >bitvector_of_nat_nat_of_bitvector //
     1247 | >bitvector_of_nat_nat_of_bitvector normalize nodelta >(sig2 ?? (expand_pseudo_instruction …)) %
     1248 | >bitvector_of_nat_nat_of_bitvector <EQ1 @assembly_1_pseudoinstruction_ok1
     1249 | //]
     1250qed.
    12881251
    12891252axiom assembly_ok:
    12901253 ∀program,pol,assembled.
    12911254  let 〈labels,costs〉 ≝ build_maps program pol in
    1292   Some … 〈assembled,costs〉 = assembly program pol →
     1255  〈assembled,costs〉 = assembly program pol →
    12931256  let code_memory ≝ load_code_memory assembled in
    12941257  let preamble ≝ \fst program in
     
    12961259  let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in
    12971260  let lookup_datalabels ≝ λx. lookup ?? x datalabels (zero ?) in
    1298    ∀ppc,len,assembledi.
    1299     let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
    1300      Some … 〈len,assembledi〉 = assembly_1_pseudoinstruction program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi →
     1261   ∀ppc,pi,newppc.
     1262   ∀prf:〈pi,newppc〉 = fetch_pseudo_instruction (\snd program) ppc.
     1263   ∀len,assembledi.
     1264     〈len,assembledi〉 = assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels pi (refl …) (refl …) ? →
    13011265      encoding_check code_memory (sigma program pol ppc) (bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len)) assembledi ∧
    13021266       sigma program pol newppc = bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len).
    1303 
    1304 axiom bitvector_of_nat_nat_of_bitvector:
    1305   ∀n,v.
    1306     bitvector_of_nat n (nat_of_bitvector n v) = v.
    1307 
     1267 <(pair_destruct_1 ????? prf) %
     1268qed.
     1269
     1270(*
    13081271axiom assembly_ok_to_expand_pseudo_instruction_ok:
    13091272 ∀program,pol,assembled,costs.
    1310   Some … 〈assembled,costs〉 = assembly program pol →
     1273  〈assembled,costs〉 = assembly program pol →
    13111274   ∀ppc.
    13121275    let code_memory ≝ load_code_memory assembled in
     
    13191282     ∃instructions.
    13201283      Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program pol ppc) expansion pi.
    1321 
    1322 axiom split_elim':
    1323   ∀A: Type[0].
    1324   ∀B: Type[1].
    1325   ∀l, m, v.
    1326   ∀T: Vector A l → Vector A m → B.
    1327   ∀P: B → Prop.
    1328     (∀lft, rgt. v = lft @@ rgt → P (T lft rgt)) →
    1329       P (let 〈lft, rgt〉 ≝ split A l m v in T lft rgt).
    1330 
    1331 axiom split_elim'':
    1332   ∀A: Type[0].
    1333   ∀B,B': Type[1].
    1334   ∀l, m, v.
    1335   ∀T: Vector A l → Vector A m → B.
    1336   ∀T': Vector A l → Vector A m → B'.
    1337   ∀P: B → B' → Prop.
    1338     (∀lft, rgt. v = lft @@ rgt → P (T lft rgt) (T' lft rgt)) →
    1339       P (let 〈lft, rgt〉 ≝ split A l m v in T lft rgt)
    1340         (let 〈lft, rgt〉 ≝ split A l m v in T' lft rgt).
     1284*)
     1285
     1286lemma fetch_assembly_pseudo2:
     1287 ∀program,pol,assembled.
     1288  let 〈labels,costs〉 ≝ build_maps program pol in
     1289  〈assembled,costs〉 = assembly program pol →
     1290   ∀ppc,pi,newppc.
     1291    let code_memory ≝ load_code_memory assembled in
     1292    let preamble ≝ \fst program in
     1293    let data_labels ≝ construct_datalabels preamble in
     1294    let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in
     1295    let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in
     1296    ∀prf:〈pi,newppc〉 = fetch_pseudo_instruction (\snd program) ppc.
     1297    let instructions ≝ expand_pseudo_instruction program pol ppc lookup_labels lookup_datalabels (sigma program pol ppc) pi (refl …) (refl …) ? (refl …) in
     1298     fetch_many code_memory (sigma program pol newppc) (sigma program pol ppc) instructions.
     1299 [2: <(pair_destruct_1 ????? prf) %]
     1300 #program #pol #assembled generalize in match (assembly_ok program pol assembled)
     1301 @pair_elim' #labels #costs #BUILD_MAPS
     1302 #H #ASSEMBLY #ppc #pi #newppc
     1303 letin code_memory ≝ (load_code_memory assembled)
     1304 letin preamble ≝ (\fst program)
     1305 letin data_labels ≝ (construct_datalabels preamble)
     1306 letin lookup_labels ≝ (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x))
     1307 letin lookup_datalabels ≝ (λx. lookup ? ? x data_labels (zero ?))
     1308 normalize nodelta #EQ generalize in match (H ASSEMBLY ppc … EQ) -H;
     1309 generalize in match (fetch_assembly_pseudo program pol ppc code_memory) in ⊢ ? normalize nodelta
     1310 @pair_elim' #len #assembledi #ASSEMBLE1
     1311 
     1312 cases
     1313  (assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels ????)
     1314 @split_elim' #len #assembledi #ASSEMBLY1
     1315 
     1316  @pair_elim'
     1317 
     1318 normalize nodelta;
     1319 whd in ⊢ (% → %) generalize in match (assembly_ok program pol assembled) >BUILD_MAPS #XX generalize in match (XX ASSEMBLY ppc) -XX;
     1320 cases (fetch_pseudo_instruction (\snd program) ppc) #pi #newppc
     1321 generalize in match (fetch_assembly_pseudo program pol ppc
     1322  (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) (λx. lookup ?? x data_labels (zero ?)) pi
     1323  (load_code_memory assembled));
     1324 whd in ⊢ ((∀_.∀_.∀_.∀_.%) → (∀_.∀_.%) → % → %) #H1 #H2 * #instructions #EXPAND
     1325 whd in H1:(∀_.∀_.∀_.∀_.? → ???% → ?) H2:(∀_.∀_.???% → ?);
     1326 normalize nodelta in EXPAND; (* HERE *)
     1327 generalize in match (λlen, assembled.H1 len assembled instructions (nat_of_bitvector … (sigma program pol ppc))) -H1; #H1
     1328 >bitvector_of_nat_nat_of_bitvector in H1; #H1
     1329 <EXPAND in H1 H2; whd in ⊢ ((∀_.∀_.? → ???% → ?) → (∀_.∀_.???% → ?) → ?)
     1330 #H1 #H2
     1331 cases (H2 ?? (refl …)) -H2; #K1 #K2 >K2
     1332 generalize in match (H1 ?? (refl …) (refl …) ?) -H1;
     1333  [ #K3 % [2: % [% | @K3]] | @K1 ]
     1334qed.
     1335
    13411336
    13421337lemma fetch_assembly_pseudo2:
Note: See TracChangeset for help on using the changeset viewer.