Changeset 985 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Jun 16, 2011, 4:50:23 PM (9 years ago)
Author:
sacerdot
Message:

1) Major refactoring: proofs moved where they should be.
2) New build_map that never fails.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r982 r985  
    44include "ASM/Fetch.ma".
    55include "ASM/Status.ma".
    6 include "ASM/FoldStuff.ma".
    76
    87definition assembly_preinstruction ≝
     
    680679    ].
    681680 
    682 definition construct_datalabels ≝
    683   λpreamble.
    684     \fst (foldl ((BitVectorTrie Identifier 16) × nat) ? (
    685     λt. λpreamble.
    686       let 〈datalabels, addr〉 ≝ t in
    687       let 〈name, size〉 ≝ preamble in
    688       let addr_16 ≝ bitvector_of_nat 16 addr in
    689         〈insert ? ? name addr_16 datalabels, addr + size〉)
    690           〈(Stub ? ?), 0〉 preamble).
    691 
    692681definition construct_costs ≝
    693682  λprogram.
     
    717706  ].
    718707
    719 definition build_maps ≝
    720   λinstr_list.
    721   let result ≝ foldl (option ((BitVectorTrie Word 16) × (nat × (nat × (BitVectorTrie Word 16))))) ?
    722     (λt. λi.
    723        let 〈label, i〉 ≝ i in
     708(* This establishes the correspondence between pseudo program counters and
     709   program counters. It is at the heart of the proof. *)
     710(*CSC: code taken from build_maps *)
     711definition sigma00: pseudo_assembly_program → list ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝
     712 λinstr_list.λl:list labelled_instruction.
     713  foldl ??
     714   (λt,i.
    724715       match t with
    725716       [ None ⇒ None ?
    726        | Some t ⇒
    727          let 〈labels, pc_ppc_costs〉 ≝ t in
    728          let 〈program_counter, ppc_costs〉 ≝ pc_ppc_costs in
    729          let 〈pseudo_program_counter, costs〉 ≝ ppc_costs in
    730          let labels ≝
    731            match label with
    732            [ None ⇒ labels
    733            | Some label ⇒
    734              let program_counter_bv ≝ bitvector_of_nat ? program_counter in
    735                insert ? ? label program_counter_bv labels
    736            ]
    737          in
    738            match construct_costs instr_list pseudo_program_counter program_counter (λx. zero ?) (λx. zero ?) costs i with
     717       | Some ppc_pc_map ⇒
     718         let 〈ppc,pc_map〉 ≝ ppc_pc_map in
     719         let 〈program_counter, sigma_map〉 ≝ pc_map in
     720         let 〈label, i〉 ≝ i in
     721          match construct_costs instr_list ppc program_counter (λx. zero ?) (λx. zero ?) (Stub …) i with
    739722           [ None ⇒ None ?
    740            | Some construct ⇒ Some ? 〈labels, 〈pseudo_program_counter + 1, construct〉〉
    741            ]
    742        ]) (Some ? 〈(Stub ? ?), 〈0, 〈0, (Stub ? ?)〉〉〉) (\snd instr_list) in
    743   match result with
     723           | Some pc_ignore ⇒
     724              let 〈pc,ignore〉 ≝ pc_ignore in
     725              Some … 〈S ppc,〈pc, insert ? ? (bitvector_of_nat ? ppc) (bitvector_of_nat ? pc) sigma_map〉〉 ]
     726       ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) l.
     727
     728definition sigma0: pseudo_assembly_program → option (nat × (nat × (BitVectorTrie Word 16)))
     729 ≝ λprog.sigma00 prog (\snd prog).
     730
     731definition tech_pc_sigma00: pseudo_assembly_program → list labelled_instruction → option (nat × nat) ≝
     732 λprogram,instr_list.
     733  match sigma00 program instr_list with
     734   [ None ⇒ None …
     735   | Some result ⇒
     736      let 〈ppc,pc_sigma_map〉 ≝ result in
     737      let 〈pc,map〉 ≝ pc_sigma_map in
     738       Some … 〈ppc,pc〉 ].
     739
     740definition sigma_safe: pseudo_assembly_program → option (Word → Word) ≝
     741 λinstr_list.
     742  match sigma0 instr_list with
    744743  [ None ⇒ None ?
    745744  | Some result ⇒
    746     let 〈labels, pc_ppc_costs〉 ≝ result in
    747     let 〈pc, ppc_costs〉 ≝ pc_ppc_costs in
    748     let 〈ppc, costs〉 ≝ ppc_costs in
     745    let 〈ppc,pc_sigma_map〉 ≝ result in
     746    let 〈pc, sigma_map〉 ≝ pc_sigma_map in
    749747      if gtb pc (2^16) then
    750748        None ?
    751749      else
    752         Some ? 〈labels, costs〉
    753   ].
     750        Some ? (λx.lookup ?? x sigma_map (zero …)) ].
     751
     752(* stuff about policy *)
     753
     754axiom policy_ok: ∀p. sigma_safe p ≠ None ….
     755
     756definition sigma: pseudo_assembly_program → Word → Word ≝
     757 λp.
     758  match sigma_safe p return λr:option (Word → Word). r ≠ None … → Word → Word with
     759   [ None ⇒ λabs. ⊥
     760   | Some r ⇒ λ_.r] (policy_ok p).
     761 cases abs //
     762qed.
     763
     764example sigma_0: ∀p. sigma p (bitvector_of_nat ? 0) = bitvector_of_nat ? 0.
     765 cases daemon.
     766qed.
     767
     768axiom construct_costs_sigma:
     769 ∀p,ppc,pc,pc',costs,costs',i.
     770  bitvector_of_nat ? pc = sigma p (bitvector_of_nat ? ppc) →
     771   Some … 〈pc',costs'〉 = construct_costs p ppc pc (λx.zero 16) (λx.zero 16) costs i →
     772    bitvector_of_nat ? pc' = sigma p (bitvector_of_nat 16 (S ppc)).
     773
     774axiom tech_pc_sigma00_append_Some:
     775 ∀program,prefix,costs,label,i,pc',code,ppc,pc.
     776  tech_pc_sigma00 program prefix = Some … 〈ppc,pc〉 →
     777   construct_costs program … ppc pc (λx.zero 16) (λx. zero 16) costs i = Some … 〈pc',code〉 →
     778    tech_pc_sigma00 program (prefix@[〈label,i〉]) = Some … 〈S ppc,pc'〉.
     779
     780axiom tech_pc_sigma00_append_None:
     781 ∀program,prefix,i,ppc,pc,costs.
     782  tech_pc_sigma00 program prefix = Some … 〈ppc,pc〉 →
     783   construct_costs program … ppc pc (λx.zero 16) (λx. zero 16) costs i = None …
     784    → False.
     785
     786definition build_maps ≝
     787  λpseudo_program.
     788  let result ≝
     789   foldl_strong
     790    (option Identifier × pseudo_instruction)
     791    (λpre. Σres:((BitVectorTrie Word 16) × (nat × (nat × (BitVectorTrie Word 16)))).
     792      let 〈labels,ppc_pc_costs〉 ≝ res in
     793      let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in
     794      let 〈pc',costs〉 ≝ pc_costs in
     795       bitvector_of_nat ? pc' = sigma pseudo_program (bitvector_of_nat ? ppc') ∧
     796       ppc' = length … pre ∧
     797       tech_pc_sigma00 pseudo_program pre = Some ? 〈ppc',pc'〉 ∧
     798       ∀id. occurs_exactly_once id pre →
     799        lookup ?? id labels (zero …) = sigma pseudo_program (address_of_word_labels_code_mem pre id))
     800    (\snd pseudo_program)
     801    (λprefix,i,tl,prf,t.
     802      let 〈labels, ppc_pc_costs〉 ≝ t in
     803      let 〈ppc, pc_costs〉 ≝ ppc_pc_costs in
     804      let 〈pc,costs〉 ≝ pc_costs in
     805       let 〈label, i'〉 ≝ i in
     806       let labels ≝
     807         match label with
     808         [ None ⇒ labels
     809         | Some label ⇒
     810           let program_counter_bv ≝ bitvector_of_nat ? pc in
     811             insert ? ? label program_counter_bv labels
     812         ]
     813       in
     814         match construct_costs pseudo_program ppc pc (λx. zero ?) (λx. zero ?) costs i' with
     815         [ None ⇒
     816            let dummy ≝ 〈labels,ppc_pc_costs〉 in
     817             dummy
     818         | Some construct ⇒ 〈labels, 〈S ppc,construct〉〉
     819         ]
     820    ) 〈(Stub ? ?), 〈0, 〈0, Stub ? ?〉〉〉
     821  in
     822   let 〈labels, ppc_pc_costs〉 ≝ result in
     823   let 〈ppc,pc_costs〉 ≝ ppc_pc_costs in
     824   let 〈pc, costs〉 ≝ pc_costs in
     825    〈labels, costs〉.
     826 [3: whd % [% [%]] // [>sigma_0//] #id normalize in ⊢ (% → ?) #abs @⊥ //
     827 | whd generalize in match (sig2 … t) >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
     828   cases construct in p4 #PC #CODE #JMEQ % [% [%]]
     829   [ @(construct_costs_sigma … IHn1) [4: <JMEQ % |*: skip]
     830   | >length_append <IH0 normalize; -IHn1; (*CSC: otherwise it diverges!*) //
     831   | @(tech_pc_sigma00_append_Some … IH1 (jmeq_to_eq … JMEQ))
     832   | #id normalize nodelta; -labels1; cases label; normalize nodelta
     833     [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 -IHn1; (*CSC: otherwise it diverges!*) //
     834     | #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?;
     835       generalize in match (refl … (eq_bv ? l id)); cases (eq_bv … l id) in ⊢ (???% → %)
     836        [ #EQ #_ <(eq_bv_eq … EQ) >lookup_insert_hit >address_of_word_labels_code_mem_Some_hit
     837          <IH0 [@IHn1 | <(eq_bv_eq … EQ) in H #H @H]
     838        | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: -IHn1; /2/]
     839          <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 -IHn1; //]]]
     840 | (* dummy case *) @⊥ generalize in match (sig2 … t) >p >p1 >p2 >p3 * *; #IH0 #IH1 #IH2
     841   @(tech_pc_sigma00_append_None … IH1 (jmeq_to_eq ??? p4)) ]
     842qed.
     843
     844(*
     845lemma build_maps_ok:
     846 ∀p:pseudo_assembly_program.
     847  let 〈labels,costs〉 ≝ build_maps' p in
     848   ∀pc.
     849    (nat_of_bitvector … pc) < length … (\snd p) →
     850     lookup ?? pc labels (zero …) = sigma p (\snd (fetch_pseudo_instruction (\snd p) pc)).
     851 #p cases p #preamble #instr_list
     852  elim instr_list
     853   [ whd #pc #abs normalize in abs; cases (not_le_Sn_O ?) [#H cases (H abs) ]
     854   | #hd #tl #IH
     855    whd in ⊢ (match % with [ _ ⇒ ?])
     856   ]
     857qed.
     858*)
    754859
    755860definition assembly: pseudo_assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
    756861  λp.
    757862    let 〈preamble, instr_list〉 ≝ p in
    758       match build_maps p with
     863    let 〈labels,costs〉 ≝ build_maps p in
     864    let datalabels ≝ construct_datalabels preamble in
     865    let lookup_labels ≝ λx. lookup ? ? x labels (zero ?) in
     866    let lookup_datalabels ≝ λx. lookup ? ? x datalabels (zero ?) in
     867    let result ≝ foldr ? ? (λx. λy.
     868        match y with
     869        [ None ⇒ None ?
     870        | Some lst ⇒
     871          let 〈pc, ppc_y〉 ≝ lst in
     872          let 〈ppc, y〉 ≝ ppc_y in
     873          let x ≝ assembly_1_pseudoinstruction p ppc pc lookup_labels lookup_datalabels (\snd x) in
     874          match x with
     875          [ None ⇒ None ?
     876          | Some x ⇒
     877            let 〈pc_delta, program〉 ≝ x in
     878            let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
     879            let new_ppc ≝ \snd (half_add ? ppc (bitvector_of_nat ? 1)) in
     880              Some ? 〈new_pc, 〈new_ppc, (program @ y)〉〉
     881          ]
     882        ]) (Some ? 〈(zero ?), 〈(zero ?), [ ]〉〉) instr_list
     883    in
     884      match result with
    759885      [ None ⇒ None ?
    760       | Some labels_costs ⇒
    761         let datalabels ≝ construct_datalabels preamble in
    762         let 〈labels,costs〉 ≝ labels_costs in
    763         let lookup_labels ≝ λx. lookup ? ? x labels (zero ?) in
    764         let lookup_datalabels ≝ λx. lookup ? ? x datalabels (zero ?) in
    765         let result ≝ foldr ? ? (λx. λy.
    766             match y with
    767             [ None ⇒ None ?
    768             | Some lst ⇒
    769               let 〈pc, ppc_y〉 ≝ lst in
    770               let 〈ppc, y〉 ≝ ppc_y in
    771               let x ≝ assembly_1_pseudoinstruction p ppc pc lookup_labels lookup_datalabels (\snd x) in
    772               match x with
    773               [ None ⇒ None ?
    774               | Some x ⇒
    775                 let 〈pc_delta, program〉 ≝ x in
    776                 let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
    777                 let new_ppc ≝ \snd (half_add ? ppc (bitvector_of_nat ? 1)) in
    778                   Some ? 〈new_pc, 〈new_ppc, (program @ y)〉〉
    779               ]
    780             ]) (Some ? 〈(zero ?), 〈(zero ?), [ ]〉〉) instr_list
    781         in
    782           match result with
    783           [ None ⇒ None ?
    784           | Some result ⇒ Some ? (〈\snd (\snd result), costs〉)
    785           ]
    786       ].
     886      | Some result ⇒ Some ? (〈\snd (\snd result), costs〉)].
    787887
    788888definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
Note: See TracChangeset for help on using the changeset viewer.