Changeset 987 for src/ASM/Assembly.ma

Timestamp:

Jun 16, 2011, 6:08:12 PM (10 years ago)

Author:

sacerdot

Message:

Real parameterization over the policy.

File:

• src/ASM/Assembly.ma (modified) (14 diffs)

src/ASM/Assembly.ma

@@ -656 +656 @@
     jump_expansion_policy_internal program old_labels old_policy in
     jump_expansion_internal n' program new_labels new_policy ].
-         
-definition jump_expansion ≝
- λpc.λprogram.
+
+definition policy_type ≝ Word → jump_length.
+
+definition jump_expansion': pseudo_assembly_program → policy_type ≝
+ λprogram.λpc.
   let policy ≝ jump_expansion_internal (length ? (\snd program)) program (Stub ? ?) (Stub ? ?) in
   lookup ? ? pc policy long_jump.
@@ -664 +666 @@
 definition assembly_1_pseudoinstruction ≝
   λprogram: pseudo_assembly_program.
+  λjump_expansion: policy_type.
   λppc: Word.
   λpc: Word.
@@ -669 +672 @@
   λlookup_datalabels.
   λi.
-  let expansion ≝ jump_expansion ppc program in
+  let expansion ≝ jump_expansion ppc in
     match expand_pseudo_instruction lookup_labels lookup_datalabels pc expansion i with
     [ None ⇒ None ?
@@ -681 +684 @@
 definition construct_costs ≝
   λprogram.
+  λjump_expansion: policy_type.
   λpseudo_program_counter: nat.
   λprogram_counter: nat.
@@ -695 +699 @@
     let ppc_bv ≝ bitvector_of_nat ? pseudo_program_counter in
     let pc_delta_assembled ≝
-      assembly_1_pseudoinstruction program ppc_bv pc_bv
+      assembly_1_pseudoinstruction program jump_expansion ppc_bv pc_bv
         lookup_labels lookup_datalabels i
     in
@@ -709 +713 @@
    program counters. It is at the heart of the proof. *)
 (*CSC: code taken from build_maps *)
-definition sigma00: pseudo_assembly_program → list ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝
- λinstr_list.λl:list labelled_instruction.
+definition sigma00: pseudo_assembly_program → policy_type → list ? → option (nat × (nat × (BitVectorTrie Word 16))) ≝
+ λinstr_list.
+ λjump_expansion: policy_type.
+ λl:list labelled_instruction.
   foldl ??
    (λt,i.
@@ -719 +725 @@
          let 〈program_counter, sigma_map〉 ≝ pc_map in
          let 〈label, i〉 ≝ i in
-          match construct_costs instr_list ppc program_counter (λx. zero ?) (λx. zero ?) (Stub …) i with
+          match construct_costs instr_list jump_expansion ppc program_counter (λx. zero ?) (λx. zero ?) (Stub …) i with
            [ None ⇒ None ?
            | Some pc_ignore ⇒
@@ -726 +732 @@
        ]) (Some ? 〈0, 〈0, (Stub ? ?)〉〉) l.
 
-definition sigma0: pseudo_assembly_program → option (nat × (nat × (BitVectorTrie Word 16)))
- ≝ λprog.sigma00 prog (\snd prog).
-
-definition tech_pc_sigma00: pseudo_assembly_program → list labelled_instruction → option (nat × nat) ≝
- λprogram,instr_list.
-  match sigma00 program instr_list with
+definition sigma0: pseudo_assembly_program → policy_type → option (nat × (nat × (BitVectorTrie Word 16)))
+ ≝ λprog.λjump_expansion.sigma00 prog jump_expansion (\snd prog).
+
+definition tech_pc_sigma00: pseudo_assembly_program → policy_type → list labelled_instruction → option (nat × nat) ≝
+ λprogram,jump_expansion,instr_list.
+  match sigma00 program jump_expansion instr_list with
    [ None ⇒ None …
    | Some result ⇒
@@ -738 +744 @@
        Some … 〈ppc,pc〉 ].
 
-definition sigma_safe: pseudo_assembly_program → option (Word → Word) ≝
- λinstr_list.
-  match sigma0 instr_list with
+definition sigma_safe: pseudo_assembly_program → policy_type → option (Word → Word) ≝
+ λinstr_list,jump_expansion.
+  match sigma0 instr_list jump_expansion with
   [ None ⇒ None ?
   | Some result ⇒
@@ -752 +758 @@
 (* stuff about policy *)
 
-axiom policy_ok: ∀p. sigma_safe p ≠ None ….
-
-definition sigma: pseudo_assembly_program → Word → Word ≝
- λp.
-  match sigma_safe p return λr:option (Word → Word). r ≠ None … → Word → Word with
+definition policy_ok ≝ λjump_expansion,p. sigma_safe p jump_expansion ≠ None ….
+
+definition policy ≝ λp. Σjump_expansion:policy_type. policy_ok jump_expansion p.
+
+lemma eject_policy: ∀p. policy p → policy_type.
+ #p #pol @(eject … pol)
+qed.
+
+coercion eject_policy nocomposites: ∀p.∀pol:policy p. policy_type ≝ eject_policy on _pol:(policy ?) to policy_type.
+
+definition sigma: ∀p:pseudo_assembly_program. policy p → Word → Word ≝
+ λp,policy.
+  match sigma_safe p (eject … policy) return λr:option (Word → Word). r ≠ None … → Word → Word with
    [ None ⇒ λabs. ⊥
-   | Some r ⇒ λ_.r] (policy_ok p).
+   | Some r ⇒ λ_.r] (sig2 … policy).
  cases abs //
 qed.
 
-example sigma_0: ∀p. sigma p (bitvector_of_nat ? 0) = bitvector_of_nat ? 0.
+example sigma_0: ∀p,pol. sigma p pol (bitvector_of_nat ? 0) = bitvector_of_nat ? 0.
  cases daemon.
 qed.
 
 axiom construct_costs_sigma:
- ∀p,ppc,pc,pc',costs,costs',i.
-  bitvector_of_nat ? pc = sigma p (bitvector_of_nat ? ppc) →
-   Some … 〈pc',costs'〉 = construct_costs p ppc pc (λx.zero 16) (λx.zero 16) costs i →
-    bitvector_of_nat ? pc' = sigma p (bitvector_of_nat 16 (S ppc)).
+ ∀p.∀pol:policy p.∀ppc,pc,pc',costs,costs',i.
+  bitvector_of_nat ? pc = sigma p pol (bitvector_of_nat ? ppc) →
+   Some … 〈pc',costs'〉 = construct_costs p pol ppc pc (λx.zero 16) (λx.zero 16) costs i →
+    bitvector_of_nat ? pc' = sigma p pol (bitvector_of_nat 16 (S ppc)).
 
 axiom tech_pc_sigma00_append_Some:
- ∀program,prefix,costs,label,i,pc',code,ppc,pc.
-  tech_pc_sigma00 program prefix = Some … 〈ppc,pc〉 →
-   construct_costs program … ppc pc (λx.zero 16) (λx. zero 16) costs i = Some … 〈pc',code〉 →
-    tech_pc_sigma00 program (prefix@[〈label,i〉]) = Some … 〈S ppc,pc'〉.
+ ∀program.∀pol:policy program.∀prefix,costs,label,i,pc',code,ppc,pc.
+  tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
+   construct_costs program pol … ppc pc (λx.zero 16) (λx. zero 16) costs i = Some … 〈pc',code〉 →
+    tech_pc_sigma00 program pol (prefix@[〈label,i〉]) = Some … 〈S ppc,pc'〉.
 
 axiom tech_pc_sigma00_append_None:
- ∀program,prefix,i,ppc,pc,costs.
-  tech_pc_sigma00 program prefix = Some … 〈ppc,pc〉 →
-   construct_costs program … ppc pc (λx.zero 16) (λx. zero 16) costs i = None …
+ ∀program.∀pol:policy program.∀prefix,i,ppc,pc,costs.
+  tech_pc_sigma00 program pol prefix = Some … 〈ppc,pc〉 →
+   construct_costs program pol … ppc pc (λx.zero 16) (λx. zero 16) costs i = None …
     → False.
 
 definition build_maps ≝
-  λpseudo_program.
+  λpseudo_program.λpol:policy pseudo_program.
   let result ≝
    foldl_strong
@@ -793 +807 @@
       let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in
       let 〈pc',costs〉 ≝ pc_costs in
-       bitvector_of_nat ? pc' = sigma pseudo_program (bitvector_of_nat ? ppc') ∧
+       bitvector_of_nat ? pc' = sigma pseudo_program pol (bitvector_of_nat ? ppc') ∧
        ppc' = length … pre ∧
-       tech_pc_sigma00 pseudo_program pre = Some ? 〈ppc',pc'〉 ∧
+       tech_pc_sigma00 pseudo_program (eject … pol) pre = Some ? 〈ppc',pc'〉 ∧
        ∀id. occurs_exactly_once id pre →
-        lookup ?? id labels (zero …) = sigma pseudo_program (address_of_word_labels_code_mem pre id))
+        lookup ?? id labels (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem pre id))
     (\snd pseudo_program)
     (λprefix,i,tl,prf,t.
@@ -812 +826 @@
          ]
        in
-         match construct_costs pseudo_program ppc pc (λx. zero ?) (λx. zero ?) costs i' with
+         match construct_costs pseudo_program pol ppc pc (λx. zero ?) (λx. zero ?) costs i' with
          [ None ⇒
             let dummy ≝ 〈labels,ppc_pc_costs〉 in
@@ -858 +872 @@
 *)
 
-definition assembly: pseudo_assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
-  λp.
+definition assembly: ∀p:pseudo_assembly_program. policy p → option (list Byte × (BitVectorTrie Identifier 16)) ≝
+  λp,pol.
     let 〈preamble, instr_list〉 ≝ p in
-    let 〈labels,costs〉 ≝ build_maps p in
+    let 〈labels,costs〉 ≝ build_maps p pol in
     let datalabels ≝ construct_datalabels preamble in
     let lookup_labels ≝ λx. lookup ? ? x labels (zero ?) in
@@ -871 +885 @@
           let 〈pc, ppc_y〉 ≝ lst in
           let 〈ppc, y〉 ≝ ppc_y in
-          let x ≝ assembly_1_pseudoinstruction p ppc pc lookup_labels lookup_datalabels (\snd x) in
+          let x ≝ assembly_1_pseudoinstruction p pol ppc pc lookup_labels lookup_datalabels (\snd x) in
           match x with
           [ None ⇒ None ?