include "ASM/ASM.ma".
include "ASM/Arithmetic.ma".
include "ASM/Fetch.ma".
include "ASM/Status.ma".
include "utilities/extralib.ma". 
include "ASM/Assembly.ma".

(* Internal types *)

(* ppc_pc_map: program length × (pseudo program counter ↦ 〈pc, jump_length〉) *)
definition ppc_pc_map ≝ ℕ × (BitVectorTrie (ℕ × jump_length) 16).

(* The different properties that we want/need to prove at some point *)
(* During our iteration, everything not yet seen is None, and vice versa *)
definition out_of_program_none ≝ 
  λprefix:list labelled_instruction.λsigma:ppc_pc_map.
  ∀i.i < 2^16 → (i > |prefix| ↔ bvt_lookup_opt … (bitvector_of_nat ? i) (\snd sigma) = 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_relative_jump ≝
  λinstr:pseudo_instruction.
  match instr with
  [ Instruction i ⇒ is_jump' i
  | _             ⇒ false
  ].
    
definition is_jump ≝
  λinstr:pseudo_instruction.
  match instr with
  [ Instruction i   ⇒ is_jump' i
  | Call _ ⇒ true
  | Jmp _ ⇒ true
  | _ ⇒ false
  ].

definition is_call ≝
  λinstr:pseudo_instruction.
  match instr with
  [ Call _ ⇒ true
  | _ ⇒ false
  ].
  
definition is_jump_to ≝
  λx:pseudo_instruction.λd:Identifier.
  match x with
  [ Instruction i ⇒ match i with
    [ JC j ⇒ d = j
    | JNC j ⇒ d = j
    | JZ j ⇒ d = j
    | JNZ j ⇒ d = j
    | JB _ j ⇒ d = j
    | JNB _ j ⇒ d = j
    | JBC _ j ⇒ d = j
    | CJNE _ j ⇒ d = j
    | DJNZ _ j ⇒ d = j
    | _ ⇒ False
    ]
  | Call c ⇒ d = c
  | Jmp j ⇒ d = j
  | _ ⇒ False
  ].
  
definition not_jump_default ≝ 
  λprefix:list labelled_instruction.λsigma:ppc_pc_map.
  ∀i:ℕ.i < |prefix| →
  ¬is_jump (\snd (nth i ? prefix 〈None ?, Comment []〉)) → 
  \snd (bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉) = short_jump.
 
(* Between two policies, jumps cannot decrease *)
definition jmpeqb: jump_length → jump_length → bool ≝
  λj1.λj2.
  match j1 with
  [ short_jump ⇒ match j2 with [ short_jump ⇒ true | _ ⇒ false ]
  | absolute_jump ⇒ match j2 with [ absolute_jump ⇒ true | _ ⇒ false ]
  | long_jump ⇒ match j2 with [ long_jump ⇒ true | _ ⇒ false ]
  ].

lemma jmpeqb_to_eq: ∀j1,j2.jmpeqb j1 j2 → j1 = j2.
 #j1 #j2 cases j1 cases j2 
 [1,5,9: / by /]
 #H cases H
qed.

definition jmple: jump_length → jump_length → Prop ≝
  λj1.λj2.
  match j1 with
  [ short_jump  ⇒ 
    match j2 with
    [ short_jump ⇒ False
    | _          ⇒ True
    ]
  | absolute_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 jump_increase ≝ 
 λprefix:list labelled_instruction.λop:ppc_pc_map.λp:ppc_pc_map.
 ∀i.i ≤ |prefix| →
   let 〈opc,oj〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd op) 〈0,short_jump〉 in
   let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd p) 〈0,short_jump〉 in
     jmpleq oj j.
     
(* this is the instruction size as determined by the jump length given *)
definition expand_relative_jump_internal_unsafe:
  jump_length → ([[relative]] → preinstruction [[relative]]) → list instruction ≝ 
  λjmp_len:jump_length.λi.
  match jmp_len with
  [ short_jump ⇒ [ RealInstruction (i (RELATIVE (zero 8))) ]
  | absolute_jump ⇒ [ ] (* this should not happen *)
  | long_jump ⇒ 
    [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2)));
      SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *)
      LJMP (ADDR16 (zero 16))
    ]
  ].
 @I
qed.

definition expand_relative_jump_unsafe:
  jump_length → preinstruction Identifier → list instruction ≝ 
  λjmp_len:jump_length.λi.
  match i with
  [ JC jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JC ?)
  | JNC jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNC ?)
  | JB baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JB ? baddr)
  | JZ jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JZ ?)
  | JNZ jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNZ ?)
  | JBC baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JBC ? baddr)
  | JNB baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNB ? baddr)
  | CJNE addr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (CJNE ? addr)
  | DJNZ addr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (DJNZ ? addr)
  | ADD arg1 arg2 ⇒ [ ADD ? arg1 arg2 ]
  | ADDC arg1 arg2 ⇒ [ ADDC ? arg1 arg2 ]
  | SUBB arg1 arg2 ⇒ [ SUBB ? arg1 arg2 ]
  | INC arg ⇒ [ INC ? arg ]
  | DEC arg ⇒ [ DEC ? arg ]
  | MUL arg1 arg2 ⇒ [ MUL ? arg1 arg2 ]
  | DIV arg1 arg2 ⇒ [ DIV ? arg1 arg2 ]
  | DA arg ⇒ [ DA ? arg ]
  | ANL arg ⇒ [ ANL ? arg ]
  | ORL arg ⇒ [ ORL ? arg ]
  | XRL arg ⇒ [ XRL ? arg ]
  | CLR arg ⇒ [ CLR ? arg ]
  | CPL arg ⇒ [ CPL ? arg ]
  | RL arg ⇒ [ RL ? arg ]
  | RR arg ⇒ [ RR ? arg ]
  | RLC arg ⇒ [ RLC ? arg ]
  | RRC arg ⇒ [ RRC ? arg ]
  | SWAP arg ⇒ [ SWAP ? arg ]
  | MOV arg ⇒ [ MOV ? arg ]
  | MOVX arg ⇒ [ MOVX ? arg ]
  | SETB arg ⇒ [ SETB ? arg ]
  | PUSH arg ⇒ [ PUSH ? arg ]
  | POP arg ⇒ [ POP ? arg ]
  | XCH arg1 arg2 ⇒ [ XCH ? arg1 arg2 ]
  | XCHD arg1 arg2 ⇒ [ XCHD ? arg1 arg2 ]
  | RET ⇒ [ RET ? ]
  | RETI ⇒ [ RETI ? ]
  | NOP ⇒ [ RealInstruction (NOP ?) ]
  ].

definition instruction_size_jmplen:
 jump_length → pseudo_instruction → ℕ ≝
  λjmp_len.
  λi.
  let pseudos ≝ match i with
  [ Cost cost ⇒ [ ]
  | Comment comment ⇒ [ ]
  | Call call ⇒
    match jmp_len with
    [ short_jump ⇒ [ ] (* this should not happen *)
    | absolute_jump ⇒ [ ACALL (ADDR11 (zero 11)) ]
    | long_jump ⇒ [ LCALL (ADDR16 (zero 16)) ]
    ]
  | Mov d trgt ⇒
     [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, DATA16 (zero 16)〉))))]
  | Instruction instr ⇒ expand_relative_jump_unsafe jmp_len instr
  | Jmp jmp ⇒
    match jmp_len with
    [ short_jump ⇒ [ SJMP (RELATIVE (zero 8)) ]
    | absolute_jump ⇒ [ AJMP (ADDR11 (zero 11)) ]
    | long_jump ⇒ [ LJMP (ADDR16 (zero 16)) ]
    ] 
  ] in
  let mapped ≝ map ? ? assembly1 pseudos in
  let flattened ≝ flatten ? mapped in
  let pc_len ≝ length ? flattened in
    pc_len.
 @I.
qed.

definition sigma_compact_unsafe ≝ 
 λprefix:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map.
 ∀n.n < |prefix| →
  match bvt_lookup_opt … (bitvector_of_nat ? n) (\snd sigma) with
  [ None ⇒ False
  | Some x ⇒ let 〈pc,j〉 ≝ x in
    match bvt_lookup_opt … (bitvector_of_nat ? (S n)) (\snd sigma) with
    [ None ⇒ False
    | Some x1 ⇒ let 〈pc1,j1〉 ≝ x1 in
       pc1 = pc + instruction_size_jmplen j (\snd (nth n ? prefix 〈None ?, Comment []〉))
    ]
  ].
   
(* new safety condition: sigma corresponds to program and resulting program is compact *)
definition sigma_compact ≝ 
 λprogram:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map.
 ∀n.n < |program| → 
  match bvt_lookup_opt … (bitvector_of_nat ? n) (\snd sigma) with
  [ None ⇒ False
  | Some x ⇒ let 〈pc,j〉 ≝ x in
    match bvt_lookup_opt … (bitvector_of_nat ? (S n)) (\snd sigma) with
    [ None ⇒ False
    | Some x1 ⇒ let 〈pc1,j1〉 ≝ x1 in
       pc1 = pc + instruction_size (λid.bitvector_of_nat ? (lookup_def ?? labels id 0))
         (λppc.bitvector_of_nat ? (\fst (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉)))
         (λppc.jmpeqb long_jump (\snd (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉)))
         (bitvector_of_nat ? n) (\snd (nth n ? program 〈None ?, Comment []〉))
    ]
  ].

(* jumps are of the proper size *)
definition sigma_safe ≝ 
 λprefix:list labelled_instruction.λlabels:label_map.λadded:ℕ.
 λold_sigma:ppc_pc_map.λsigma:ppc_pc_map.
 ∀i.i < |prefix| →
 let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉 in
 let pc_plus_jmp_length ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat ? (S i)) (\snd sigma) 〈0,short_jump〉)) in
 let 〈label,instr〉 ≝ nth i ? prefix 〈None ?, Comment [ ]〉 in
 ∀dest.is_jump_to instr dest → 
   let paddr ≝ lookup_def … labels dest 0 in
   let addr ≝ bitvector_of_nat ? (if leb paddr (|prefix|) (* jump to address already known *)
   then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd sigma) 〈0,short_jump〉)
   else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in
   match j with
   [ short_jump ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = true ∧
       bool_to_Prop (¬is_call instr)
   | absolute_jump ⇒  \fst (absolute_jump_cond pc_plus_jmp_length addr) = true ∧
       \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧
       bool_to_Prop (¬is_relative_jump instr)
   | long_jump   ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧
       \fst (absolute_jump_cond pc_plus_jmp_length addr) = false
   ].
  
(* 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
  | absolute_jump ⇒
    match j2 with
    [ absolute_jump ⇒ absolute_jump
    | _           ⇒ long_jump
    ]
  | short_jump  ⇒
    match j2 with
    [ short_jump ⇒ short_jump
    | _          ⇒ long_jump
    ]
  ].

lemma dec_jmple: ∀x,y:jump_length.Sum (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.Sum (a = b) (a ≠ b).
  #a #b cases a cases b /2/
  %2 @nmk #H destruct (H)
qed.
  
(* The function that creates the label-to-address map *)
definition create_label_map: ∀program:list labelled_instruction.
  (Σlabels:label_map.
    ∀l.occurs_exactly_once ?? l program →
    And (bitvector_of_nat ? (lookup_def ?? labels l 0) =
     address_of_word_labels_code_mem program l)
    (lookup_def ?? labels l 0 < |program|)
  ) ≝
 λprogram.
   \fst (create_label_cost_map program).
 #l #Hl lapply (pi2 ?? (create_label_cost_map0 program)) @pair_elim
 #labels #costs #EQ normalize nodelta #H whd in match create_label_cost_map;
 normalize nodelta >EQ @(H l Hl)
qed.

(* General note on jump length selection: the jump displacement is added/replaced
 * AFTER the fetch (and attendant PC increase), but we calculate before the
 * fetch, which means that in the case of a short and medium jump we are 2
 * bytes off and have to compensate.
 * For the long jump we don't care, because the PC gets replaced integrally anyway. *)
definition select_reljump_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → ℕ →
  Identifier → jump_length ≝
  λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl.
  let pc ≝ \fst inc_sigma in
  let pc_plus_jmp_length ≝ bitvector_of_nat ? (pc+2) in
  let paddr ≝ lookup_def … labels lbl 0 in
  let addr ≝ bitvector_of_nat ? (if leb paddr ppc (* jump to address already known *)
  then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉)
  else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in
  let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length addr in
  if sj_possible
  then short_jump
  else long_jump.

definition select_call_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → ℕ →
  Identifier → jump_length ≝
  λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl.
  let pc ≝ \fst inc_sigma in
  let pc_plus_jmp_length ≝ bitvector_of_nat ? (pc+2) in
  let paddr ≝ lookup_def ? ? labels lbl 0 in
  let addr ≝ bitvector_of_nat ?
    (if leb paddr ppc (* jump to address already known *)
    then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉)
    else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in
  let 〈aj_possible, disp〉 ≝ absolute_jump_cond pc_plus_jmp_length addr in   
  if aj_possible
  then absolute_jump
  else long_jump.
  
definition select_jump_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → ℕ →
  Identifier → jump_length ≝
  λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl.
  let pc ≝ \fst inc_sigma in
  let pc_plus_jmp_length ≝ bitvector_of_nat ? (pc+2) in
  let paddr ≝ lookup_def … labels lbl 0 in
  let addr ≝ bitvector_of_nat ? (if leb paddr ppc (* jump to address already known *)
  then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉)
  else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in
  let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length addr in
  if sj_possible
  then short_jump
  else select_call_length labels old_sigma inc_sigma added ppc lbl.

definition destination_of: preinstruction Identifier → option Identifier ≝
  λi.
  match i with
  [ JC j     ⇒ Some ? j
  | JNC j    ⇒ Some ? j
  | JZ j     ⇒ Some ? j
  | JNZ j    ⇒ Some ? j
  | JB _ j   ⇒ Some ? j
  | JBC _ j  ⇒ Some ? j
  | JNB _ j  ⇒ Some ? j
  | CJNE _ j ⇒ Some ? j
  | DJNZ _ j ⇒ Some ? j
  | _        ⇒ None ?
  ].

definition jump_expansion_step_instruction: label_map → ppc_pc_map → ppc_pc_map →
  ℕ → ℕ → preinstruction Identifier → option jump_length ≝
  λlabels.λold_sigma.λinc_sigma.λadded.λppc.λi.
  match destination_of i with
  [ Some j     ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
  | None       ⇒ None ?
  ].

(* The first step of the jump expansion: everything to short. *)
definition jump_expansion_start:
  ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16 ∧ is_well_labelled_p l).
  ∀labels:label_map.
  Σpolicy:option ppc_pc_map.
    match policy with
    [ None ⇒ True
    | Some p ⇒ And (And (And (And (And 
       (not_jump_default (pi1 ?? program) p)
       (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0))
       (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉)))
       (sigma_compact_unsafe program labels p))
       (∀i.i ≤ |program| → ∃pc.
         bvt_lookup_opt … (bitvector_of_nat ? i) (\snd p) = Some ? 〈pc,short_jump〉))
       (\fst p ≤ 2^16)         
    ] ≝ 
  λprogram.λlabels.
  let final_policy ≝ foldl_strong (option Identifier × pseudo_instruction)
  (λprefix.Σpolicy:ppc_pc_map.And (And (And (And 
    (not_jump_default prefix policy)
    (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
    (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉)))
    (sigma_compact_unsafe prefix labels policy))
    (∀i.i ≤ |prefix| → ∃pc.
      bvt_lookup_opt … (bitvector_of_nat ? i) (\snd policy) = Some ? 〈pc,short_jump〉))
  program
  (λprefix.λx.λtl.λprf.λp.
   let 〈pc,sigma〉 ≝ pi1 ?? p in
   let 〈label,instr〉 ≝ x in
   let isize ≝ instruction_size_jmplen short_jump instr in
   〈pc + isize, bvt_insert … (bitvector_of_nat 16 (S (|prefix|))) 〈pc+isize,short_jump〉 sigma〉
  ) 〈0, bvt_insert ?? (bitvector_of_nat 16 0) 〈0,short_jump〉 (Stub ??)〉 in
  if gtb (\fst (pi1 ?? final_policy)) 2^16 then
    None ?
  else
    Some ? (pi1 ?? final_policy).
[ / by I/
| lapply p -p cases final_policy -final_policy #p #Hp #hg
  @conj [ @Hp | @not_lt_to_le @ltb_false_to_not_lt @hg ]
| @conj [ @conj [ @conj [ @conj
  [ (* not_jump_default *) cases p -p #p cases p -p #pc #sigma #Hp
    cases x in prf; #lbl #ins #prf #i >append_length <commutative_plus #Hi
    normalize in Hi; normalize nodelta cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    [ >lookup_insert_miss
      [ (* USE[pass]: not_jump_default *)
        lapply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))) i Hi)
        >nth_append_first
        [ #H #H2 @H @H2
        | @Hi
        ]
      | @bitvector_of_nat_abs
        [ @(transitive_lt ??? Hi) @le_S_to_le]
        [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length
          <plus_n_Sm @le_S_S @le_plus_n_r
        | @lt_to_not_eq @le_S @Hi
        ]
      ]
    | >Hi >lookup_insert_miss
      [ #_ (* USE: everything is short *)
        elim ((proj2 ?? Hp) (|prefix|) (le_n (|prefix|))) #pc #Hl
        >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) @refl
      | @bitvector_of_nat_abs
        [ @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length @le_plus_n_r
        | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <plus_n_Sm @le_S_S
          @le_plus_n_r
        | @lt_to_not_eq @le_n
        ]
      ]
    ]
  | (* 0 ↦ 0 *)
    cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta
    >lookup_insert_miss
    [ (* USE[pass]: 0 ↦ 0 *)
      @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))
    | @bitvector_of_nat_abs
      [ / by /
      | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S <plus_n_Sm
        @le_S_S @le_plus_n_r
      | @lt_to_not_eq / by /
      ]
    ]
  ]
  | (* fst p = pc *)
    cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta
    >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl
  ]
  | (* policy_compact_unsafe *) #i >append_length <commutative_plus #Hi normalize in Hi;
    cases p -p #p cases p -p #fpc #sigma #Hp cases x #lbl #instr normalize nodelta
    cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    [ >lookup_opt_insert_miss
      [ >lookup_opt_insert_miss
        [ (* USE[pass]: policy_compact_unsafe *)
          lapply (proj2 ?? (proj1 ?? Hp) i Hi) 
          lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? i) sigma))
          cases (bvt_lookup_opt … (bitvector_of_nat ? i) sigma) in ⊢ (???% → %);
          [ #_ normalize nodelta / by /
          | #x cases x -x #pci #ji #EQi
            lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) sigma))
            cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) sigma) in ⊢ (???% → %);
            [ #_ normalize nodelta / by /
            | #x cases x -x #pcSi #jSi #EQSi normalize nodelta >nth_append_first
              [ / by /
              | @Hi
              ]
            ]
          ]
        ]
      ]
      [2: lapply (le_S_to_le … Hi) -Hi #Hi]
      @bitvector_of_nat_abs
      [1,4: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <commutative_plus
        @le_plus_a @Hi
      |2,5: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <plus_n_Sm
        @le_S_S @le_plus_n_r
      |3,6: @lt_to_not_eq @le_S_S @Hi
      ]
    | >lookup_opt_insert_miss
      [ >Hi >lookup_opt_insert_hit normalize nodelta
        (* USE: everything is short, fst p = pc *)
        elim ((proj2 ?? Hp) (|prefix|) (le_n ?)) #pc #Hl
        lapply (proj2 ?? (proj1 ?? (proj1 ?? Hp))) >Hl
        >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) #EQ normalize nodelta >nth_append_second
        [ <minus_n_n whd in match (nth ????); >EQ @refl
        | @le_n
        ]
      | @bitvector_of_nat_abs
        [ @(transitive_lt … (proj1 ?? (pi2 ?? program))) >Hi >prf @le_S_S >append_length <commutative_plus
          @le_plus_a @le_n
        | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <plus_n_Sm
          @le_S_S @le_plus_n_r
        | @lt_to_not_eq @le_S_S >Hi @le_n
        ]
      ]
    ]
  ]
  | (* everything is short *) #i >append_length <commutative_plus #Hi normalize in Hi;
    cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta
    cases (le_to_or_lt_eq … Hi) -Hi #Hi
    [ >lookup_opt_insert_miss
      [ (* USE[pass]: everything is short *)
        @((proj2 ?? Hp) i (le_S_S_to_le … Hi))
      | @bitvector_of_nat_abs
        [ @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S
          >commutative_plus @le_plus_a @le_S_S_to_le @Hi
        | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length <plus_n_Sm
          @le_S_S @le_S_S @le_plus_n_r
        | @lt_to_not_eq @Hi
        ]
      ]
    | >Hi >lookup_opt_insert_hit @(ex_intro ?? (pc+instruction_size_jmplen short_jump instr))
      @refl
    ]
  ]
| @conj [ @conj [ @conj [ @conj 
  [ #i cases i
    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O 
    | -i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O
    ]
  ] ]
  >lookup_insert_hit @refl
  | #i cases i
    [ #Hi @⊥ @(absurd … Hi) @le_to_not_lt @le_n
    | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    ]
  ]
  | #i cases i
    [ #Hi >lookup_opt_insert_hit @(ex_intro ?? 0) @refl
    | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    ]
  ]
]
qed.

(* NOTE: we only compare the first elements here because otherwise the 
 * added = 0 → policy_equal property of jump_expansion_step doesn't hold:
 * if we have not added anything to the pc, we only know the PC hasn't changed,
 * there might still have been a short/medium jump change *)
definition sigma_pc_equal ≝
  λprogram:list labelled_instruction.λp1,p2:ppc_pc_map.
  (∀n.n ≤ |program| →
    \fst (bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉) =
    \fst (bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉)).

definition sigma_jump_equal ≝
  λprogram:list labelled_instruction.λp1,p2:ppc_pc_map.
  (∀n.n < |program| →
    \snd (bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉) =
    \snd (bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉)).
    
definition nec_plus_ultra ≝
  λprogram:list labelled_instruction.λp:ppc_pc_map.
  ¬(∀i.i < |program| → is_jump (\snd (nth i ? program 〈None ?, Comment []〉)) → 
  \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,short_jump〉) = long_jump). 
  
(*include alias "common/Identifiers.ma".*)
include alias "ASM/BitVector.ma".
include alias "basics/lists/list.ma".
include alias "arithmetics/nat.ma".
include alias "basics/logic.ma".

lemma jump_length_equal_max: ∀a,b,i.
  is_jump i → instruction_size_jmplen (max_length a b) i = instruction_size_jmplen a i →
  (max_length a b) = a.
 #a #b #i cases i
 [1: #pi cases pi
   try (#x #y #H #EQ) try (#x #H #EQ) try (#H #EQ) cases H
   cases a in EQ; cases b #EQ try %
   try (normalize in EQ; destruct(EQ) @False)
   try (lapply EQ @(subaddressing_mode_elim … x) #w #EQ normalize in EQ; destruct(EQ) @False)
   lapply EQ -EQ cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w
   try (#EQ normalize in EQ; destruct(EQ) @False)
   @(subaddressing_mode_elim … a1) #w
   #EQ normalize in EQ; destruct(EQ)
  |2,3,6: #x [3: #y] #H cases H
  |4,5: #id #_ cases a cases b #H try % normalize in H; destruct(H)
 ]
qed.

lemma jump_length_le_max: ∀a,b,i.is_jump i → 
  instruction_size_jmplen a i ≤ instruction_size_jmplen (max_length a b) i.
 #a #b #i cases i
 [2,3,6: #x [3: #y] #H cases H
 |4,5: #id #_ cases a cases b / by le_n/
 |1: #pi cases pi
    try (#x #y #H) try (#x #H) try (#H) cases H
    -H cases a cases b @leb_true_to_le try %
    try (@(subaddressing_mode_elim … x) #w % @False)
    cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w try %
    @(subaddressing_mode_elim … a1) #w %
 ]
qed.

lemma equal_compact_unsafe_compact: ∀program:(Σl.(S (|l|)) < 2^16 ∧ is_well_labelled_p l).
  ∀old_sigma.∀sigma.
  sigma_pc_equal program old_sigma sigma → 
  sigma_safe program (create_label_map program) 0 old_sigma sigma → 
  sigma_compact_unsafe program (create_label_map program) sigma →
  sigma_compact program (create_label_map program) sigma.
  #program cases program -program #program #Hprogram #old_sigma #sigma #Hequal
  #Hsafe #Hcp_unsafe #i #Hi
  lapply (Hcp_unsafe i Hi) lapply (Hsafe i Hi)
  lapply (refl ? (lookup_opt … (bitvector_of_nat ? i) (\snd sigma)))
  cases (lookup_opt … (bitvector_of_nat ? i) (\snd sigma)) in ⊢ (???% → %);
  [ / by /
  | #x cases x -x #x1 #x2 #EQ
    cases (lookup_opt … (bitvector_of_nat ? (S i)) (\snd sigma))
    [ / by /
    | #y cases y -y #y1 #y2 normalize nodelta #H #H2
      cut (instruction_size_jmplen x2 
       (\snd (nth i ? program 〈None ?, Comment []〉)) =
       instruction_size … (bitvector_of_nat ? i)
       (\snd (nth i ? program 〈None ?, Comment []〉)))
      [5: #H3 <H3 @H2
      |4: whd in match (instruction_size_jmplen ??);
          whd in match (instruction_size …);
          whd in match (assembly_1_pseudoinstruction …);
          whd in match (expand_pseudo_instruction …);
          normalize nodelta whd in match (append …) in H;
          lapply (refl ? (nth i ? program 〈None ?, Comment []〉)) lapply H
          cases (nth i ? program 〈None ?,Comment []〉) in ⊢ (% → ???% → %);
          #lbl #instr cases instr
          [2,3,6: #x [3: #y] normalize nodelta #H #_ %
          |4,5: #x >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #Hj #Heq
            lapply (Hj x (refl ? x)) -Hj normalize nodelta
            >add_bitvector_of_nat_plus <(plus_n_Sm i 0) <plus_n_O
            cases x2 normalize nodelta
            [1,4: whd in match short_jump_cond; normalize nodelta
              cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
              [1,3: cases (create_label_map program) #clm #Hclm
                @le_S_to_le @(proj2 ?? (Hclm x ?))
                [1: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Jmp x) ??)
                |2: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Call x) ??)]
                [1,4: >nat_of_bitvector_bitvector_of_nat_inverse
                  [2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi
                |2,5: whd in match fetch_pseudo_instruction; normalize nodelta
                  >nth_safe_nth
                  [1,3: >nat_of_bitvector_bitvector_of_nat_inverse
                    [1,3: >Heq / by refl/
                    |2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi
                    ]
                  ]
                |3,6: / by /
                ]
              |2,4: #H >(le_to_leb_true … H) normalize nodelta <plus_n_O
              cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
              #result #flags normalize nodelta
              cases (vsplit bool 9 7 result) #upper #lower normalize nodelta
              cases (get_index' bool 2 0 flags) normalize nodelta
              [3,4: #H cases (proj2 ?? H)
              |1,2: cases (eq_bv 9 upper ?)
                [2,4: #H lapply (proj1 ?? H) #H3 destruct (H3)
                |1,3: #_ normalize nodelta @refl
                ]
              ]
              ]
            |2,5: whd in match short_jump_cond; whd in match absolute_jump_cond;
              cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
              [1,3: cases (create_label_map program) #clm #Hclm
                @le_S_to_le @(proj2 ?? (Hclm x ?))
                [1: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Jmp x) ??)
                |2: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Call x) ??)]
                [1,4: >nat_of_bitvector_bitvector_of_nat_inverse
                  [2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi
                |2,5: whd in match fetch_pseudo_instruction; normalize nodelta
                  >nth_safe_nth
                  [1,3: >nat_of_bitvector_bitvector_of_nat_inverse
                    [1,3: >Heq / by refl/
                    |2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi
                    ]
                  ]
                |3,6: / by /
                ]
              |2,4: #H >(le_to_leb_true … H) normalize nodelta <plus_n_O
              normalize nodelta cases (vsplit bool 5 11 ?) #addr1 #addr2
              cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta
              cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
              #result #flags normalize nodelta
              cases (vsplit bool 9 7 result) #upper #lower normalize nodelta
              cases (get_index' bool 2 0 flags) normalize nodelta
              #H >(proj2 ?? (proj1 ?? H)) >(proj1 ?? (proj1 ?? H)) normalize nodelta @refl
              ]
            |3,6: whd in match short_jump_cond; whd in match absolute_jump_cond;
              cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
              [1,3: cases (create_label_map program) #clm #Hclm
                @le_S_to_le @(proj2 ?? (Hclm x ?))
                [1: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Jmp x) ??)
                |2: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Call x) ??)]
                [1,4: >nat_of_bitvector_bitvector_of_nat_inverse
                  [2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi
                |2,5: whd in match fetch_pseudo_instruction; normalize nodelta
                  >nth_safe_nth
                  [1,3: >nat_of_bitvector_bitvector_of_nat_inverse
                    [1,3: >Heq / by refl/
                    |2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi
                    ]
                  ]
                |3,6: / by /
                ]
              |2,4: #H >(le_to_leb_true … H) normalize nodelta <plus_n_O
              cases (vsplit bool 5 11 ?) #addr1 #addr2
              cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta
              cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
              #result #flags normalize nodelta
              cases (vsplit bool 9 7 result) #upper #lower normalize nodelta
              cases (get_index' bool 2 0 flags) normalize nodelta
              #H >(proj1 ?? H) >(proj2 ?? H) normalize nodelta @refl
              ]
            ]
          |1: cut (∀A,B,ab.fst A B ab = (let 〈a,b〉 ≝ ab in a))
              [#A #B * / by refl/] #fst_foo
              cut (∀x.
                    instruction_has_label x (\snd  (nth i labelled_instruction program 〈None (identifier ASMTag),Comment []〉)) →
               lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
              [#x #Heq cases (create_label_map program) #clm #Hclm
               @le_S_to_le @(proj2 ?? (Hclm x ?))
               @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (\snd (nth i ? program 〈None ?, Comment []〉)) ??)
               [ >nat_of_bitvector_bitvector_of_nat_inverse
                 [2: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi
               | whd in match fetch_pseudo_instruction; normalize nodelta
                 >nth_safe_nth
                 [ >nat_of_bitvector_bitvector_of_nat_inverse
                   [ @pair_elim // ]
                   @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi ]
                 | assumption ]] #lookup_in_program
              -H #pi cases pi
              try (#y #x #H #Heq) try (#x #H #Heq) try (#H #Heq) try %
              normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) in H;
              #Hj lapply (Hj x (refl ? x)) -Hj
              whd in match expand_relative_jump; normalize nodelta
              whd in match expand_relative_jump_internal; normalize nodelta
              whd in match expand_relative_jump_unsafe; normalize nodelta
              whd in match expand_relative_jump_internal_unsafe;
              normalize nodelta >(add_bitvector_of_nat_plus ? i 1)
              <(plus_n_Sm i 0) <plus_n_O <plus_n_O cases x2 normalize nodelta
              [1,4,7,10,13,16,19,22,25:
                >fst_foo @pair_elim #sj_possible #disp #H #H2
                @(pair_replace ?????????? (eq_to_jmeq … H))
                [1,3,5,7,9,11,13,15,17: >(le_to_leb_true … (lookup_in_program …))
                  try % >Heq % ]
                >(proj1 ?? H2) try (@refl) normalize nodelta
                [1,2,3,5: @(subaddressing_mode_elim … y) #w %
                | cases y * #sth #sth2 @(subaddressing_mode_elim … sth) 
                  @(subaddressing_mode_elim … sth2) #x [3,4: #x2] %
                ]
              |2,5,8,11,14,17,20,23,26: ** #_ #_ #abs cases abs
              ]
              * #H #_ >fst_foo in H; @pair_elim #sj_possible #disp #H 
              @(pair_replace ?????????? (eq_to_jmeq … H))
                [1,3,5,7,9,11,13,15,17: >(le_to_leb_true … (lookup_in_program …))
                  try % >Heq % ]
                #H2 >H2 try (@refl) normalize nodelta
                [1,2,3,5: @(subaddressing_mode_elim … y) #w %
                | cases y * #sth #sth2 @(subaddressing_mode_elim … sth2) #w
                  [1,2: %] whd in match (map ????); whd in match (flatten ??);
                  whd in match (map ????) in ⊢ (???%); whd in match (flatten ??) in ⊢ (???%);
                  >length_append >length_append %]]]]]
qed.

lemma instruction_size_irrelevant: ∀i.
  ¬is_jump i → ∀j1,j2.instruction_size_jmplen j1 i = instruction_size_jmplen j2 i.
 #i cases i 
 [2,3,6: #x [3: #y] #Hj #j1 #j2 %
 |4,5: #x #Hi cases Hi
 |1: #pi cases pi try (#x #y #Hj #j1 #j2) try (#y #Hj #j1 #j2) try (#Hj #j1 #j2)
     try % cases Hj ]
qed.