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".

definition max_length: jump_length → jump_length → jump_length ≝
  λj1.λj2.
  match j1 with
  [ long_jump   ⇒ long_jump
  | medium_jump ⇒
    match j2 with
    [ long_jump ⇒ long_jump
    | _         ⇒ medium_jump
    ]
  | short_jump  ⇒ j2
  ].

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.
  
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.

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

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

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

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) (λ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|).

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 //
     ]
   | #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 //
       | normalize #_ @(IH i) @H
       ]
     ]
   ]
 ]
qed.  

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; //
        ]
      ]
      >(label_does_not_occur i … Hl) normalize nodelta @nmk //
    ]
  | #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 ?
  ].

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
  ].

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 //
 |11,12,13,16,17: #x #y %1 //
 ]
|2,3: #x %2 /2 by nmk/
|4,5: #x %1 //
|6: #x #y %2 /2 by nmk/
]
qed.
 

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〉).

(* these should be moved to BitVector at some point *)  
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 //
 | #H //
 ]
qed.

lemma jump_not_in_policy: ∀prefix:list labelled_instruction.
 ∀policy:(Σp:jump_expansion_policy.
 (∀i.i ≥ |prefix| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
 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.

definition jump_expansion_start:
  ∀program:(Σl:list labelled_instruction.|l| < 2^16).
  Σpolicy:jump_expansion_policy.
    (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
    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.
    (∀i.i ≥ |prefix| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
    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; //
 ]
 >(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 //
  ]
  @(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 //
  | whd #i #Hi @⊥ @(absurd (i < 0) Hi (not_le_Sn_O ?))
  ]
 | #i #Hi >nth_nil #Hj @⊥ @Hj
]
qed.

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).

definition policy_safe: (*label_map → *)jump_expansion_policy → Prop ≝
 (*λlabels.*)λpolicy.
 bvt_forall (ℕ×ℕ×jump_length) 16 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
    ]
  ).
  
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.
    (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
    jump_in_policy program policy).
  (Σpolicy.
    (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
    jump_in_policy program policy ∧
    policy_increase program old_policy policy)
    ≝ 
  λprogram.λlabels.λold_policy.
  let 〈final_pc, final_policy〉 ≝
    foldl_strong (option Identifier × pseudo_instruction)
    (λprefix.ℕ × Σpolicy.
      (∀i.i ≥ |prefix| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
      jump_in_policy prefix policy ∧
      policy_increase prefix old_policy policy
    )
    program
    (λprefix.λx.λtl.λprf.λacc.
      let 〈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 〈new_pc, new_policy〉 ≝
        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 *)
          〈add_instruction_size pc long_jump instr, policy〉
        | Some z ⇒ let 〈addr,ai〉 ≝ z in
          let new_length ≝ max_length old_length ai in
          〈add_instruction_size pc new_length instr, insert … (bitvector_of_nat 16 (|prefix|)) 〈pc, addr, new_length〉 policy〉 
        ] in
      〈new_pc, new_policy〉
    ) 〈0, Stub ? ?〉 in
    final_policy.
[ @conj [ @conj #i >append_length <commutative_plus #Hi normalize in Hi;
[ #Hi2 cases (lookup ??? old_policy ?) #h #n cases add_instr
  [ @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2)
  | #z cases z -z #z1 #z2 whd in match (snd ???); >lookup_opt_insert_miss
    [ @(proj1 ?? (proj1 ?? (pi2 ?? policy)) 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
      ]
    ]
  ]
| cases (le_to_or_lt_eq … Hi) -Hi;
  [ #Hi; >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) @conj
    [ #Hj lapply (proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc
      cases add_instr cases (lookup ??? old_policy ?) normalize nodelta #x #y
      [ @(proj1 ?? Hacc Hj)
      | #z cases z -z #z1 #z2 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 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc
      #H elim H -H; #h #H elim H -H; #n #H elim H -H #j cases add_instr cases (lookup ??? old_policy ?)
      normalize nodelta #x #y [2: #z]
      #Hl @(proj2 ?? Hacc) @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?)))
      [ <Hl @sym_eq cases z #z1 #z2 whd in match (snd ???); @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
      | @Hl
      ] 
    ]
  | #Hi >(injective_S … Hi) >(nth_append_second ? ? prefix ? ? (le_n (|prefix|)))
     <minus_n_n whd in match (nth ????); whd in match (add_instr); cases instr
     [1: #pi | 2,3: #x | 4,5: #id | 6: #x #y] @conj normalize nodelta
     [3,5,11: #H @⊥ @H (* instr is not a jump *)
     |4,6,12: #H elim H -H; #h #H elim H -H #n #H elim H -H #j cases (lookup ??? old_policy ?)
       #x #y normalize nodelta >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
       [1,3,5: #H destruct (H)]
       @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
       @le_S_S @le_plus_n_r
     |7,9: (* instr is a jump *) #_ cases (lookup ??? old_policy ?) #x cases x #h #n #j 
       whd in match (snd ???); @(ex_intro ?? pc) 
       [ @(ex_intro ?? (\fst (select_jump_length labels pc id)))
         @(ex_intro ?? (max_length j (\snd (select_jump_length labels pc id))))
         cases (select_jump_length labels pc id)
       | @(ex_intro ?? (\fst (select_call_length labels pc id)))
         @(ex_intro ?? (max_length j (\snd (select_call_length labels pc id))))
         cases (select_call_length labels pc id)
       ] #z1 #z2 normalize nodelta @lookup_opt_insert_hit
     |8,10: #_ //
     |1,2: cases pi
       [35,36,37: #H @⊥ @H
       |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #H @⊥ @H
       |1,2,3,6,7,33,34: #x #y #H @⊥ @H
       |9,10,14,15: #id #_ cases (lookup ??? old_policy ?) #x cases x #h #n #j
         whd in match (snd ???); @(ex_intro ?? pc)
         @(ex_intro ?? (\fst (select_reljump_length labels pc id)))
         @(ex_intro ?? (max_length j (\snd (select_reljump_length labels pc id))))
         normalize nodelta cases (select_reljump_length labels pc id) #z1 #z2 normalize nodelta
         @lookup_opt_insert_hit
       |11,12,13,16,17: #x #id #_ cases (lookup ??? old_policy ?) #x cases x #h #n #j
         whd in match (snd ???); @(ex_intro ?? pc)
         @(ex_intro ?? (\fst (select_reljump_length labels pc id)))
         @(ex_intro ?? (max_length j (\snd (select_reljump_length labels pc id))))
         normalize nodelta cases (select_reljump_length labels pc id) #z1 #z2 normalize nodelta
         @lookup_opt_insert_hit
       |72,73,74: #H elim H -H; #h #H elim H -H #n #H elim H -H #j cases (lookup ??? old_policy ?)
        #z cases z -z #x #y #z normalize nodelta
        >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
        [1,3,5: #H destruct (H)]
        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
        @le_S_S @le_plus_n_r      
       |41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69: #x 
        #H elim H -H; #h #H elim H -H #n #H elim H -H #j cases (lookup ??? old_policy ?)
        #z cases z -z #x #y #z normalize nodelta
        >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
        [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35: #H destruct (H)]
        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
        @le_S_S @le_plus_n_r
       |38,39,40,43,44,70,71: #x #y #H elim H -H; #h #H elim H -H #n #H elim H -H #j
        cases (lookup ??? old_policy ?) #z cases z -z #x #y #z normalize nodelta
        >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
        [1,3,5,7,9,11,13: #H destruct (H)]
        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
        @le_S_S @le_plus_n_r              
       |46,47,51,52: #id #_ //
       |48,49,50,53,54: #x #id #_ //
       ]
     ]
   ]
  ]
| lapply (refl ? add_instr) cases add_instr in ⊢ (???% → %); 
  [ #Ha #i >append_length >commutative_plus #Hi normalize in Hi;
    cases (le_to_or_lt_eq … Hi) -Hi; #Hi
    [ cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,0,short_jump〉)
      #x #y @((proj2 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
    | normalize nodelta >(injective_S … Hi)
      >lookup_opt_lookup_miss
      [ >lookup_opt_lookup_miss
        [ //
        | cases (lookup ?? (bitvector_of_nat ? (|prefix|)) old_policy 〈0,0,short_jump〉)
          #x #y normalize nodelta
          >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|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 >p1 >nth_append_second [ <minus_n_n
        generalize in match Ha; normalize nodelta cases instr normalize nodelta 
        [1: #pi cases pi
         [1,2,3,6,7,33,34: #x #y #H normalize /2 by nmk/
         |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #H normalize /2 by nmk/
         |35,36,37: #H normalize /2 by nmk/
         |9,10,14,15: #id whd in match (jump_expansion_step_instruction ???);
           #H destruct (H)
         |11,12,13,16,17: #x #id whd in match (jump_expansion_step_instruction ???);
           #H destruct (H)
         ]
        |2,3: #x #H normalize /2 by nmk/
        |6: #x #y #H normalize /2 by nmk/
        |4,5: #id #H destruct (H)
        ] | @le_n ] 
        | >prf >append_length normalize <plus_n_Sm @le_plus_n_r
        ] 
      ]
    ]
  | #x cases x -x #x1 #x2 #Ha #i >append_length >commutative_plus #Hi normalize in Hi;
    cases (le_to_or_lt_eq … Hi) -Hi; #Hi 
    [ cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,0,short_jump〉)
      #y cases y -y #y1 #y2 #z whd in match (snd ???); normalize nodelta >lookup_insert_miss
      [ @((proj2 ?? (pi2 ?? policy)) 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) elim (proj1 ?? (proj2 ?? (pi2 ?? old_policy) (|prefix|) ?) ?)
      [ #a #H elim H -H; #b #H elim H -H #c #H >H >(lookup_opt_lookup_hit … 〈a,b,c〉 H)
        normalize nodelta >lookup_insert_hit @jmpleq_max_length
      | >prf >p1 >nth_append_second
        [ <minus_n_n generalize in match Ha; normalize nodelta cases instr normalize nodelta 
          [1: #pi cases pi
           [1,2,3,6,7,33,34: #x #y #H normalize in H; destruct (H) 
           |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #H normalize in H; destruct (H)
           |35,36,37: #H normalize in H; destruct (H)
           |9,10,14,15: #id #H //
           |11,12,13,16,17: #x #id #H //
           ]
          |2,3: #x #H normalize in H; destruct (H) 
          |6: #x #y #H normalize in H; destruct (H)
          |4,5: #id #H //
          ]
        | @le_n ] 
      | >prf >append_length normalize <plus_n_Sm @le_plus_n_r
      ]
    ] 
  ] ]
| @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) ]
]
qed.
 
let rec jump_expansion_internal (program: Σl:list labelled_instruction.|l| < 2^16)
  (n: ℕ) on n: (Σpolicy:jump_expansion_policy.
    And
    (∀i:ℕ.i ≥ |program| → i < 2^16 → lookup_opt ? 16 (bitvector_of_nat ? i) policy = None ?)
    (jump_in_policy program policy)) ≝
  match n with
  [ O   ⇒ jump_expansion_start program
  | S m ⇒ let old_policy ≝ jump_expansion_internal program m in
    jump_expansion_step program (create_label_map program old_policy) old_policy
  ].
[ @(proj1 ?? (pi2 ?? (jump_expansion_start program)))
| @(proj1 ?? (pi2 ?? (jump_expansion_step program (create_label_map program old_policy) old_policy)))
]
qed.

definition policy_equal ≝
  λ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.

lemma pe_refl:
  ∀program.reflexive ? (policy_equal 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_sym:
  ∀program.symmetric ? (policy_equal 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_trans:
  ∀program.transitive ? (policy_equal program).
 #program whd #x #y #z whd in match (policy_equal ???); whd in match (policy_equal ?y ?);
 whd in match (policy_equal ? 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.

lemma pe_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
 ∀p1,p2:Σpolicy.
 (∀i:ℕ.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) policy = None ?)
 ∧jump_in_policy program policy.
  policy_equal program p1 p2 →
  policy_equal program (jump_expansion_step program (create_label_map program p1) p1)
    (jump_expansion_step program (create_label_map program p2) p2).
 #program #p1 #p2 #Heq whd #n #Hn lapply (Heq n Hn) #H
 lapply (refl ? (lookup_opt … (bitvector_of_nat ? n) p1))
 cases (lookup_opt … (bitvector_of_nat ? n) p1) in ⊢ (???% → ?);
 [ #Hl lapply ((proj2 ?? (jump_not_in_policy program p1 n Hn)) Hl)
   #Hnotjmp >lookup_opt_lookup_miss
   [ >lookup_opt_lookup_miss
     [ @refl
     | @(proj1 ?? (jump_not_in_policy program (pi1 … (jump_expansion_step program (create_label_map program p2) p2)) n Hn))
       [ @(proj1 ?? (pi2 … (jump_expansion_step program (create_label_map program p2) p2)))
       | @Hnotjmp
       ]
     ]
   | @(proj1 ?? (jump_not_in_policy program (pi1 … (jump_expansion_step program (create_label_map program p1) p1)) n Hn))
     [ @(proj1 ?? (pi2 ?? (jump_expansion_step program (create_label_map program p1) p1)))
     | @Hnotjmp
     ]
   ]
 | #x #Hl 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 (jump_expansion_internal program n) (jump_expansion_internal program (S n)) →
  ∀k.k ≥ n → policy_equal program (jump_expansion_internal program n) (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 … (jump_expansion_internal program (S n)))
   [ @Heq
   | @pe_step @Hind @Heq
   ]
 ]
qed.

lemma thingie:
  ∀A:Prop.(A + ¬A) → (¬¬A) → A.
 #A #Adec #nnA cases Adec
 [ //
 | #H @⊥ @(absurd (¬A) H nnA)
 ]
qed.
 
lemma policy_not_equal_incr: ∀program:(Σl:list labelled_instruction.|l|<2^16).
 ∀policy:(Σp:jump_expansion_policy.
    (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
    jump_in_policy program p).
  ¬policy_equal program policy (jump_expansion_step program (create_label_map program policy) policy) →
  ∃n:ℕ.n < (|program|) ∧ jmple
    (\snd (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,0,short_jump〉))
    (\snd (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉)).
 #program #policy #Hp
 cases (dec_bounded_exists (λn.jmple
   (\snd (bvt_lookup ?? (bitvector_of_nat ? n) policy 〈0,0,short_jump〉))
   (\snd (bvt_lookup ?? (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉))) ? (|program|))
 [ #H elim H; -H #i #Hi @(ex_intro ?? i) @Hi
 | #abs @⊥ @(absurd ?? Hp) #n #Hn
   lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) n Hn)
   lapply (refl ? (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,0,short_jump〉))
   cases (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,0,short_jump〉) in ⊢ (???% → %);
   #z cases z -z #x1 #x2 #x3 #Hx
   lapply (refl ? (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉)) 
   cases (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉) in ⊢ (???% → %); 
   #z cases z -z #y1 #y2 #y3 #Hy
   normalize nodelta #Hj cases Hj
   [ #Hj @⊥ @(absurd ?? abs) @(ex_intro ?? n) @conj [ @Hn | >Hx >Hy @Hj ]
   | //
   ]
 | #n @dec_jmple
 ]
qed.

lemma stupid:
  ∀program,n.
  pi1 … (jump_expansion_step program (create_label_map program (jump_expansion_internal program n)) (jump_expansion_internal program n)) =
  pi1 … (jump_expansion_internal program (S n)).
 //
qed.

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,0,short_jump〉)) with
   [ long_jump   ⇒ measure_int t policy (acc + 2)
   | medium_jump ⇒ measure_int t policy (acc + 1)
   | _           ⇒ measure_int t policy acc
   ]
 ].

(* definition measure ≝ 
  λprogram.λpolicy.measure_int program policy 0. *)
 
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
   [ //
   | #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_incr_or_equal: ∀program:Σl:list labelled_instruction.|l|<2^16.
  ∀policy:Σp:jump_expansion_policy.
    (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
    jump_in_policy program p.∀l.|l| ≤ |program| → ∀acc:ℕ.
  measure_int l policy acc ≤ measure_int l (jump_expansion_step program (create_label_map program policy) policy) acc.
#program #policy #l elim l -l;
  [ #Hp #acc normalize @le_n
  | #h #t #Hind #Hp #acc
    lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) (|t|) Hp)
    whd in match (measure_int ???); whd in match (measure_int ?(jump_expansion_step ???)?);
    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|)) (jump_expansion_step program (create_label_map program policy) policy) 〈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 (jump_expansion_step program (create_label_map program policy) policy) acc))
        |3: @(transitive_le ? (measure_int t (jump_expansion_step program (create_label_map program policy) policy) (acc+1)))
        ]
        [1,3,5: @Hind @(transitive_le … Hp) @le_n_Sn 
        |2,4,6: >measure_plus [1,2: @le_plus_n_r] >measure_plus @le_plus [ @le_n | //] 
        ] 
      ]
    | #Heq >Heq cases y3 normalize nodelta @Hind @(transitive_le … Hp) @le_n_Sn
    ] 
  ]
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.

(* 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.
    (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
    jump_in_policy program p.
  measure_int program policy 0 = measure_int program (jump_expansion_step program (create_label_map program policy) policy) 0 →
  policy_equal program policy (jump_expansion_step program (create_label_map program policy) policy).
#program #policy lapply (le_n (|program|)) @(list_ind ?
  (λx.|x| ≤ |program| → measure_int x (pi1 … policy) 0 = measure_int x (pi1 … (jump_expansion_step program (create_label_map program policy) policy)) 0 →
      policy_equal x (pi1 … policy) (pi1 … (jump_expansion_step program (create_label_map program policy) policy)))
   ?? program)
 [ #Hp #Hm #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 ?(jump_expansion_step ???)?) in Hm;
       lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) (|t|) ?)
       [ @(lt_to_le_to_lt … (|h::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: #H #_ @H
         |2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
           @measure_incr_or_equal @(transitive_le … Hp) @le_n_Sn
         |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
            @measure_incr_or_equal @(transitive_le … Hp) @le_n_Sn 
         |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 ?(jump_expansion_step ???)?) in Hm;
     lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) (|t|) ?)
     [ @(lt_to_le_to_lt … (|h::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
         @measure_incr_or_equal @(transitive_le … Hp) @le_n_Sn
       |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
          @measure_incr_or_equal @(transitive_le … Hp) @le_n_Sn 
       ]
     ]
   ]
 ]  
qed.

lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction.|l| < 2^16.
  |l| ≤ |program| → measure_int l (jump_expansion_internal program 0) 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 (jump_expansion_internal program 0) (|t|) ?) Hj) 〈0,0,short_jump〉)
     [ normalize nodelta @Hind @le_S_to_le ]
     @Hp
   ]
 ]
qed.
  
definition je_fixpoint: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
  Σp:jump_expansion_policy.∃n.∀k.n < k → policy_equal program (jump_expansion_internal program k) p.
 #program @(mk_Sig … (jump_expansion_internal program (2*|program|)))
 @(ex_intro … (2*|program|)) #k #Hk
 cases (dec_bounded_exists (λk.policy_equal program (jump_expansion_internal program k)
   (jump_expansion_internal program (S k))) ? (2*|program|))
 [ #H elim H -H #x #Hx @pe_trans 
   [ @(jump_expansion_internal program x)
   | @pe_sym @equal_remains_equal
     [ @(proj2 ?? Hx)
     | @(transitive_le ? (2*|program|)) 
       [ @le_S_S_to_le @le_S @(proj1 ?? 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 @pe_sym @equal_remains_equal
   [ lapply (measure_full program (jump_expansion_internal program (2*|program|)))
     #Hfull #i #Hi
     lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program (jump_expansion_internal program (2*|program|))) (jump_expansion_internal program (2*|program|)))) i Hi)
     lapply (Hfull ? i Hi)
     [ -i @le_to_le_to_eq
       [ @measure_le 
       | lapply (le_n (2*|program|)) elim (2*|program|) in ⊢ (?%? → %);
         [ #_ >measure_zero @le_n
         | #x #Hind #Hx
           cut (measure_int program (jump_expansion_internal program x) 0 <
                measure_int program (jump_expansion_internal program (S x)) 0)
           [ elim (le_to_or_lt_eq …
               (measure_incr_or_equal program (jump_expansion_internal program x) program (le_n (|program|)) 0))
             [ //
             | #H @⊥ @(absurd ?? (Hfa x Hx)) @measure_special @H
             ]
           | #H lapply (Hind (le_S_to_le … Hx)) #H2 @(le_to_lt_to_lt … H) @H2
           ]
         ]
       ]
     | -Hfull cases (bvt_lookup ?? (bitvector_of_nat 16 i) (jump_expansion_internal program (2*|program|)) 〈0,0,short_jump〉)
       #x cases x -x #x1 #x2 #x3 normalize nodelta #Hfull
       >Hfull cases (bvt_lookup ?? (bitvector_of_nat ? i) ? 〈0,0,short_jump〉)
       #y cases y -y #y1 #y2 #y3 normalize nodelta cases y3 normalize nodelta  
       [1,2: #H elim H #H2 [1,3: @⊥ @H2 |2,4: destruct (H2) ]
       | #_ //
       ]
     ]
   | @le_S_to_le @Hk
   ]
 | #n @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.

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)
    ]
  ].

definition jump_expansion':
 ∀program:preamble × (Σl:list labelled_instruction.|l| < 2^16).
 policy_type ≝
 λprogram.λpc.
  let policy ≝
    transform_policy (|\snd program|) (pi1 … (je_fixpoint (\snd program))) (Stub ??) in
  lookup ? ? pc policy long_jump.
/2 by Stub, mk_Sig/
qed.