Changeset 1950 for src/ASM/Policy.ma

Timestamp:

May 15, 2012, 6:20:31 PM (8 years ago)

Author:

boender

Message:

• advances in policy

File:

• src/ASM/Policy.ma (modified) (21 diffs)

src/ASM/Policy.ma

@@ -39 +39 @@
   
 definition is_jump ≝
-  λx:labelled_instruction.
-  let 〈label,instr〉 ≝ x in
+  λinstr:pseudo_instruction.
   match instr with
   [ Instruction i   ⇒ is_jump' i
@@ -67 +66 @@
   ].
   
-(*definition jump_in_policy: list labelled_instruction → ppc_pc_map → Prop ≝
+definition jump_not_in_policy: list labelled_instruction → ppc_pc_map → Prop ≝
   λprefix.λsigma.
   ∀i:ℕ.i < |prefix| →
-  iff (is_jump (nth i ? prefix 〈None ?, Comment []〉))
-   (∃x:jump_length.
-   \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,None ?〉) = Some ? x).*)
+  ¬is_jump (\snd (nth i ? prefix 〈None ?, Comment []〉)) → 
+  \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,short_jump〉) = short_jump.
 
 (* if the instruction 〈p,a〉 is a jump to label l, then label l is at address a *)
@@ -122 +120 @@
    let 〈opc,oj〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd op) 〈0,short_jump〉 in
    let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,short_jump〉 in
-     opc ≤ pc ∧ jmpleq oj j.
+     (*opc ≤ pc ∧*) jmpleq oj j.
 
 (* Policy safety *)
@@ -307 +305 @@
     (bitvector_of_nat 16 (\fst sigma)) (\snd x)))
   0.
-
+  
 (* The function that creates the label-to-address map *)
 definition create_label_map: ∀program:list labelled_instruction.
   (Σlabels:label_map.
-    ∀i:ℕ.lt i (|program|) →
     ∀l.occurs_exactly_once ?? l program →
-    is_label (nth i ? program 〈None ?, Comment [ ]〉) l →
-    lookup ?? labels l = Some ? i 
+    bitvector_of_nat ? (lookup_def ?? labels l 0) =
+     address_of_word_labels_code_mem program l
   ) ≝
  λprogram.
    \fst (create_label_cost_map program).
- #i #Hi #l #Hl1 #Hl2 lapply (pi2 ?? (create_label_cost_map program)) @pair_elim
- #labels #costs #EQ normalize nodelta #H @(H i Hi l Hl1 Hl2)
+ #l #Hl lapply (pi2 ?? (create_label_cost_map program)) @pair_elim
+ #labels #costs #EQ normalize nodelta #H @(H l Hl)
 qed.
 
@@ -388 +385 @@
 
 lemma dec_is_jump: ∀x.Sum (is_jump x) (¬is_jump x).
-#x cases x #l #i cases i
+#i cases i
 [#id cases id
  [1,2,3,6,7,33,34:
@@ -408 +405 @@
 qed.
 
-(*lemma jump_not_in_policy: ∀prefix:list labelled_instruction.
- ∀policy:(Σp:ppc_pc_map.
- out_of_program_none prefix p ∧ jump_in_policy prefix p).
-  ∀i:ℕ.i < |prefix| →
-  iff (¬is_jump (nth i ? prefix 〈None ?, Comment []〉))
-  (\snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd policy) 〈0,None ?〉) = None ?).
- #prefix #policy #i #Hi @conj
-[ #Hnotjmp lapply (refl ? (bvt_lookup … (bitvector_of_nat 16 i) (\snd policy) 〈0,None ?〉))
-  cases (bvt_lookup … (bitvector_of_nat 16 i) (\snd policy) 〈0,None ?〉) in ⊢ (???% → ?);
-  #pc #j cases j
-  [ #H >H @refl
-  | #x #H >H @⊥ @(absurd ? ? Hnotjmp) @(proj2 ?? (proj2 ?? (pi2 ?? policy) i Hi))
-    >H @(ex_intro ?? x ?) / by /
-  ]
-| #Hnone @nmk #Hj lapply (proj1 ?? (proj2 ?? (pi2 ?? policy) i Hi) Hj)
-  #H elim H -H; #x #H >H in Hnone; #abs destruct (abs)
-]  
-qed.*)
-
 (* The first step of the jump expansion: everything to short.
  * The third condition of the dependent type implies jump_in_policy;
@@ -438 +416 @@
     | Some p ⇒
        And (And (out_of_program_none (pi1 ?? program) p)
-       (policy_isize_sum (pi1 ?? program) labels p))
+       (jump_not_in_policy (pi1 ?? program) p))
        (\fst p < 2^16)
     ] ≝ 
@@ -445 +423 @@
   (λprefix.Σpolicy:ppc_pc_map.
     And (out_of_program_none prefix policy)
-    (policy_isize_sum prefix labels policy))
+    (jump_not_in_policy prefix policy))
   program
   (λprefix.λx.λtl.λprf.λp.
@@ -560 +538 @@
         ]
       ]
-| cases daemon
+| (* jump_not_in_policy *) #i >append_length <commutative_plus
+  #Hi normalize in Hi; cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
+  [ cases p -p #p cases p -p #pc #sigma #Hp cases x #l #ins cases ins
+    [ #pi cases pi normalize nodelta
+      [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
+        [1,2,3,6,7,24,25: #x #y
+        |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] >lookup_insert_miss
+        [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55:
+          >(nth_append_first ? i prefix ?? Hi) @((proj2 ?? Hp) i Hi)
+        |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
+          @bitvector_of_nat_abs
+          [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82:
+            @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus
+            @le_plus_a @Hi
+          |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83:
+            @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S
+            @le_plus_n_r
+          |3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84:
+            @lt_to_not_eq @Hi
+          ]
+        ]
+      |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] >lookup_insert_miss
+        [1,3,5,7,9,11,13,15,17:
+          >(nth_append_first ? i prefix ?? Hi) @((proj2 ?? Hp) i Hi)
+        |2,4,6,8,10,12,14,16,18:
+          @bitvector_of_nat_abs
+          [1,4,7,10,13,16,19,22,25:
+            @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus
+            @le_plus_a @Hi
+          |2,5,8,11,14,17,20,23,26:
+            @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S
+            @le_plus_n_r
+          |3,6,9,12,15,18,21,24,27:
+            @lt_to_not_eq @Hi
+          ]
+        ]
+      ]
+    |2,3,4,5,6: #x [5: #y] >lookup_insert_miss
+      [1,3,5,7,9:
+        >(nth_append_first ? i prefix ?? Hi) @((proj2 ?? Hp) i Hi)
+      |2,4,6,8,10:
+        @bitvector_of_nat_abs
+        [1,4,7,10,13:
+          @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus
+          @le_plus_a @Hi
+        |2,5,8,11,14:
+          @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S
+          @le_plus_n_r
+        |3,6,9,12,15:
+          @lt_to_not_eq @Hi
+        ]
+      ]
+    ]
+  | >Hi >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????);
+    cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #ins cases ins
+    normalize nodelta
+    [2,3,6: #x [3: #y] >lookup_insert_hit #_ / by /
+    |4,5: #x #H @⊥ cases H #H2 @H2 / by I/
+    |1: #pi cases pi
+      [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
+        [1,2,3,6,7,24,25: #x #y
+        |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
+        #_ >lookup_insert_hit / by /
+      |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
+        #H @⊥ cases H #H2 @H2 / by I/
+      ]
+    ]
+  ]
 ]
 | @conj
   [ #i #_ #Hi2 / by refl/
-  | whd in match policy_isize_sum; normalize nodelta 
-    cases daemon
+  | #i #H @⊥ @(absurd … H) @not_le_Sn_O
   ]
 ]
@@ -576 +620 @@
     let pc1 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉 in
     let pc2 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉 in
-    pc1 = pc2).
+    \snd pc1 = \snd pc2).
     
 (*definition nec_plus_ultra ≝
@@ -588 +632 @@
 include alias "basics/logic.ma".
 
+lemma blerpque: ∀a,b,i.
+  is_jump i → instruction_size_jmplen (max_length a b) i = instruction_size_jmplen a i →
+  (max_length a b) = a.
+ #a #b #i cases i
+ [1: #pi cases pi
+   [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
+     [1,2,3,6,7,24,25: #x #y
+     |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
+     #H cases H
+   |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
+     #_ cases a cases b
+     [1,5,7,8,9: #_ / by refl/
+     |10,14,16,17,18: #_ / by refl/
+     |19,23,25,26,27: #_ / by refl/
+     |28,32,34,35,36: #_ / by refl/
+     |37,41,43,44,45: #_ / by refl/
+     |46,50,52,53,54: #_ / by refl/
+     |55,59,61,62,63: #_ / by refl/
+     |64,68,70,71,72: #_ / by refl/
+     |73,77,79,80,81: #_ / by refl/
+     |2,3,4,6: cases x #a cases a
+       [1,2,3,4,8,9,16,17,18,19: #b #Hb cases Hb
+       |20,21,22,23,27,28,35,36,37,38: #b #Hb cases Hb
+       |39,40,41,42,46,47,54,55,56,57: #b #Hb cases Hb
+       |58,59,60,61,65,66,73,74,75,76: #b #Hb cases Hb
+       |5,6,7,10,11,12,13,14: #Hb cases Hb
+       |24,25,26,29,30,31,32,33: #Hb cases Hb
+       |43,44,45,48,49,50,51,52: #Hb cases Hb
+       |62,63,64,67,68,69,70,71: #Hb cases Hb
+       |15,34,53,72: #b #Hb #H normalize in H; destruct (H)
+       ]
+     |11,12,13,15: cases x #a cases a
+       [1,2,3,4,8,9,16,17,18,19: #b #Hb cases Hb
+       |20,21,22,23,27,28,35,36,37,38: #b #Hb cases Hb
+       |39,40,41,42,46,47,54,55,56,57: #b #Hb cases Hb
+       |58,59,60,61,65,66,73,74,75,76: #b #Hb cases Hb
+       |5,6,7,10,11,12,13,14: #Hb cases Hb
+       |24,25,26,29,30,31,32,33: #Hb cases Hb
+       |43,44,45,48,49,50,51,52: #Hb cases Hb
+       |62,63,64,67,68,69,70,71: #Hb cases Hb
+       |15,34,53,72: #b #Hb #H normalize in H; destruct (H)
+       ]
+     |20,21,22,24: cases x #a cases a
+       [1,2,3,4,8,9,16,17,18,19: #b #Hb cases Hb
+       |20,21,22,23,27,28,35,36,37,38: #b #Hb cases Hb
+       |39,40,41,42,46,47,54,55,56,57: #b #Hb cases Hb
+       |58,59,60,61,65,66,73,74,75,76: #b #Hb cases Hb
+       |5,6,7,10,11,12,13,14: #Hb cases Hb
+       |24,25,26,29,30,31,32,33: #Hb cases Hb
+       |43,44,45,48,49,50,51,52: #Hb cases Hb
+       |62,63,64,67,68,69,70,71: #Hb cases Hb
+       |15,34,53,72: #b #Hb #H normalize in H; destruct (H)
+       ]
+     |29,30,31,33: cases x #a cases a #a1 #a2
+       [1,3,5,7: cases a2 #b cases b
+         [2,3,4,9,15,16,17,18,19: #b #Hb cases Hb
+         |21,22,23,28,34,35,36,37,38: #b #Hb cases Hb
+         |40,41,42,47,53,54,55,56,57: #b #Hb cases Hb
+         |59,60,61,66,72,73,74,75,76: #b #Hb cases Hb
+         |5,6,7,10,11,12,13,14: #Hb cases Hb
+         |24,25,26,29,30,31,32,33: #Hb cases Hb
+         |43,44,45,48,49,50,51,52: #Hb cases Hb
+         |62,63,64,67,68,69,70,71: #Hb cases Hb
+         |1,8: #b #Hb #H normalize in H; destruct (H)
+         |20,27: #b #Hb #H normalize in H; destruct (H)
+         |39,46: #b #Hb #H normalize in H; destruct (H)
+         |58,65: #b #Hb #H normalize in H; destruct (H)
+         ]
+       |2,4,6,8: cases a1 #b cases b
+         [1,3,8,9,15,16,17,18,19: #b #Hb cases Hb
+         |20,22,27,28,34,35,36,37,38: #b #Hb cases Hb
+         |39,41,46,47,53,54,55,56,57: #b #Hb cases Hb
+         |58,60,65,66,72,73,74,75,76: #b #Hb cases Hb
+         |5,6,7,10,11,12,13,14: #Hb cases Hb
+         |24,25,26,29,30,31,32,33: #Hb cases Hb
+         |43,44,45,48,49,50,51,52: #Hb cases Hb
+         |62,63,64,67,68,69,70,71: #Hb cases Hb
+         |2,4: #b #Hb #H normalize in H; destruct (H)
+         |21,23: #b #Hb #H normalize in H; destruct (H)
+         |40,42: #b #Hb #H normalize in H; destruct (H)
+         |59,61: #b #Hb #H normalize in H; destruct (H)
+         ]
+       ]
+     |38,39,40,42: cases x #a cases a
+       [2,3,8,9,15,16,17,18,19: #b #Hb cases Hb
+       |21,22,27,28,34,35,36,37,38: #b #Hb cases Hb
+       |40,41,46,47,53,54,55,56,57: #b #Hb cases Hb
+       |59,60,65,66,72,73,74,75,76: #b #Hb cases Hb
+       |5,6,7,10,11,12,13,14: #Hb cases Hb
+       |24,25,26,29,30,31,32,33: #Hb cases Hb
+       |43,44,45,48,49,50,51,52: #Hb cases Hb
+       |62,63,64,67,68,69,70,71: #Hb cases Hb
+       |1,4: #b #Hb #H normalize in H; destruct (H)
+       |20,23: #b #Hb #H normalize in H; destruct (H)
+       |39,42: #b #Hb #H normalize in H; destruct (H)
+       |58,61: #b #Hb #H normalize in H; destruct (H)
+       ]
+     |47,48,49,51: cases x #a #H normalize in H; destruct (H)
+     |56,57,58,60: cases x #a #H normalize in H; destruct (H) 
+     |65,66,67,69: cases x #a #H normalize in H; destruct (H)
+     |74,75,76,78: cases x #a #H normalize in H; destruct (H)
+     ]
+   ]
+  |2,3,6: #x [3: #y] #H cases H
+  |4,5: #id #_ cases a cases b
+    [2,3,4,6,11,12,13,15: normalize #H destruct (H)
+    |1,5,7,8,9,10,14,16,17,18: #H / by refl/
+    ]
+  ]
+qed. 
+
+lemma etblorp: ∀a,b,i.is_jump i → 
+  instruction_size_jmplen a i ≤ instruction_size_jmplen (max_length a b) i.
+ #a #b #i cases i
+ [2,3,6: #x [3: #y] #H cases H
+ |4,5: #id #_ cases a cases b / by le_n/
+ |1: #pi cases pi
+   [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
+     [1,2,3,6,7,24,25: #x #y
+     |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
+     #H cases H
+   |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
+     #_ cases a cases b
+     [2,3: cases x #ad cases ad
+       [15,34: #b #Hb / by le_n/
+       |1,2,3,4,8,9,16,17,18,19,20,21,22,23,27,28,35,36,37,38: #b] #Hb cases Hb
+     |1,4,5,6,7,8,9: / by le_n/
+     |11,12: cases x #ad cases ad
+       [15,34: #b #Hb / by le_n/
+       |1,2,3,4,8,9,16,17,18,19,20,21,22,23,27,28,35,36,37,38: #b] #Hb cases Hb
+     |10,13,14,15,16,17,18: / by le_n/
+     |20,21: cases x #ad cases ad
+       [15,34: #b #Hb / by le_n/
+       |1,2,3,4,8,9,16,17,18,19,20,21,22,23,27,28,35,36,37,38: #b] #Hb cases Hb
+     |19,22,23,24,25,26,27: / by le_n/
+     |29,30: cases x #ad cases ad #a1 #a2
+       [ cases a2 #ad2 cases ad2
+       ]
+     ]
+   ]
+ ]
+ cases daemon (* XXX see if it works first *)
+qed.
+
+lemma minus_zero_to_le: ∀n,m:ℕ.n - m = 0 → n ≤ m.
+ #n
+ elim n
+ [ #m #_ @le_O_n
+ | #n' #Hind #m cases m
+   [ #H -n whd in match (minus ??) in H; >H @le_n
+   | #m' -m #H whd in match (minus ??) in H; @le_S_S @Hind @H
+   ]
+ ]
+qed.
+
+lemma plus_zero_zero: ∀n,m:ℕ.n + m = 0 → m = 0.
+ #n #m #Hn @sym_eq @le_n_O_to_eq <Hn >commutative_plus @le_plus_n_r
+qed.
+
 (* One step in the search for a jump expansion fixpoint. *)
 definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
@@ -596 +799 @@
   ∀old_policy:(Σpolicy:ppc_pc_map.
     And (And (out_of_program_none program policy)
-    (policy_isize_sum program labels policy))
+    (jump_not_in_policy program policy))
     (\fst policy < 2^16)).
   (Σx:bool × (option ppc_pc_map).
@@ -602 +805 @@
     match y with
     [ None ⇒ (* nec_plus_ultra program old_policy *) True
-    | Some p ⇒ And (And (And (And (And (out_of_program_none (pi1 ?? program) p)
-       (policy_isize_sum program labels p))
+    | Some p ⇒ And (And (And (And (And (out_of_program_none program p)
+       (jump_not_in_policy program p))
        (policy_increase program old_policy p))
        (policy_compact program labels p))
@@ -616 +819 @@
       let 〈added,policy〉 ≝ x in
       And (And (And (And (out_of_program_none prefix policy)
-      (policy_isize_sum prefix labels policy)) 
+      (jump_not_in_policy prefix policy)) 
       (policy_increase prefix old_sigma policy))
       (policy_compact prefix labels policy))
@@ -666 +869 @@
   ]
 | lapply (pi2 ?? acc) >p cases inc_pc_sigma #inc_pc #inc_sigma
-  cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉)
-  #old_pc #old_length #Hpolicy @pair_elim #added #policy normalize nodelta
+  lapply (refl ? (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉))
+  cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉) in ⊢ (???% → %);
+  #old_pc #old_length #Holdeq #Hpolicy @pair_elim #added #policy normalize nodelta
   @pair_elim #new_length #isize normalize nodelta #Heq1 #Heq2
   @conj [ @conj [ @conj [ @conj
@@ -681 +885 @@
       ]
     ]
-  | cases daemon (* XXX *)
+  | (* jump_not_in_policy *) #i >append_length <commutative_plus #Hi normalize in Hi;
+    cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
+    [ <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
+      [ >(nth_append_first ? i prefix ?? Hi)
+        @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i Hi)
+      | @bitvector_of_nat_abs
+        [ @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus
+          @le_plus_a @Hi
+        | @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S
+          @le_plus_n_r
+        | @lt_to_not_eq @Hi
+        ]
+      ]
+    | >Hi <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_hit
+      >nth_append_second
+      [ <minus_n_n whd in match (nth ????); cases instr in Heq1;
+        [4,5: #x #_ #H cases H #H2 @⊥ @H2 / by I/
+        |2,3,6: #x [3: #y] #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ / by /
+        |1: #pi cases pi
+          [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
+            [1,2,3,6,7,24,25: #x #y
+            |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] #Heq1
+              <(proj1 ?? (pair_destruct ?????? Heq1)) #_ / by /
+          |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] 
+            #_ #H @⊥ cases H #H2 @H2 / by I/
+          ]
+        ]
+      | @le_n
+      ]
+    ]
   ]
   | (* policy_increase *) #i >append_length >commutative_plus #Hi normalize in Hi;
-    cases (le_to_or_lt_eq … Hi) -Hi; #Hi
-    [ lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)) i (le_S_S_to_le … Hi))
+    cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi; #Hi
+    [ lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)) i Hi)
       <(proj2 ?? (pair_destruct ?????? Heq2))     
       @pair_elim #opc #oj #EQ1 >lookup_insert_miss
@@ -691 +924 @@
       | @bitvector_of_nat_abs
         [ @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus @le_plus_a
-          @(le_S_S_to_le … Hi)
+          @Hi
         | @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
-        | @lt_to_not_eq @(le_S_S_to_le … Hi)
+        | @lt_to_not_eq @Hi
         ]
       ]
-    | <(proj2 ?? (pair_destruct ?????? Heq2)) >(injective_S … Hi) >lookup_insert_hit
-      cases instr in Heq1 Heq2;
-      [2,3,6: #x [3: #y] normalize nodelta #Heq1 #Heq2 <(proj1 ?? (pair_destruct ?????? Heq1))
-      cases daemon
-      |1,4,5: cases daemon
-      ]
-    ]
-  ]
-  | (* policy_compact *) cases daemon
-  ]
-  | (* added = 0 → policy_equal *) cases daemon
-  ]
+    | >Hi <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_hit
+      cases (dec_is_jump instr)
+      [ cases instr in Heq1; normalize nodelta
+        [ #pi cases pi
+          [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
+            [1,2,3,6,7,24,25: #x #y
+            |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] #_ #Hj cases Hj
+          |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
+            whd in match jump_expansion_step_instruction; normalize nodelta #Heq1
+            <(proj1 ?? (pair_destruct ?????? Heq1)) #_ >Holdeq normalize nodelta
+            @jmpleq_max_length
+          ]
+        |2,3,6: #x [3: #y] #_ #Hj cases Hj
+        |4,5: #x #Heq1 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) >Holdeq normalize nodelta
+          @jmpleq_max_length
+        ]
+      | lapply Heq1 -Heq1; lapply (refl ? instr); cases instr in ⊢ (???% → %); normalize nodelta
+        [ #pi cases pi
+          [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
+            [1,2,3,6,7,24,25: #x #y
+            |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
+            whd in match jump_expansion_step_instruction; normalize nodelta #Heqi #Heq1
+            #Hj <(proj1 ?? (pair_destruct ?????? Heq1))
+            lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ??)
+            [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82:
+              >prf >nth_append_second
+              [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55:
+                <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj
+              |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
+                @le_n
+              ]
+            |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83:
+              >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
+            |3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84:
+              cases (lookup ?? (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉)
+              #a #b #H >H normalize nodelta %2 @refl
+            ]
+          |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
+            #_ #_ #abs cases abs #ABS @⊥ @ABS / by I/
+          ]
+        |2,3,6: #x [3: #y] #Heqi #Heq1 #Hj <(proj1 ?? (pair_destruct ?????? Heq1))
+          lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ??)
+          [1,4,7: >prf >nth_append_second
+            [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj
+            |2,4,6: @le_n
+            ]
+          |2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
+          |3,6,9: cases (lookup ?? (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉)
+            #a #b #H >H normalize nodelta %2 @refl
+          ]
+        |4,5: #x #_ #_ #abs cases abs #ABS @⊥ @ABS / by I/
+        ]
+      ]
+    ]
+  ]
+  | (* policy_compact *) (*XXX*) cases daemon
+  ]
+  | (* added = 0 → policy_equal *) lapply (proj2 ?? Hpolicy)
+    lapply Heq2 -Heq2 lapply Heq1 -Heq1 lapply (refl ? instr)
+    cases instr in ⊢ (???% → % → % → %); normalize nodelta
+    [ #pi cases pi normalize nodelta
+      [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
+        [1,2,3,6,7,24,25: #x #y
+        |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
+        #Hins #Heq1 #Heq2 #Hold <(proj1 ?? (pair_destruct ?????? Heq2)) #Hadded
+        #i >append_length >commutative_plus #Hi normalize in Hi;
+        cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
+        [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55:
+          <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
+          [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55:
+            @(Hold Hadded i Hi)
+          |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
+            @bitvector_of_nat_abs
+            [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82:
+              @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus
+              @le_plus_a @Hi
+            |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83:
+              @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S
+              @le_plus_n_r
+            |3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84:
+              @lt_to_not_eq @Hi
+            ]
+          ]
+        |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
+           <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit
+           lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ??)
+           [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82:
+             >prf >nth_append_second
+             [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55:
+               <minus_n_n whd in match (nth ????); >p1 >Hins @nmk #H @H
+             |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
+               @le_n
+             ]
+           |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83:
+             >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
+           |3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84:
+             cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉)
+             #a #b #H >H <(proj1 ?? (pair_destruct ?????? Heq1)) normalize nodelta @refl
+           ]
+         ]
+       |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Hins #Heq1 #Heq2 #Hold
+         <(proj1 ?? (pair_destruct ?????? Heq2)) <(proj2 ?? (pair_destruct ?????? Heq1))
+         #H #i >append_length >commutative_plus #Hi normalize in Hi;
+         cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
+         [1,3,5,7,9,11,13,15,17: <(proj2 ?? (pair_destruct ?????? Heq2))
+           >lookup_insert_miss
+           [1,3,5,7,9,11,13,15,17: @(Hold ? i Hi)
+             [1,2,3,4,5,6,7,8,9: @sym_eq @le_n_O_to_eq <H @le_plus_n_r]
+           ]
+           @bitvector_of_nat_abs
+           [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf
+             >append_length >commutative_plus @le_plus_a @Hi
+           |2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf
+             >append_length <plus_n_Sm @le_S_S
+           |3,6,9,12,15,18,21,24,27: @lt_to_not_eq @Hi
+           ] @le_plus_n_r
+         |2,4,6,8,10,12,14,16,18: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi
+           >lookup_insert_hit <(proj1 ?? (pair_destruct ?????? Heq1))
+           >Holdeq normalize nodelta @sym_eq @blerpque
+           [3,6,9,12,15,18,21,24,27:
+             elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … H)))
+             [1,3,5,7,9,11,13,15,17: #H @⊥ @(absurd ? H) @le_to_not_lt @etblorp
+             |2,4,6,8,10,12,14,16,18: #H @H
+             ]
+             / by I/
+           |2,5,8,11,14,17,20,23,26: / by I/
+           ]
+         ]
+       ]
+     |2,3,6: #x [3: #y] #Hins #Heq1 #Heq2 #Hold <(proj1 ?? (pair_destruct ?????? Heq2))
+       #Hadded #i >append_length >commutative_plus #Hi normalize in Hi;
+       cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
+       [1,3,5: <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
+         [1,3,5: @(Hold Hadded i Hi)
+         |2,4,6: @bitvector_of_nat_abs
+           [1,4,7: @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus
+             @le_plus_a @Hi
+           |2,5,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S
+             @le_plus_n_r
+           |3,6,9: @lt_to_not_eq @Hi
+           ]
+         ]
+       |2,4,6: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit
+         lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ??)
+         [1,4,7: >prf >nth_append_second
+           [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Hins @nmk #H @H
+           |2,4,6: @le_n
+           ]
+         |2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
+         |3,6,9: cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉)
+           #a #b #H >H <(proj1 ?? (pair_destruct ?????? Heq1)) normalize nodelta @refl
+         ]
+       ]
+     |4,5: #x #Hins #Heq1 #Heq2 #Hold
+       <(proj1 ?? (pair_destruct ?????? Heq2)) <(proj2 ?? (pair_destruct ?????? Heq1))
+       #H #i >append_length >commutative_plus #Hi normalize in Hi;
+       cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
+       [1,3: <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
+         [1,3: @(Hold ? i Hi)
+           [1,2: @sym_eq @le_n_O_to_eq <H @le_plus_n_r]
+         ]
+         @bitvector_of_nat_abs
+         [1,4: @(transitive_lt … (pi2 ?? program)) >prf
+           >append_length >commutative_plus @le_plus_a @Hi
+         |2,5: @(transitive_lt … (pi2 ?? program)) >prf
+           >append_length <plus_n_Sm @le_S_S
+         |3,6: @lt_to_not_eq @Hi
+         ] @le_plus_n_r
+         |2,4: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit
+           <(proj1 ?? (pair_destruct ?????? Heq1))>Holdeq normalize nodelta
+           @sym_eq @blerpque
+           [3,6: elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … H)))
+             [1,3: #H @⊥ @(absurd ? H) @le_to_not_lt @etblorp
+             |2,4: #H @H
+             ]
+             / by I/
+           |2,5: / by I/
+           ]
+         ]
+       ]
+     ]
 | normalize nodelta @conj [ @conj [ @conj [ @conj
   [ #i #Hi / by refl/
@@ -716 +1118 @@
 ]
 qed.
+
      
 (* old proof | lapply (pi2 ?? acc) >p #Hpolicy normalize nodelta in Hpolicy;
@@ -1665 +2068 @@
 qed.
 
-include alias "arithmetics/nat.ma".
+nclude alias "arithmetics/nat.ma".
 include alias "basics/logic.ma".
 
@@ -1672 +2075 @@
 (* The glue between Policy and Assembly. *)
 definition jump_expansion':
- ∀program:preamble × (Σl:list labelled_instruction.|l| < 2^16).
-  option (Σsigma:Word → Word × bool.
+∀program:preamble × (Σl:list labelled_instruction.|l| < 2^16).
+ option (Σsigma:Word → Word × bool.
    ∀ppc: Word.
    let pc ≝ \fst (sigma ppc) in
@@ -1687 +2090 @@
       ∨
        (nat_of_bitvector … ppc = |\snd program| → next_pc = (zero …)))).
+≝ λprogram.
+  let policy ≝ pi1 … (je_fixpoint (\snd program)) in
+  match policy with
+  [ None ⇒ None ?
+  | Some x ⇒ Some ?
+      «λppc.let 〈pc,jl〉 ≝ bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉 in
+        〈bitvector_of_nat 16 pc,jmpeqb jl long_jump〉,?»
+  ].
  cases daemon
 qed.