Changeset 1879


Ignore:
Timestamp:
Apr 5, 2012, 6:13:26 PM (8 years ago)
Author:
boender
Message:
  • Policy compiles until the end, still some (fairly trivial) cases daemon left
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r1810 r1879  
    1313definition label_map ≝ identifier_map ASMTag (ℕ × ℕ).
    1414
    15 (* jump_expansion_policy: instruction number ↦ 〈pc, addr, jump_length〉 *)
    16 definition jump_expansion_policy ≝ BitVectorTrie (ℕ × ℕ × jump_length) 16.
     15(* jump_expansion_policy: instruction number ↦ 〈pc, [addr, jump_length]〉 *)
     16definition jump_expansion_policy ≝ ℕ × (BitVectorTrie (ℕ × ℕ × jump_length) 16).
    1717
    1818(* The different properties that we want/need to prove at some point *)
     
    2020definition out_of_program_none ≝
    2121  λprefix:list labelled_instruction.λpolicy:jump_expansion_policy.
    22   ∀i.i ≥ |prefix| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) policy = None ?.
     22  ∀i.i ≥ |prefix| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) (\snd policy) = None ?.
    2323
    2424(* If instruction i is a jump, then there will be something in the policy at
     
    5353  ∀i:ℕ.i < |prefix| →
    5454  (is_jump (nth i ? prefix 〈None ?, Comment []〉) ↔
    55    ∃p,a,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,a,j〉).
     55   ∃p:ℕ.∃a:ℕ.∃j:jump_length.
     56     lookup_opt … (bitvector_of_nat 16 i) (\snd policy) = Some ? 〈p,a,j〉).
    5657
    5758definition labels_okay ≝
    5859  λlabels:label_map.λpolicy:jump_expansion_policy.
    59   bvt_forall ?? policy (λn.λx.let 〈pc,addr_nat,i〉 ≝ x in
    60     ∃id:Identifier.
    61       \snd (lookup_def … labels id 〈0,pc〉) = addr_nat
     60  bvt_forall ?? (\snd policy) (λn.λx.
     61   let 〈pc,addr_nat,j〉 ≝ x in
     62   ∃id:Identifier.\snd (lookup_def … labels id 〈0,pc〉) = addr_nat
    6263  ).
    6364 
     
    8687 λprogram.λop.λp.
    8788  (∀i:ℕ.i < |program| →
    88     let 〈i1,i2,oj〉 ≝ bvt_lookup ?? (bitvector_of_nat ? i) op 〈0,0,short_jump〉 in
    89     let 〈i3,i4,j〉 ≝ bvt_lookup ?? (bitvector_of_nat ? i) p 〈0,0,short_jump〉 in
    90     jmpleq oj j).
     89    let 〈pc1,i1,oj〉 ≝ bvt_lookup ?? (bitvector_of_nat ? i) (\snd op) 〈0,0,short_jump〉 in
     90    let 〈pc2,i2,j〉 ≝ bvt_lookup ?? (bitvector_of_nat ? i) (\snd p) 〈0,0,short_jump〉 in
     91    jmpleq oj j
     92  ).
    9193
    9294(* Policy safety *)
    9395definition policy_safe: jump_expansion_policy → Prop ≝
    9496 λpolicy.
    95  bvt_forall ?? policy (λn.λx.let 〈pc_nat,addr_nat,jmp_len〉 ≝ x in
     97 bvt_forall ?? (\snd policy) (λn.λx.let 〈pc_nat,addr_nat,jmp_len〉 ≝ x in
    9698   match jmp_len with
    9799   [ short_jump  ⇒ if leb pc_nat addr_nat
    98100      then le (addr_nat - pc_nat) 126
    99101      else le (pc_nat - addr_nat) 129
    100    | medium_jump ⇒
     102   | medium_jump ⇒  
    101103      let addr ≝ bitvector_of_nat 16 addr_nat in
    102104      let pc ≝ bitvector_of_nat 16 pc_nat in
     
    174176qed.
    175177
    176 definition add_instruction_size: ℕ → jump_length → pseudo_instruction → ℕ ≝
    177   λpc.λjmp_len.λinstr.
    178   let bv_pc ≝ bitvector_of_nat 16 pc in
    179   let ilist ≝ expand_pseudo_instruction_safe (λx.bv_pc) bv_pc jmp_len ? instr in
     178definition expand_relative_jump_internal_unsafe:
     179  jump_length → ([[relative]] → preinstruction [[relative]]) → option (list instruction) ≝
     180  λjmp_len,i.
     181  match jmp_len with
     182  [ short_jump ⇒ Some ? [ RealInstruction (i (RELATIVE (zero 8))) ]
     183  | medium_jump ⇒ None …
     184  | long_jump ⇒ Some ?
     185    [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2)));
     186      SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *)
     187      LJMP (ADDR16 (zero 16))
     188    ]
     189  ].
     190 @I
     191qed.
     192
     193definition expand_relative_jump_unsafe:
     194  jump_length → preinstruction Identifier → option (list instruction) ≝
     195  λjmp_len,i.
     196  match i with
     197  [ JC jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JC ?)
     198  | JNC jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNC ?)
     199  | JB baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JB ? baddr)
     200  | JZ jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JZ ?)
     201  | JNZ jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNZ ?)
     202  | JBC baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JBC ? baddr)
     203  | JNB baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNB ? baddr)
     204  | CJNE addr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (CJNE ? addr)
     205  | DJNZ addr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (DJNZ ? addr)
     206  | ADD arg1 arg2 ⇒ Some … [ ADD ? arg1 arg2 ]
     207  | ADDC arg1 arg2 ⇒ Some … [ ADDC ? arg1 arg2 ]
     208  | SUBB arg1 arg2 ⇒ Some … [ SUBB ? arg1 arg2 ]
     209  | INC arg ⇒ Some … [ INC ? arg ]
     210  | DEC arg ⇒ Some … [ DEC ? arg ]
     211  | MUL arg1 arg2 ⇒ Some … [ MUL ? arg1 arg2 ]
     212  | DIV arg1 arg2 ⇒  Some … [ DIV ? arg1 arg2 ]
     213  | DA arg ⇒ Some … [ DA ? arg ]
     214  | ANL arg ⇒ Some … [ ANL ? arg ]
     215  | ORL arg ⇒ Some … [ ORL ? arg ]
     216  | XRL arg ⇒ Some … [ XRL ? arg ]
     217  | CLR arg ⇒ Some … [ CLR ? arg ]
     218  | CPL arg ⇒ Some … [ CPL ? arg ]
     219  | RL arg ⇒ Some … [ RL ? arg ]
     220  | RR arg ⇒ Some … [ RR ? arg ]
     221  | RLC arg ⇒ Some … [ RLC ? arg ]
     222  | RRC arg ⇒ Some … [ RRC ? arg ]
     223  | SWAP arg ⇒ Some … [ SWAP ? arg ]
     224  | MOV arg ⇒ Some … [ MOV ? arg ]
     225  | MOVX arg ⇒ Some … [ MOVX ? arg ]
     226  | SETB arg ⇒ Some … [ SETB ? arg ]
     227  | PUSH arg ⇒ Some … [ PUSH ? arg ]
     228  | POP arg ⇒ Some … [ POP ? arg ]
     229  | XCH arg1 arg2 ⇒ Some … [ XCH ? arg1 arg2 ]
     230  | XCHD arg1 arg2 ⇒ Some … [ XCHD ? arg1 arg2 ]
     231  | RET ⇒ Some … [ RET ? ]
     232  | RETI ⇒ Some … [ RETI ? ]
     233  | NOP ⇒ Some … [ RealInstruction (NOP ?) ]
     234  ].
     235
     236definition expand_pseudo_instruction_unsafe:
     237 jump_length → pseudo_instruction → option (list instruction) ≝
     238  λjmp_len.
     239  λi.
     240  match i with
     241  [ Cost cost ⇒ Some ? [ ]
     242  | Comment comment ⇒ Some ? [ ]
     243  | Call call ⇒
     244    match jmp_len with
     245    [ short_jump ⇒ None ?
     246    | medium_jump ⇒ Some ? [ ACALL (ADDR11 (zero 11)) ]
     247    | long_jump ⇒ Some ? [ LCALL (ADDR16 (zero 16)) ]
     248    ]
     249  | Mov d trgt ⇒
     250      Some ? [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, DATA16 (zero 16)〉))))]
     251  | Instruction instr ⇒ expand_relative_jump_unsafe jmp_len instr
     252  | Jmp jmp ⇒
     253    match jmp_len with
     254    [ short_jump ⇒ Some ? [ SJMP (RELATIVE (zero 8)) ]
     255    | medium_jump ⇒ Some ? ([ AJMP (ADDR11 (zero 11)) ])
     256    | long_jump ⇒ Some ? [ LJMP (ADDR16 (zero 16)) ]
     257    ]
     258  ].
     259 @I
     260qed.
     261
     262definition instruction_size: (* ℕ → *) jump_length → pseudo_instruction → ℕ ≝
     263  λjmp_len.λinstr.
     264  let ilist ≝ expand_pseudo_instruction_unsafe jmp_len instr in
    180265  let bv: list (BitVector 8) ≝ match ilist with
    181266    [ None   ⇒ (* this shouldn't happen *) [ ]
    182267    | Some l ⇒ flatten … (map … assembly1 l)
    183268    ] in
    184   pc + (|bv|).
    185  @(λx.bv_pc)
    186 qed.
     269  |bv|.
     270 
     271definition policy_isize_sum ≝
     272  λprefix:list labelled_instruction.λpolicy:jump_expansion_policy.
     273  (\fst policy) = foldl_strong (option Identifier × pseudo_instruction)
     274  (λacc.ℕ)
     275  prefix
     276  (λhd.λx.λtl.λp.λacc.
     277    let 〈i1,i2,jl〉 ≝ bvt_lookup … (bitvector_of_nat ? (|hd|)) (\snd policy) 〈0,0,short_jump〉 in
     278    acc + (instruction_size jl (\snd x)))
     279  0.
    187280
    188281(* The function that creates the label-to-address map *)
     
    213306       | Some l ⇒ add … labels l 〈|prefix|, pc〉
    214307       ] in
    215      let 〈i1,i2,jmp_len〉 ≝ bvt_lookup ?? (bitvector_of_nat 16 (|prefix|)) policy 〈0, 0, long_jump〉 in
    216        〈add_instruction_size pc jmp_len instr, new_labels〉
     308     let 〈i1,i2,jmp_len〉 ≝
     309       bvt_lookup ?? (bitvector_of_nat 16 (|prefix|)) (\snd policy) 〈0,0,short_jump〉 in
     310       〈pc + (instruction_size jmp_len instr), new_labels〉
    217311    ) 〈0, empty_map …〉 in
    218312    final_labels.
    219 [ #i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
     313[#i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
    220314  [ #Hi #l normalize nodelta; cases label normalize nodelta
    221315    [ >occurs_exactly_once_None #Hocc >(nth_append_first ? ? prefix ? ? (le_S_S_to_le ? ? Hi)) #Hl
     
    226320      [ normalize in Hocc;
    227321        >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; #Hl 
    228         @⊥ @(absurd … Hocc) 
     322        @⊥ @(absurd … Hocc)
    229323      | normalize nodelta lapply (pi2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc ?)
    230324        [ #addr #Haddr % [ @addr | <Haddr @lookup_add_miss /2/ ]
     
    312406qed.
    313407
    314 (* these should be moved to BitVector at some point, and proven *) 
    315 lemma bitvector_of_nat_ok:
    316   ∀n,x,y:ℕ.x < 2^n → y < 2^n → eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y) → x = y.
    317  #n elim n -n
    318  [ #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
    319  | #n #Hind #x #y #Hx #Hy #Heq cases daemon (* XXX *)
    320  ]
    321 qed.
    322 
    323 lemma bitvector_of_nat_abs:
    324   ∀n,x,y:ℕ.x < 2^n → y < 2^n → x ≠ y → ¬eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y).
    325  #n #x #y #Hx #Hy #Heq @notb_elim
    326  lapply (refl ? (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)))
    327  cases (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)) in ⊢ (???% → %);
    328  [ #H @⊥ @(absurd ?? Heq) @(bitvector_of_nat_ok n x y Hx Hy) >H / by I/
    329  | #H / by I/
    330  ]
    331 qed.
    332 
    333408lemma jump_not_in_policy: ∀prefix:list labelled_instruction.
    334409 ∀policy:(Σp:jump_expansion_policy.
     
    336411  ∀i:ℕ.i < |prefix| →
    337412  iff (¬is_jump (nth i ? prefix 〈None ?, Comment []〉))
    338   (lookup_opt … (bitvector_of_nat 16 i) policy = None ?).
     413  (lookup_opt … (bitvector_of_nat 16 i) (\snd policy) = None ?).
    339414 #prefix #policy #i #Hi @conj
    340  [ #Hnotjmp lapply (refl ? (lookup_opt … (bitvector_of_nat 16 i) policy))
    341    cases (lookup_opt … (bitvector_of_nat 16 i) policy) in ⊢ (???% → ?);
    342    [ #H @H
    343    | #x cases x -x #x #z cases x -x #x #y #H @⊥ @(absurd ? ? Hnotjmp) @(proj2 ?? (proj2 ?? (pi2 ?? policy) i Hi))
    344      @(ex_intro ?? x (ex_intro ?? y (ex_intro ?? z H)))
    345    ]
    346  | #Hnone @nmk #Hj lapply (proj1 ?? (proj2 ?? (pi2 ?? policy) i Hi) Hj)
    347    #H elim H -H; #x #H elim H -H; #y #H elim H -H; #z #H >H in Hnone; #abs destruct (abs)
    348  
     415[ #Hnotjmp lapply (refl ? (lookup_opt … (bitvector_of_nat 16 i) (\snd policy)))
     416  cases (lookup_opt … (bitvector_of_nat 16 i) (\snd policy)) in ⊢ (???% → ?);
     417  [ #H @H
     418  | #x cases x -x #x cases x -x #x #y #z #H @⊥ @(absurd ? ? Hnotjmp) @(proj2 ?? (proj2 ?? (pi2 ?? policy) i Hi))
     419    @(ex_intro ?? x (ex_intro ?? y (ex_intro ?? z H)))
     420  ]
     421| #Hnone @nmk #Hj lapply (proj1 ?? (proj2 ?? (pi2 ?? policy) i Hi) Hj)
     422  #H elim H -H; #x #H elim H -H; #y #H elim H -H #z #H >H in Hnone; #abs destruct (abs)
     423
    349424qed.
    350425
     
    369444    jump_in_policy program policy ∧
    370445    ∀i.i < |program| → is_jump (nth i ? program 〈None ?, Comment []〉) →
    371      lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈0,0,short_jump〉 ≝
     446     lookup_opt … (bitvector_of_nat 16 i) (\snd policy) = Some ? 〈0,0,short_jump〉 ≝
    372447  λprogram.
    373448  foldl_strong (option Identifier × pseudo_instruction)
     
    376451    jump_in_policy prefix policy ∧
    377452    ∀i.i < |prefix| → is_jump (nth i ? prefix 〈None ?, Comment []〉) →
    378       lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈0,0,short_jump〉)
     453      lookup_opt … (bitvector_of_nat 16 i) (\snd policy) = Some ? 〈0,0,short_jump〉)
    379454  program
    380   (λprefix.λx.λtl.λprf.λpolicy.
     455  (λprefix.λx.λtl.λprf.λp.
     456   let 〈pc,policy〉 ≝ p in
    381457   let 〈label,instr〉 ≝ x in
    382    match instr with
     458   〈pc + instruction_size short_jump instr,match instr with
    383459   [ Instruction i ⇒ match i with
    384460     [ JC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
     
    391467     | CJNE _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
    392468     | DJNZ _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
    393      | _ ⇒ (pi1 … policy)
     469     | _ ⇒ policy
    394470     ]
    395    | Call c ⇒ bvt_insert (ℕ×ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
     471   | Call c ⇒ bvt_insert (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
    396472   | Jmp j  ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
    397    | _      ⇒ (pi1 ?? policy)
    398    ]
    399   ) (Stub ? ?).
    400 [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:
    401  @conj
    402  [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:
    403   @conj
    404   #i >append_length <commutative_plus #Hi normalize in Hi;
    405   [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:
    406    #Hi2 cases (le_to_or_lt_eq … Hi) -Hi; #Hi @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i)
    407    [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:
    408      @le_S_to_le @le_S_to_le @Hi
    409    |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:
    410      @Hi2
    411    |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:
    412      <Hi @le_n_Sn
    413    |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:
    414      @Hi2
    415    ]
    416   ]
    417   cases (le_to_or_lt_eq … Hi) -Hi; #Hi
    418   [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:
    419     >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi))
    420     @(proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
    421   ]
    422   @conj >(injective_S … Hi)
    423    [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:
    424     >(nth_append_second ? ? prefix ? ? (le_n (|prefix|))) <minus_n_n #H @⊥ @H
    425    ]
    426    #H elim H; -H; #t1 #H elim H; -H #t2 #H elim H; -H; #t3 #H
    427    >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?) in H;
    428    [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:
    429      #H destruct (H)
    430    ]
    431    @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm @le_S_S
    432    @le_plus_n_r
    433  ]
    434  #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
    435  -Hi; #Hi
    436  [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:
    437   #Hj @(proj2 ?? (pi2 ?? policy) i (le_S_S_to_le … Hi))
    438   >(nth_append_first ?? prefix ?? (le_S_S_to_le ?? Hi)) in Hj; / by /
    439  ]
    440  >(injective_S … Hi) >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n
    441  #H @⊥ @H
    442 |2,3,26,27,28,29,30,31,32,33,34: @conj
    443  [1,3,5,7,9,11,13,15,17,19,21: @conj
    444   [1,3,5,7,9,11,13,15,17,19,21:
    445     #i >append_length <commutative_plus #Hi #Hi2 normalize in Hi; >lookup_opt_insert_miss
    446    [1,3,5,7,9,11,13,15,17,19,21:
    447      @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2)
    448    ]
    449    >eq_bv_sym @bitvector_of_nat_abs
    450    [1,4,7,10,13,16,19,22,25,28,31:
    451      @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm @le_S_S
    452      @le_plus_n_r
    453    |2,5,8,11,14,17,20,23,26,29,32: @Hi2
    454    |3,6,9,12,15,18,21,24,27,30,33: @lt_to_not_eq @Hi
    455    ]
    456   ]
    457   #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
    458   -Hi #Hi
    459   [1,3,5,7,9,11,13,15,17,19,21:
    460    >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) >lookup_opt_insert_miss
    461    [1,3,5,7,9,11,13,15,17,19,21:
    462     @(proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
    463    ]
    464    @bitvector_of_nat_abs
    465    [3,6,9,12,15,18,21,24,27,30,33: @(lt_to_not_eq … (le_S_S_to_le … Hi))
    466    |1,4,7,10,13,16,19,22,25,28,31: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
    467    ]
    468    @(transitive_lt … (pi2 ?? program))
    469    >prf >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r
    470   ]
    471   @conj >(injective_S … Hi) #H
    472   [2,4,6,8,10,12,14,16,18,20,22:
    473    >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n / by I/
    474   ]
    475   @(ex_intro ?? 0 (ex_intro ?? 0 (ex_intro ?? short_jump (lookup_opt_insert_hit ?? 16 ? policy))))
    476  ]
    477  #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
    478   -Hi #Hi
    479  [1,3,5,7,9,11,13,15,17,19,21:
    480   >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) #Hj >lookup_opt_insert_miss
    481   [1,3,5,7,9,11,13,15,17,19,21:
    482    @(proj2 ?? (pi2 ?? policy) i (le_S_S_to_le … Hi) Hj)
    483   ]
    484   @bitvector_of_nat_abs
    485   [3,6,9,12,15,18,21,24,27,30,33: @(lt_to_not_eq … (le_S_S_to_le … Hi))
    486   |1,4,7,10,13,16,19,22,25,28,31: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
    487   ]
    488   @(transitive_lt … (pi2 ?? program))
    489   >prf >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r
    490  ]
    491  #_ >(injective_S … Hi) @lookup_opt_insert_hit
    492 |@conj
    493  [@conj
    494   [ #i #Hi / by refl/
    495   | whd #i #Hi @⊥ @(absurd (i < 0) Hi (not_le_Sn_O ?))
    496   ]
    497  | #i #Hi >nth_nil #Hj @⊥ @Hj
     473   | _      ⇒ policy
     474   ]〉
     475  ) 〈0, Stub ? ?〉.
     476[ @conj
     477  [ @conj
     478    #i >append_length <commutative_plus #Hi normalize in Hi;
     479    [ #Hi2 cases (le_to_or_lt_eq … Hi) -Hi #Hi
     480      cases p -p #p cases p -p #pc #p #Hp cases x -x #l #pi cases pi
     481      [1,7: #id cases id normalize nodelta
     482        [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
     483          [1,2,3,6,7,24,25: #x #y
     484          |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
     485          @(proj1 ?? (proj1 ?? Hp) i ? Hi2) @le_S_to_le @le_S_to_le @Hi
     486        |38,39,40,41,42,43,44,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74:
     487          [1,2,3,6,7,24,25: #x #y
     488          |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
     489          <Hi @(proj1 ?? (proj1 ?? Hp) (S (|prefix|)) (le_S ?? (le_n (|prefix|))) ?)
     490          >Hi @Hi2
     491        |9,10,11,12,13,14,15,16,17:
     492          [1,2,6,7: #x |3,4,5,8,9: #x #id] >lookup_opt_insert_miss
     493          [2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
     494            [1,4,7,10,13,16,19,22,25: @Hi2
     495            |2,5,8,11,14,17,20,23,26: @(transitive_lt … Hi2) @le_S_to_le @Hi
     496            |3,6,9,12,15,18,21,24,27: @sym_neq @lt_to_not_eq @le_S_to_le @Hi
     497            ]
     498          |1,3,5,7,9,11,13,15,17:
     499            @(proj1 ?? (proj1 ?? Hp) i ? Hi2) @le_S_to_le @le_S_to_le @Hi
     500          ]
     501        |46,47,48,49,50,51,52,53,54:
     502          [1,2,6,7: #x |3,4,5,8,9: #x #id] >lookup_opt_insert_miss
     503          [2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
     504            [1,4,7,10,13,16,19,22,25: @Hi2
     505            |2,5,8,11,14,17,20,23,26: @(transitive_lt … Hi2) <Hi @le_n
     506            |3,6,9,12,15,18,21,24,27: @sym_neq @lt_to_not_eq <Hi @le_n
     507            ]
     508          |1,3,5,7,9,11,13,15,17:
     509            @(proj1 ?? (proj1 ?? Hp) i ? Hi2) <Hi @le_S @le_n
     510          ]
     511        ]
     512      |2,3,6,8,9,12: [3,6: #w] #z normalize nodelta
     513        [1,3,4: @(proj1 ?? (proj1 ?? Hp) i ? Hi2) @le_S_to_le @le_S_to_le @Hi
     514        |2,5,6:
     515          <Hi @(proj1 ?? (proj1 ?? Hp) (S (|prefix|)) (le_S ?? (le_n (|prefix|))) ?)
     516          >Hi @Hi2
     517        ]
     518      |4,5,10,11: #dst normalize nodelta >lookup_opt_insert_miss
     519        [2,4,6,8: @bitvector_of_nat_abs
     520          [1,4,7,10: @Hi2
     521          |2,5: @(transitive_lt … Hi2) @le_S_to_le @Hi
     522          |8,11: @(transitive_lt … Hi2) <Hi @le_n
     523          |3,6: @sym_neq @lt_to_not_eq @le_S_to_le @Hi
     524          |9,12: @sym_neq @lt_to_not_eq <Hi @le_n
     525          ]         
     526        |1,3: @(proj1 ?? (proj1 ?? Hp) i ? Hi2) @le_S_to_le @le_S_to_le @Hi
     527        |5,7: @(proj1 ?? (proj1 ?? Hp) i ? Hi2) <Hi @le_S @le_n
     528        ]
     529      ]
     530    | cases (le_to_or_lt_eq … Hi) -Hi #Hi
     531      [ >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) @conj
     532        [ #Hj @(ex_intro ?? 0 (ex_intro ?? 0 (ex_intro ?? short_jump ?)))
     533          cases p -p #p cases p #pc #pol #Hp cases x #l #ins cases ins normalize nodelta
     534          [1: #pi cases pi normalize nodelta
     535            [1,2,3,6,7,33,34: #x #y
     536            |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x
     537            |9,10,11,12,13,14,15,16,17:
     538              [1,2,6,7: #x | 3,4,5,8,9: #x #id] >lookup_opt_insert_miss
     539              [2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
     540               [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf
     541                 >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)
     542                 @le_S_S_to_le @le_plus_n_r
     543               |2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf
     544                 >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r
     545               |3,6,9,12,15,18,21,24,27: @lt_to_not_eq @(le_S_S_to_le … Hi)
     546               ]
     547              ]
     548            ]
     549          |2,3: #x
     550          |4,5: #id >lookup_opt_insert_miss
     551            [2,4: @bitvector_of_nat_abs
     552              [1,4: @(transitive_lt … (pi2 ?? program)) >prf
     553                 >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)
     554                 @le_S_S_to_le @le_plus_n_r
     555              |2,5: @(transitive_lt … (pi2 ?? program)) >prf
     556                 >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r
     557              |3,6: @lt_to_not_eq @(le_S_S_to_le … Hi)
     558              ]
     559            ]
     560          |6: #x #id
     561          ]
     562          @((proj2 ?? Hp) i (le_S_S_to_le … Hi) Hj)
     563        | #H @(proj2 ?? (proj2 ?? (proj1 ?? (pi2 ?? p)) i ?))
     564          [ @(le_S_S_to_le … Hi)
     565          | cases p in H; -p #p cases p #pc #pol #Hp cases x #l #ins cases ins normalize nodelta
     566            [1: #id cases id
     567              [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
     568                [1,2,3,6,7,24,25: #x #y
     569                |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
     570                normalize nodelta / by /
     571              |9,10,11,12,13,14,15,16,17: [1,2,6,7: #x |3,4,5,8,9: #x #id]
     572                normalize nodelta >lookup_opt_insert_miss
     573                [1,3,5,7,9,11,13,15,17: / by /
     574                |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
     575                  [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf
     576                    >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)
     577                    @le_S_S_to_le @le_plus_n_r
     578                  |2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf
     579                    >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r 
     580                  |3,6,9,12,15,18,21,24,27: @lt_to_not_eq @(le_S_S_to_le … Hi)
     581                  ]
     582                ]
     583              ]
     584            |2,3: #x / by /
     585            |4,5: #id >lookup_opt_insert_miss
     586              [2,4: @bitvector_of_nat_abs
     587                [1,4: @(transitive_lt … (pi2 ?? program)) >prf
     588                   >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)
     589                   @le_S_S_to_le @le_plus_n_r
     590                |2,5: @(transitive_lt … (pi2 ?? program)) >prf
     591                   >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r
     592                |3,6: @lt_to_not_eq @(le_S_S_to_le … Hi)
     593                ]
     594              |1,3: / by /
     595              ]
     596            |6: #x #id / by /
     597            ]
     598          ]
     599        ]
     600      | >(injective_S … Hi) >(nth_append_second ?? prefix ?? (le_n (|prefix|)))
     601        <minus_n_n whd in match (nth ????);
     602        cases x #l #ins cases ins
     603        [1: #pi cases pi
     604          [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
     605            [1,2,3,6,7,24,25: #x #y
     606            |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
     607            @conj
     608            [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:
     609              #H @⊥ @H
     610            |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
     611              cases p -p #p cases p -p #pc #pol #Hp #H elim H -H #p #H elim H -H #a #H elim H -H #j
     612              normalize nodelta >(proj1 ?? (proj1 ?? Hp) (|prefix|) (le_n (|prefix|)) ?)
     613              [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:
     614                #H destruct (H)
     615              |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
     616                @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm
     617                @le_S_S_to_le @le_plus_n_r
     618              ]
     619            ]
     620          |9,10,11,12,13,14,15,16,17: [1,2,6,7: #x | 3,4,5,8,9: #x #id]
     621            @conj
     622            [1,3,5,7,9,11,13,15,17:
     623              #_ @(ex_intro ?? 0 (ex_intro ?? 0 (ex_intro ?? short_jump ?)))
     624              cases p -p #p cases p -p #pc #pol #Hp @lookup_opt_insert_hit
     625            |2,4,6,8,10,12,14,16,18:
     626              #_ / by I/
     627            ]
     628          ]
     629        |2,3,6: #x [3: #id] @conj
     630          [1,3,5: #H @⊥ @H
     631          |2,4,6:
     632            cases p -p #p cases p -p #pc #pol #Hp #H elim H -H #p #H elim H -H #a #H elim H -H #j
     633            normalize nodelta >(proj1 ?? (proj1 ?? Hp) (|prefix|) (le_n (|prefix|)) ?)
     634            [1,3,5: #H destruct (H)
     635            |2,4,6: @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm
     636              @le_S_S_to_le @le_plus_n_r
     637            ]
     638          ]
     639        |4,5: #x @conj
     640          [1,3: #_ @(ex_intro ?? 0 (ex_intro ?? 0 (ex_intro ?? short_jump ?)))
     641            cases p -p #p cases p -p #pc #pol #Hp @lookup_opt_insert_hit
     642          |2,4: #_ / by I/
     643        ]
     644      ]
     645    ]
     646  ]
     647| #i >append_length <commutative_plus #Hi normalize in Hi;
     648  elim (le_to_or_lt_eq … Hi) -Hi #Hi
     649  [ >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) #H
     650    cases p -p #p cases p #pc #pol #Hp cases x #l #ins cases ins normalize nodelta
     651    [1: #pi cases pi
     652      [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
     653        [1,2,3,6,7,24,25: #x #y
     654        |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
     655        normalize nodelta
     656        @((proj2 ?? Hp) i (le_S_S_to_le … Hi) H)
     657      |9,10,11,12,13,14,15,16,17: [1,2,6,7: #x | 3,4,5,8,9: #x #id]
     658        normalize nodelta >lookup_opt_insert_miss
     659        [1,3,5,7,9,11,13,15,17: @((proj2 ?? Hp) i (le_S_S_to_le … Hi) H)
     660        |2,4,6,8,10,12,14,16,18,20: @bitvector_of_nat_abs
     661          [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf
     662            >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)
     663            @le_S_S_to_le @le_plus_n_r
     664          |2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf
     665            >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r
     666          |3,6,9,12,15,18,21,24,27: @lt_to_not_eq @(le_S_S_to_le … Hi)
     667          ]
     668        ]
     669      ]
     670    |2,3,6: #x [3: #id]
     671      normalize nodelta @((proj2 ?? Hp) i (le_S_S_to_le … Hi) H)
     672    |4,5: #x >lookup_opt_insert_miss
     673      [1,3: @((proj2 ?? Hp) i (le_S_S_to_le … Hi) H)
     674      |2,4: @bitvector_of_nat_abs
     675        [1,4: @(transitive_lt … (pi2 ?? program)) >prf
     676          >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)
     677          @le_S_S_to_le @le_plus_n_r
     678        |2,5: @(transitive_lt … (pi2 ?? program)) >prf
     679          >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r
     680        |3,6: @lt_to_not_eq @(le_S_S_to_le … Hi)
     681        ]
     682      ]
     683    ]
     684  | >(injective_S … Hi) >(nth_append_second ?? prefix ?? (le_n (|prefix|)))
     685    <minus_n_n whd in match (nth ????); cases x #l #ins cases ins
     686    [1: #pi cases pi
     687      [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
     688        [1,2,3,6,7,24,25: #x #y
     689        |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
     690        #H @⊥ @H
     691      |9,10,11,12,13,14,15,16,17: [1,2,6,7: #x | 3,4,5,8,9: #x #id]
     692        #_ cases p -p #p cases p -p #pc #pol #Hp >lookup_opt_insert_hit / by /
     693      ]
     694    |2,3,6: #x [3: #id] #H @⊥ @H
     695    |4,5: #id #_ cases p -p #p cases p -p #pc #pol #Hp >lookup_opt_insert_hit / by /
     696    ]
     697  ]
     698]
     699| @conj
     700  [ @conj
     701    [ #i #_ #Hi2 / by refl/
     702    | #i #_ @conj
     703      [ >nth_nil #H @⊥ @H
     704      | #H elim H -H #p #H elim H -H #a #H elim H -H #j #H normalize in H; destruct (H)
     705      ]
     706    ]
     707  | #i #Hi >nth_nil #H @⊥ @H
     708  ]
    498709]
    499710qed.
     
    502713  λprogram:list labelled_instruction.λp1,p2:jump_expansion_policy.
    503714  ∀n:ℕ.n < |program| →
    504     let 〈i1,i2,j1〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) p1 〈0,0,short_jump〉 in
    505     let 〈i3,i4,j2〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) p2 〈0,0,short_jump〉 in
     715    let 〈pc1,i1,j1〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,0,short_jump〉 in
     716    let 〈pc2,i2,j2〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,0,short_jump〉 in
    506717    j1 = j2.
    507718   
    508719definition nec_plus_ultra ≝
    509720  λprogram:list labelled_instruction.λp:jump_expansion_policy.
    510   ¬(∀i.i < |program| → \snd (bvt_lookup … (bitvector_of_nat 16 i) p 〈0,0,short_jump〉) = long_jump).
     721  ¬(∀i.i < |program| → \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,0,short_jump〉) = long_jump).
    511722 
     723lemma geb_to_leb: ∀a,b:ℕ.geb a b = leb b a.
     724  #a #b / by refl/
     725qed.
     726
    512727(* One step in the search for a jump expansion fixpoint. *)
    513728definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
     
    516731    is_label (nth i ? program 〈None ?, Comment [ ]〉) l →
    517732    ∃a.lookup … lm l = Some ? 〈i,a〉).
    518   ∀old_policy:(Σpolicy.
    519     out_of_program_none program policy ∧ jump_in_policy program policy).
    520   (Σx:bool × ℕ × (option jump_expansion_policy).
    521     let 〈changed,pc,y〉 ≝ x in
     733  ∀old_policy:(Σpolicy:jump_expansion_policy.
     734    out_of_program_none program policy ∧ jump_in_policy program policy ∧ (\fst policy < 2^16) ∧
     735    policy_isize_sum program policy).
     736  (Σx:bool × (option jump_expansion_policy).
     737    let 〈ch,y〉 ≝ x in
    522738    match y with
    523     [ None ⇒ pc > 2^16 ∧ nec_plus_ultra program old_policy
     739    [ None ⇒ nec_plus_ultra program old_policy
    524740    | Some p ⇒ out_of_program_none program p ∧ labels_okay labels p ∧
    525741        jump_in_policy program p ∧
    526         policy_increase program old_policy p ∧
    527         policy_safe p
    528         (changed = false → policy_equal_int program old_policy p)
     742        policy_increase program old_policy p ∧ policy_safe p ∧
     743        (ch = false → policy_equal_int program old_policy p (*sic!*))
     744        policy_isize_sum program p ∧ \fst p < 2^16
    529745    ])
    530746    ≝
    531747  λprogram.λlabels.λold_policy.
    532   let 〈final_changed, final_pc, final_policy〉 ≝
     748  let 〈final_changed, final_policy〉 ≝
    533749    foldl_strong (option Identifier × pseudo_instruction)
    534     (λprefix.Σx:bool × ℕ × jump_expansion_policy.
    535         let 〈changed,pc,policy〉 ≝ x in
     750    (λprefix.Σx:bool × jump_expansion_policy.
     751        let 〈changed,policy〉 ≝ x in
    536752        out_of_program_none prefix policy ∧ labels_okay labels policy ∧
    537753        jump_in_policy prefix policy ∧
    538754        policy_increase prefix old_policy policy ∧
    539755        policy_safe policy ∧
    540         (changed = false → policy_equal_int prefix old_policy policy))
     756        (changed = false → policy_equal_int prefix old_policy policy) ∧
     757        policy_isize_sum prefix policy)
    541758    program
    542759    (λprefix.λx.λtl.λprf.λacc.
    543       let 〈changed, pc, policy〉 ≝ acc in
     760      let 〈changed, pol〉 ≝ acc in
     761      (* let 〈pc,pol〉 ≝ p in *)
    544762      let 〈label,instr〉 ≝ x in
    545 (*      let old_jump_length ≝ lookup_opt ? ? (bitvector_of_nat 16 (|prefix|)) old_policy in *)
    546763      let add_instr ≝
    547764        match instr with
    548         [ Instruction i ⇒ jump_expansion_step_instruction labels pc i
    549         | Call c        ⇒ Some ? (select_call_length labels pc c)
    550         | Jmp j         ⇒ Some ? (select_jump_length labels pc j)
     765        [ Instruction i ⇒ jump_expansion_step_instruction labels (\fst pol) i
     766        | Call c        ⇒ Some ? (select_call_length labels (\fst pol) c)
     767        | Jmp j         ⇒ Some ? (select_jump_length labels (\fst pol) j)
    551768        | _             ⇒ None ?
    552769        ] in
    553         let 〈ignore,old_length〉 ≝ bvt_lookup … (bitvector_of_nat 16 (|prefix|)) old_policy 〈0, 0, short_jump〉 in
    554         match add_instr with
    555         [ None    ⇒ (* i.e. it's not a jump *)
    556           〈changed, add_instruction_size pc long_jump instr, policy〉
    557         | Some z ⇒ let 〈addr,ai〉 ≝ z in
    558           let new_length ≝ max_length old_length ai in
    559           〈match dec_eq_jump_length new_length old_length with
    560            [ inl _ ⇒ changed
    561            | inr _ ⇒ true], add_instruction_size pc new_length instr, insert … (bitvector_of_nat 16 (|prefix|)) 〈pc, addr, new_length〉 policy〉
    562         ]
    563     ) 〈false, 0, Stub ? ?〉 in
    564     if geb final_pc 2^16 then
    565       〈final_changed,final_pc,None ?〉
     770      let old_length ≝ \snd (bvt_lookup … (bitvector_of_nat 16 (|prefix|)) (\snd old_policy) 〈0,0,short_jump〉) in
     771      match add_instr with
     772      [ None    ⇒ (* i.e. it's not a jump *)
     773        let isize ≝ instruction_size short_jump instr in
     774        〈changed, 〈(\fst pol) + isize, (\snd pol)〉〉
     775      | Some z ⇒ let 〈addr,ai〉 ≝ z in
     776        let new_length ≝ max_length old_length ai in
     777        let isize ≝ instruction_size new_length instr in
     778        〈match dec_eq_jump_length new_length old_length with
     779         [ inl _ ⇒ changed
     780         | inr _ ⇒ true], 〈(\fst pol) + isize,
     781         insert … (bitvector_of_nat 16 (|prefix|)) 〈(\fst pol), addr, new_length〉 (\snd pol)〉〉
     782      ]
     783    ) 〈false, 〈0, Stub ? ?〉〉 in
     784    if geb (\fst final_policy) 2^16 then
     785      〈final_changed,None ?〉
    566786    else
    567       〈final_changed,final_pc,Some jump_expansion_policy final_policy〉.
    568 [ normalize nodelta @conj
    569   [ @leb_true_to_le @p2
    570   | @nmk #Hfull (* XXX *) cases daemon
     787      〈final_changed,Some ? final_policy〉.
     788[ @pair_elim #fch #x #Heq <(pair_eq2 ?????? Heq) normalize nodelta
     789  @nmk #Hfull lapply p generalize in match (foldl_strong ?????); * #x #H #H2
     790  >H2 in H; normalize nodelta -H2 -x #H
     791  @(absurd ((\fst final_policy) ≥ 2^16))
     792  [ @leb_true_to_le <geb_to_leb @p1
     793  | @lt_to_not_le @(le_to_lt_to_lt … (proj2 ?? (proj1 ?? (pi2 ?? old_policy))))
     794    >(proj2 ?? H) >(proj2 ?? (pi2 ?? old_policy))
     795    cases daemon (* XXX *)
    571796  ]
    572797| normalize nodelta lapply p generalize in match (foldl_strong ?????); * #x #H #H2
    573   >H2 in H; >p1 normalize nodelta //
    574 | lapply (pi2 ?? acc) >p >p1 normalize nodelta #Hpolicy
    575  @conj [ @conj [ @conj [ @conj [ @conj
    576 [ (* out_of_policy_none *)
     798  >H2 in H; normalize nodelta #H @conj
     799  [ @H
     800  | @not_le_to_lt @leb_false_to_not_le <geb_to_leb @p1
     801  ]
     802| lapply (pi2 ?? acc) >p #Hpolicy normalize nodelta in Hpolicy;
     803  cases (dec_eq_jump_length new_length old_length) #Hlength normalize nodelta
     804  @conj [1,3: @conj [1,3: @conj [1,3: @conj [1,3: @conj [1,3: @conj
     805[1,3: (* out_of_policy_none *)
    577806  #i >append_length <commutative_plus #Hi normalize in Hi;
    578807  #Hi2 >lookup_opt_insert_miss
    579   [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_to_le … Hi)) @Hi2
    580   | >eq_bv_sym @bitvector_of_nat_abs
    581     [ @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
     808  [1,3: @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i (le_S_to_le … Hi)) @Hi2
     809  |2,4: >eq_bv_sym @bitvector_of_nat_abs
     810    [1,4: @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    582811      @le_S_S @le_plus_n_r
    583     | @Hi2
    584     | @lt_to_not_eq @Hi
    585     ]
    586   ]
    587 | (* labels_okay *)
    588   @lookup_forall #i cases i -i #i cases i -i #p #a #j #n (*lapply (refl ? add_instr)
    589   cases (lookup ??? old_policy ?); #x cases x -x #p1 #p2 #p3
    590   cases add_instr in ⊢ (???% → %);
    591   [ #Hai normalize nodelta #Hl
    592     elim (forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) ? n Hl)
     812    |2,5: @Hi2
     813    |3,6: @lt_to_not_eq @Hi
     814    ]
     815  ]
     816|2,4: (* labels_okay *)
     817  @lookup_forall #i cases i -i #i cases i -i #p #a #j #n #Hl
     818  elim (insert_lookup_opt ?? 〈p,a,j〉 ???? Hl) -Hl #Hl
     819  [1,3: elim (forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) ? n Hl)
    593820    #i #Hi @(ex_intro ?? i Hi)
    594   | #x cases x -x #np #nl #Hai normalize nodelta *) #Hl
    595     elim (insert_lookup_opt ?? 〈p,a,j〉 ???? Hl) -Hl #Hl
    596     [ elim (forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) ? n Hl)
    597       #i #Hi @(ex_intro ?? i Hi)
    598     | (*whd in match add_instr in Hai; cases instr in Hai;*) normalize nodelta
    599       normalize nodelta in p4; cases instr in p4;
    600       [2,3: #x #abs normalize nodelta in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
    601       |6: #x #y #abs normalize nodelta in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
    602       |1: #pi cases pi
    603         [35,36,37: #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
    604         |1,2,3,6,7,33,34: #x #y #abs normalize in abs; lapply (jmeq_to_eq ??? abs)
    605           #H destruct (H)
    606         |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #abs normalize in abs;
    607           lapply (jmeq_to_eq ??? abs) #H destruct (H)
    608         |9,10,14,15: #id normalize nodelta whd in match (jump_expansion_step_instruction ???);
    609           whd in match (select_reljump_length ???); >p5
    610           lapply (refl ? (lookup_def ?? labels id 〈0,pc〉))
    611           cases (lookup_def ?? labels id 〈0,pc〉) in ⊢ (???% → %); #q1 #q2
    612           normalize nodelta #H
    613           >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
    614           >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb pc q2))
    615           cases (leb pc q2) in ⊢ (???% → %); #Hle1
    616           [1,3,5,7: lapply (refl ? (leb (q2-pc) 126)) cases (leb (q2-pc) 126) in ⊢ (???% → %);
    617           |2,4,6,8: lapply (refl ? (leb (pc-q2) 129)) cases (leb (pc-q2) 129) in ⊢ (???% → %);
    618           ]
    619           #Hle2 normalize nodelta #Hli @(ex_intro ?? id) >H
    620           <(pair_eq1 ?????? (Some_eq ??? Hli)) @refl
    621         |11,12,13,16,17: #x #id normalize nodelta whd in match (jump_expansion_step_instruction ???);
    622           whd in match (select_reljump_length ???); >p5
    623           lapply (refl ? (lookup_def ?? labels id 〈0,pc〉))
    624           cases (lookup_def ?? labels id 〈0,pc〉) in ⊢ (???% → %); #q1 #q2
    625           normalize nodelta #H
    626           >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
    627           >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb pc q2))
    628           cases (leb pc q2) in ⊢ (???% → %); #Hle1
    629           [1,3,5,7,9: lapply (refl ? (leb (q2-pc) 126)) cases (leb (q2-pc) 126) in ⊢ (???% → %);
    630           |2,4,6,8,10: lapply (refl ? (leb (pc-q2) 129)) cases (leb (pc-q2) 129) in ⊢ (???% → %);
    631           ]
    632           #Hle2 normalize nodelta #Hli @(ex_intro ?? id) >H
    633           <(pair_eq1 ?????? (Some_eq ??? Hli)) @refl
     821  |2,4: normalize nodelta normalize nodelta in p2; cases instr in p2;
     822    [2,3,8,9: #x #abs normalize nodelta in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
     823    |6,12: #x #y #abs normalize nodelta in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
     824    |1,7: #pi cases pi
     825      [35,36,37,72,73,74: #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
     826      |1,2,3,6,7,33,34,38,39,40,43,44,70,71:
     827        #x #y #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
     828      |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69:
     829        #x #abs normalize in abs;lapply (jmeq_to_eq ??? abs) #H destruct (H)
     830      |9,10,14,15,46,47,51,52:
     831        #id normalize nodelta whd in match (jump_expansion_step_instruction ???);
     832        whd in match (select_reljump_length ???); >p3
     833        lapply (refl ? (lookup_def ?? (pi1 ?? labels) id 〈0,\fst pol〉))
     834        cases (lookup_def ?? labels id 〈0,\fst pol〉) in ⊢ (???% → %); #q1 #q2
     835        normalize nodelta #H
     836        >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
     837        >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb (\fst pol) q2))
     838        cases (leb (\fst pol) q2) in ⊢ (???% → %); #Hle1
     839        [1,3,5,7,9,11,13,15: lapply (refl ? (leb (q2-\fst pol) 126)) cases (leb (q2-\fst pol) 126) in ⊢ (???% → %);
     840        |2,4,6,8,10,12,14,16: lapply (refl ? (leb (\fst pol-q2) 129)) cases (leb (\fst pol-q2) 129) in ⊢ (???% → %);
    634841        ]
    635       |4,5: #id normalize nodelta whd in match (select_jump_length ???);
    636           whd in match (select_call_length ???); >p5
    637           lapply (refl ? (lookup_def ?? labels id 〈0,pc〉))
    638           cases (lookup_def ?? labels id 〈0,pc〉) in ⊢ (???% → %); #q1 #q2
    639           normalize nodelta #H
    640           [1: cases (leb pc q2)
    641             [ cases (leb (q2-pc) 126) | cases (leb (pc-q2) 129) ]
    642             [1,3: normalize nodelta #H2 >(pair_eq1 ?????? (Some_eq ??? H2)) in H;
    643             #Hli @(ex_intro ?? id) lapply (proj2 ?? Hl)
    644             #H >(pair_eq1 ?????? (pair_eq1 ?????? H))
    645             >(pair_eq2 ?????? (pair_eq1 ?????? H)) >Hli @refl]
    646           ]
    647           cases (split ? 5 11 (bitvector_of_nat 16 q2)) #n1 #n2
    648           cases (split ? 5 11 (bitvector_of_nat 16 pc)) #m1 #m2
    649           normalize nodelta cases (eq_bv ? n1 m1)
    650           normalize nodelta #H2 >(pair_eq1 ?????? (Some_eq ??? H2)) in H; #H
    651           @(ex_intro ?? id) lapply (proj2 ?? Hl) #H2
    652           >(pair_eq1 ?????? (pair_eq1 ?????? H2)) >(pair_eq2 ?????? (pair_eq1 ?????? H2))
    653           >H @refl
    654       ]
    655     ]
    656   ]
    657 | (* jump_in_policy *)
     842        #Hle2 normalize nodelta #Hli @(ex_intro ?? id) >H
     843        <(pair_eq1 ?????? (Some_eq ??? Hli)) @refl
     844      |11,12,13,16,17,48,49,50,53,54:
     845        #x #id normalize nodelta whd in match (jump_expansion_step_instruction ???);
     846        whd in match (select_reljump_length ???); >p3
     847        lapply (refl ? (lookup_def ?? labels id 〈0,\fst pol〉))
     848        cases (lookup_def ?? labels id 〈0,\fst pol〉) in ⊢ (???% → %); #q1 #q2
     849        normalize nodelta #H
     850        >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
     851        >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb (\fst pol) q2))
     852        cases (leb (\fst pol) q2) in ⊢ (???% → %); #Hle1
     853        [1,3,5,7,9,11,13,15,17,19: lapply (refl ? (leb (q2-\fst pol) 126)) cases (leb (q2-\fst pol) 126) in ⊢ (???% → %);
     854        |2,4,6,8,10,12,14,16,18,20: lapply (refl ? (leb (\fst pol-q2) 129)) cases (leb (\fst pol-q2) 129) in ⊢ (???% → %);
     855        ]
     856        #Hle2 normalize nodelta #Hli @(ex_intro ?? id) >H
     857        <(pair_eq1 ?????? (Some_eq ??? Hli)) @refl
     858      ]
     859    |4,5,10,11: #id normalize nodelta whd in match (select_jump_length ???);
     860      whd in match (select_call_length ???); >p3
     861      lapply (refl ? (lookup_def ?? labels id 〈0,\fst pol〉))
     862      cases (lookup_def ?? labels id 〈0,\fst pol〉) in ⊢ (???% → %); #q1 #q2
     863      normalize nodelta #H
     864      [1,3: cases (leb (\fst pol) q2)
     865        [1,3: cases (leb (q2-\fst pol) 126) |2,4: cases (leb (\fst pol-q2) 129) ]
     866        [1,3,5,7: normalize nodelta #H2 >(pair_eq1 ?????? (Some_eq ??? H2)) in H;
     867        #Hli @(ex_intro ?? id) lapply (proj2 ?? Hl)
     868        #H >(pair_eq1 ?????? (pair_eq1 ?????? H))
     869        >(pair_eq2 ?????? (pair_eq1 ?????? H)) >Hli @refl]
     870      ]
     871      cases (split ? 5 11 (bitvector_of_nat 16 q2)) #n1 #n2
     872      cases (split ? 5 11 (bitvector_of_nat 16 (\fst pol))) #m1 #m2
     873      normalize nodelta cases (eq_bv ? n1 m1)
     874      normalize nodelta #H2 >(pair_eq1 ?????? (Some_eq ??? H2)) in H; #H
     875      @(ex_intro ?? id) lapply (proj2 ?? Hl) #H2
     876      >(pair_eq1 ?????? (pair_eq1 ?????? H2)) >(pair_eq2 ?????? (pair_eq1 ?????? H2))
     877      >H @refl
     878    ]
     879  ]
     880 ]
     881|2,4: (* jump_in_policy *)
    658882  #i #Hi cases (le_to_or_lt_eq … Hi) -Hi;
    659   [ >append_length <commutative_plus #Hi normalize in Hi;
     883  [1,3: >append_length <commutative_plus #Hi normalize in Hi;
    660884    >(nth_append_first ?? prefix ??(le_S_S_to_le ?? Hi)) @conj
    661     [ #Hj lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i (le_S_S_to_le … Hi))
     885    [1,3: #Hj lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_S_to_le … Hi))
    662886      #Hacc elim (proj1 ?? Hacc Hj) #h #n elim n -n #n #H elim H -H #j #Hj
    663887      @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?))) whd in match (snd ???);
    664       >lookup_opt_insert_miss [ @Hj |  @bitvector_of_nat_abs ]
    665       [3: @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
    666       |1: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
     888      >lookup_opt_insert_miss [1,3: @Hj |2,4:  @bitvector_of_nat_abs ]
     889      [3,6: @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
     890      |1,4: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
    667891      ]
    668892      @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    669893      @le_S_S @le_plus_n_r
    670     | lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i (le_S_S_to_le … Hi)) #Hacc
    671       #H elim H -H; #h #H elim H -H; #n #H elim H -H #j
    672       #Hl @(proj2 ?? Hacc) @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?)))
     894    |2,4: lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_S_to_le … Hi))
     895      #Hacc #H elim H -H; #h #H elim H -H; #n #H elim H -H #j #Hl
     896      @(proj2 ?? Hacc) @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?)))
    673897      <Hl @sym_eq @lookup_opt_insert_miss @bitvector_of_nat_abs
    674       [3: @lt_to_not_eq @(le_S_S_to_le … Hi)
    675       |1: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
     898      [3,6: @lt_to_not_eq @(le_S_S_to_le … Hi)
     899      |1,4: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
    676900      ]
    677901      @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    678902      @le_S_S @le_plus_n_r
    679903    ]
    680   | >append_length <commutative_plus #Hi normalize in Hi; >(injective_S … Hi)
     904  |2,4: >append_length <commutative_plus #Hi normalize in Hi; >(injective_S … Hi)
    681905    >(nth_append_second ?? prefix ?? (le_n (|prefix|)))
    682      <minus_n_n whd in match (nth ????); normalize nodelta in p4; cases instr in p4;
    683      [1: #pi | 2,3: #x | 4,5: #id | 6: #x #y] #Hinstr @conj normalize nodelta
    684      [3,5,11: #H @⊥ @H (* instr is not a jump *)
    685      |4,6,12: normalize nodelta in Hinstr; lapply (jmeq_to_eq ??? Hinstr)
     906     <minus_n_n whd in match (nth ????); normalize nodelta in p2; cases instr in p2;
     907     [1,7: #pi | 2,3,8,9: #x | 4,5,10,11: #id | 6,12: #x #y] #Hinstr @conj normalize nodelta
     908     [5,7,9,11,21,23: #H @⊥ @H (* instr is not a jump *)
     909     |6,8,10,12,22,24: normalize nodelta in Hinstr; lapply (jmeq_to_eq ??? Hinstr)
    686910      #H destruct (H)
    687      |7,9: (* instr is a jump *) #_ @(ex_intro ?? pc)
     911     |13,15,17,19: (* instr is a jump *) #_ @(ex_intro ?? (\fst pol))
    688912       @(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai))
    689913       @lookup_opt_insert_hit
    690      |8,10: #_ / by I/
    691      |1,2: cases pi in Hinstr;
    692        [35,36,37: #Hinstr #H @⊥ @H
    693        |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #Hinstr #H @⊥ @H
    694        |1,2,3,6,7,33,34: #x #y #Hinstr #H @⊥ @H
    695        |9,10,14,15: #id #Hinstr #_
    696          @(ex_intro ?? pc) @(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai))
     914     |14,16,18,20: #_ / by I/
     915     |1,2,3,4: cases pi in Hinstr;
     916       [35,36,37,109,110,111: #Hinstr #H @⊥ @H
     917       |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,78,79,82,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106:
     918         #x #Hinstr #H @⊥ @H
     919       |1,2,3,6,7,33,34,75,76,77,80,81,107,108: #x #y #Hinstr #H @⊥ @H
     920       |9,10,14,15,83,84,88,89: #id #Hinstr #_
     921         @(ex_intro ?? (\fst pol)) @(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai))
    697922         @lookup_opt_insert_hit
    698        |11,12,13,16,17: #x #id #Hinstr #_
    699          @(ex_intro ?? pc) @(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai))
     923       |11,12,13,16,17,85,86,87,90,91: #x #id #Hinstr #_
     924         @(ex_intro ?? (\fst pol)) @(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai))
    700925         @lookup_opt_insert_hit
    701        |72,73,74: #Hinstr lapply (jmeq_to_eq ??? Hinstr) #H normalize in H; destruct (H)
    702        |41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69: #x #Hinstr
    703         lapply (jmeq_to_eq ??? Hinstr) #H normalize in H; destruct (H)
    704        |38,39,40,43,44,70,71: #x #y #Hinstr lapply (jmeq_to_eq ??? Hinstr) #H
     926       |72,73,74,146,147,148: #Hinstr lapply (jmeq_to_eq ??? Hinstr) #H normalize in H; destruct (H)
     927       |41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,115,116,119,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143:
     928        #x #Hinstr lapply (jmeq_to_eq ??? Hinstr) #H normalize in H; destruct (H)
     929       |38,39,40,43,44,70,71,112,113,114,117,118,144,145: #x #y #Hinstr lapply (jmeq_to_eq ??? Hinstr) #H
    705930         normalize in H; destruct (H)
    706        |46,47,51,52: #id #Hinstr #_ / by I/
    707        |48,49,50,53,54: #x #id #Hinstr #_ / by I/
     931       |46,47,51,52,120,121,125,126: #id #Hinstr #_ / by I/
     932       |48,49,50,53,54,122,123,124,127,128: #x #id #Hinstr #_ / by I/
    708933       ]
    709934     ]
    710935   ]
    711936 ]
    712 | (* policy increase *)
     937|2,4: (* policy increase *)
    713938  #i >append_length >commutative_plus #Hi normalize in Hi;
    714939  cases (le_to_or_lt_eq … Hi) -Hi; #Hi
    715   [ >lookup_insert_miss
    716     [ @(proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)) i (le_S_S_to_le … Hi))
    717     | @bitvector_of_nat_abs
    718       [3: @lt_to_not_eq @(le_S_S_to_le … Hi)
    719       |1: @(transitive_lt ??? (le_S_S_to_le … Hi))
     940  [1,3: >lookup_insert_miss
     941    [1,3: @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i (le_S_S_to_le … Hi))
     942    |2,4: @bitvector_of_nat_abs
     943      [3,6: @lt_to_not_eq @(le_S_S_to_le … Hi)
     944      |1,4: @(transitive_lt ??? (le_S_S_to_le … Hi))
    720945      ]
    721946      @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    722947      @le_S_S @le_plus_n_r
    723948    ]
    724   | >(injective_S … Hi) >p3 >lookup_insert_hit normalize nodelta
    725     @pair_elim #x #y #_ @jmpleq_max_length
     949  |2: >(injective_S … Hi) normalize nodelta in Hlength; >lookup_insert_hit normalize nodelta
     950    >Hlength @pair_elim #l1 #l2 #Hl @pair_elim #y1 #y2 #Hy
     951    >Hl %2 @refl
     952  |4: cases daemon (* XXX get rest of proof done first *)
    726953  ]
    727954 ]
    728 | (* policy_safe *)
     955|2,4: (* policy_safe *)
    729956  @lookup_forall #x cases x -x #x cases x -x #p #a #j #n normalize nodelta #Hl
    730957  elim (insert_lookup_opt ?? 〈p,a,j〉 ???? Hl) -Hl #Hl
    731   [ @(forall_lookup … (proj2 ?? (proj1 ?? Hpolicy)) ? n Hl)
    732   | normalize nodelta in p4; cases instr in p4;
    733     [2,3: #x #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
    734     |6: #x #y #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
    735     |1: #pi cases pi normalize nodelta
    736      [35,36,37: #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
    737      |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32:
    738        #x #abs @⊥ normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
    739      |1,2,3,6,7,33,34: #x #y #abs @⊥ normalize in abs; lapply (jmeq_to_eq ??? abs) #H
    740        destruct (H)
    741      |9,10,14,15: #id >p5 whd in match (jump_expansion_step_instruction ???);
     958  [1,3: @(forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy))) ? n Hl)
     959  |2,4: normalize nodelta in p2; cases instr in p2;
     960    [2,3,8,9: #x #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
     961    |6,12: #x #y #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
     962    |1,7: #pi cases pi normalize nodelta
     963     [35,36,37,72,73,74: #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
     964     |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69:
     965       #x #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
     966     |1,2,3,6,7,33,34,38,39,40,43,44,70,71:
     967       #x #y #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
     968     |9,10,14,15,46,47,51,52: #id >p3 whd in match (jump_expansion_step_instruction ???);
    742969       whd in match (select_reljump_length ???);
    743        cases (lookup_def ?? labels id 〈0,pc〉) #q1 #q2 normalize nodelta
     970       cases (lookup_def ?? labels id 〈0,\fst pol〉) #q1 #q2 normalize nodelta
    744971       >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
    745        >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb pc q2))
    746        cases (leb pc q2) in ⊢ (???% → %); #Hle1
    747        [1,3,5,7: lapply (refl ? (leb (q2-pc) 126)) cases (leb (q2-pc) 126) in ⊢ (???% → %);
    748        |2,4,6,8: lapply (refl ? (leb (pc-q2) 129)) cases (leb (pc-q2) 129) in ⊢ (???% → %);
     972       >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb (\fst pol) q2))
     973       cases (leb (\fst pol) q2) in ⊢ (???% → %); #Hle1
     974       [1,3,5,7,9,11,13,15: lapply (refl ? (leb (q2-\fst pol) 126)) cases (leb (q2-\fst pol) 126) in ⊢ (???% → %);
     975       |2,4,6,8,10,12,14,16: lapply (refl ? (leb (\fst pol-q2) 129)) cases (leb (\fst pol-q2) 129) in ⊢ (???% → %);
    749976       ]
    750977       #Hle2 normalize nodelta #Hli
    751978       <(pair_eq1 ?????? (Some_eq ??? Hli)) >Hle1
    752979       >(pair_eq2 ?????? (proj2 ?? Hl)) <(pair_eq2 ?????? (Some_eq ??? Hli))
    753        cases old_length
    754        [1,7,13,19,25,31,37,43: @(leb_true_to_le … Hle2)
     980       cases (\snd (lookup ?? (bitvector_of_nat ? (|prefix|)) (\snd old_policy) ?))
     981       [1,7,13,19,25,31,37,43,49,55,61,67,73,79,85,91: @(leb_true_to_le … Hle2)
    755982       ] normalize @I (* much faster than / by I/, strangely enough *)
    756      |11,12,13,16,17: #x #id >p5 whd in match (jump_expansion_step_instruction ???);
     983     |11,12,13,16,17,48,49,50,53,54: #x #id >p3 whd in match (jump_expansion_step_instruction ???);
    757984       whd in match (select_reljump_length ???);
    758        cases (lookup_def ?? labels id 〈0,pc〉) #q1 #q2 normalize nodelta
     985       cases (lookup_def ?? labels id 〈0,\fst pol〉) #q1 #q2 normalize nodelta
    759986       >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
    760        >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb pc q2))
    761        cases (leb pc q2) in ⊢ (???% → %); #Hle1
    762        [1,3,5,7,9: lapply (refl ? (leb (q2-pc) 126)) cases (leb (q2-pc) 126) in ⊢ (???% → %);
    763        |2,4,6,8,10: lapply (refl ? (leb (pc-q2) 129)) cases (leb (pc-q2) 129) in ⊢ (???% → %);
     987       >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb (\fst pol) q2))
     988       cases (leb (\fst pol) q2) in ⊢ (???% → %); #Hle1
     989       [1,3,5,7,9,11,13,15,17,19: lapply (refl ? (leb (q2-\fst pol) 126)) cases (leb (q2-\fst pol) 126) in ⊢ (???% → %);
     990       |2,4,6,8,10,12,14,16,18,20: lapply (refl ? (leb (\fst pol-q2) 129)) cases (leb (\fst pol-q2) 129) in ⊢ (???% → %);
    764991       ]
    765992       #Hle2 normalize nodelta #Hli
    766993       <(pair_eq1 ?????? (Some_eq ??? Hli)) >Hle1 >(pair_eq2 ?????? (proj2 ?? Hl))
    767994       <(pair_eq2 ?????? (Some_eq ??? Hli))
    768        cases old_length
    769        [1,7,13,19,25,31,37,43,49,55: @(leb_true_to_le … Hle2)
     995       cases (\snd (lookup ?? (bitvector_of_nat ? (|prefix|)) (\snd old_policy) ?))
     996       [1,7,13,19,25,31,37,43,49,55,61,67,73,79,85,91,97,103,109,115: @(leb_true_to_le … Hle2)
    770997       ] normalize @I (* vide supra *)
    771998     ]
    772     |4,5: #id >p5 normalize nodelta whd in match (select_jump_length ???);
    773       whd in match (select_call_length ???); cases (lookup_def ?? labels id 〈0,pc〉)
     999    |4,5,10,11: #id >p3 normalize nodelta whd in match (select_jump_length ???);
     1000      whd in match (select_call_length ???); cases (lookup_def ?? labels id 〈0,\fst pol〉)
    7741001      #q1 #q2 normalize nodelta
    7751002      >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
    7761003      >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
    777       [1: lapply (refl ? (leb pc q2)) cases (leb pc q2) in ⊢ (???% → %); #Hle1
    778         [ lapply (refl ? (leb (q2-pc) 126)) cases (leb (q2-pc) 126) in ⊢ (???% → %);
    779         | lapply (refl ? (leb (pc-q2) 129)) cases (leb (pc-q2) 129) in ⊢ (???% → %);
     1004      [1,3: lapply (refl ? (leb (\fst pol) q2)) cases (leb (\fst pol) q2) in ⊢ (???% → %); #Hle1
     1005        [1,3: lapply (refl ? (leb (q2-\fst pol) 126)) cases (leb (q2-\fst pol) 126) in ⊢ (???% → %);
     1006        |2,4: lapply (refl ? (leb (\fst pol-q2) 129)) cases (leb (\fst pol-q2) 129) in ⊢ (???% → %);
    7801007        ]
    7811008       #Hle2 normalize nodelta
    7821009      ]
    783       [2,4,5: lapply (refl ? (split ? 5 11 (bitvector_of_nat ? q2)))
     1010      [2,4,6,8,9,10: lapply (refl ? (split ? 5 11 (bitvector_of_nat ? q2)))
    7841011        cases (split ??? (bitvector_of_nat ? q2)) in ⊢ (???% → %); #x1 #x2 #Hle3
    785         lapply (refl ? (split ? 5 11 (bitvector_of_nat ? pc)))
    786         cases (split ??? (bitvector_of_nat ? pc)) in ⊢ (???% → %); #y1 #y2 #Hle4
     1012        lapply (refl ? (split ? 5 11 (bitvector_of_nat ? (\fst pol))))
     1013        cases (split ??? (bitvector_of_nat ? (\fst pol))) in ⊢ (???% → %); #y1 #y2 #Hle4
    7871014        normalize nodelta lapply (refl ? (eq_bv 5 x1 y1))
    7881015        cases (eq_bv 5 x1 y1) in ⊢ (???% → %); #Hle5
     
    7901017      #Hli <(pair_eq1 ?????? (Some_eq ??? Hli)) >(pair_eq2 ?????? (proj2 ?? Hl))
    7911018      <(pair_eq2 ?????? (Some_eq ??? Hli))
    792       cases old_length
    793       [2,8,14: >Hle3 @Hle5
    794       |19,22: >Hle1 @(leb_true_to_le … Hle2)
     1019      cases (\snd (lookup ?? (bitvector_of_nat ? (|prefix|)) (\snd old_policy) ?))
     1020      [2,8,14,20,26,32: >Hle3 @Hle5
     1021      |37,40,43,46: >Hle1 @(leb_true_to_le … Hle2)
    7951022      ] normalize @I (* here too *)
    7961023    ]
    7971024  ]
    7981025 ]
    799 | (* changed *)
    800   cases (dec_eq_jump_length (max_length old_length ai) old_length) normalize nodelta
    801   [ #Hml #Hc #i #Hi cases (le_to_or_lt_eq … Hi) -Hi >append_length >commutative_plus #Hi
    802     normalize in Hi;
    803     [ >lookup_insert_miss
    804       [ @((proj2 ?? Hpolicy) Hc i (le_S_S_to_le … Hi))
    805       | @bitvector_of_nat_abs
    806         [3: @lt_to_not_eq @(le_S_S_to_le … Hi)
    807         |1: @(transitive_lt ??? (le_S_S_to_le … Hi))
    808         ]
    809         @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    810         @le_S_S @le_plus_n_r
    811       ]
    812     | >(injective_S … Hi) >p3 >lookup_insert_hit normalize nodelta
    813       @pair_elim #x #y #_ @(sym_eq ??? Hml)
    814     ]
    815   | #_ #H destruct (H)
    816   ]
     1026|2,4: (* changed *)
     1027  normalize nodelta #Hc [2: destruct (Hc)] #i #Hi cases (le_to_or_lt_eq … Hi) -Hi
     1028  >append_length >commutative_plus #Hi
     1029  normalize in Hi;
     1030  [ >lookup_insert_miss
     1031    [ @(proj2 ?? (proj1 ?? Hpolicy) Hc i (le_S_S_to_le … Hi))
     1032    | @bitvector_of_nat_abs
     1033      [3: @lt_to_not_eq @(le_S_S_to_le … Hi)
     1034      |1: @(transitive_lt ??? (le_S_S_to_le … Hi))
     1035      ]
     1036      @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
     1037      @le_S_S @le_plus_n_r
     1038    ]
     1039  | >(injective_S … Hi) >lookup_insert_hit normalize nodelta in Hlength; >Hlength
     1040    normalize nodelta @pair_elim #l1 #l2 #Hl @pair_elim #y1 #y2 #Hy >Hl @refl
     1041  ]
    8171042 ]
     1043|2,4: (* policy_isize_sum XXX *) cases daemon
     1044]
    8181045| (* Case where add_instr = None *) normalize nodelta lapply (pi2 ?? acc) >p >p1
    8191046  normalize nodelta #Hpolicy
    820   @conj [ @conj [ @conj [ @conj [ @conj
     1047  @conj [ @conj [ @conj [ @conj [ @conj [ @conj
    8211048[ (* out_of_program_none *) #i >append_length >commutative_plus #Hi normalize in Hi;
    822   #Hi2 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_to_le ?? Hi) Hi2)
     1049  #Hi2 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i (le_S_to_le ?? Hi) Hi2)
    8231050| (* labels_okay *) @lookup_forall #x cases x -x #x cases x #p #a #j #lbl #Hl normalize nodelta
    824   elim (forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) ? lbl Hl)
     1051  elim (forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) ? lbl Hl)
    8251052  #id #Hid @(ex_intro … id Hid)
    8261053 ]
     
    8281055  elim (le_to_or_lt_eq … Hi) -Hi #Hi
    8291056  [ >(nth_append_first ?? prefix ?? (le_S_S_to_le ?? Hi))
    830     @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i (le_S_S_to_le ?? Hi))
     1057    @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_S_to_le ?? Hi))
    8311058  | >(injective_S … Hi) @conj
    8321059    [ >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n whd in match (nth ????);
    833       normalize nodelta in p4; cases instr in p4;
     1060      normalize nodelta in p2; cases instr in p2;
    8341061      [ #pi cases pi
    8351062        [1,2,3,6,7,33,34: #x #y #_ #H @⊥ @H
     
    8481075      ]
    8491076    | #H elim H -H #p #H elim H -H #a #H elim H -H #j #H
    850       >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) (|prefix|) (le_n (|prefix|)) ?) in H;
     1077      >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) (|prefix|) (le_n (|prefix|)) ?) in H;
    8511078      [ #H destruct (H)
    8521079      | @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
     
    8581085| (* policy_increase *) #i >append_length >commutative_plus #Hi normalize in Hi;
    8591086  elim (le_to_or_lt_eq … Hi) -Hi #Hi
    860   [ @(proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)) i (le_S_S_to_le … Hi))
     1087  [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i (le_S_S_to_le … Hi))
    8611088  | >(injective_S … Hi) >lookup_opt_lookup_miss
    8621089    [ >lookup_opt_lookup_miss
    8631090      [ normalize nodelta %2 @refl
    864       | @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) (|prefix|) (le_n (|prefix|)) ?)
     1091      | @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) (|prefix|) (le_n (|prefix|)) ?)
    8651092        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    8661093        @le_S_S @le_plus_n_r
    8671094      ]
    868     | @(proj1 ?? (jump_not_in_policy (pi1 … program) old_policy (|prefix|) ?)) >prf
     1095    | @(proj1 ?? (jump_not_in_policy (pi1 … program) «pi1 ?? old_policy,proj1 ?? (proj1 ?? (pi2 ?? old_policy))» (|prefix|) ?)) >prf
    8691096      [ >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r
    870       | >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n >p2
    871         whd in match (nth ????); normalize nodelta in p4; cases instr in p4;
     1097      | >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n >p1
     1098        whd in match (nth ????); normalize nodelta in p2; cases instr in p2;
    8721099        [ #pi cases pi
    8731100          [1,2,3,6,7,33,34: #x #y #_ normalize /2 by nmk/
     
    8901117 ]
    8911118| (* policy_safe *) @lookup_forall #x cases x -x #x cases x -x #p #a #j #n #Hl
    892   @(forall_lookup … (proj2 ?? (proj1 ?? Hpolicy)) ? n Hl)
     1119  @(forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy))) ? n Hl)
    8931120 ]
    8941121| (* changed *) #Hc #i >append_length >commutative_plus #Hi normalize in Hi;
    8951122  elim (le_to_or_lt_eq … Hi) -Hi #Hi
    896   [ @((proj2 ?? Hpolicy) Hc i (le_S_S_to_le … Hi))
     1123  [ @(proj2 ?? (proj1 ?? Hpolicy) Hc i (le_S_S_to_le … Hi))
    8971124  | >(injective_S … Hi) >lookup_opt_lookup_miss
    8981125    [ >lookup_opt_lookup_miss
    8991126      [ normalize nodelta @refl
    900       | @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) (|prefix|) (le_n (|prefix|)) ?)
     1127      | @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) (|prefix|) (le_n (|prefix|)) ?)
    9011128        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    9021129        @le_S_S @le_plus_n_r
    9031130      ]
    904     | @(proj1 ?? (jump_not_in_policy (pi1 … program) old_policy (|prefix|) ?)) >prf
     1131    | @(proj1 ?? (jump_not_in_policy (pi1 … program) «pi1 ?? old_policy,proj1 ?? (proj1 ?? (pi2 ?? old_policy))» (|prefix|) ?)) >prf
    9051132      [ >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r
    906       | >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n >p2
    907         whd in match (nth ????); normalize nodelta in p4; cases instr in p4;
     1133      | >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n >p1
     1134        whd in match (nth ????); normalize nodelta in p2; cases instr in p2;
    9081135        [ #pi cases pi
    9091136          [1,2,3,6,7,33,34: #x #y #_ normalize /2 by nmk/
     
    9241151    ]
    9251152  ]
    926  ]       
    927 | @conj [ @conj [ @conj [ @conj [ @conj
    928   [ #i #Hi //
    929   | //
     1153 ]
     1154| (* XXX policy_isize_sum *) cases daemon
     1155]
     1156| @conj [ @conj [ @conj [ @conj [ @conj [ @conj
     1157  [ #i #Hi / by refl/
     1158  | / by I/
    9301159  ]
    9311160  | #i #Hi @conj [ >nth_nil #H @⊥ @H | #H elim H #x #H1 elim H1 #y #H2 elim H2 #z #H3
     
    9341163  | #i #Hi @⊥ @(absurd (i<0)) [ @Hi | @(not_le_Sn_O) ]
    9351164  ]
    936   | //
     1165  | / by I/
    9371166  ]
    9381167  | #_ #i #Hi @⊥ @(absurd (i < 0)) [ @Hi | @not_le_Sn_O ]
    9391168  ]
     1169  | / by refl/
     1170  ]
     1171]
    9401172qed.
    9411173
     
    9791211
    9801212let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (|l|) 2^16) (n: ℕ)
    981   on n:(Σx:bool × ℕ × (option jump_expansion_policy).
    982     let 〈c,pc,y〉 ≝ x in
    983     match y with
    984     [ None ⇒ pc > 2^16
    985     | Some p ⇒ And (out_of_program_none program p) (jump_in_policy program p)
     1213  on n:(Σx:bool × (option jump_expansion_policy).
     1214    let 〈c,pol〉 ≝ x in
     1215    match pol with
     1216    [ None ⇒ True
     1217    | Some x ⇒ And (And (And (out_of_program_none program x) (jump_in_policy program x)) (\fst x < 2^16)) (policy_isize_sum program x)
    9861218    ]) ≝
    9871219  match n with
    988   [ O   ⇒ 〈true,0,Some ? (pi1 ?? (jump_expansion_start program))〉
    989   | S m ⇒ let 〈ch,pc,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in
    990           match z return λx. z=x → Σa:bool × ℕ × (option jump_expansion_policy).? with
    991           [ None    ⇒ λp2.〈false,pc,None ?〉
     1220  [ O   ⇒ 〈true,Some ? (pi1 ?? (jump_expansion_start program))〉
     1221  | S m ⇒ let 〈ch,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in
     1222          match z return λx. z=x → Σa:bool × (option jump_expansion_policy).? with
     1223          [ None    ⇒ λp2.〈false,None ?〉
    9921224          | Some op ⇒ λp2.if ch
    9931225            then pi1 ?? (jump_expansion_step program (create_label_map program op) «op,?»)
     
    9951227          ] (refl … z)
    9961228  ].
    997 [ normalize nodelta @(proj1 ?? (pi2 ?? (jump_expansion_start program)))
     1229[ normalize nodelta @conj
     1230  [ @conj
     1231    [ @(proj1 ?? (pi2 ?? (jump_expansion_start program)))
     1232    | (* XXX *) cases daemon
     1233    ]
     1234  | (* XXX *) cases daemon
     1235  ]
    9981236| lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta / by /
    999 |3: lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta / by /
     1237| lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta / by /
    10001238| normalize nodelta cases (jump_expansion_step program (create_label_map program op) «op,?»)
    1001   #p cases p -p #p cases p -p #p #q #r cases r normalize nodelta
    1002   [ #H @(proj1 ?? H)
     1239  #p cases p -p #p #r cases r normalize nodelta
     1240  [ #H / by I/
    10031241  | #j #H @conj
    1004     [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
    1005     | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
     1242    [ @conj
     1243      [ @conj
     1244        [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))))
     1245        | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))))
     1246        ]
     1247      | @(proj2 ?? H)
     1248      ]
     1249    | @(proj2 ?? (proj1 ?? H))
    10061250    ]
    10071251  ]
     
    10111255lemma pe_int_refl: ∀program.reflexive ? (policy_equal_int program).
    10121256#program whd #x whd #n #Hn
    1013 cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉)
     1257cases (bvt_lookup … (bitvector_of_nat 16 n) (\snd x) 〈0,0,short_jump〉)
    10141258#y cases y -y #y #z normalize nodelta @refl
    10151259qed.
     
    10171261lemma pe_int_sym: ∀program.symmetric ? (policy_equal_int program).
    10181262#program whd #x #y #Hxy whd #n #Hn
    1019 lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉)
     1263lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,0,short_jump〉)
    10201264#z cases z -z #x1 #x2 #x3
    1021 cases (bvt_lookup … (bitvector_of_nat ? n) y 〈0,0,short_jump〉)
     1265cases (bvt_lookup … (bitvector_of_nat ? n) (\snd y) 〈0,0,short_jump〉)
    10221266#z cases z -z #y1 #y2 #y3 normalize nodelta //
    10231267qed.
     
    10261270#program whd #x #y #z whd in match (policy_equal_int ???); whd in match (policy_equal_int ?y ?);
    10271271whd in match (policy_equal_int ? x z); #Hxy #Hyz #n #Hn lapply (Hxy n Hn) -Hxy
    1028 lapply (Hyz n Hn) -Hyz cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉)
     1272lapply (Hyz n Hn) -Hyz cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,0,short_jump〉)
    10291273#z cases z -z #x1 #x2 #x3
    1030 cases (bvt_lookup … (bitvector_of_nat ? n) y 〈0,0,short_jump〉) #z cases z -z 
     1274cases (bvt_lookup … (bitvector_of_nat ? n) (\snd y) 〈0,0,short_jump〉) #z cases z -z 
    10311275#y1 #y2 #y3
    1032 cases (bvt_lookup … (bitvector_of_nat ? n) z 〈0,0,short_jump〉) #z cases z -z 
     1276cases (bvt_lookup … (bitvector_of_nat ? n) (\snd z) 〈0,0,short_jump〉) #z cases z -z 
    10331277#z1 #z2 #z3 normalize nodelta //
    10341278qed.
     
    10871331  lapply (refl ? (jump_expansion_internal program (n+k')))
    10881332  cases (jump_expansion_internal program (n+k')) in ⊢ (???% → % → %);
    1089   #x2 cases x2 -x2 #x2 cases x2 -x2 #c2 #p2 #j2 normalize nodelta #H #Heqj2
    1090   cases j2 in H Heqj2;
     1333  #x2 cases x2 -x2 #c2 #p2 normalize nodelta #H #Heqj2
     1334  cases p2 in H Heqj2;
    10911335  [ #H #Heqj2 #_ whd in match (jump_expansion_internal ??);
    10921336    >Heqj2 normalize nodelta @refl
     
    11301374 match program with
    11311375 [ nil      ⇒ acc
    1132  | cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,00
     1376 | cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,00
    11331377,short_jump〉)) with
    11341378   [ long_jump   ⇒ measure_int t policy (acc + 2)
     
    11451389  [ / by refl/
    11461390  | #h #t #Hd #x whd in match (measure_int ???); whd in match (measure_int ?? x);
    1147     cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉))
     1391    cases (\snd (lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,0,short_jump〉))
    11481392    [ normalize nodelta @Hd
    11491393    |2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus
     
    11591403[ normalize @le_n
    11601404| #h #t #Hind whd in match (measure_int ???);
    1161   cases (\snd (lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉))
     1405  cases (\snd (lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,0,short_jump〉))
    11621406  [ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/
    11631407  |2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?)
    1164     @le_plus [1,3: @Hind |2,4: // ]
     1408    @le_plus [1,3: @Hind |2,4: / by le_n/ ]
    11651409  ]
    11661410]
     
    11691413lemma measure_incr_or_equal: ∀program:Σl:list labelled_instruction.|l|<2^16.
    11701414  ∀policy:Σp:jump_expansion_policy.
    1171     out_of_program_none program p ∧ jump_in_policy program p.
     1415    out_of_program_none program p ∧ jump_in_policy program p ∧ \fst p < 2^16 ∧ policy_isize_sum program p.
    11721416  ∀l.|l| ≤ |program| → ∀acc:ℕ.
    11731417  match \snd (jump_expansion_step program (create_label_map program policy) policy) with
     
    11791423| #h #t #Hind #Hp #acc
    11801424  lapply (refl ? (jump_expansion_step program (create_label_map program policy) policy))
    1181   cases (jump_expansion_step ???) in ⊢ (???% → %); #pi1 cases pi1 -pi1 #pi1 cases pi1
    1182   #p #q #r -pi1; cases r
    1183   [ //
    1184   | #x normalize nodelta #Hx #Hjeq lapply (proj2 ?? (proj1 ?? (proj1 ?? Hx)) (|t|) Hp)
     1425  cases (jump_expansion_step ???) in ⊢ (???% → %); #pi1 cases pi1 -pi1 #c #r cases r
     1426  [ / by I/
     1427  | #x normalize nodelta #Hx #Hjeq lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx)))) (|t|) Hp)
    11851428    whd in match (measure_int ???); whd in match (measure_int ? x ?);
    1186     cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)
     1429    cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,0,short_jump〉)
    11871430    #z cases z -z #x1 #x2 #x3
    1188     cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) x 〈0,0,short_jump〉)
     1431    cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd x) 〈0,0,short_jump〉)
    11891432    #z cases z -z #y1 #y2 #y3
    11901433    normalize nodelta #Hj cases Hj
     
    12231466lemma measure_full: ∀program.∀policy.
    12241467  measure_int program policy 0 = 2*|program| → ∀i.i<|program| →
    1225   (\snd (bvt_lookup ?? (bitvector_of_nat ? i) policy 〈0,0,short_jump〉)) = long_jump.
     1468  (\snd (bvt_lookup ?? (bitvector_of_nat ? i) (\snd policy) 〈0,0,short_jump〉)) = long_jump.
    12261469#program #policy elim program
    12271470[ #Hm #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    12281471| #h #t #Hind #Hm #i #Hi cut (measure_int t policy 0 = 2*|t|)
    12291472  [ whd in match (measure_int ???) in Hm;
    1230     cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) in Hm;
     1473    cases (\snd (lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,0,short_jump〉)) in Hm;
    12311474    normalize nodelta
    12321475    [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/
     
    12401483  [ #Hi @(Hind Hmt i (le_S_S_to_le … Hi))
    12411484  | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm;
    1242     cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) in Hm;
     1485    cases (\snd (lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,0,short_jump〉)) in Hm;
    12431486    normalize nodelta
    12441487    [ >Hmt normalize <plus_n_O >(commutative_plus (|t|) (S (|t|)))
     
    12541497lemma measure_special: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
    12551498  ∀policy:Σp:jump_expansion_policy.
    1256     out_of_program_none program p ∧ jump_in_policy program p.
     1499    out_of_program_none program p ∧ jump_in_policy program p ∧ \fst p < 2^16 ∧ policy_isize_sum program p.
    12571500  match (\snd (pi1 ?? (jump_expansion_step program (create_label_map program policy) policy))) with
    12581501  [ None ⇒ True
     
    12601503#program #policy lapply (refl ? (pi1 ?? (jump_expansion_step program (create_label_map program policy) policy)))
    12611504cases (jump_expansion_step program (create_label_map program policy) policy) in ⊢ (???% → %);
    1262 #p cases p -p #p cases p -p #ch #pc #pol normalize nodelta cases pol
    1263 [ //
     1505#p cases p -p #ch #pol normalize nodelta cases pol
     1506[ / by I/
    12641507| #p normalize nodelta #Hpol #eqpol lapply (le_n (|program|))
    12651508  @(list_ind ?  (λx.|x| ≤ |pi1 ?? program| →
     
    12691512 | #h #t #Hind #Hp #Hm #i #Hi cases (le_to_or_lt_eq … Hi) -Hi;
    12701513   [ #Hi @Hind
    1271      [ @(transitive_le … Hp) //
     1514     [ @(transitive_le … Hp) / by /
    12721515     | whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm;
    1273        lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpol)) (|t|) Hp)
     1516       lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (|t|) Hp)
    12741517       cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉) in Hm;
    12751518       #x cases x -x #x1 #x2 #x3
     
    12961539   | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm;
    12971540     whd in match (measure_int ? p ?) in Hm;
    1298      lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpol)) (|t|) Hp)
     1541     lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (|t|) Hp)
    12991542     cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉) in   
    13001543Hm;
     
    13781621  [ lapply (refl ? (jump_expansion_internal program (2*|program|)))
    13791622    cases (jump_expansion_internal program (2*|program|)) in ⊢ (???% → %);
    1380     #x cases x -x #x cases x #Fch #Fpc #Fpol normalize nodelta #HFpol cases Fpol in HFpol;
     1623    #x cases x -x #Fch #Fpol normalize nodelta #HFpol cases Fpol in HFpol; normalize nodelta
    13811624    [ (* if we're at None in 2*|program|, we're at None in S 2*|program| too *)
    13821625      #HFpol #EQ whd in match (jump_expansion_internal ??); >EQ
    1383       normalize nodelta //
     1626      normalize nodelta / by /
    13841627    | #Fp #HFp #EQ whd in match (jump_expansion_internal ??);
    13851628      >EQ normalize nodelta
     
    13891632        [ @le_to_le_to_eq
    13901633          [ @measure_le
    1391           | (* XXX *) cases daemon
     1634          | cut (∀x:ℕ.x ≤ 2*|program| →
     1635             ∃p.(\snd (pi1 ?? (jump_expansion_internal program x)) = Some ? p ∧       
     1636                x ≤ measure_int program p 0))
     1637            [ #x elim x
     1638              [ #Hx @(ex_intro ?? (jump_expansion_start program)) @conj
     1639                [ whd in match (jump_expansion_internal ??); @refl
     1640                | @le_O_n
     1641                ]
     1642              | -x #x #Hind #Hx
     1643                lapply (refl ? (jump_expansion_internal program (S x)))
     1644                cases (jump_expansion_internal program (S x)) in ⊢ (???% → %);
     1645                #z cases z -z #Sxch #Sxpol cases Sxpol -Sxpol normalize nodelta
     1646                [ #H #HeqSxpol @⊥ elim (le_to_eq_plus ?? Hx) #k #Hk
     1647                  @(absurd … (step_none program (S x) ? k))
     1648                  [ >HeqSxpol / by /
     1649                  | <Hk >EQ @nmk #H destruct (H)
     1650                  ]
     1651                | #Sxpol #HSxpol #HeqSxpol @(ex_intro ?? Sxpol) @conj
     1652                  [ @refl
     1653                  | elim (Hind (transitive_le … (le_n_Sn x) Hx))
     1654                    #xpol #Hxpol @(le_to_lt_to_lt … (proj2 ?? Hxpol))
     1655                    lapply (measure_incr_or_equal program xpol program (le_n (|program|)) 0)
     1656                    [ cases (jump_expansion_internal program x) in Hxpol;
     1657                      #z cases z -z #xch #xpol normalize nodelta #H #H2 >(proj1 ?? H2) in H;
     1658                      normalize nodelta / by /
     1659                    | lapply (Hfa x Hx) lapply HeqSxpol -HeqSxpol
     1660                      whd in match (jump_expansion_internal program (S x));
     1661                      lapply (refl ? (jump_expansion_internal program x))
     1662                      lapply Hxpol -Hxpol cases (jump_expansion_internal program x) in ⊢ (% → ???% → %);
     1663                      #z cases z -z #xch #b normalize nodelta #H #Heq >(proj1 ?? Heq) in H;
     1664                      #H #Heq cases xch in Heq; #Heq normalize nodelta
     1665                      [ lapply (refl ? (jump_expansion_step program (create_label_map (pi1 ?? program) xpol) «xpol,H»))
     1666                        cases (jump_expansion_step ???) in ⊢ (???% → %); #z cases z -z #a #c
     1667                        normalize nodelta cases c normalize nodelta
     1668                        [ #H1 #Heq #H2 destruct (H2)
     1669                        | #d #H1 #Heq #H2 destruct (H2) #Hfull #H2 elim (le_to_or_lt_eq … H2)
     1670                          [ / by /
     1671                          | #H3 lapply (measure_special program «xpol,H») >Heq
     1672                            normalize nodelta #H4 @⊥
     1673                            @(absurd … (H4 H3))
     1674                            @Hfull
     1675                          ]
     1676                        ]
     1677                      | lapply (refl ? (jump_expansion_step program (create_label_map (pi1 ?? program) xpol) «xpol,H»))
     1678                        cases (jump_expansion_step ???) in ⊢ (???% → %); #z cases z -z #a #c
     1679                        normalize nodelta cases c normalize nodelta
     1680                        [ #H1 #Heq #H2 #H3 #_ @⊥ @(absurd ?? H3) @pe_refl
     1681                        | #d #H1 #Heq #H2 #H3 @⊥ @(absurd ?? H3) @pe_refl
     1682                        ]
     1683                      ]
     1684                    ]
     1685                  ]
     1686                ]
     1687              ]
     1688            | #H elim (H (2*|program|) (le_n ?)) #plp >EQ #Hplp
     1689              >(Some_eq ??? (proj1 ?? Hplp)) @(proj2 ?? Hplp)
     1690            ]
    13921691          ]
    13931692        | #Hfull cases (jump_expansion_step program (create_label_map program Fp) «Fp,?») in ⊢ (???% → %);
    1394           #x cases x -x #x cases x -x #Gch #Gpc #Gpol cases Gpol normalize nodelta
    1395           [ #H #EQ2 @⊥ @(absurd ?? (proj2 ?? H)) @Hfull
     1693          #x cases x -x #Gch #Gpol cases Gpol normalize nodelta
     1694          [ #H #EQ2 @⊥ @(absurd ?? H) @Hfull
    13961695          | #Gp #HGp #EQ2 cases Fch
    13971696            [ normalize nodelta #i #Hi
    1398               lapply (refl ? (lookup ?? (bitvector_of_nat 16 i) Fp 〈0,0,short_jump〉))
    1399               cases (lookup ?? (bitvector_of_nat 16 i) Fp 〈0,0,short_jump〉) in ⊢ (???% → %);
     1697              lapply (refl ? (lookup ?? (bitvector_of_nat 16 i) (\snd Fp) 〈0,0,short_jump〉))
     1698              cases (lookup ?? (bitvector_of_nat 16 i) (\snd Fp) 〈0,0,short_jump〉) in ⊢ (???% → %);
    14001699              #x cases x -x #p #a #j normalize nodelta #H
    1401               lapply (proj2 ?? (proj1 ?? (proj1 ?? HGp)) i Hi) lapply (Hfull i Hi) >H
    1402               #H2 >H2 normalize nodelta cases (lookup ?? (bitvector_of_nat 16 i) Gp 〈0,0,short_jump\rangle)
     1700              lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))) i Hi) lapply (Hfull i Hi) >H
     1701              #H2 >H2 normalize nodelta cases (lookup ?? (bitvector_of_nat 16 i) (\snd Gp) 〈0,0,short_jump〉)
    14031702              #x cases x -x #p #a #j' cases j' normalize nodelta #H elim H -H #H
    14041703              [1,3: @⊥ @H
     
    14151714  ]
    14161715| #n cases (jump_expansion_internal program n) cases (jump_expansion_internal program (S n))
    1417   #x cases x -x #x cases x -x #nch #npc #npol normalize nodelta #Hnpol
    1418   #x cases x -x #x cases x -x #Sch #Scp #Spol normalize nodelta #HSpol
     1716  #x cases x -x #nch #npol normalize nodelta #Hnpol
     1717  #x cases x -x #Sch #Spol normalize nodelta #HSpol
    14191718  cases npol in Hnpol; cases Spol in HSpol;
    14201719  [ #Hnpol #HSpol %1 //
     
    14341733 * a map from pc to jump_length. This cannot be done earlier because the pc
    14351734 * changes between iterations. *)
    1436 let rec transform_policy (n: nat) policy (acc: BitVectorTrie jump_length 16) on n:
     1735let rec transform_policy (n: nat) (policy: jump_expansion_policy) (acc: BitVectorTrie jump_length 16) on n:
    14371736  BitVectorTrie jump_length 16 ≝
    14381737  match n with
    14391738  [ O    ⇒ acc
    14401739  | S n' ⇒
    1441     match lookup_opt … (bitvector_of_nat 16 n') policy with
     1740    match lookup_opt … (bitvector_of_nat 16 n') (\snd policy) with
    14421741    [ None   ⇒ transform_policy n' policy acc
    1443     | Some x ⇒ let 〈pc,length〉 ≝ x in
    1444       transform_policy n' policy (insert … pc length acc)
     1742    | Some x ⇒ let 〈pc,addr,length〉 ≝ x in
     1743      transform_policy n' policy (insert … (bitvector_of_nat 16 pc) length acc)
    14451744    ]
    14461745  ].
     
    14531752  let policy ≝
    14541753    transform_policy (|\snd program|) (pi1 … (je_fixpoint (\snd program))) (Stub ??) in
    1455   (* here we must use jump_length_ok *)
    1456   bvt_lookup ? ? pc policy long_jump.
    1457 /2 by Stub, mk_Sig/
    1458 qed.
     1754  «bvt_lookup ? ? pc policy long_jump,?».
     1755  cases daemon (* XXX later *)
     1756qed.
Note: See TracChangeset for help on using the changeset viewer.