include "ASM/ASM.ma".
include "ASM/Arithmetic.ma".
include "ASM/Fetch.ma".
include "ASM/Status.ma".
include alias "basics/logic.ma".
include alias "arithmetics/nat.ma".
include "utilities/extralib.ma". 
include "ASM/Assembly.ma".

(* Internal types *)

(* label_map: identifier ↦ 〈instruction number, address〉 *)
definition label_map ≝ identifier_map ASMTag (ℕ × ℕ).

(* jump_expansion_policy: instruction number ↦ 〈pc, addr, jump_length〉 *)
definition jump_expansion_policy ≝ BitVectorTrie (ℕ × ℕ × jump_length) 16.

(* The different properties that we want/need to prove at some point *)
(* Anything that's not in the program doesn't end up in the policy *)
definition out_of_program_none ≝
  λprefix:list labelled_instruction.λpolicy:jump_expansion_policy.
  ∀i.i ≥ |prefix| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) policy = None ?.

(* If instruction i is a jump, then there will be something in the policy at
 * position i *)
definition is_jump' ≝
  λx:preinstruction Identifier.
  match x with
  [ JC _ ⇒ True
  | JNC _ ⇒ True
  | JZ _ ⇒ True
  | JNZ _ ⇒ True
  | JB _ _ ⇒ True
  | JNB _ _ ⇒ True
  | JBC _ _ ⇒ True
  | CJNE _ _ ⇒ True
  | DJNZ _ _ ⇒ True
  | _ ⇒ False
  ].
  
definition is_jump ≝
  λx:labelled_instruction.
  let 〈label,instr〉 ≝ x in
  match instr with
  [ Instruction i   ⇒ is_jump' i
  | Call _ ⇒ True
  | Jmp _ ⇒ True
  | _ ⇒ False
  ].

definition jump_in_policy ≝
  λprefix:list labelled_instruction.λpolicy:jump_expansion_policy.
  ∀i:ℕ.i < |prefix| →
  (is_jump (nth i ? prefix 〈None ?, Comment []〉) ↔
   ∃p,a,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,a,j〉).

definition labels_okay ≝
  λlabels:label_map.λpolicy:jump_expansion_policy.
  bvt_forall ?? policy (λn.λx.let 〈pc,addr_nat,i〉 ≝ x in
    ∃id:Identifier.
      \snd (lookup_def … labels id 〈0,pc〉) = addr_nat
  ).
  
(* Between two policies, jumps cannot decrease *)
definition jmple: jump_length → jump_length → Prop ≝
  λj1.λj2.
  match j1 with
  [ short_jump  ⇒ 
    match j2 with
    [ short_jump ⇒ False
    | _          ⇒ True
    ]
  | medium_jump ⇒
    match j2 with
    [ long_jump ⇒ True
    | _         ⇒ False
    ]
  | long_jump   ⇒ False
  ].

definition jmpleq: jump_length → jump_length → Prop ≝
  λj1.λj2.jmple j1 j2 ∨ j1 = j2.
  
definition policy_increase: list labelled_instruction → jump_expansion_policy →
  jump_expansion_policy → Prop ≝
 λprogram.λop.λp.
  (∀i:ℕ.i < |program| →
    let 〈i1,i2,oj〉 ≝ bvt_lookup ?? (bitvector_of_nat ? i) op 〈0,0,short_jump〉 in
    let 〈i3,i4,j〉 ≝ bvt_lookup ?? (bitvector_of_nat ? i) p 〈0,0,short_jump〉 in 
    jmpleq oj j).

(* Policy safety *)
definition policy_safe: jump_expansion_policy → Prop ≝
 λpolicy.
 bvt_forall ?? policy (λn.λx.let 〈pc_nat,addr_nat,jmp_len〉 ≝ x in
   match jmp_len with
   [ short_jump  ⇒ if leb pc_nat addr_nat
      then le (addr_nat - pc_nat) 126
      else le (pc_nat - addr_nat) 129
   | medium_jump ⇒ 
      let addr ≝ bitvector_of_nat 16 addr_nat in
      let pc ≝ bitvector_of_nat 16 pc_nat in
      let 〈fst_5_addr, rest_addr〉 ≝ split bool 5 11 addr in
      let 〈fst_5_pc, rest_pc〉 ≝ split bool 5 11 pc in
      eq_bv 5 fst_5_addr fst_5_pc = true
   | long_jump   ⇒ True
   ]
 ).
  
(* Definitions and theorems for the jump_length type (itself defined in Assembly) *)
definition max_length: jump_length → jump_length → jump_length ≝
  λj1.λj2.
  match j1 with
  [ long_jump   ⇒ long_jump
  | medium_jump ⇒
    match j2 with
    [ medium_jump ⇒ medium_jump
    | _           ⇒ long_jump
    ]
  | short_jump  ⇒
    match j2 with
    [ short_jump ⇒ short_jump
    | _          ⇒ long_jump
    ]
  ].

lemma dec_jmple: ∀x,y:jump_length.jmple x y + ¬(jmple x y).
 #x #y cases x cases y /3 by inl, inr, nmk, I/
qed.
  
lemma jmpleq_max_length: ∀ol,nl.
  jmpleq ol (max_length ol nl).
 #ol #nl cases ol cases nl
 /2 by or_introl, or_intror, I/
qed.

lemma dec_eq_jump_length: ∀a,b:jump_length.(a = b) + (a ≠ b).
  #a #b cases a cases b /2/
  %2 @nmk #H destruct (H)
qed.

(* Labels *) 
definition is_label ≝ 
  λx:labelled_instruction.λl:Identifier. 
  let 〈lbl,instr〉 ≝ x in
  match lbl with
  [ Some l' ⇒ l' = l
  | _       ⇒ False
  ].

lemma label_does_not_occur:
  ∀i,p,l.
  is_label (nth i ? p 〈None ?, Comment [ ]〉) l → does_not_occur l p = false.
 #i #p #l generalize in match i; elim p
 [ #i >nth_nil #H @⊥ @H
 | #h #t #IH #i cases i -i 
   [ cases h #hi #hp cases hi
     [ normalize #H @⊥ @H
     | #l' #Heq whd in ⊢ (??%?); change with (eq_identifier ? l' l) in match (instruction_matches_identifier ??);
       whd in Heq; >Heq
       >eq_identifier_refl / by refl/
     ]
   | #i #H whd in match (does_not_occur ??);
     whd in match (instruction_matches_identifier ??);
     cases h #hi #hp cases hi normalize nodelta
     [ @(IH i) @H
     | #l' @eq_identifier_elim
       [ normalize / by /
       | normalize #_ @(IH i) @H
       ]
     ]
   ]
 ]
qed.

definition add_instruction_size: ℕ → jump_length → pseudo_instruction → ℕ ≝
  λpc.λjmp_len.λinstr.
  let bv_pc ≝ bitvector_of_nat 16 pc in
  let ilist ≝ expand_pseudo_instruction_safe (λx.bv_pc) bv_pc jmp_len ? instr in
  let bv: list (BitVector 8) ≝ match ilist with
    [ None   ⇒ (* this shouldn't happen *) [ ]
    | Some l ⇒ flatten … (map … assembly1 l)
    ] in 
  pc + (|bv|). 
 @(λx.bv_pc)
qed.

(* The function that creates the label-to-address map *)
definition create_label_map: ∀program:list labelled_instruction.
  ∀policy:jump_expansion_policy.
  (Σlabels:label_map.
    ∀i:ℕ.lt i (|program|) →
    ∀l.occurs_exactly_once l program →
    is_label (nth i ? program 〈None ?, Comment [ ]〉) l →
    ∃a.lookup … labels l = Some ? 〈i,a〉 
  ) ≝
  λprogram.λpolicy.
  let 〈final_pc, final_labels〉 ≝
    foldl_strong (option Identifier × pseudo_instruction)
    (λprefix.ℕ × (Σlabels.
      ∀i:ℕ.lt i (|prefix|) →
      ∀l.occurs_exactly_once l prefix →
      is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l →
      ∃a.lookup … labels l = Some ? 〈i,a〉)
    )
    program
    (λprefix.λx.λtl.λprf.λacc.
     let 〈pc,labels〉 ≝ acc in
     let 〈label,instr〉 ≝ x in
       let new_labels ≝ 
       match label with
       [ None   ⇒ labels
       | Some l ⇒ add … labels l 〈|prefix|, pc〉
       ] in
     let 〈i1,i2,jmp_len〉 ≝ bvt_lookup ?? (bitvector_of_nat 16 (|prefix|)) policy 〈0, 0, long_jump〉 in
       〈add_instruction_size pc jmp_len instr, new_labels〉
    ) 〈0, empty_map …〉 in
    final_labels.
[ #i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
  [ #Hi #l normalize nodelta; cases label normalize nodelta
    [ >occurs_exactly_once_None #Hocc >(nth_append_first ? ? prefix ? ? (le_S_S_to_le ? ? Hi)) #Hl
      lapply (pi2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #addr #Haddr  
      % [ @addr | @Haddr ]
    | #l' #Hocc #Hl lapply (occurs_exactly_once_Some_stronger … Hocc) -Hocc;
      @eq_identifier_elim #Heq #Hocc
      [ normalize in Hocc;
        >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; #Hl  
        @⊥ @(absurd … Hocc) 
      | normalize nodelta lapply (pi2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc ?)
        [ #addr #Haddr % [ @addr | <Haddr @lookup_add_miss /2/ ]
        | >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; / by /
        ]
      ]
      >(label_does_not_occur i … Hl) normalize nodelta @nmk / by /
    ]
  | #Hi #l #Hocc >(injective_S … Hi) >nth_append_second 
    [ <minus_n_n #Hl normalize in Hl; normalize nodelta cases label in Hl;
      [ normalize nodelta #H @⊥ @H
      | #l' normalize nodelta #Heq % [ @pc | <Heq normalize nodelta @lookup_add_hit ]
      ]
    | @le_n
    ]
  ]
| #i #Hi #l #Hl @⊥ @Hl
]
qed.

definition select_reljump_length: label_map → ℕ → Identifier → ℕ ×jump_length ≝
  λlabels.λpc.λlbl.
  let 〈n, addr〉 ≝ lookup_def … labels lbl 〈0, pc〉 in
  if leb pc addr (* forward jump *)
  then if leb (addr - pc) 126
       then 〈addr, short_jump〉
       else 〈addr, long_jump〉
  else if leb (pc - addr) 129
       then 〈addr, short_jump〉
       else 〈addr, long_jump〉.

definition select_call_length: label_map → ℕ → Identifier → ℕ × jump_length ≝
  λlabels.λpc_nat.λlbl.
  let pc ≝ bitvector_of_nat 16 pc_nat in
  let addr_nat ≝ (\snd (lookup_def ? ? labels lbl 〈0, pc_nat〉)) in
  let addr ≝ bitvector_of_nat 16 addr_nat in
  let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 addr in
  let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
  if eq_bv ? fst_5_addr fst_5_pc
  then 〈addr_nat, medium_jump〉
  else 〈addr_nat, long_jump〉.
  
definition select_jump_length: label_map → ℕ → Identifier → ℕ × jump_length ≝
  λlabels.λpc.λlbl.
  let 〈n, addr〉 ≝ lookup_def … labels lbl 〈0, pc〉 in
  if leb pc addr
  then if leb (addr - pc) 126
       then 〈addr, short_jump〉
       else select_call_length labels pc lbl
  else if leb (pc - addr) 129
       then 〈addr, short_jump〉
       else select_call_length labels pc lbl.
 
definition jump_expansion_step_instruction: label_map → ℕ →
  preinstruction Identifier → option (ℕ × jump_length) ≝
  λlabels.λpc.λi.
  match i with
  [ JC j     ⇒ Some ? (select_reljump_length labels pc j)
  | JNC j    ⇒ Some ? (select_reljump_length labels pc j)
  | JZ j     ⇒ Some ? (select_reljump_length labels pc j)
  | JNZ j    ⇒ Some ? (select_reljump_length labels pc j)
  | JB _ j   ⇒ Some ? (select_reljump_length labels pc j)
  | JBC _ j  ⇒ Some ? (select_reljump_length labels pc j)
  | JNB _ j  ⇒ Some ? (select_reljump_length labels pc j)
  | CJNE _ j ⇒ Some ? (select_reljump_length labels pc j)
  | DJNZ _ j ⇒ Some ? (select_reljump_length labels pc j)
  | _        ⇒ None ?
  ].

lemma dec_is_jump: ∀x.(is_jump x) + (¬is_jump x).
#x cases x #l #i cases i
[#id cases id
 [1,2,3,6,7,33,34:
  #x #y %2 whd in match (is_jump ?); /2 by nmk/
 |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32:
  #x %2 whd in match (is_jump ?); /2 by nmk/
 |35,36,37: %2 whd in match (is_jump ?); /2 by nmk/
 |9,10,14,15: #x %1 / by I/
 |11,12,13,16,17: #x #y %1 / by I/
 ]
|2,3: #x %2 /2 by nmk/
|4,5: #x %1 / by I/
|6: #x #y %2 /2 by nmk/
]
qed.

(* these should be moved to BitVector at some point, and proven *)  
lemma bitvector_of_nat_ok:
  ∀n,x,y:ℕ.x < 2^n → y < 2^n → eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y) → x = y.
 #n elim n -n
 [ #x #y #Hx #Hy #Heq <(le_n_O_to_eq ? (le_S_S_to_le ?? Hx)) <(le_n_O_to_eq ? (le_S_S_to_le ?? Hy)) @refl
 | #n #Hind #x #y #Hx #Hy #Heq cases daemon (* XXX *)
 ]
qed.

lemma bitvector_of_nat_abs:
  ∀n,x,y:ℕ.x < 2^n → y < 2^n → x ≠ y → ¬eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y).
 #n #x #y #Hx #Hy #Heq @notb_elim
 lapply (refl ? (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)))
 cases (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)) in ⊢ (???% → %);
 [ #H @⊥ @(absurd ?? Heq) @(bitvector_of_nat_ok n x y Hx Hy) >H / by I/
 | #H / by I/
 ]
qed.

lemma jump_not_in_policy: ∀prefix:list labelled_instruction.
 ∀policy:(Σp:jump_expansion_policy.
 out_of_program_none prefix p ∧ jump_in_policy prefix p).
  ∀i:ℕ.i < |prefix| →
  iff (¬is_jump (nth i ? prefix 〈None ?, Comment []〉))
  (lookup_opt … (bitvector_of_nat 16 i) policy = None ?).
 #prefix #policy #i #Hi @conj
 [ #Hnotjmp lapply (refl ? (lookup_opt … (bitvector_of_nat 16 i) policy))
   cases (lookup_opt … (bitvector_of_nat 16 i) policy) in ⊢ (???% → ?);
   [ #H @H
   | #x cases x -x #x #z cases x -x #x #y #H @⊥ @(absurd ? ? Hnotjmp) @(proj2 ?? (proj2 ?? (pi2 ?? policy) i Hi))
     @(ex_intro ?? x (ex_intro ?? y (ex_intro ?? z H)))
   ]
 | #Hnone @nmk #Hj lapply (proj1 ?? (proj2 ?? (pi2 ?? policy) i Hi) Hj)
   #H elim H -H; #x #H elim H -H; #y #H elim H -H; #z #H >H in Hnone; #abs destruct (abs)
 ]  
qed.

(* these two obviously belong somewhere else *)  
lemma pi1_eq: ∀A:Type[0].∀P:A->Prop.∀s1:Σa1:A.P a1.∀s2:Σa2:A.P a2.
  s1 = s2 → (pi1 ?? s1) = (pi1 ?? s2).
 #A #P #s1 #s2 / by /
qed.

lemma Some_eq:
 ∀T:Type[0].∀x,y:T. Some T x = Some T y → x = y.
 #T #x #y #H @option_destruct_Some @H
qed.

(* The first step of the jump expansion: everything to short.
 * The third condition of the dependent type implies jump_in_policy;
 * I've left it in for convenience of type-checking. *)
definition jump_expansion_start:
  ∀program:(Σl:list labelled_instruction.|l| < 2^16).
  Σpolicy:jump_expansion_policy.
    out_of_program_none program policy ∧
    jump_in_policy program policy ∧
    ∀i.i < |program| → is_jump (nth i ? program 〈None ?, Comment []〉) →
     lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈0,0,short_jump〉 ≝ 
  λprogram.
  foldl_strong (option Identifier × pseudo_instruction)
  (λprefix.Σpolicy:jump_expansion_policy.
    out_of_program_none prefix policy ∧
    jump_in_policy prefix policy ∧
    ∀i.i < |prefix| → is_jump (nth i ? prefix 〈None ?, Comment []〉) →
      lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈0,0,short_jump〉)
  program
  (λprefix.λx.λtl.λprf.λpolicy.
   let 〈label,instr〉 ≝ x in
   match instr with
   [ Instruction i ⇒ match i with
     [ JC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
     | JNC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
     | JZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
     | JNZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
     | JB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
     | JNB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
     | JBC _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
     | CJNE _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
     | DJNZ _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
     | _ ⇒ (pi1 … policy)
     ]
   | Call c ⇒ bvt_insert (ℕ×ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
   | Jmp j  ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
   | _      ⇒ (pi1 ?? policy)
   ]
  ) (Stub ? ?).
[1,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,35,36,37,38,39,40,41,42:
 @conj
 [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,57,59,61:
  @conj
  #i >append_length <commutative_plus #Hi normalize in 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,57,59,61:
   #Hi2 cases (le_to_or_lt_eq … Hi) -Hi; #Hi @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i)
   [1,5,9,13,17,21,25,29,33,37,41,45,49,53,57,61,65,69,73,77,81,85,89,93,97,101,105,109,113,117,121:
     @le_S_to_le @le_S_to_le @Hi
   |2,6,10,14,18,22,26,30,34,38,42,46,50,54,58,62,66,70,74,78,82,86,90,94,98,102,106,110,114,118,122:
     @Hi2
   |3,7,11,15,19,23,27,31,35,39,43,47,51,55,59,63,67,71,75,79,83,87,91,95,99,103,107,111,115,119,123:
     <Hi @le_n_Sn
   |4,8,12,16,20,24,28,32,36,40,44,48,52,56,60,64,68,72,76,80,84,88,92,96,100,104,108,112,116,120,124:
     @Hi2
   ]
  ]
  cases (le_to_or_lt_eq … 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,57,59,61:
    >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi))
    @(proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
  ]
  @conj >(injective_S … 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,57,59,61:
    >(nth_append_second ? ? prefix ? ? (le_n (|prefix|))) <minus_n_n #H @⊥ @H
   ]
   #H elim H; -H; #t1 #H elim H; -H #t2 #H elim H; -H; #t3 #H
   >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?) in H;
   [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,57,59,61:
     #H destruct (H)
   ]
   @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm @le_S_S
   @le_plus_n_r
 ]
 #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … 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,57,59,61:
  #Hj @(proj2 ?? (pi2 ?? policy) i (le_S_S_to_le … Hi))
  >(nth_append_first ?? prefix ?? (le_S_S_to_le ?? Hi)) in Hj; / by /
 ]
 >(injective_S … Hi) >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n
 #H @⊥ @H
|2,3,26,27,28,29,30,31,32,33,34: @conj
 [1,3,5,7,9,11,13,15,17,19,21: @conj
  [1,3,5,7,9,11,13,15,17,19,21:
    #i >append_length <commutative_plus #Hi #Hi2 normalize in Hi; >lookup_opt_insert_miss
   [1,3,5,7,9,11,13,15,17,19,21:
     @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2)
   ]
   >eq_bv_sym @bitvector_of_nat_abs
   [1,4,7,10,13,16,19,22,25,28,31:
     @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm @le_S_S
     @le_plus_n_r
   |2,5,8,11,14,17,20,23,26,29,32: @Hi2 
   |3,6,9,12,15,18,21,24,27,30,33: @lt_to_not_eq @Hi
   ]
  ]
  #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
  -Hi #Hi
  [1,3,5,7,9,11,13,15,17,19,21:
   >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) >lookup_opt_insert_miss
   [1,3,5,7,9,11,13,15,17,19,21:
    @(proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
   ]
   @bitvector_of_nat_abs
   [3,6,9,12,15,18,21,24,27,30,33: @(lt_to_not_eq … (le_S_S_to_le … Hi))
   |1,4,7,10,13,16,19,22,25,28,31: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
   ]
   @(transitive_lt … (pi2 ?? program))
   >prf >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r
  ]
  @conj >(injective_S … Hi) #H
  [2,4,6,8,10,12,14,16,18,20,22:
   >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n / by I/
  ]
  @(ex_intro ?? 0 (ex_intro ?? 0 (ex_intro ?? short_jump (lookup_opt_insert_hit ?? 16 ? policy))))
 ]
 #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
  -Hi #Hi
 [1,3,5,7,9,11,13,15,17,19,21:
  >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) #Hj >lookup_opt_insert_miss 
  [1,3,5,7,9,11,13,15,17,19,21:
   @(proj2 ?? (pi2 ?? policy) i (le_S_S_to_le … Hi) Hj)
  ]
  @bitvector_of_nat_abs
  [3,6,9,12,15,18,21,24,27,30,33: @(lt_to_not_eq … (le_S_S_to_le … Hi))
  |1,4,7,10,13,16,19,22,25,28,31: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
  ]
  @(transitive_lt … (pi2 ?? program))
  >prf >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r
 ]
 #_ >(injective_S … Hi) @lookup_opt_insert_hit
|@conj
 [@conj
  [ #i #Hi / by refl/
  | whd #i #Hi @⊥ @(absurd (i < 0) Hi (not_le_Sn_O ?))
  ]
 | #i #Hi >nth_nil #Hj @⊥ @Hj
]
qed.

definition policy_equal_int ≝
  λprogram:list labelled_instruction.λp1,p2:jump_expansion_policy.
  ∀n:ℕ.n < |program| →
    let 〈i1,i2,j1〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) p1 〈0,0,short_jump〉 in
    let 〈i3,i4,j2〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) p2 〈0,0,short_jump〉 in
    j1 = j2.
    
definition nec_plus_ultra ≝
  λprogram:list labelled_instruction.λp:jump_expansion_policy.
  ¬(∀i.i < |program| → \snd (bvt_lookup … (bitvector_of_nat 16 i) p 〈0,0,short_jump〉) = long_jump).
  
(* One step in the search for a jump expansion fixpoint. *)
definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
  ∀labels:(Σlm:label_map.∀i:ℕ.lt i (|program|) →
    ∀l.occurs_exactly_once l program →
    is_label (nth i ? program 〈None ?, Comment [ ]〉) l →
    ∃a.lookup … lm l = Some ? 〈i,a〉).
  ∀old_policy:(Σpolicy.
    out_of_program_none program policy ∧ jump_in_policy program policy).
  (Σx:bool × ℕ × (option jump_expansion_policy).
    let 〈changed,pc,y〉 ≝ x in
    match y with
    [ None ⇒ pc > 2^16 ∧ nec_plus_ultra program old_policy
    | Some p ⇒ out_of_program_none program p ∧ labels_okay labels p ∧
        jump_in_policy program p ∧
        policy_increase program old_policy p ∧
        policy_safe p ∧
        (changed = false → policy_equal_int program old_policy p)
    ])
    ≝ 
  λprogram.λlabels.λold_policy.
  let 〈final_changed, final_pc, final_policy〉 ≝
    foldl_strong (option Identifier × pseudo_instruction)
    (λprefix.Σx:bool × ℕ × jump_expansion_policy.
        let 〈changed,pc,policy〉 ≝ x in
        out_of_program_none prefix policy ∧ labels_okay labels policy ∧
        jump_in_policy prefix policy ∧
        policy_increase prefix old_policy policy ∧
        policy_safe policy ∧
        (changed = false → policy_equal_int prefix old_policy policy))
    program
    (λprefix.λx.λtl.λprf.λacc.
      let 〈changed, pc, policy〉 ≝ acc in
      let 〈label,instr〉 ≝ x in
(*      let old_jump_length ≝ lookup_opt ? ? (bitvector_of_nat 16 (|prefix|)) old_policy in *)
      let add_instr ≝
        match instr with
        [ Instruction i ⇒ jump_expansion_step_instruction labels pc i 
        | Call c        ⇒ Some ? (select_call_length labels pc c)
        | Jmp j         ⇒ Some ? (select_jump_length labels pc j)
        | _             ⇒ None ?
        ] in
        let 〈ignore,old_length〉 ≝ bvt_lookup … (bitvector_of_nat 16 (|prefix|)) old_policy 〈0, 0, short_jump〉 in
        match add_instr with
        [ None    ⇒ (* i.e. it's not a jump *)
          〈changed, add_instruction_size pc long_jump instr, policy〉
        | Some z ⇒ let 〈addr,ai〉 ≝ z in
          let new_length ≝ max_length old_length ai in
          〈match dec_eq_jump_length new_length old_length with
           [ inl _ ⇒ changed
           | inr _ ⇒ true], add_instruction_size pc new_length instr, insert … (bitvector_of_nat 16 (|prefix|)) 〈pc, addr, new_length〉 policy〉 
        ]
    ) 〈false, 0, Stub ? ?〉 in
    if geb final_pc 2^16 then
      〈final_changed,final_pc,None ?〉
    else
      〈final_changed,final_pc,Some jump_expansion_policy final_policy〉.
[ normalize nodelta @conj
  [ @leb_true_to_le @p2
  | @nmk #Hfull (* XXX *) cases daemon
  ]
| normalize nodelta lapply p generalize in match (foldl_strong ?????); * #x #H #H2
  >H2 in H; >p1 normalize nodelta //
| lapply (pi2 ?? acc) >p >p1 normalize nodelta #Hpolicy
 @conj [ @conj [ @conj [ @conj [ @conj
[ (* out_of_policy_none *) 
  #i >append_length <commutative_plus #Hi normalize in Hi;
  #Hi2 >lookup_opt_insert_miss
  [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_to_le … Hi)) @Hi2
  | >eq_bv_sym @bitvector_of_nat_abs
    [ @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
      @le_S_S @le_plus_n_r 
    | @Hi2
    | @lt_to_not_eq @Hi
    ]
  ]
| (* labels_okay *)
  @lookup_forall #i cases i -i #i cases i -i #p #a #j #n (*lapply (refl ? add_instr)
  cases (lookup ??? old_policy ?); #x cases x -x #p1 #p2 #p3
  cases add_instr in ⊢ (???% → %); 
  [ #Hai normalize nodelta #Hl
    elim (forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) ? n Hl)
    #i #Hi @(ex_intro ?? i Hi)
  | #x cases x -x #np #nl #Hai normalize nodelta *) #Hl
    elim (insert_lookup_opt ?? 〈p,a,j〉 ???? Hl) -Hl #Hl
    [ elim (forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) ? n Hl)
      #i #Hi @(ex_intro ?? i Hi)
    | (*whd in match add_instr in Hai; cases instr in Hai;*) normalize nodelta
      normalize nodelta in p4; cases instr in p4;
      [2,3: #x #abs normalize nodelta in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
      |6: #x #y #abs normalize nodelta in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
      |1: #pi cases pi
        [35,36,37: #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
        |1,2,3,6,7,33,34: #x #y #abs normalize in abs; lapply (jmeq_to_eq ??? abs)
          #H destruct (H)
        |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #abs normalize in abs;
          lapply (jmeq_to_eq ??? abs) #H destruct (H)
        |9,10,14,15: #id normalize nodelta whd in match (jump_expansion_step_instruction ???);
          whd in match (select_reljump_length ???); >p5
          lapply (refl ? (lookup_def ?? labels id 〈0,pc〉))
          cases (lookup_def ?? labels id 〈0,pc〉) in ⊢ (???% → %); #q1 #q2
          normalize nodelta #H
          >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
          >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb pc q2))
          cases (leb pc q2) in ⊢ (???% → %); #Hle1
          [1,3,5,7: lapply (refl ? (leb (q2-pc) 126)) cases (leb (q2-pc) 126) in ⊢ (???% → %);
          |2,4,6,8: lapply (refl ? (leb (pc-q2) 129)) cases (leb (pc-q2) 129) in ⊢ (???% → %);
          ]
          #Hle2 normalize nodelta #Hli @(ex_intro ?? id) >H
          <(pair_eq1 ?????? (Some_eq ??? Hli)) @refl
        |11,12,13,16,17: #x #id normalize nodelta whd in match (jump_expansion_step_instruction ???);
          whd in match (select_reljump_length ???); >p5
          lapply (refl ? (lookup_def ?? labels id 〈0,pc〉))
          cases (lookup_def ?? labels id 〈0,pc〉) in ⊢ (???% → %); #q1 #q2
          normalize nodelta #H
          >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
          >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb pc q2))
          cases (leb pc q2) in ⊢ (???% → %); #Hle1
          [1,3,5,7,9: lapply (refl ? (leb (q2-pc) 126)) cases (leb (q2-pc) 126) in ⊢ (???% → %);
          |2,4,6,8,10: lapply (refl ? (leb (pc-q2) 129)) cases (leb (pc-q2) 129) in ⊢ (???% → %);
          ]
          #Hle2 normalize nodelta #Hli @(ex_intro ?? id) >H
          <(pair_eq1 ?????? (Some_eq ??? Hli)) @refl
        ]
      |4,5: #id normalize nodelta whd in match (select_jump_length ???);
          whd in match (select_call_length ???); >p5
          lapply (refl ? (lookup_def ?? labels id 〈0,pc〉))
          cases (lookup_def ?? labels id 〈0,pc〉) in ⊢ (???% → %); #q1 #q2 
          normalize nodelta #H
          [1: cases (leb pc q2)
            [ cases (leb (q2-pc) 126) | cases (leb (pc-q2) 129) ]
            [1,3: normalize nodelta #H2 >(pair_eq1 ?????? (Some_eq ??? H2)) in H;
            #Hli @(ex_intro ?? id) lapply (proj2 ?? Hl)
            #H >(pair_eq1 ?????? (pair_eq1 ?????? H))
            >(pair_eq2 ?????? (pair_eq1 ?????? H)) >Hli @refl]
          ]
          cases (split ? 5 11 (bitvector_of_nat 16 q2)) #n1 #n2
          cases (split ? 5 11 (bitvector_of_nat 16 pc)) #m1 #m2 
          normalize nodelta cases (eq_bv ? n1 m1)
          normalize nodelta #H2 >(pair_eq1 ?????? (Some_eq ??? H2)) in H; #H
          @(ex_intro ?? id) lapply (proj2 ?? Hl) #H2
          >(pair_eq1 ?????? (pair_eq1 ?????? H2)) >(pair_eq2 ?????? (pair_eq1 ?????? H2))
          >H @refl
      ]
    ]
  ]
| (* jump_in_policy *)
  #i #Hi cases (le_to_or_lt_eq … Hi) -Hi;
  [ >append_length <commutative_plus #Hi normalize in Hi;
    >(nth_append_first ?? prefix ??(le_S_S_to_le ?? Hi)) @conj
    [ #Hj lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i (le_S_S_to_le … Hi))
      #Hacc elim (proj1 ?? Hacc Hj) #h #n elim n -n #n #H elim H -H #j #Hj
      @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?))) whd in match (snd ???);
      >lookup_opt_insert_miss [ @Hj |  @bitvector_of_nat_abs ]
      [3: @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
      |1: @(transitive_lt ??? (le_S_S_to_le ?? Hi)) 
      ]
      @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
      @le_S_S @le_plus_n_r
    | lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i (le_S_S_to_le … Hi)) #Hacc
      #H elim H -H; #h #H elim H -H; #n #H elim H -H #j 
      #Hl @(proj2 ?? Hacc) @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?)))
      <Hl @sym_eq @lookup_opt_insert_miss @bitvector_of_nat_abs
      [3: @lt_to_not_eq @(le_S_S_to_le … Hi)
      |1: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
      ]
      @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
      @le_S_S @le_plus_n_r
    ]
  | >append_length <commutative_plus #Hi normalize in Hi; >(injective_S … Hi)
    >(nth_append_second ?? prefix ?? (le_n (|prefix|)))
     <minus_n_n whd in match (nth ????); normalize nodelta in p4; cases instr in p4;
     [1: #pi | 2,3: #x | 4,5: #id | 6: #x #y] #Hinstr @conj normalize nodelta
     [3,5,11: #H @⊥ @H (* instr is not a jump *)
     |4,6,12: normalize nodelta in Hinstr; lapply (jmeq_to_eq ??? Hinstr)
      #H destruct (H)
     |7,9: (* instr is a jump *) #_ @(ex_intro ?? pc) 
       @(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai))
       @lookup_opt_insert_hit
     |8,10: #_ / by I/
     |1,2: cases pi in Hinstr; 
       [35,36,37: #Hinstr #H @⊥ @H
       |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #Hinstr #H @⊥ @H
       |1,2,3,6,7,33,34: #x #y #Hinstr #H @⊥ @H
       |9,10,14,15: #id #Hinstr #_
         @(ex_intro ?? pc) @(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai))
         @lookup_opt_insert_hit
       |11,12,13,16,17: #x #id #Hinstr #_ 
         @(ex_intro ?? pc) @(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai))
         @lookup_opt_insert_hit
       |72,73,74: #Hinstr lapply (jmeq_to_eq ??? Hinstr) #H normalize in H; destruct (H)
       |41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69: #x #Hinstr
        lapply (jmeq_to_eq ??? Hinstr) #H normalize in H; destruct (H)
       |38,39,40,43,44,70,71: #x #y #Hinstr lapply (jmeq_to_eq ??? Hinstr) #H
         normalize in H; destruct (H)
       |46,47,51,52: #id #Hinstr #_ / by I/
       |48,49,50,53,54: #x #id #Hinstr #_ / by I/
       ]
     ]
   ]
 ]
| (* policy increase *)
  #i >append_length >commutative_plus #Hi normalize in Hi;
  cases (le_to_or_lt_eq … Hi) -Hi; #Hi
  [ >lookup_insert_miss
    [ @(proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)) i (le_S_S_to_le … Hi))
    | @bitvector_of_nat_abs
      [3: @lt_to_not_eq @(le_S_S_to_le … Hi)
      |1: @(transitive_lt ??? (le_S_S_to_le … Hi))
      ]
      @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
      @le_S_S @le_plus_n_r
    ]
  | >(injective_S … Hi) >p3 >lookup_insert_hit normalize nodelta
    @pair_elim #x #y #_ @jmpleq_max_length
  ]
 ]
| (* policy_safe *)
  @lookup_forall #x cases x -x #x cases x -x #p #a #j #n normalize nodelta #Hl
  elim (insert_lookup_opt ?? 〈p,a,j〉 ???? Hl) -Hl #Hl
  [ @(forall_lookup … (proj2 ?? (proj1 ?? Hpolicy)) ? n Hl)
  | normalize nodelta in p4; cases instr in p4;
    [2,3: #x #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
    |6: #x #y #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
    |1: #pi cases pi normalize nodelta
     [35,36,37: #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
     |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32:
       #x #abs @⊥ normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
     |1,2,3,6,7,33,34: #x #y #abs @⊥ normalize in abs; lapply (jmeq_to_eq ??? abs) #H
       destruct (H)
     |9,10,14,15: #id >p5 whd in match (jump_expansion_step_instruction ???);
       whd in match (select_reljump_length ???);
       cases (lookup_def ?? labels id 〈0,pc〉) #q1 #q2 normalize nodelta
       >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
       >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb pc q2))
       cases (leb pc q2) in ⊢ (???% → %); #Hle1
       [1,3,5,7: lapply (refl ? (leb (q2-pc) 126)) cases (leb (q2-pc) 126) in ⊢ (???% → %);
       |2,4,6,8: lapply (refl ? (leb (pc-q2) 129)) cases (leb (pc-q2) 129) in ⊢ (???% → %);
       ]
       #Hle2 normalize nodelta #Hli
       <(pair_eq1 ?????? (Some_eq ??? Hli)) >Hle1 
       >(pair_eq2 ?????? (proj2 ?? Hl)) <(pair_eq2 ?????? (Some_eq ??? Hli))
       cases old_length
       [1,7,13,19,25,31,37,43: @(leb_true_to_le … Hle2)
       ] normalize @I (* much faster than / by I/, strangely enough *)
     |11,12,13,16,17: #x #id >p5 whd in match (jump_expansion_step_instruction ???);
       whd in match (select_reljump_length ???); 
       cases (lookup_def ?? labels id 〈0,pc〉) #q1 #q2 normalize nodelta
       >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
       >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb pc q2))
       cases (leb pc q2) in ⊢ (???% → %); #Hle1
       [1,3,5,7,9: lapply (refl ? (leb (q2-pc) 126)) cases (leb (q2-pc) 126) in ⊢ (???% → %);
       |2,4,6,8,10: lapply (refl ? (leb (pc-q2) 129)) cases (leb (pc-q2) 129) in ⊢ (???% → %);
       ]
       #Hle2 normalize nodelta #Hli
       <(pair_eq1 ?????? (Some_eq ??? Hli)) >Hle1 >(pair_eq2 ?????? (proj2 ?? Hl))
       <(pair_eq2 ?????? (Some_eq ??? Hli))
       cases old_length
       [1,7,13,19,25,31,37,43,49,55: @(leb_true_to_le … Hle2)
       ] normalize @I (* vide supra *)
     ]
    |4,5: #id >p5 normalize nodelta whd in match (select_jump_length ???);
      whd in match (select_call_length ???); cases (lookup_def ?? labels id 〈0,pc〉)
      #q1 #q2 normalize nodelta
      >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
      >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
      [1: lapply (refl ? (leb pc q2)) cases (leb pc q2) in ⊢ (???% → %); #Hle1
        [ lapply (refl ? (leb (q2-pc) 126)) cases (leb (q2-pc) 126) in ⊢ (???% → %);
        | lapply (refl ? (leb (pc-q2) 129)) cases (leb (pc-q2) 129) in ⊢ (???% → %);
        ]
       #Hle2 normalize nodelta
      ]
      [2,4,5: lapply (refl ? (split ? 5 11 (bitvector_of_nat ? q2)))
        cases (split ??? (bitvector_of_nat ? q2)) in ⊢ (???% → %); #x1 #x2 #Hle3
        lapply (refl ? (split ? 5 11 (bitvector_of_nat ? pc)))
        cases (split ??? (bitvector_of_nat ? pc)) in ⊢ (???% → %); #y1 #y2 #Hle4
        normalize nodelta lapply (refl ? (eq_bv 5 x1 y1))
        cases (eq_bv 5 x1 y1) in ⊢ (???% → %); #Hle5
      ]
      #Hli <(pair_eq1 ?????? (Some_eq ??? Hli)) >(pair_eq2 ?????? (proj2 ?? Hl))
      <(pair_eq2 ?????? (Some_eq ??? Hli))
      cases old_length
      [2,8,14: >Hle3 @Hle5
      |19,22: >Hle1 @(leb_true_to_le … Hle2)
      ] normalize @I (* here too *)
    ]
  ]
 ]
| (* changed *)
  cases (dec_eq_jump_length (max_length old_length ai) old_length) normalize nodelta
  [ #Hml #Hc #i #Hi cases (le_to_or_lt_eq … Hi) -Hi >append_length >commutative_plus #Hi
    normalize in Hi;
    [ >lookup_insert_miss
      [ @((proj2 ?? Hpolicy) Hc i (le_S_S_to_le … Hi))
      | @bitvector_of_nat_abs
        [3: @lt_to_not_eq @(le_S_S_to_le … Hi)
        |1: @(transitive_lt ??? (le_S_S_to_le … Hi))
        ]
        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
        @le_S_S @le_plus_n_r
      ]
    | >(injective_S … Hi) >p3 >lookup_insert_hit normalize nodelta
      @pair_elim #x #y #_ @(sym_eq ??? Hml)
    ]
  | #_ #H destruct (H)
  ] 
 ]
| (* Case where add_instr = None *) normalize nodelta lapply (pi2 ?? acc) >p >p1
  normalize nodelta #Hpolicy
  @conj [ @conj [ @conj [ @conj [ @conj
[ (* out_of_program_none *) #i >append_length >commutative_plus #Hi normalize in Hi;
  #Hi2 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_to_le ?? Hi) Hi2)
| (* labels_okay *) @lookup_forall #x cases x -x #x cases x #p #a #j #lbl #Hl normalize nodelta
  elim (forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) ? lbl Hl)
  #id #Hid @(ex_intro … id Hid)
 ]
| (* jump_in_policy *) #i >append_length >commutative_plus #Hi normalize in Hi;
  elim (le_to_or_lt_eq … Hi) -Hi #Hi
  [ >(nth_append_first ?? prefix ?? (le_S_S_to_le ?? Hi)) 
    @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i (le_S_S_to_le ?? Hi))
  | >(injective_S … Hi) @conj
    [ >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n whd in match (nth ????);
      normalize nodelta in p4; cases instr in p4;
      [ #pi cases pi
        [1,2,3,6,7,33,34: #x #y #_ #H @⊥ @H
        |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #_ #H @⊥ @H
        |9,10,14,15: #id (* normalize segfaults here *) normalize nodelta
          whd in match (jump_expansion_step_instruction ???);
          #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
        |11,12,13,16,17: #x #id normalize nodelta
          whd in match (jump_expansion_step_instruction ???);
          #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
        |35,36,37: #_ #H @⊥ @H
        ]
      |2,3: #x #_ #H @⊥ @H
      |4,5: #id normalize nodelta #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
      |6: #x #id #_ #H @⊥ @H
      ]
    | #H elim H -H #p #H elim H -H #a #H elim H -H #j #H
      >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) (|prefix|) (le_n (|prefix|)) ?) in H;
      [ #H destruct (H)
      | @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
        @le_S_S @le_plus_n_r
      ]
    ]
  ]
 ]
| (* policy_increase *) #i >append_length >commutative_plus #Hi normalize in Hi;
  elim (le_to_or_lt_eq … Hi) -Hi #Hi
  [ @(proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)) i (le_S_S_to_le … Hi))
  | >(injective_S … Hi) >lookup_opt_lookup_miss
    [ >lookup_opt_lookup_miss
      [ normalize nodelta %2 @refl
      | @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) (|prefix|) (le_n (|prefix|)) ?)
        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
        @le_S_S @le_plus_n_r
      ]
    | @(proj1 ?? (jump_not_in_policy (pi1 … program) old_policy (|prefix|) ?)) >prf
      [ >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r
      | >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n >p2
        whd in match (nth ????); normalize nodelta in p4; cases instr in p4;
        [ #pi cases pi
          [1,2,3,6,7,33,34: #x #y #_ normalize /2 by nmk/
          |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #_ normalize /2 by nmk/
          |9,10,14,15: #id (* normalize segfaults here *) normalize nodelta
            whd in match (jump_expansion_step_instruction ???);
            #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
          |11,12,13,16,17: #x #id normalize nodelta
            whd in match (jump_expansion_step_instruction ???);
            #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
          |35,36,37: #_ normalize /2 by nmk/
          ]
        |2,3: #x #_ normalize /2 by nmk/
        |4,5: #id normalize nodelta #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
        |6: #x #id #_ normalize /2 by nmk/
        ]
      ]
    ]
  ]
 ]
| (* policy_safe *) @lookup_forall #x cases x -x #x cases x -x #p #a #j #n #Hl
  @(forall_lookup … (proj2 ?? (proj1 ?? Hpolicy)) ? n Hl)
 ]
| (* changed *) #Hc #i >append_length >commutative_plus #Hi normalize in Hi;
  elim (le_to_or_lt_eq … Hi) -Hi #Hi
  [ @((proj2 ?? Hpolicy) Hc i (le_S_S_to_le … Hi))
  | >(injective_S … Hi) >lookup_opt_lookup_miss
    [ >lookup_opt_lookup_miss
      [ normalize nodelta @refl
      | @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) (|prefix|) (le_n (|prefix|)) ?)
        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
        @le_S_S @le_plus_n_r
      ]
    | @(proj1 ?? (jump_not_in_policy (pi1 … program) old_policy (|prefix|) ?)) >prf
      [ >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r
      | >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n >p2
        whd in match (nth ????); normalize nodelta in p4; cases instr in p4;
        [ #pi cases pi
          [1,2,3,6,7,33,34: #x #y #_ normalize /2 by nmk/
          |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #_ normalize /2 by nmk/
          |9,10,14,15: #id (* normalize segfaults here *) normalize nodelta
            whd in match (jump_expansion_step_instruction ???);
            #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
          |11,12,13,16,17: #x #id normalize nodelta
            whd in match (jump_expansion_step_instruction ???);
            #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
          |35,36,37: #_ normalize /2 by nmk/
          ]
        |2,3: #x #_ normalize /2 by nmk/
        |4,5: #id normalize nodelta #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
        |6: #x #id #_ normalize /2 by nmk/
        ]
      ]
    ]
  ]
 ]       
| @conj [ @conj [ @conj [ @conj [ @conj
  [ #i #Hi //
  | //
  ]
  | #i #Hi @conj [ >nth_nil #H @⊥ @H | #H elim H #x #H1 elim H1 #y #H2 elim H2 #z #H3
                   normalize in H3; destruct (H3) ]
  ]                 
  | #i #Hi @⊥ @(absurd (i<0)) [ @Hi | @(not_le_Sn_O) ]
  ]
  | //
  ]
  | #_ #i #Hi @⊥ @(absurd (i < 0)) [ @Hi | @not_le_Sn_O ]
  ]
qed.

(* this might be replaced by a coercion: (∀x.A x → B x) → Σx.A x → Σx.B x *)
(* definition weaken_policy:
  ∀program,op.
  option (Σp:jump_expansion_policy.
    And (And (And (And (out_of_program_none program p)
    (labels_okay (create_label_map program op) p))
    (jump_in_policy program p)) (policy_increase program op p))
    (policy_safe p)) →
  option (Σp:jump_expansion_policy.And (out_of_program_none program p)
    (jump_in_policy program p)) ≝
 λprogram.λop.λx.
 match x return λ_.option (Σp.And (out_of_program_none program p) (jump_in_policy program p)) with
 [ None ⇒ None ?
 | Some z ⇒ Some ? (mk_Sig ?? (pi1 ?? z) ?)
 ].
@conj
[ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? z)))))
| @(proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? z))))
]
qed. *)

(* This function executes n steps from the starting point. *)
(*let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (|l|) 2^16)
  (n: ℕ) on n:(Σx:bool × ℕ × (option jump_expansion_policy).
    let 〈ch,pc,y〉 ≝ x in
    match y with
    [ None ⇒ pc > 2^16
    | Some p ⇒ And (out_of_program_none program p) (jump_in_policy program p)
    ]) ≝
  match n with
  [ O   ⇒ 〈0,Some ? (pi1 … (jump_expansion_start program))〉
  | S m ⇒ let 〈ch,pc,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in
          match z return λx. z=x → Σa:bool × ℕ × (option jump_expansion_policy).? with
          [ None    ⇒ λp2.〈pc,None ?〉
          | Some op ⇒ λp2.pi1 … (jump_expansion_step program (create_label_map program op) «op,?»)
          ] (refl … z)
  ].*)

let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (|l|) 2^16) (n: ℕ)
  on n:(Σx:bool × ℕ × (option jump_expansion_policy).
    let 〈c,pc,y〉 ≝ x in
    match y with
    [ None ⇒ pc > 2^16
    | Some p ⇒ And (out_of_program_none program p) (jump_in_policy program p)
    ]) ≝
  match n with
  [ O   ⇒ 〈true,0,Some ? (pi1 ?? (jump_expansion_start program))〉
  | S m ⇒ let 〈ch,pc,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in
          match z return λx. z=x → Σa:bool × ℕ × (option jump_expansion_policy).? with
          [ None    ⇒ λp2.〈false,pc,None ?〉
          | Some op ⇒ λp2.if ch
            then pi1 ?? (jump_expansion_step program (create_label_map program op) «op,?»)
            else (jump_expansion_internal program m)
          ] (refl … z)
  ].
[ normalize nodelta @(proj1 ?? (pi2 ?? (jump_expansion_start program)))
| lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta / by /
|3: lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta / by /
| normalize nodelta cases (jump_expansion_step program (create_label_map program op) «op,?»)
  #p cases p -p #p cases p -p #p #q #r cases r normalize nodelta
  [ #H @(proj1 ?? H)
  | #j #H @conj
    [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
    | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
    ]
  ]
]
qed.

lemma pe_int_refl: ∀program.reflexive ? (policy_equal_int program).
#program whd #x whd #n #Hn
cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉)
#y cases y -y #y #z normalize nodelta @refl
qed.

lemma pe_int_sym: ∀program.symmetric ? (policy_equal_int program).
#program whd #x #y #Hxy whd #n #Hn
lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉)
#z cases z -z #x1 #x2 #x3
cases (bvt_lookup … (bitvector_of_nat ? n) y 〈0,0,short_jump〉)
#z cases z -z #y1 #y2 #y3 normalize nodelta //
qed.
  
lemma pe_int_trans: ∀program.transitive ? (policy_equal_int program).
#program whd #x #y #z whd in match (policy_equal_int ???); whd in match (policy_equal_int ?y ?);
whd in match (policy_equal_int ? x z); #Hxy #Hyz #n #Hn lapply (Hxy n Hn) -Hxy
lapply (Hyz n Hn) -Hyz cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉)
#z cases z -z #x1 #x2 #x3
cases (bvt_lookup … (bitvector_of_nat ? n) y 〈0,0,short_jump〉) #z cases z -z  
#y1 #y2 #y3
cases (bvt_lookup … (bitvector_of_nat ? n) z 〈0,0,short_jump〉) #z cases z -z  
#z1 #z2 #z3 normalize nodelta //
qed.

definition policy_equal ≝
  λprogram:list labelled_instruction.λp1,p2:option jump_expansion_policy.
  match p1 with
  [ Some x1 ⇒ match p2 with
              [ Some x2 ⇒ policy_equal_int program x1 x2
              | _       ⇒ False
              ]
  | None    ⇒ p2 = None ?
  ].

lemma pe_refl: ∀program.reflexive ? (policy_equal program).
#program whd #x whd cases x
[ //
| #y @pe_int_refl
]
qed.

lemma pe_sym: ∀program.symmetric ? (policy_equal program).
#program whd #x #y #Hxy whd cases y in Hxy;
[ cases x
  [ //
  | #x' #H @⊥ @(absurd ? H) /2 by nmk/
  ]
| #y' cases x
  [ #H @⊥ @(absurd ? H) whd in match (policy_equal ???); @nmk #H destruct (H)
  | #x' #H @pe_int_sym @H
  ]
]
qed.

lemma pe_trans: ∀program.transitive ? (policy_equal program).
#program whd #x #y #z cases x
[ #Hxy #Hyz >Hxy in Hyz; //
| #x' cases y
  [ #H @⊥ @(absurd ? H) /2 by nmk/
  | #y' cases z
    [ #_ #H @⊥ @(absurd ? H) /2 by nmk/
    | #z' @pe_int_trans
    ]
  ]
]
qed.

definition step_none: ∀program.∀n.
  (\snd (pi1 ?? (jump_expansion_internal program n))) = None ? →
  ∀k.(\snd (pi1 ?? (jump_expansion_internal program (n+k)))) = None ?.
#program #n lapply (refl ? (jump_expansion_internal program n))
 cases (jump_expansion_internal program n) in ⊢ (???% → %);
 #x1 cases x1 #p1 #j1 -x1; #H1 #Heqj #Hj #k elim k
[ <plus_n_O >Heqj @Hj
| #k' -k <plus_n_Sm whd in match (jump_expansion_internal program (S (n+k')));
  lapply (refl ? (jump_expansion_internal program (n+k')))
  cases (jump_expansion_internal program (n+k')) in ⊢ (???% → % → %);
  #x2 cases x2 -x2 #x2 cases x2 -x2 #c2 #p2 #j2 normalize nodelta #H #Heqj2
  cases j2 in H Heqj2;
  [ #H #Heqj2 #_ whd in match (jump_expansion_internal ??);
    >Heqj2 normalize nodelta @refl
  | #x #H #Heqj2 #abs destruct (abs)
  ]
]
qed.

lemma pe_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
  ∀n.policy_equal program (\snd (pi1 ?? (jump_expansion_internal program n)))
   (\snd (pi1 ?? (jump_expansion_internal program (S n)))) →
  policy_equal program (\snd (pi1 ?? (jump_expansion_internal program (S n))))
    (\snd (pi1 ?? (jump_expansion_internal program (S (S n))))).
#program #n #Heq
cases daemon (* XXX *)
qed.

(* this is in the stdlib, but commented out, why? *)
theorem plus_Sn_m1: ∀n,m:nat. S m + n = m + S n.
  #n (elim n) normalize /2 by S_pred/ qed.
  
lemma equal_remains_equal: ∀program:(Σl:list labelled_instruction.|l| < 2^16).∀n:ℕ.
  policy_equal program (\snd (pi1 … (jump_expansion_internal program n)))
   (\snd (pi1 … (jump_expansion_internal program (S n)))) →
  ∀k.k ≥ n → policy_equal program (\snd (pi1 … (jump_expansion_internal program n)))
   (\snd (pi1 … (jump_expansion_internal program k))).
#program #n #Heq #k #Hk elim (le_plus_k … Hk); #z #H >H -H -Hk -k;
lapply Heq -Heq; lapply n -n; elim z -z;
[ #n #Heq <plus_n_O @pe_refl
| #z #Hind #n #Heq <plus_Sn_m1 whd in match (plus (S n) z);
  @(pe_trans … (\snd (pi1 … (jump_expansion_internal program (S n)))))
  [ @Heq
  | @Hind @pe_step @Heq
  ]
]
qed.

(* this number monotonically increases over iterations, maximum 2*|program| *)
let rec measure_int (program: list labelled_instruction) (policy: jump_expansion_policy) (acc: ℕ)
 on program: ℕ ≝
 match program with
 [ nil      ⇒ acc
 | cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,00
,short_jump〉)) with
   [ long_jump   ⇒ measure_int t policy (acc + 2)
   | medium_jump ⇒ measure_int t policy (acc + 1)
   | _           ⇒ measure_int t policy acc
   ]
 ].

lemma measure_plus: ∀program.∀policy.∀x,d:ℕ.
 measure_int program policy (x+d) = measure_int program policy x + d.
#program #policy #x #d generalize in match x; -x elim d
[ //
| -d; #d #Hind elim program
  [ / by refl/
  | #h #t #Hd #x whd in match (measure_int ???); whd in match (measure_int ?? x);
    cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉))
    [ normalize nodelta @Hd
    |2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus
      @Hd
    ]
  ]
]
qed.

lemma measure_le: ∀program.∀policy.
  measure_int program policy 0 ≤ 2*|program|.
#program #policy elim program
[ normalize @le_n
| #h #t #Hind whd in match (measure_int ???);
  cases (\snd (lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉))
  [ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/
  |2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?)
    @le_plus [1,3: @Hind |2,4: // ]
  ]
]
qed.

lemma measure_incr_or_equal: ∀program:Σl:list labelled_instruction.|l|<2^16.
  ∀policy:Σp:jump_expansion_policy.
    out_of_program_none program p ∧ jump_in_policy program p.
  ∀l.|l| ≤ |program| → ∀acc:ℕ.
  match \snd (jump_expansion_step program (create_label_map program policy) policy) with
  [ None   ⇒ True
  | Some p ⇒ measure_int l policy acc ≤ measure_int l p acc
  ].
#program #policy #l elim l -l;
[ #Hp #acc cases (jump_expansion_step ???) #pi1 cases pi1 #p #q -pi1; cases q [ // | #x #_ @le_n ]
| #h #t #Hind #Hp #acc
  lapply (refl ? (jump_expansion_step program (create_label_map program policy) policy))
  cases (jump_expansion_step ???) in ⊢ (???% → %); #pi1 cases pi1 -pi1 #pi1 cases pi1
  #p #q #r -pi1; cases r
  [ //
  | #x normalize nodelta #Hx #Hjeq lapply (proj2 ?? (proj1 ?? (proj1 ?? Hx)) (|t|) Hp)
    whd in match (measure_int ???); whd in match (measure_int ? x ?);
    cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)
    #z cases z -z #x1 #x2 #x3
    cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) x 〈0,0,short_jump〉)
    #z cases z -z #y1 #y2 #y3
    normalize nodelta #Hj cases Hj
    [ cases x3 cases y3
      [1,4,5,7,8,9: #H @⊥ @H
      |2,3,6: #_ normalize nodelta
        [1,2: @(transitive_le ? (measure_int t x acc))
        |3: @(transitive_le ? (measure_int t x (acc+1)))
        ]
        [2,4,5,6: >measure_plus [1,2: @le_plus_n_r] >measure_plus @le_plus / by le_n/]
        >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn
        ]
    | #Heq >Heq cases y3 normalize nodelta
      [2,3: >measure_plus >measure_plus @le_plus / by le_n/]
      >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn
    ]
  ]
]
qed.

(* these lemmas seem superfluous, but not sure how *)
lemma bla: ∀a,b:ℕ.a + a = b + b → a = b.
 #a elim a
 [ normalize #b //
 | -a #a #Hind #b cases b [ /2 by le_n_O_to_eq/ | -b #b normalize
   <plus_n_Sm <plus_n_Sm #H
   >(Hind b (injective_S ?? (injective_S ?? H))) // ]
 ]
qed.

lemma sth_not_s: ∀x.x ≠ S x.
 #x cases x
 [ // | #y // ]
qed.
  
lemma measure_full: ∀program.∀policy.
  measure_int program policy 0 = 2*|program| → ∀i.i<|program| →
  (\snd (bvt_lookup ?? (bitvector_of_nat ? i) policy 〈0,0,short_jump〉)) = long_jump.
#program #policy elim program
[ #Hm #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
| #h #t #Hind #Hm #i #Hi cut (measure_int t policy 0 = 2*|t|)
  [ whd in match (measure_int ???) in Hm;
    cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) in Hm;
    normalize nodelta
    [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/
    | >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy))
      <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize
      >(commutative_plus (|t|) 0) <plus_O_n <minus_n_O
      >plus_n_Sm @le_n
    | >measure_plus <times_n_Sm >commutative_plus #H lapply (injective_plus_r … H) //
    ]
  | #Hmt cases (le_to_or_lt_eq … Hi) -Hi;
  [ #Hi @(Hind Hmt i (le_S_S_to_le … Hi))
  | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm;
    cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) in Hm;
    normalize nodelta
    [ >Hmt normalize <plus_n_O >(commutative_plus (|t|) (S (|t|)))
      >plus_n_Sm #H @⊥ @(absurd ? (bla ?? H)) @sth_not_s
    | >measure_plus >Hmt normalize <plus_n_O >commutative_plus normalize
      #H @⊥ @(absurd ? (injective_plus_r … (injective_S ?? H))) @sth_not_s
    | #_ //
    ]
  ]]
]
qed.

lemma measure_special: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
  ∀policy:Σp:jump_expansion_policy.
    out_of_program_none program p ∧ jump_in_policy program p.
  match (\snd (pi1 ?? (jump_expansion_step program (create_label_map program policy) policy))) with
  [ None ⇒ True
  | Some p ⇒ measure_int program policy 0 = measure_int program p 0 → policy_equal_int program policy p ].
#program #policy lapply (refl ? (pi1 ?? (jump_expansion_step program (create_label_map program policy) policy)))
cases (jump_expansion_step program (create_label_map program policy) policy) in ⊢ (???% → %);
#p cases p -p #p cases p -p #ch #pc #pol normalize nodelta cases pol
[ //
| #p normalize nodelta #Hpol #eqpol lapply (le_n (|program|))
  @(list_ind ?  (λx.|x| ≤ |pi1 ?? program| →
      measure_int x policy 0 = measure_int x p 0 →
      policy_equal_int x policy p) ?? (pi1 ?? program))
 [ #_ #_ #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O
 | #h #t #Hind #Hp #Hm #i #Hi cases (le_to_or_lt_eq … Hi) -Hi;
   [ #Hi @Hind
     [ @(transitive_le … Hp) //
     | whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm;
       lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpol)) (|t|) Hp)
       cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉) in Hm;
       #x cases x -x #x1 #x2 #x3
       cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉);
       #y cases y -y #y1 #y2 #y3
       cases x3 cases y3 normalize nodelta
       [1: #H #_ @H
       |2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
         lapply (measure_incr_or_equal program policy t ? 0)
         [1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
       |4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 |2,4,6: destruct (H2) ]
       |5: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 1)
         #H #_ @(injective_plus_r … H)
       |6: >measure_plus >measure_plus
          change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???))
          #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l
          lapply (measure_incr_or_equal program policy t ? 0)
          [ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
       |9: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 2)
         #H #_ @(injective_plus_r … H)
       ]
     | @(le_S_S_to_le … Hi)
     ]
   | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm;
     whd in match (measure_int ? p ?) in Hm;
     lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpol)) (|t|) Hp)
     cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉) in   
Hm;
     #x cases x -x #x1 #x2 #x3
     cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉);
     #y cases y -y #y1 #y2 #y3
     normalize nodelta cases x3 cases y3 normalize nodelta
     [1,5,9: #_ #_ //
     |4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 |2,4,6: destruct (H2) ]
     |2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
       lapply (measure_incr_or_equal program policy t ? 0)
       [1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
     |6: >measure_plus >measure_plus
        change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???))
        #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l
        lapply (measure_incr_or_equal program policy t ? 0)
        [ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
     ]
   ]
 ] 
qed.

lemma le_to_eq_plus: ∀n,z.
  n ≤ z → ∃k.z = n + k.
 #n #z elim z
 [ #H cases (le_to_or_lt_eq … H)
   [ #H2 @⊥ @(absurd … H2) @not_le_Sn_O
   | #H2 @(ex_intro … 0) >H2 //
   ]
 | #z' #Hind #H cases (le_to_or_lt_eq … H)
   [ #H' elim (Hind (le_S_S_to_le … H')) #k' #H2 @(ex_intro … (S k'))
     >H2 >plus_n_Sm //
   | #H' @(ex_intro … 0) >H' //
   ]
 ]
qed.

lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction.|l| < 2^16.
  |l| ≤ |program| → measure_int l (jump_expansion_start program) 0 = 0.
 #l #program elim l
 [ //
 | #h #t #Hind #Hp whd in match (measure_int ???);
   cases (dec_is_jump (nth (|t|) ? program 〈None ?, Comment []〉)) #Hj
   [ >(lookup_opt_lookup_hit … (proj2 ?? (pi2 ?? (jump_expansion_start program)) (|t|) ? Hj) 〈0,0,short_jump〉)
     [ normalize nodelta @Hind @le_S_to_le ]
     @Hp
   | >(lookup_opt_lookup_miss … (proj1 ?? (jump_not_in_policy program (pi1 ?? (jump_expansion_start program)) (|t|) ?) Hj) 〈0,0,short_jump〉)
     [ normalize nodelta @Hind @le_S_to_le @Hp
     | @Hp
     | % 
       [ @(proj1 ?? (proj1 ?? (pi2 ?? (jump_expansion_start program))))
       | @(proj2 ?? (proj1 ?? (pi2 ?? (jump_expansion_start program))))
       ]
     ]
   ]
 ]
qed.

(* the actual computation of the fixpoint *)
definition je_fixpoint: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
  Σp:option jump_expansion_policy.∃n.∀k.n < k →
    policy_equal program (\snd (pi1 ?? (jump_expansion_internal program k))) p.
#program @(\snd (pi1 ?? (jump_expansion_internal program (2*|program|))))
cases (dec_bounded_exists (λk.policy_equal (pi1 ?? program)
   (\snd (pi1 ?? (jump_expansion_internal program k)))
   (\snd (pi1 ?? (jump_expansion_internal program (S k))))) ? (2*|program|))
[ #Hex elim Hex -Hex #x #Hx @(ex_intro … x) #k #Hk
  @pe_trans
  [ @(\snd (pi1 ?? (jump_expansion_internal program x)))
  | @pe_sym @equal_remains_equal
    [ @(proj2 ?? Hx)
    | @le_S_S_to_le @le_S @Hk
    ]
  | @equal_remains_equal
    [ @(proj2 ?? Hx)
    | @le_S_S_to_le @le_S @(proj1 ?? Hx)
    ]    
  ]
| #Hnex lapply (not_exists_forall … Hnex) -Hnex; #Hfa @(ex_intro … (2*|program|)) #k #Hk
  @pe_sym @equal_remains_equal
  [ lapply (refl ? (jump_expansion_internal program (2*|program|)))
    cases (jump_expansion_internal program (2*|program|)) in ⊢ (???% → %);
    #x cases x -x #x cases x #Fch #Fpc #Fpol normalize nodelta #HFpol cases Fpol in HFpol;
    [ (* if we're at None in 2*|program|, we're at None in S 2*|program| too *)
      #HFpol #EQ whd in match (jump_expansion_internal ??); >EQ
      normalize nodelta //
    | #Fp #HFp #EQ whd in match (jump_expansion_internal ??);
      >EQ normalize nodelta
      lapply (refl ? (jump_expansion_step program (create_label_map program Fp) «Fp,?»))
      [ @HFp
      | lapply (measure_full program Fp ?)
        [ @le_to_le_to_eq
          [ @measure_le
          | (* XXX *) cases daemon 
          ]
        | #Hfull cases (jump_expansion_step program (create_label_map program Fp) «Fp,?») in ⊢ (???% → %);
          #x cases x -x #x cases x -x #Gch #Gpc #Gpol cases Gpol normalize nodelta
          [ #H #EQ2 @⊥ @(absurd ?? (proj2 ?? H)) @Hfull
          | #Gp #HGp #EQ2 cases Fch
            [ normalize nodelta #i #Hi
              lapply (refl ? (lookup ?? (bitvector_of_nat 16 i) Fp 〈0,0,short_jump〉))
              cases (lookup ?? (bitvector_of_nat 16 i) Fp 〈0,0,short_jump〉) in ⊢ (???% → %);
              #x cases x -x #p #a #j normalize nodelta #H
              lapply (proj2 ?? (proj1 ?? (proj1 ?? HGp)) i Hi) lapply (Hfull i Hi) >H
              #H2 >H2 normalize nodelta cases (lookup ?? (bitvector_of_nat 16 i) Gp 〈0,0,short_jump\rangle)
              #x cases x -x #p #a #j' cases j' normalize nodelta #H elim H -H #H
              [1,3: @⊥ @H
              |2,4: destruct (H)
              |5,6: @refl
              ]
            | normalize nodelta /2 by pe_int_refl/
            ]
          ]
        ]
      ]
    ]
  | @le_S_S_to_le @le_S @Hk
  ]
| #n cases (jump_expansion_internal program n) cases (jump_expansion_internal program (S n))
  #x cases x -x #x cases x -x #nch #npc #npol normalize nodelta #Hnpol
  #x cases x -x #x cases x -x #Sch #Scp #Spol normalize nodelta #HSpol
  cases npol in Hnpol; cases Spol in HSpol;
  [ #Hnpol #HSpol %1 //
  |2,3: #x #Hnpol #HSpol %2 @nmk whd in match (policy_equal ???); //
    #H destruct (H)
  |4: #np #Hnp #Sp #HSp whd in match (policy_equal ???); @dec_bounded_forall #m
      cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,0,short_jump〉)
      #x cases x -x #x1 #x2 #x3
      cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,0,short_jump〉)
      #y cases y -y #y1 #y2 #y3 normalize nodelta
      @dec_eq_jump_length  
  ]
]
qed.

(* Take a policy of 〈pc, addr, jump_length〉 tuples, and transform it into
 * a map from pc to jump_length. This cannot be done earlier because the pc
 * changes between iterations. *)
let rec transform_policy (n: nat) policy (acc: BitVectorTrie jump_length 16) on n:
  BitVectorTrie jump_length 16 ≝ 
  match n with
  [ O    ⇒ acc
  | S n' ⇒ 
    match lookup_opt … (bitvector_of_nat 16 n') policy with 
    [ None   ⇒ transform_policy n' policy acc
    | Some x ⇒ let 〈pc,length〉 ≝ x in
      transform_policy n' policy (insert … pc length acc)
    ]
  ].

(* The glue between Policy and Assembly. *)
definition jump_expansion':
 ∀program:preamble × (Σl:list labelled_instruction.|l| < 2^16).
 ∀lookup_labels.policy_type lookup_labels ≝
 λprogram.λlookup_labels.λpc.
  let policy ≝
    transform_policy (|\snd program|) (pi1 … (je_fixpoint (\snd program))) (Stub ??) in
  (* here we must use jump_length_ok *)
  bvt_lookup ? ? pc policy long_jump.
/2 by Stub, mk_Sig/
qed.