Changeset 998


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

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

Location:
src/ASM
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r993 r998  
    591591  ].
    592592
    593 definition expand_pseudo_instruction: ? → ? → Word → jump_length → pseudo_instruction → option (list instruction) ≝
     593definition expand_pseudo_instruction_safe: ? → ? → Word → jump_length → pseudo_instruction → option (list instruction) ≝
    594594  λlookup_labels.
    595595  λlookup_datalabels.
     
    675675  λi.
    676676  let expansion ≝ jump_expansion ppc in
    677     match expand_pseudo_instruction lookup_labels lookup_datalabels pc expansion i with
     677    match expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc expansion i with
    678678    [ None ⇒ None ?
    679679    | Some pseudos ⇒
     
    715715   program counters. It is at the heart of the proof. *)
    716716(*CSC: code taken from build_maps *)
    717 definition sigma00: pseudo_assembly_program → policy_type → list ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝
     717definition sigma00: pseudo_assembly_program → policy_type → list ? → ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝
    718718 λinstr_list.
    719719 λjump_expansion: policy_type.
    720720 λl:list labelled_instruction.
     721 λacc.
    721722  foldl ??
    722723   (λt,i.
     
    732733              let 〈pc,ignore〉 ≝ pc_ignore in
    733734              Some … 〈S ppc,〈pc, insert ? ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? pc) sigma_map〉〉 ]
    734        ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) l.
     735       ]) acc l.
    735736
    736737definition sigma0: pseudo_assembly_program → policy_type → option (nat × (nat × (BitVectorTrie Word 16)))
    737  ≝ λprog.λjump_expansion.sigma00 prog jump_expansion (\snd prog).
     738 ≝ λprog.λjump_expansion.sigma00 prog jump_expansion (\snd prog) (Some ? 〈0, 〈0, (Stub ? ?)〉〉).
    738739
    739740definition tech_pc_sigma00: pseudo_assembly_program → policy_type → list labelled_instruction → option (nat × nat) ≝
    740741 λprogram,jump_expansion,instr_list.
    741   match sigma00 program jump_expansion instr_list with
     742  match sigma00 program jump_expansion instr_list (Some ? 〈0, 〈0, (Stub ? ?)〉〉) (* acc copied from sigma0 *) with
    742743   [ None ⇒ None …
    743744   | Some result ⇒
     
    782783qed.
    783784
     785definition expand_pseudo_instruction:
     786 ∀program:pseudo_assembly_program.∀pol: policy program.
     787  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pc,pi.
     788  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
     789  lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)) →
     790  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
     791  pc = sigma program pol ppc →
     792  Σres:list instruction. Some … res = expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc (pol ppc) pi
     793≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pc,pi,prf1,prf2,prf3,prf4.
     794   match expand_pseudo_instruction_safe lookup_labels lookup_datalabels pc (pol ppc) pi with
     795    [ None ⇒ let dummy ≝ [ ] in dummy
     796    | Some res ⇒ res ].
     797 [ cases daemon
     798 | >p %]
     799qed.
     800
    784801(* MAIN AXIOM HERE, HIDDEN USING cases daemon *)
    785 definition assembly_1_pseudoinstruction:
     802definition assembly_1_pseudoinstruction':
    786803 ∀program:pseudo_assembly_program.∀pol: policy program.
    787804  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
     
    790807  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
    791808  Σres:(nat × (list Byte)).
     809   Some … res = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi ∧
    792810   let 〈len,code〉 ≝ res in
    793811    sigma program pol (\snd (half_add ? ppc (bitvector_of_nat ? 1))) =
     
    809827   (* WRONG HERE, NEEDS LEMMA SAYING THAT THE POLICY DOES NOT RETURN MEDIUM! *)
    810828   cases daemon
    811  | cases res in p ⊢ %; -res; #len #code #EQ normalize nodelta;
     829 | % [ >p %]
     830   cases res in p ⊢ %; -res; #len #code #EQ normalize nodelta;
    812831   (* THIS SHOULD BE TRUE INSTEAD *)
    813832   cases daemon]
    814833qed.
    815834
     835definition assembly_1_pseudoinstruction:
     836 ∀program:pseudo_assembly_program.∀pol: policy program.
     837  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
     838  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
     839  lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)) →
     840  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
     841   nat × (list Byte)
     842≝ λprogram,pol,ppc,lookup_labels,lookup_datalabels,pi,prf1,prf2,prf3.
     843   assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1
     844    prf2 prf3.
     845
     846lemma assembly_1_pseudoinstruction_ok1:
     847 ∀program:pseudo_assembly_program.∀pol: policy program.
     848  ∀ppc:Word.∀lookup_labels,lookup_datalabels,pi.
     849  ∀prf1:lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)).
     850  ∀prf2:lookup_datalabels = (λx. lookup ?? x (construct_datalabels (\fst program)) (zero ?)).
     851  ∀prf3:\fst (fetch_pseudo_instruction (\snd program) ppc) = pi.
     852     Some … (assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3)
     853   = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi.
     854 #program #pol #ppc #lookup_labels #lookup_datalabels #pi #prf1 #prf2 #prf3
     855 cases (sig2 … (assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3))
     856 #H1 #_ @H1
     857qed.
     858
    816859(* MAIN AXIOM HERE, HIDDEN USING cases daemon *)
    817860definition construct_costs':
    818  ∀program. policy program → nat → nat → ? → ? →
    819   Σres:(nat × (BitVectorTrie Word 16)). True
     861 ∀program. ∀pol:policy program. ∀ppc,pc,costs,i.
     862  Σres:(nat × (BitVectorTrie Word 16)). Some … res = construct_costs_safe program pol ppc pc costs i
    820863
    821864  λprogram.λpol: policy program.λppc,pc,costs,i.
     
    824867    | Some res ⇒ res ].
    825868 [ cases daemon
    826  | %]
     869 | >p %]
    827870qed.
    828871
    829872definition construct_costs ≝
    830873 λprogram,pol,ppc,pc,costs,i. eject … (construct_costs' program pol ppc pc costs i).
     874
     875(*
     876axiom suffix_of: ∀A:Type[0]. ∀l,prefix:list A. list A.
     877axiom suffix_of_ok: ∀A,l,prefix. prefix @ suffix_of A l prefix = l.
     878
     879let rec foldl_strong_internal
     880  (A: Type[0]) (P: list A → Type[0]) (l: list A) (suffix2: list A)
     881  (H: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl @suffix2 → P prefix → P (prefix @ [hd]))
     882  (prefix: list A) (suffix: list A) (acc: P prefix) on suffix:
     883    l = prefix @ suffix @ suffix2 → P(prefix @ suffix) ≝
     884  match suffix return λl'. l = prefix @ l' @ suffix2 → P (prefix @ l') with
     885  [ nil ⇒ λprf. ?
     886  | cons hd tl ⇒ λprf. ?
     887  ].
     888  [ > (append_nil ?)
     889    @ acc
     890  | applyS (foldl_strong_internal A P l suffix2 H (prefix @ [hd]) tl ? ?)
     891    [ @(H prefix hd tl prf acc)
     892    | >prf /2/]]
     893qed.
     894
     895definition foldl_strong ≝
     896  λA: Type[0].
     897  λP: list A → Type[0].
     898  λl: list A.
     899  λH: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]).
     900  λacc: P [ ].
     901    foldl_strong_internal A P l [ ] ? [ ] l acc ?.
     902 [ #prefix #hd #tl >append_nil @H
     903 | >append_nil % ]
     904qed.
     905
     906axiom foldl_strong_step:
     907 ∀A:Type[0].
     908  ∀P: list A → Type[0].
     909   ∀l: list A.
     910    ∀H: ∀prefix,hd,tl. l =  prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]).
     911     ∀acc: P [ ].
     912      ∀Q: ∀prefix. P prefix → Prop.
     913       ∀HQ: ∀prefix,hd,tl.∀prf: l = prefix @ [hd] @ tl.
     914        ∀acc: P prefix. Q prefix acc → Q (prefix @ [hd]) (H prefix hd tl prf acc).
     915       Q [ ] acc →
     916        Q l (foldl_strong A P l H acc).
     917(*
     918 #A #P #l #H #acc #Q #HQ #Hacc normalize;
     919 generalize in match
     920  (foldl_strong ?
     921   (λpre. Q pre (foldl_strong_internal A P l (suffix_of A l pre) ? [ ] pre acc ?))
     922   l ? Hacc)
     923 [3: >suffix_of_ok % | 2: #prefix #hd #tl #EQ @(H prefix hd (tl@suffix_of A l pre) EQ) ]
     924 [2: #prefix #hd #tl #prf #X whd in ⊢ (??%)
     925 #K
     926
     927 generalize in match
     928  (foldl_strong ?
     929   (λpre. Q pre (foldl_strong_internal A P l H pre (suffix_of A l pre) acc (suffix_of_ok A l pre))))
     930 [2: @H
     931*)
     932
     933axiom foldl_elim:
     934 ∀A:Type[0].
     935  ∀B: Type[0].
     936   ∀H: A → B → A.
     937    ∀acc: A.
     938     ∀l: list B.
     939      ∀Q: A → Prop.
     940       (∀acc:A.∀b:B. Q acc → Q (H acc b)) →
     941         Q acc →
     942          Q (foldl A B H acc l).
     943*)
     944
     945lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b.
     946 #A #a #b #EQ destruct //
     947qed.
     948
     949lemma sigma00_strict:
     950 ∀instr_list,jump_expansion,l,acc. acc = None ? →
     951  sigma00 instr_list jump_expansion l acc = None ….
     952 #instr_list #jump_expansion #l elim l
     953  [ #acc #H >H %
     954  | #hd #tl #IH #acc #H >H change with (sigma00 ?? tl ? = ?) @IH % ]
     955qed.
     956
     957lemma sigma00_append:
     958 ∀instr_list,jump_expansion,l1,l2,acc.
     959  sigma00 instr_list jump_expansion (l1@l2) acc =
     960   sigma00 instr_list jump_expansion
     961    l2 (sigma00 instr_list jump_expansion l1 acc).
     962 whd in match sigma00; normalize nodelta;
     963 #instr_list #jump_expansion #l1 #l2 #acc @foldl_append
     964qed.
     965
     966lemma policy_ok_prefix_ok:
     967 ∀program.∀pol:policy program.∀suffix,prefix.
     968  prefix@suffix = \snd program →
     969   sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) ≠ None ….
     970 * #preamble #instr_list #pol #suffix #prefix #prf whd in prf:(???%);
     971 generalize in match (sig2 ?? pol) whd in prf:(???%) <prf in pol; #pol
     972 whd in match policy_ok; whd in match sigma_safe; whd in match sigma0
     973 normalize nodelta >sigma00_append
     974 cases (sigma00 ?? prefix ?)
     975  [2: #x #_ % #abs destruct(abs)
     976  | * #abs @⊥ @abs >sigma00_strict % ]
     977qed.
     978
     979lemma policy_ok_prefix_hd_ok:
     980 ∀program.∀pol:policy program.∀suffix,hd,prefix,ppc_pc_map.
     981  (prefix@[hd])@suffix = \snd program →
     982   Some ? ppc_pc_map = sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) →
     983    let 〈ppc,pc_map〉 ≝ ppc_pc_map in
     984    let 〈program_counter, sigma_map〉 ≝ pc_map in
     985    let 〈label, i〉 ≝ hd in
     986     construct_costs_safe program pol ppc program_counter (Stub …) i ≠ None ….
     987 * #preamble #instr_list #pol #suffix #hd #prefix #ppc_pc_map #EQ1 #EQ2
     988 generalize in match (policy_ok_prefix_ok 〈preamble,instr_list〉 pol suffix
     989  (prefix@[hd]) EQ1) in ⊢ ? >sigma00_append <EQ2 whd in ⊢ (?(??%?) → ?)
     990 @pair_elim' #ppc #pc_map #EQ3 normalize nodelta
     991 @pair_elim' #pc #map #EQ4 normalize nodelta
     992 @pair_elim' #l' #i' #EQ5 normalize nodelta
     993 cases (construct_costs_safe ??????) normalize
     994  [* #abs @⊥ @abs % | #X #_ % #abs destruct(abs)]
     995qed.
     996
     997(*
     998lemma tech_pc_sigma00_append_Some:
     999 ∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc.
     1000  tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
     1001   tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉.
     1002 #program #pol #prefix #costs #label #i #ppc #pc #H
     1003  whd in match tech_pc_sigma00 in ⊢ %; normalize nodelta;
     1004  whd in match sigma00 in ⊢ %; normalize nodelta in ⊢ %;
     1005  generalize in match (sig2 … pol) whd in ⊢ (% → ?) whd in ⊢ (?(??%?) → ?)
     1006  whd in match sigma0; normalize nodelta;
     1007  >foldl_step
     1008  change with (? → match match sigma00 program pol prefix with [None ⇒ ? | Some res ⇒ ?] with [ None ⇒ ? | Some res ⇒ ? ] = ?)
     1009  whd in match tech_pc_sigma00 in H; normalize nodelta in H;
     1010  cases (sigma00 program pol prefix) in H ⊢ %
     1011   [ whd in ⊢ (??%% → ?) #abs destruct(abs)
     1012   | * #ppc' * #pc' #sigma_map normalize nodelta; #H generalize in match (option_destruct_Some ??? H)
     1013     
     1014     normalize nodelta; -H;
     1015     
     1016 
     1017   generalize in match H; -H;
     1018  generalize in match (foldl ?????); in H ⊢ (??match match % with [_ ⇒ ? | _ ⇒ ?] with [_ ⇒ ? | _ ⇒ ?]?)
     1019   [2: whd in ⊢ (??%%)
     1020XXX
     1021*)
    8311022
    8321023axiom construct_costs_sigma:
  • 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:
  • src/ASM/Util.ma

    r993 r998  
    139139  ].
    140140
     141lemma foldl_step:
     142 ∀A:Type[0].
     143  ∀B: Type[0].
     144   ∀H: A → B → A.
     145    ∀acc: A.
     146     ∀pre: list B.
     147      ∀hd:B.
     148       foldl A B H acc (pre@[hd]) = (H (foldl A B H acc pre) hd).
     149 #A #B #H #acc #pre generalize in match acc; -acc; elim pre
     150  [ normalize; //
     151  | #hd #tl #IH #acc #X normalize; @IH ]
     152qed.
     153
     154lemma foldl_append:
     155 ∀A:Type[0].
     156  ∀B: Type[0].
     157   ∀H: A → B → A.
     158    ∀acc: A.
     159     ∀suff,pre: list B.
     160      foldl A B H acc (pre@suff) = (foldl A B H (foldl A B H acc pre) suff).
     161 #A #B #H #acc #suff elim suff
     162  [ #pre >append_nil %
     163  | #hd #tl #IH #pre whd in ⊢ (???%) <(foldl_step … H ??) applyS (IH (pre@[hd])) ]
     164qed.
     165
    141166definition flatten ≝
    142167  λA: Type[0].
  • src/ASM/Vector.ma

    r961 r998  
    170170 split' A m n v.
    171171
    172 
    173172definition head: ∀A: Type[0]. ∀n: nat. Vector A (S n) → A × (Vector A n) ≝
    174173  λA: Type[0].
     
    306305   
    307306interpretation "Vector append" 'vappend v1 v2 = (append ??? v1 v2).
     307
     308axiom split_elim':
     309  ∀A: Type[0].
     310  ∀B: Type[1].
     311  ∀l, m, v.
     312  ∀T: Vector A l → Vector A m → B.
     313  ∀P: B → Prop.
     314    (∀lft, rgt. v = lft @@ rgt → P (T lft rgt)) →
     315      P (let 〈lft, rgt〉 ≝ split A l m v in T lft rgt).
     316
     317axiom split_elim'':
     318  ∀A: Type[0].
     319  ∀B,B': Type[1].
     320  ∀l, m, v.
     321  ∀T: Vector A l → Vector A m → B.
     322  ∀T': Vector A l → Vector A m → B'.
     323  ∀P: B → B' → Prop.
     324    (∀lft, rgt. v = lft @@ rgt → P (T lft rgt) (T' lft rgt)) →
     325      P (let 〈lft, rgt〉 ≝ split A l m v in T lft rgt)
     326        (let 〈lft, rgt〉 ≝ split A l m v in T' lft rgt).
    308327   
    309328let rec scan_left (A: Type[0]) (B: Type[0]) (n: nat)
Note: See TracChangeset for help on using the changeset viewer.