Changeset 993 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Jun 17, 2011, 6:28:49 PM (8 years ago)
Author:
sacerdot
Message:

More Russell everywhere; getting closer to the goal.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r989 r993  
    666666  lookup ? ? pc policy long_jump.
    667667 
    668 definition assembly_1_pseudoinstruction
     668definition assembly_1_pseudoinstruction_safe
    669669  λprogram: pseudo_assembly_program.
    670670  λjump_expansion: policy_type.
     
    684684    ].
    685685 
    686 definition construct_costs
     686definition construct_costs_safe
    687687  λprogram.
    688688  λjump_expansion: policy_type.
    689689  λpseudo_program_counter: nat.
    690690  λprogram_counter: nat.
    691   λlookup_labels.
    692   λlookup_datalabels.
    693691  λcosts: BitVectorTrie Word 16.
    694692  λi.
     
    700698    let pc_bv ≝ bitvector_of_nat ? program_counter in
    701699    let ppc_bv ≝ bitvector_of_nat ? pseudo_program_counter in
     700    let lookup_labels ≝ λx.pc_bv in
     701    let lookup_datalabels ≝ λx.zero ? in
    702702    let pc_delta_assembled ≝
    703       assembly_1_pseudoinstruction program jump_expansion ppc_bv pc_bv
     703      assembly_1_pseudoinstruction_safe program jump_expansion ppc_bv pc_bv
    704704        lookup_labels lookup_datalabels i
    705705    in
     
    727727         let 〈program_counter, sigma_map〉 ≝ pc_map in
    728728         let 〈label, i〉 ≝ i in
    729           match construct_costs instr_list jump_expansion ppc program_counter (λx. zero ?) (λx. zero ?) (Stub …) i with
     729          match construct_costs_safe instr_list jump_expansion ppc program_counter (Stub …) i with
    730730           [ None ⇒ None ?
    731731           | Some pc_ignore ⇒
     
    775775   [ None ⇒ λabs. ⊥
    776776   | Some r ⇒ λ_.r] (sig2 … policy).
    777  cases abs //
     777 cases abs /2/
    778778qed.
    779779
     
    782782qed.
    783783
     784(* MAIN AXIOM HERE, HIDDEN USING cases daemon *)
     785definition assembly_1_pseudoinstruction:
     786 ∀program:pseudo_assembly_program.∀pol: policy program.
     787  ∀ppc:Word.∀lookup_labels,lookup_datalabels,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  Σres:(nat × (list Byte)).
     792   let 〈len,code〉 ≝ res in
     793    sigma program pol (\snd (half_add ? ppc (bitvector_of_nat ? 1))) =
     794     bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len)
     795≝ λprogram: pseudo_assembly_program.
     796  λpol: policy program.
     797  λppc: Word.
     798  λlookup_labels.
     799  λlookup_datalabels.
     800  λpi.
     801  λprf1,prf2,prf3.
     802   match assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi with
     803    [ None ⇒ let dummy ≝ 〈0,[ ]〉 in dummy
     804    | Some res ⇒ res ].
     805 [ @⊥ elim pi in p [*]
     806   try (#ARG1 #ARG2 #ARG3 #abs) try (#ARG1 #ARG2 #abs) try (#ARG1 #abs) try #abs
     807   generalize in match (jmeq_to_eq ??? abs) -abs; #abs whd in abs:(??%?); try destruct(abs)
     808   whd in abs:(??match % with [_ ⇒ ? | _ ⇒ ?]?);
     809   (* WRONG HERE, NEEDS LEMMA SAYING THAT THE POLICY DOES NOT RETURN MEDIUM! *)
     810   cases daemon
     811 | cases res in p ⊢ %; -res; #len #code #EQ normalize nodelta;
     812   (* THIS SHOULD BE TRUE INSTEAD *)
     813   cases daemon]
     814qed.
     815
     816(* MAIN AXIOM HERE, HIDDEN USING cases daemon *)
     817definition construct_costs':
     818 ∀program. policy program → nat → nat → ? → ? →
     819  Σres:(nat × (BitVectorTrie Word 16)). True
     820
     821  λprogram.λpol: policy program.λppc,pc,costs,i.
     822   match construct_costs_safe program pol ppc pc costs i with
     823    [ None ⇒ let dummy ≝ 〈0, Stub ??〉 in dummy
     824    | Some res ⇒ res ].
     825 [ cases daemon
     826 | %]
     827qed.
     828
     829definition construct_costs ≝
     830 λprogram,pol,ppc,pc,costs,i. eject … (construct_costs' program pol ppc pc costs i).
     831
    784832axiom construct_costs_sigma:
    785  ∀p.∀pol:policy p.∀ppc,pc,pc',costs,costs',i.
     833 ∀p.∀pol:policy p.∀ppc,pc,costs,i.
    786834  bitvector_of_nat ? pc = sigma p pol (bitvector_of_nat ? ppc) →
    787    Some … 〈pc',costs'〉 = construct_costs p pol ppc pc (λx.zero 16) (λx.zero 16) costs i →
    788     bitvector_of_nat ? pc' = sigma p pol (bitvector_of_nat 16 (S ppc)).
     835   bitvector_of_nat ? (\fst (construct_costs p pol ppc pc costs i)) = sigma p pol (bitvector_of_nat 16 (S ppc)).
    789836
    790837axiom tech_pc_sigma00_append_Some:
    791  ∀program.∀pol:policy program.∀prefix,costs,label,i,pc',code,ppc,pc.
     838 ∀program.∀pol:policy program.∀prefix,costs,label,i,ppc,pc.
    792839  tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
    793    construct_costs program pol … ppc pc (λx.zero 16) (λx. zero 16) costs i = Some … 〈pc',code〉 →
    794     tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,pc'〉.
    795 
    796 axiom tech_pc_sigma00_append_None:
    797  ∀program.∀pol:policy program.∀prefix,i,ppc,pc,costs.
    798   tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
    799    construct_costs program pol … ppc pc (λx.zero 16) (λx. zero 16) costs i = None …
    800     → False.
     840   tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,\fst (construct_costs program pol … ppc pc costs i)〉.
    801841
    802842definition build_maps:
     
    806846    ∀id. occurs_exactly_once id (\snd pseudo_program) →
    807847     lookup ?? id labels (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem (\snd pseudo_program) id)
    808  
     848
    809849  λpseudo_program.λpol:policy pseudo_program.
    810850  let result ≝
     
    815855      let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in
    816856      let 〈pc',costs〉 ≝ pc_costs in
    817        bitvector_of_nat ? pc' = sigma pseudo_program pol (bitvector_of_nat ? ppc') ∧
    818        ppc' = length … pre ∧
    819        tech_pc_sigma00 pseudo_program (eject … pol) pre = Some ? 〈ppc',pc'〉 ∧
    820        ∀id. occurs_exactly_once id pre →
    821         lookup ?? id labels (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem pre id))
     857       And ( And (
     858       And (bitvector_of_nat ? pc' = sigma pseudo_program pol (bitvector_of_nat ? ppc')) (*∧*)
     859       (ppc' = length … pre)) (*∧ *)
     860       (tech_pc_sigma00 pseudo_program (eject … pol) pre = Some ? 〈ppc',pc'〉)) (*∧*)
     861       (∀id. occurs_exactly_once id pre →
     862        lookup ?? id labels (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem pre id)))
    822863    (\snd pseudo_program)
    823864    (λprefix,i,tl,prf,t.
     
    831872         | Some label ⇒
    832873           let program_counter_bv ≝ bitvector_of_nat ? pc in
    833              insert ? ? label program_counter_bv labels
    834          ]
     874             insert ? ? label program_counter_bv labels]
    835875       in
    836          match construct_costs pseudo_program pol ppc pc (λx. zero ?) (λx. zero ?) costs i' with
    837          [ None ⇒
    838             let dummy ≝ 〈labels,ppc_pc_costs〉 in
    839              dummy
    840          | Some construct ⇒ 〈labels, 〈S ppc,construct〉〉
    841          ]
     876         let construct ≝ construct_costs pseudo_program pol ppc pc costs i' in
     877          〈labels, 〈S ppc,construct〉〉
    842878    ) 〈(Stub ? ?), 〈0, 〈0, Stub ? ?〉〉〉
    843879  in
     
    846882   let 〈pc, costs〉 ≝ pc_costs in
    847883    〈labels, costs〉.
    848  [4: whd % [% [%]] // [>sigma_0//] #id normalize in ⊢ (% → ?) #abs @⊥ //
    849  |2: whd generalize in match (sig2 … t) >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
    850    cases construct in p4 #PC #CODE #JMEQ % [% [%]]
    851    [ @(construct_costs_sigma … IHn1) [4: <JMEQ % |*: skip]
     884 [2: whd generalize in match (sig2 … t) >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
     885   generalize in match (refl … construct); cases construct in ⊢ (???% → %) #PC #CODE #JMEQ % [% [%]]
     886   [ <(construct_costs_sigma … costs i1 IHn1) change with (? = ?(\fst construct)) >JMEQ %
    852887   | >length_append <IH0 normalize; -IHn1; (*CSC: otherwise it diverges!*) //
    853    | @(tech_pc_sigma00_append_Some … IH1 (jmeq_to_eq … JMEQ))
     888   | >(tech_pc_sigma00_append_Some … costs … IH1) change with (Some … 〈S ppc,\fst construct〉 = ?) >JMEQ %
    854889   | #id normalize nodelta; -labels1; cases label; normalize nodelta
    855890     [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 -IHn1; (*CSC: otherwise it diverges!*) //
     
    860895        | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: -IHn1; /2/]
    861896          <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 -IHn1; //]]]
    862  |3: (* dummy case *) @⊥ generalize in match (sig2 … t) >p >p1 >p2 >p3 * *; #IH0 #IH1 #IH2
    863    @(tech_pc_sigma00_append_None … IH1 (jmeq_to_eq ??? p4))
    864  | generalize in match (sig2 … result) >p normalize nodelta; >p1 normalize nodelta;
    865    >p2; normalize nodelta; * #_; #H @H]
     897 |3: whd % [% [%]] // [>sigma_0//] #id normalize in ⊢ (% → ?) #abs @⊥ //
     898 | generalize in match (sig2 … result) in ⊢ ?;
     899   normalize nodelta in p ⊢ %; -result; >p in ⊢ (match % with [_ ⇒ ?] → ?)
     900   normalize nodelta; >p1 normalize nodelta; >p2; normalize nodelta; * #_; #H @H]
    866901qed.
    867902
    868 definition assembly: ∀p:pseudo_assembly_program. policy p → option (list Byte × (BitVectorTrie Identifier 16)) ≝
    869   λp,pol.
    870     let 〈preamble, instr_list〉 ≝ p in
    871     let 〈labels,costs〉 ≝ build_maps p pol in
     903definition assembly:
     904 ∀p:pseudo_assembly_program. policy p → list Byte × (BitVectorTrie Identifier 16) ≝
     905  λp.let 〈preamble, instr_list〉 ≝ p in
     906   λpol.
     907    let 〈labels,costs〉 ≝ build_maps 〈preamble,instr_list〉 pol in
    872908    let datalabels ≝ construct_datalabels preamble in
    873909    let lookup_labels ≝ λx. lookup ? ? x labels (zero ?) in
    874910    let lookup_datalabels ≝ λx. lookup ? ? x datalabels (zero ?) in
    875     let result ≝ foldr ? ? (λx. λy.
    876         match y with
    877         [ None ⇒ None ?
    878         | Some lst ⇒
    879           let 〈pc, ppc_y〉 ≝ lst in
    880           let 〈ppc, y〉 ≝ ppc_y in
    881           let x ≝ assembly_1_pseudoinstruction p pol ppc pc lookup_labels lookup_datalabels (\snd x) in
    882           match x with
    883           [ None ⇒ None ?
    884           | Some x ⇒
    885             let 〈pc_delta, program〉 ≝ x in
    886             let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
    887             let new_ppc ≝ \snd (half_add ? ppc (bitvector_of_nat ? 1)) in
    888               Some ? 〈new_pc, 〈new_ppc, (program @ y)〉〉
    889           ]
    890         ]) (Some ? 〈(zero ?), 〈(zero ?), [ ]〉〉) instr_list
     911    let result ≝
     912     foldl_strong
     913      (option Identifier × pseudo_instruction)
     914      (λpre. Σpc_ppc_code:(Word × (Word × (list Byte))).
     915        let 〈pc,ppc_code〉 ≝ pc_ppc_code in
     916        let 〈ppc,code〉 ≝ ppc_code in
     917         ∀ppc'.
     918          let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc' in
     919          let 〈len,assembledi〉 ≝
     920           assembly_1_pseudoinstruction 〈preamble,instr_list〉 pol ppc' lookup_labels lookup_datalabels pi ??? in
     921           True)
     922      instr_list
     923      (λprefix,hd,tl,prf,pc_ppc_code.
     924        let 〈pc, ppc_code〉 ≝ pc_ppc_code in
     925        let 〈ppc, code〉 ≝ ppc_code in
     926        let 〈pc_delta, program〉 ≝ assembly_1_pseudoinstruction 〈preamble,instr_list〉 pol ppc lookup_labels lookup_datalabels (\snd hd) ??? in
     927        let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
     928        let new_ppc ≝ \snd (half_add ? ppc (bitvector_of_nat ? 1)) in
     929         〈new_pc, 〈new_ppc, (code @ program)〉〉)
     930      〈(zero ?), 〈(zero ?), [ ]〉〉
    891931    in
    892       match result with
    893       [ None ⇒ None ?
    894       | Some result ⇒ Some ? (〈\snd (\snd result), costs〉)].
     932     〈\snd (\snd result), costs〉.
     933 [2,5: %
     934 |*: cases daemon ]
     935qed.
    895936
    896937definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
Note: See TracChangeset for help on using the changeset viewer.