Changeset 987 for src/ASM/AssemblyProof.ma

Timestamp:

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

Author:

sacerdot

Message:

Real parameterization over the policy.

File:

• src/ASM/AssemblyProof.ma (modified) (18 diffs)

src/ASM/AssemblyProof.ma

@@ -681 +681 @@
 
 lemma fetch_assembly_pseudo:
- ∀program,ppc,lookup_labels,lookup_datalabels.
+ ∀program.∀pol:policy program.∀ppc,lookup_labels,lookup_datalabels.
   ∀pi,code_memory,len,assembled,instructions,pc.
-   let expansion ≝ jump_expansion ppc program in
+   let expansion ≝ pol ppc in
    Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (bitvector_of_nat ? pc) expansion pi →
-    Some … 〈len,assembled〉 = assembly_1_pseudoinstruction program ppc (bitvector_of_nat ? pc) lookup_labels lookup_datalabels pi →
+    Some … 〈len,assembled〉 = assembly_1_pseudoinstruction program pol ppc (bitvector_of_nat ? pc) lookup_labels lookup_datalabels pi →
      encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →
       fetch_many code_memory (bitvector_of_nat … (pc + len)) (bitvector_of_nat … pc) instructions.
- #program #ppc #lookup_labels #lookup_datalabels #pi #code_memory #len #assembled #instructions #pc
+ #program #pol #ppc #lookup_labels #lookup_datalabels #pi #code_memory #len #assembled #instructions #pc
  #EQ1 whd in ⊢ (???% → ?) <EQ1 whd in ⊢ (???% → ?) #EQ2
  cases (pair_destruct ?????? (option_destruct_Some … EQ2)) -EQ2; #EQ2a #EQ2b
@@ -779 +779 @@
 
 axiom assembly_ok:
- ∀program,assembled.
-  let 〈labels,costs〉 ≝ build_maps program in
-  Some … 〈assembled,costs〉 = assembly program →
+ ∀program,pol,assembled.
+  let 〈labels,costs〉 ≝ build_maps program pol in
+  Some … 〈assembled,costs〉 = assembly program pol →
   let code_memory ≝ load_code_memory assembled in
   let preamble ≝ \fst program in
   let datalabels ≝ construct_datalabels preamble in
-  let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in
+  let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in
   let lookup_datalabels ≝ λx. lookup ?? x datalabels (zero ?) in
    ∀ppc,len,assembledi.
     let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
-     Some … 〈len,assembledi〉 = assembly_1_pseudoinstruction program ppc (sigma program ppc) lookup_labels lookup_datalabels pi →
-      encoding_check code_memory (sigma program ppc) (bitvector_of_nat … (nat_of_bitvector … (sigma program ppc) + len)) assembledi ∧
-       sigma program newppc = bitvector_of_nat … (nat_of_bitvector … (sigma program ppc) + len).
+     Some … 〈len,assembledi〉 = assembly_1_pseudoinstruction program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi →
+      encoding_check code_memory (sigma program pol ppc) (bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len)) assembledi ∧
+       sigma program pol newppc = bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len).
 
 axiom bitvector_of_nat_nat_of_bitvector:
@@ -798 +798 @@
 
 axiom assembly_ok_to_expand_pseudo_instruction_ok:
- ∀program,assembled,costs.
-  Some … 〈assembled,costs〉 = assembly program →
+ ∀program,pol,assembled,costs.
+  Some … 〈assembled,costs〉 = assembly program pol →
    ∀ppc.
     let code_memory ≝ load_code_memory assembled in
     let preamble ≝ \fst program in   
     let data_labels ≝ construct_datalabels preamble in
-    let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in
+    let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in
     let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in
-    let expansion ≝ jump_expansion ppc program in
+    let expansion ≝ pol ppc in
     let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
      ∃instructions.
-      Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi.
+      Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program pol ppc) expansion pi.
 
 axiom pair_elim':
@@ -849 +849 @@
 
 lemma fetch_assembly_pseudo2:
- ∀program,assembled.
-  let 〈labels,costs〉 ≝ build_maps program in
-  Some … 〈assembled,costs〉 = assembly program →
+ ∀program,pol,assembled.
+  let 〈labels,costs〉 ≝ build_maps program pol in
+  Some … 〈assembled,costs〉 = assembly program pol →
    ∀ppc.
     let code_memory ≝ load_code_memory assembled in
     let preamble ≝ \fst program in
     let data_labels ≝ construct_datalabels preamble in
-    let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in
+    let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in
     let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in
-    let expansion ≝ jump_expansion ppc program in
+    let expansion ≝ pol ppc in
     let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
      ∃instructions.
-      Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi ∧
-       fetch_many code_memory (sigma program newppc) (sigma program ppc) instructions.
- #program #assembled @pair_elim' #labels #costs #BUILD_MAPS #ASSEMBLY #ppc
- generalize in match (assembly_ok_to_expand_pseudo_instruction_ok program assembled costs ASSEMBLY ppc)
+      Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program pol ppc) expansion pi ∧
+       fetch_many code_memory (sigma program pol newppc) (sigma program pol ppc) instructions.
+ #program #pol #assembled @pair_elim' #labels #costs #BUILD_MAPS #ASSEMBLY #ppc
+ generalize in match (assembly_ok_to_expand_pseudo_instruction_ok program pol assembled costs ASSEMBLY ppc)
  letin code_memory ≝ (load_code_memory assembled)
  letin preamble ≝ (\fst program)
  letin data_labels ≝ (construct_datalabels preamble)
- letin lookup_labels ≝ (λx. sigma program (address_of_word_labels_code_mem (\snd program) x))
+ letin lookup_labels ≝ (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x))
  letin lookup_datalabels ≝ (λx. lookup ? ? x data_labels (zero ?))
- whd in ⊢ (% → %) generalize in match (assembly_ok program assembled) >BUILD_MAPS #XX generalize in match (XX ASSEMBLY ppc) -XX;
+ whd in ⊢ (% → %) generalize in match (assembly_ok program pol assembled) >BUILD_MAPS #XX generalize in match (XX ASSEMBLY ppc) -XX;
  cases (fetch_pseudo_instruction (\snd program) ppc) #pi #newppc
- generalize in match (fetch_assembly_pseudo program ppc
-  (λx. sigma program (address_of_word_labels_code_mem (\snd program) x)) (λx. lookup ?? x data_labels (zero ?)) pi
+ generalize in match (fetch_assembly_pseudo program pol ppc
+  (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) (λx. lookup ?? x data_labels (zero ?)) pi
   (load_code_memory assembled));
  whd in ⊢ ((∀_.∀_.∀_.∀_.%) → (∀_.∀_.%) → % → %) #H1 #H2 * #instructions #EXPAND
  whd in H1:(∀_.∀_.∀_.∀_.? → ???% → ?) H2:(∀_.∀_.???% → ?);
  normalize nodelta in EXPAND; (* HERE *)
- generalize in match (λlen, assembled.H1 len assembled instructions (nat_of_bitvector … (sigma program ppc))) -H1; #H1
+ generalize in match (λlen, assembled.H1 len assembled instructions (nat_of_bitvector … (sigma program pol ppc))) -H1; #H1
  >bitvector_of_nat_nat_of_bitvector in H1; #H1
  <EXPAND in H1 H2; whd in ⊢ ((∀_.∀_.? → ???% → ?) → (∀_.∀_.???% → ?) → ?)
@@ -943 +943 @@
 
 axiom low_internal_ram_of_pseudo_internal_ram_hit:
- ∀M:internal_pseudo_address_map.∀s:PseudoStatus.∀addr:BitVector 7.
+ ∀M:internal_pseudo_address_map.∀s:PseudoStatus.∀pol:policy (code_memory … s).∀addr:BitVector 7.
   member ? (eq_bv 8) (false:::addr) M = true →
    let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in 
@@ -950 +950 @@
    let bl ≝ lookup ? 7 addr ram (zero 8) in
    let bu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) ram (zero 8) in
-    bu@@bl = sigma (code_memory … s) (pbu@@pbl).
+    bu@@bl = sigma (code_memory … s) pol (pbu@@pbl).
 
 (* changed from add to sub *)
@@ -1033 +1033 @@
     
 definition status_of_pseudo_status:
- internal_pseudo_address_map → PseudoStatus → option Status ≝
- λM,ps.
+ internal_pseudo_address_map → ∀ps:PseudoStatus. policy (code_memory … ps) → option Status ≝
+ λM,ps,pol.
   let pap ≝ code_memory … ps in
-   match assembly pap with
+   match assembly pap pol with
     [ None ⇒ None …
     | Some p ⇒
        let cm ≝ load_code_memory (\fst p) in
-       let pc ≝ sigma pap (program_counter ? ps) in
+       let pc ≝ sigma pap pol (program_counter ? ps) in
        let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in
        let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in
@@ -1156 +1156 @@
  ∀M:internal_pseudo_address_map.
  ∀ps,ps': PseudoStatus.
-  code_memory … ps = code_memory … ps' →
-   match status_of_pseudo_status M ps with
-    [ None ⇒ status_of_pseudo_status M ps' = None …
-    | Some _ ⇒ ∃w. status_of_pseudo_status M ps' = Some … w
+ ∀pol.
+  ∀prf:code_memory … ps = code_memory … ps'.
+   let pol' ≝ ? in
+   match status_of_pseudo_status M ps pol with
+    [ None ⇒ status_of_pseudo_status M ps' pol' = None …
+    | Some _ ⇒ ∃w. status_of_pseudo_status M ps' pol' = Some … w
     ].
- #M #ps #ps' #H whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
- generalize in match (refl … (assembly (code_memory … ps)))
- cases (assembly ?) in ⊢ (???% → %)
+ [2: <prf @pol]
+ #M #ps #ps' #pol #H normalize nodelta; whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
+ generalize in match (refl … (assembly (code_memory … ps) pol))
+ cases (assembly ??) in ⊢ (???% → %)
   [ #K whd whd in ⊢ (??%?) <H >K %
   | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
 qed.
 
-definition ticks_of0: pseudo_assembly_program → Word → ? → nat × nat ≝
-  λprogram: pseudo_assembly_program.
+definition ticks_of0: ∀p:pseudo_assembly_program. policy p → Word → ? → nat × nat ≝
+  λprogram: pseudo_assembly_program.λpol.
   λppc: Word.
   λfetched.
@@ -1176 +1179 @@
       match instr with
       [ JC lbl ⇒
-        match jump_expansion ppc program with
+        match pol ppc with
         [ short_jump ⇒ 〈2, 2〉
         | medium_jump ⇒ ?
@@ -1182 +1185 @@
         ]
       | JNC lbl ⇒
-        match jump_expansion ppc program with
+        match pol ppc with
         [ short_jump ⇒ 〈2, 2〉
         | medium_jump ⇒ ?
@@ -1188 +1191 @@
         ]
       | JB bit lbl ⇒
-        match jump_expansion ppc program with
+        match pol ppc with
         [ short_jump ⇒ 〈2, 2〉
         | medium_jump ⇒ ?
@@ -1194 +1197 @@
         ]
       | JNB bit lbl ⇒
-        match jump_expansion ppc program with
+        match pol ppc with
         [ short_jump ⇒ 〈2, 2〉
         | medium_jump ⇒ ?
@@ -1200 +1203 @@
         ]
       | JBC bit lbl ⇒
-        match jump_expansion ppc program with
+        match pol ppc with
         [ short_jump ⇒ 〈2, 2〉
         | medium_jump ⇒ ?
@@ -1206 +1209 @@
         ]
       | JZ lbl ⇒
-        match jump_expansion ppc program with
+        match pol ppc with
         [ short_jump ⇒ 〈2, 2〉
         | medium_jump ⇒ ?
@@ -1212 +1215 @@
         ]
       | JNZ lbl ⇒
-        match jump_expansion ppc program with
+        match pol ppc with
         [ short_jump ⇒ 〈2, 2〉
         | medium_jump ⇒ ?
@@ -1218 +1221 @@
         ]
       | CJNE arg lbl ⇒
-        match jump_expansion ppc program with
+        match pol ppc with
         [ short_jump ⇒ 〈2, 2〉
         | medium_jump ⇒ ?
@@ -1224 +1227 @@
         ]
       | DJNZ arg lbl ⇒
-        match jump_expansion ppc program with
+        match pol ppc with
         [ short_jump ⇒ 〈2, 2〉
         | medium_jump ⇒ ?
@@ -1323 +1326 @@
 qed.
 
-definition ticks_of: pseudo_assembly_program → Word → nat × nat ≝
-  λprogram: pseudo_assembly_program.
+definition ticks_of: ∀p:pseudo_assembly_program. policy p → Word → nat × nat ≝
+  λprogram: pseudo_assembly_program.λpol.
   λppc: Word.
     let 〈preamble, pseudo〉 ≝ program in
     let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc in
-     ticks_of0 program ppc fetched.
+     ticks_of0 program pol ppc fetched.
 
 lemma get_register_set_program_counter: