Changeset 998 for src/ASM/Assembly.ma


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.

File:
1 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:
Note: See TracChangeset for help on using the changeset viewer.