Changeset 1809 for src/ASM/Policy.ma


Ignore:
Timestamp:
Mar 7, 2012, 1:27:17 PM (8 years ago)
Author:
boender
Message:
  • committed partially compiling version of policy (up until jump_expansion_step)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r1615 r1809  
    88include "ASM/Assembly.ma".
    99
    10 definition max_length: jump_length → jump_length → jump_length ≝
    11   λj1.λj2.
    12   match j1 with
    13   [ long_jump   ⇒ long_jump
    14   | medium_jump ⇒
    15     match j2 with
    16     [ long_jump ⇒ long_jump
    17     | _         ⇒ medium_jump
    18     ]
    19   | short_jump  ⇒ j2
     10(* Internal types *)
     11
     12(* label_map: identifier ↦ 〈instruction number, address〉 *)
     13definition label_map ≝ identifier_map ASMTag (ℕ × ℕ).
     14
     15(* jump_expansion_policy: instruction number ↦ 〈pc, addr, jump_length〉 *)
     16definition jump_expansion_policy ≝ BitVectorTrie (ℕ × ℕ × jump_length) 16.
     17
     18(* The different properties that we want/need to prove at some point *)
     19(* Anything that's not in the program doesn't end up in the policy *)
     20definition out_of_program_none ≝
     21  λprefix:list labelled_instruction.λpolicy:jump_expansion_policy.
     22  ∀i.i ≥ |prefix| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) policy = None ?.
     23
     24(* If instruction i is a jump, then there will be something in the policy at
     25 * position i *)
     26definition is_jump' ≝
     27  λx:preinstruction Identifier.
     28  match x with
     29  [ JC _ ⇒ True
     30  | JNC _ ⇒ True
     31  | JZ _ ⇒ True
     32  | JNZ _ ⇒ True
     33  | JB _ _ ⇒ True
     34  | JNB _ _ ⇒ True
     35  | JBC _ _ ⇒ True
     36  | CJNE _ _ ⇒ True
     37  | DJNZ _ _ ⇒ True
     38  | _ ⇒ False
    2039  ].
    21 
     40 
     41definition is_jump ≝
     42  λx:labelled_instruction.
     43  let 〈label,instr〉 ≝ x in
     44  match instr with
     45  [ Instruction i   ⇒ is_jump' i
     46  | Call _ ⇒ True
     47  | Jmp _ ⇒ True
     48  | _ ⇒ False
     49  ].
     50
     51definition jump_in_policy ≝
     52  λprefix:list labelled_instruction.λpolicy:jump_expansion_policy.
     53  ∀i:ℕ.i < |prefix| →
     54  (is_jump (nth i ? prefix 〈None ?, Comment []〉) ↔
     55   ∃p,a,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,a,j〉).
     56
     57definition labels_okay ≝
     58  λ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
     62  ).
     63 
     64(* Between two policies, jumps cannot decrease *)
    2265definition jmple: jump_length → jump_length → Prop ≝
    2366  λj1.λj2.
     
    3982  λj1.λj2.jmple j1 j2 ∨ j1 = j2.
    4083 
     84definition policy_increase: list labelled_instruction → jump_expansion_policy →
     85  jump_expansion_policy → Prop ≝
     86 λprogram.λop.λp.
     87  (∀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).
     91
     92(* Policy safety *)
     93definition policy_safe: jump_expansion_policy → Prop ≝
     94 λpolicy.
     95 bvt_forall ?? policy (λn.λx.let 〈pc_nat,addr_nat,jmp_len〉 ≝ x in
     96   match jmp_len with
     97   [ short_jump  ⇒ if leb pc_nat addr_nat
     98      then le (addr_nat - pc_nat) 126
     99      else le (pc_nat - addr_nat) 129
     100   | medium_jump ⇒
     101      let addr ≝ bitvector_of_nat 16 addr_nat in
     102      let pc ≝ bitvector_of_nat 16 pc_nat in
     103      let 〈fst_5_addr, rest_addr〉 ≝ split bool 5 11 addr in
     104      let 〈fst_5_pc, rest_pc〉 ≝ split bool 5 11 pc in
     105      eq_bv 5 fst_5_addr fst_5_pc = true
     106   | long_jump   ⇒ True
     107   ]
     108 ).
     109 
     110(* Definitions and theorems for the jump_length type (itself defined in Assembly) *)
     111definition max_length: jump_length → jump_length → jump_length ≝
     112  λj1.λj2.
     113  match j1 with
     114  [ long_jump   ⇒ long_jump
     115  | medium_jump ⇒
     116    match j2 with
     117    [ medium_jump ⇒ medium_jump
     118    | _           ⇒ long_jump
     119    ]
     120  | short_jump  ⇒
     121    match j2 with
     122    [ short_jump ⇒ short_jump
     123    | _          ⇒ long_jump
     124    ]
     125  ].
     126
    41127lemma dec_jmple: ∀x,y:jump_length.jmple x y + ¬(jmple x y).
    42128 #x #y cases x cases y /3 by inl, inr, nmk, I/
     
    54140qed.
    55141
    56  
    57 (* jump_expansion_policy: instruction number ↦ 〈pc, addr, jump_length〉 *)
    58 definition jump_expansion_policy ≝ BitVectorTrie (ℕ × ℕ × jump_length) 16.
    59 
    60 (* label_map: identifier ↦ 〈instruction number, address〉 *)
    61 definition label_map ≝ identifier_map ASMTag (nat × nat).
    62 
     142(* Labels *)
    63143definition is_label ≝
    64144  λx:labelled_instruction.λl:Identifier.
     
    68148  | _       ⇒ False
    69149  ].
    70 
    71 definition add_instruction_size: ℕ → jump_length → pseudo_instruction → ℕ ≝
    72   λpc.λjmp_len.λinstr.
    73   let bv_pc ≝ bitvector_of_nat 16 pc in
    74   let ilist ≝ expand_pseudo_instruction_safe (λx.bv_pc) (λx.bv_pc) bv_pc jmp_len instr in
    75   let bv: list (BitVector 8) ≝ match ilist with
    76     [ None   ⇒ (* this shouldn't happen *) [ ]
    77     | Some l ⇒ flatten … (map … assembly1 l)
    78     ] in
    79   pc + (|bv|).
    80150
    81151lemma label_does_not_occur:
     
    89159     | #l' #Heq whd in ⊢ (??%?); change with (eq_identifier ? l' l) in match (instruction_matches_identifier ??);
    90160       whd in Heq; >Heq
    91        >eq_identifier_refl //
     161       >eq_identifier_refl / by refl/
    92162     ]
    93163   | #i #H whd in match (does_not_occur ??);
     
    96166     [ @(IH i) @H
    97167     | #l' @eq_identifier_elim
    98        [ normalize //
     168       [ normalize / by /
    99169       | normalize #_ @(IH i) @H
    100170       ]
     
    102172   ]
    103173 ]
    104 qed. 
    105 
     174qed.
     175
     176definition 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
     180  let bv: list (BitVector 8) ≝ match ilist with
     181    [ None   ⇒ (* this shouldn't happen *) [ ]
     182    | Some l ⇒ flatten … (map … assembly1 l)
     183    ] in
     184  pc + (|bv|).
     185 @(λx.bv_pc)
     186qed.
     187
     188(* The function that creates the label-to-address map *)
    106189definition create_label_map: ∀program:list labelled_instruction.
    107190  ∀policy:jump_expansion_policy.
     
    146229      | normalize nodelta lapply (pi2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc ?)
    147230        [ #addr #Haddr % [ @addr | <Haddr @lookup_add_miss /2/ ]
    148         | >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; //
     231        | >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; / by /
    149232        ]
    150233      ]
    151       >(label_does_not_occur i … Hl) normalize nodelta @nmk //
     234      >(label_does_not_occur i … Hl) normalize nodelta @nmk / by /
    152235    ]
    153236  | #Hi #l #Hocc >(injective_S … Hi) >nth_append_second
     
    212295  ].
    213296
    214 definition is_jump' ≝
    215   λx:preinstruction Identifier.
    216   match x with
    217   [ JC _ ⇒ True
    218   | JNC _ ⇒ True
    219   | JZ _ ⇒ True
    220   | JNZ _ ⇒ True
    221   | JB _ _ ⇒ True
    222   | JNB _ _ ⇒ True
    223   | JBC _ _ ⇒ True
    224   | CJNE _ _ ⇒ True
    225   | DJNZ _ _ ⇒ True
    226   | _ ⇒ False
    227   ].
    228  
    229 definition is_jump ≝
    230   λx:labelled_instruction.
    231   let 〈label,instr〉 ≝ x in
    232   match instr with
    233   [ Instruction i   ⇒ is_jump' i
    234   | Call _ ⇒ True
    235   | Jmp _ ⇒ True
    236   | _ ⇒ False
    237   ].
    238 
    239297lemma dec_is_jump: ∀x.(is_jump x) + (¬is_jump x).
    240298#x cases x #l #i cases i
     
    245303  #x %2 whd in match (is_jump ?); /2 by nmk/
    246304 |35,36,37: %2 whd in match (is_jump ?); /2 by nmk/
    247  |9,10,14,15: #x %1 //
    248  |11,12,13,16,17: #x #y %1 //
     305 |9,10,14,15: #x %1 / by I/
     306 |11,12,13,16,17: #x #y %1 / by I/
    249307 ]
    250308|2,3: #x %2 /2 by nmk/
    251 |4,5: #x %1 //
     309|4,5: #x %1 / by I/
    252310|6: #x #y %2 /2 by nmk/
    253311]
    254312qed.
    255  
    256 
    257 definition jump_in_policy ≝
    258   λprefix:list labelled_instruction.λpolicy:jump_expansion_policy.
    259   ∀i:ℕ.i < |prefix| →
    260   (is_jump (nth i ? prefix 〈None ?, Comment []〉) ↔
    261    ∃p,a,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,a,j〉).
    262 
    263 (* these should be moved to BitVector at some point *) 
     313
     314(* these should be moved to BitVector at some point, and proven *) 
    264315lemma bitvector_of_nat_ok:
    265316  ∀n,x,y:ℕ.x < 2^n → y < 2^n → eq_bv n (bitvector_of_nat n x) (bitvector_of_nat n y) → x = y.
     
    275326 lapply (refl ? (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)))
    276327 cases (eq_bv ? (bitvector_of_nat n x) (bitvector_of_nat n y)) in ⊢ (???% → %);
    277  [ #H @⊥ @(absurd ?? Heq) @(bitvector_of_nat_ok n x y Hx Hy) >H //
    278  | #H //
     328 [ #H @⊥ @(absurd ?? Heq) @(bitvector_of_nat_ok n x y Hx Hy) >H / by I/
     329 | #H / by I/
    279330 ]
    280331qed.
     
    282333lemma jump_not_in_policy: ∀prefix:list labelled_instruction.
    283334 ∀policy:(Σp:jump_expansion_policy.
    284  (∀i.i ≥ |prefix| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
    285  jump_in_policy prefix p).
     335 out_of_program_none prefix p ∧ jump_in_policy prefix p).
    286336  ∀i:ℕ.i < |prefix| →
    287337  iff (¬is_jump (nth i ? prefix 〈None ?, Comment []〉))
     
    299349qed.
    300350
     351(* these two obviously belong somewhere else *) 
     352lemma pi1_eq: ∀A:Type[0].∀P:A->Prop.∀s1:Σa1:A.P a1.∀s2:Σa2:A.P a2.
     353  s1 = s2 → (pi1 ?? s1) = (pi1 ?? s2).
     354 #A #P #s1 #s2 / by /
     355qed.
     356
     357lemma Some_eq:
     358 ∀T:Type[0].∀x,y:T. Some T x = Some T y → x = y.
     359 #T #x #y #H @option_destruct_Some @H
     360qed.
     361
     362(* The first step of the jump expansion: everything to short.
     363 * The third condition of the dependent type implies jump_in_policy;
     364 * I've left it in for convenience of type-checking. *)
    301365definition jump_expansion_start:
    302366  ∀program:(Σl:list labelled_instruction.|l| < 2^16).
    303367  Σpolicy:jump_expansion_policy.
    304     (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?)
     368    out_of_program_none program policy
    305369    jump_in_policy program policy ∧
    306370    ∀i.i < |program| → is_jump (nth i ? program 〈None ?, Comment []〉) →
     
    309373  foldl_strong (option Identifier × pseudo_instruction)
    310374  (λprefix.Σpolicy:jump_expansion_policy.
    311     (∀i.i ≥ |prefix| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?)
     375    out_of_program_none prefix policy
    312376    jump_in_policy prefix policy ∧
    313377    ∀i.i < |prefix| → is_jump (nth i ? prefix 〈None ?, Comment []〉) →
     
    372436 [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:
    373437  #Hj @(proj2 ?? (pi2 ?? policy) i (le_S_S_to_le … Hi))
    374   >(nth_append_first ?? prefix ?? (le_S_S_to_le ?? Hi)) in Hj; //
     438  >(nth_append_first ?? prefix ?? (le_S_S_to_le ?? Hi)) in Hj; / by /
    375439 ]
    376440 >(injective_S … Hi) >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n
     
    407471  @conj >(injective_S … Hi) #H
    408472  [2,4,6,8,10,12,14,16,18,20,22:
    409    >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n //
     473   >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n / by I/
    410474  ]
    411475  @(ex_intro ?? 0 (ex_intro ?? 0 (ex_intro ?? short_jump (lookup_opt_insert_hit ?? 16 ? policy))))
     
    428492|@conj
    429493 [@conj
    430   [ #i #Hi //
     494  [ #i #Hi / by refl/
    431495  | whd #i #Hi @⊥ @(absurd (i < 0) Hi (not_le_Sn_O ?))
    432496  ]
     
    435499qed.
    436500
    437 definition policy_increase: list labelled_instruction → jump_expansion_policy →
    438   jump_expansion_policy → Prop ≝
    439  λprogram.λop.λp.
    440   (∀i:ℕ.i < |program| →
    441     let 〈i1,i2,oj〉 ≝ bvt_lookup ?? (bitvector_of_nat ? i) op 〈0,0,short_jump〉 in
    442     let 〈i3,i4,j〉 ≝ bvt_lookup ?? (bitvector_of_nat ? i) p 〈0,0,short_jump〉 in
    443     jmpleq oj j).
    444 
    445 definition policy_safe: (*label_map → *)jump_expansion_policy → Prop ≝
    446  (*λlabels.*)λpolicy.
    447  bvt_forall (ℕ×ℕ×jump_length) 16 policy (λn.λx.let 〈pc_nat,addr_nat,jmp_len〉 ≝ x in
    448     match jmp_len with
    449     [ short_jump  ⇒ if leb pc_nat addr_nat
    450        then le (addr_nat - pc_nat) 126
    451        else le (pc_nat - addr_nat) 129
    452     | medium_jump ⇒
    453        let addr ≝ bitvector_of_nat 16 addr_nat in
    454        let pc ≝ bitvector_of_nat 16 pc_nat in
    455        let 〈fst_5_addr, rest_addr〉 ≝ split bool 5 11 addr in
    456        let 〈fst_5_pc, rest_pc〉 ≝ split bool 5 11 pc in
    457        eq_bv 5 fst_5_addr fst_5_pc = true
    458     | long_jump   ⇒ True
    459     ]
    460   ).
    461  
     501definition policy_equal_int ≝
     502  λprogram:list labelled_instruction.λp1,p2:jump_expansion_policy.
     503  ∀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
     506    j1 = j2.
     507   
     508(* One step in the search for a jump expansion fixpoint. *)
    462509definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
    463510  ∀labels:(Σlm:label_map.∀i:ℕ.lt i (|program|) →
     
    466513    ∃a.lookup … lm l = Some ? 〈i,a〉).
    467514  ∀old_policy:(Σpolicy.
    468     (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
    469     jump_in_policy program policy).
    470   (Σpolicy.
    471     (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
    472     jump_in_policy program policy ∧
    473     policy_increase program old_policy policy)
     515    out_of_program_none program policy ∧ jump_in_policy program policy).
     516  (Σx:bool × ℕ × (option jump_expansion_policy).
     517    let 〈changed,pc,y〉 ≝ x in
     518    match y with
     519    [ None ⇒ pc > 2^16
     520    | Some p ⇒ out_of_program_none program p ∧ labels_okay labels p ∧
     521        jump_in_policy program p ∧
     522        policy_increase program old_policy p ∧
     523        policy_safe p ∧
     524        (changed = false → policy_equal_int program old_policy p)
     525    ])
    474526    ≝
    475527  λprogram.λlabels.λold_policy.
    476   let 〈final_pc, final_policy〉 ≝
     528  let 〈final_changed, final_pc, final_policy〉 ≝
    477529    foldl_strong (option Identifier × pseudo_instruction)
    478     (λprefix.ℕ × Σpolicy.
    479       (∀i.i ≥ |prefix| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
    480       jump_in_policy prefix policy ∧
    481       policy_increase prefix old_policy policy
    482     )
     530    (λprefix.Σx:bool × ℕ × jump_expansion_policy.
     531        let 〈changed,pc,policy〉 ≝ x in
     532        out_of_program_none prefix policy ∧ labels_okay labels policy ∧
     533        jump_in_policy prefix policy ∧
     534        policy_increase prefix old_policy policy ∧
     535        policy_safe policy ∧
     536        (changed = false → policy_equal_int prefix old_policy policy))
    483537    program
    484538    (λprefix.λx.λtl.λprf.λacc.
    485       let 〈pc, policy〉 ≝ acc in
     539      let 〈changed, pc, policy〉 ≝ acc in
    486540      let 〈label,instr〉 ≝ x in
    487       let old_jump_length ≝ lookup_opt ? ? (bitvector_of_nat 16 (|prefix|)) old_policy in
     541(*      let old_jump_length ≝ lookup_opt ? ? (bitvector_of_nat 16 (|prefix|)) old_policy in *)
    488542      let add_instr ≝
    489543        match instr with
     
    493547        | _             ⇒ None ?
    494548        ] in
    495       let 〈new_pc, new_policy〉 ≝
    496549        let 〈ignore,old_length〉 ≝ bvt_lookup … (bitvector_of_nat 16 (|prefix|)) old_policy 〈0, 0, short_jump〉 in
    497550        match add_instr with
    498551        [ None    ⇒ (* i.e. it's not a jump *)
    499           〈add_instruction_size pc long_jump instr, policy〉
     552          〈changed, add_instruction_size pc long_jump instr, policy〉
    500553        | Some z ⇒ let 〈addr,ai〉 ≝ z in
    501554          let new_length ≝ max_length old_length ai in
    502           〈add_instruction_size pc new_length instr, insert … (bitvector_of_nat 16 (|prefix|)) 〈pc, addr, new_length〉 policy〉
    503         ] in
    504       〈new_pc, new_policy〉
    505     ) 〈0, Stub ? ?〉 in
    506     final_policy.
    507 [ @conj [ @conj #i >append_length <commutative_plus #Hi normalize in Hi;
    508 [ #Hi2 cases (lookup ??? old_policy ?) #h #n cases add_instr
    509   [ @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2)
    510   | #z cases z -z #z1 #z2 whd in match (snd ???); >lookup_opt_insert_miss
    511     [ @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2)
    512     | >eq_bv_sym @bitvector_of_nat_abs
    513       [ @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    514         @le_S_S @le_plus_n_r
    515       | @Hi2
    516       | @lt_to_not_eq @Hi
    517       ]
    518     ]
    519   ]
    520 | cases (le_to_or_lt_eq … Hi) -Hi;
    521   [ #Hi; >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) @conj
    522     [ #Hj lapply (proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc
    523       cases add_instr cases (lookup ??? old_policy ?) normalize nodelta #x #y
    524       [ @(proj1 ?? Hacc Hj)
    525       | #z cases z -z #z1 #z2 elim (proj1 ?? Hacc Hj) #h #n elim n -n #n #H elim H -H #j #Hj
    526         @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?))) whd in match (snd ???);
    527         >lookup_opt_insert_miss [ @Hj |  @bitvector_of_nat_abs ]
    528         [3: @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
    529         |1: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
     555          〈match dec_eq_jump_length new_length old_length with
     556           [ inl _ ⇒ changed
     557           | inr _ ⇒ true], add_instruction_size pc new_length instr, insert … (bitvector_of_nat 16 (|prefix|)) 〈pc, addr, new_length〉 policy〉
    530558        ]
    531         @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    532         @le_S_S @le_plus_n_r
    533       ]
    534     | lapply (proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc
    535       #H elim H -H; #h #H elim H -H; #n #H elim H -H #j cases add_instr cases (lookup ??? old_policy ?)
    536       normalize nodelta #x #y [2: #z]
     559    ) 〈false, 0, Stub ? ?〉 in
     560    if geb final_pc 2^16 then
     561      〈final_changed,final_pc,None ?〉
     562    else
     563      〈final_changed,final_pc,Some jump_expansion_policy final_policy〉.
     564[ normalize nodelta @leb_true_to_le @p2
     565| normalize nodelta lapply p generalize in match (foldl_strong ?????); * #x #H #H2
     566  >H2 in H; >p1 normalize nodelta //
     567| lapply (pi2 ?? acc) >p >p1 normalize nodelta #Hpolicy
     568 @conj [ @conj [ @conj [ @conj [ @conj
     569[ (* out_of_policy_none *)
     570  #i >append_length <commutative_plus #Hi normalize in Hi;
     571  #Hi2 >lookup_opt_insert_miss
     572  [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_to_le … Hi)) @Hi2
     573  | >eq_bv_sym @bitvector_of_nat_abs
     574    [ @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
     575      @le_S_S @le_plus_n_r
     576    | @Hi2
     577    | @lt_to_not_eq @Hi
     578    ]
     579  ]
     580| (* labels_okay *)
     581  @lookup_forall #i cases i -i #i cases i -i #p #a #j #n (*lapply (refl ? add_instr)
     582  cases (lookup ??? old_policy ?); #x cases x -x #p1 #p2 #p3
     583  cases add_instr in ⊢ (???% → %);
     584  [ #Hai normalize nodelta #Hl
     585    elim (forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) ? n Hl)
     586    #i #Hi @(ex_intro ?? i Hi)
     587  | #x cases x -x #np #nl #Hai normalize nodelta *) #Hl
     588    elim (insert_lookup_opt ?? 〈p,a,j〉 ???? Hl) -Hl #Hl
     589    [ elim (forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) ? n Hl)
     590      #i #Hi @(ex_intro ?? i Hi)
     591    | (*whd in match add_instr in Hai; cases instr in Hai;*) normalize nodelta
     592      normalize nodelta in p4; cases instr in p4;
     593      [2,3: #x #abs normalize nodelta in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
     594      |6: #x #y #abs normalize nodelta in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
     595      |1: #pi cases pi
     596        [35,36,37: #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
     597        |1,2,3,6,7,33,34: #x #y #abs normalize in abs; lapply (jmeq_to_eq ??? abs)
     598          #H destruct (H)
     599        |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #abs normalize in abs;
     600          lapply (jmeq_to_eq ??? abs) #H destruct (H)
     601        |9,10,14,15: #id normalize nodelta whd in match (jump_expansion_step_instruction ???);
     602          whd in match (select_reljump_length ???); >p5
     603          lapply (refl ? (lookup_def ?? labels id 〈0,pc〉))
     604          cases (lookup_def ?? labels id 〈0,pc〉) in ⊢ (???% → %); #q1 #q2
     605          normalize nodelta #H
     606          >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
     607          >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb pc q2))
     608          cases (leb pc q2) in ⊢ (???% → %); #Hle1
     609          [1,3,5,7: lapply (refl ? (leb (q2-pc) 126)) cases (leb (q2-pc) 126) in ⊢ (???% → %);
     610          |2,4,6,8: lapply (refl ? (leb (pc-q2) 129)) cases (leb (pc-q2) 129) in ⊢ (???% → %);
     611          ]
     612          #Hle2 normalize nodelta #Hli @(ex_intro ?? id) >H
     613          <(pair_eq1 ?????? (Some_eq ??? Hli)) @refl
     614        |11,12,13,16,17: #x #id normalize nodelta whd in match (jump_expansion_step_instruction ???);
     615          whd in match (select_reljump_length ???); >p5
     616          lapply (refl ? (lookup_def ?? labels id 〈0,pc〉))
     617          cases (lookup_def ?? labels id 〈0,pc〉) in ⊢ (???% → %); #q1 #q2
     618          normalize nodelta #H
     619          >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
     620          >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb pc q2))
     621          cases (leb pc q2) in ⊢ (???% → %); #Hle1
     622          [1,3,5,7,9: lapply (refl ? (leb (q2-pc) 126)) cases (leb (q2-pc) 126) in ⊢ (???% → %);
     623          |2,4,6,8,10: lapply (refl ? (leb (pc-q2) 129)) cases (leb (pc-q2) 129) in ⊢ (???% → %);
     624          ]
     625          #Hle2 normalize nodelta #Hli @(ex_intro ?? id) >H
     626          <(pair_eq1 ?????? (Some_eq ??? Hli)) @refl
     627        ]
     628      |4,5: #id normalize nodelta whd in match (select_jump_length ???);
     629          whd in match (select_call_length ???); >p5
     630          lapply (refl ? (lookup_def ?? labels id 〈0,pc〉))
     631          cases (lookup_def ?? labels id 〈0,pc〉) in ⊢ (???% → %); #q1 #q2
     632          normalize nodelta #H
     633          [1: cases (leb pc q2)
     634            [ cases (leb (q2-pc) 126) | cases (leb (pc-q2) 129) ]
     635            [1,3: normalize nodelta #H2 >(pair_eq1 ?????? (Some_eq ??? H2)) in H;
     636            #Hli @(ex_intro ?? id) lapply (proj2 ?? Hl)
     637            #H >(pair_eq1 ?????? (pair_eq1 ?????? H))
     638            >(pair_eq2 ?????? (pair_eq1 ?????? H)) >Hli @refl]
     639          ]
     640          cases (split ? 5 11 (bitvector_of_nat 16 q2)) #n1 #n2
     641          cases (split ? 5 11 (bitvector_of_nat 16 pc)) #m1 #m2
     642          normalize nodelta cases (eq_bv ? n1 m1)
     643          normalize nodelta #H2 >(pair_eq1 ?????? (Some_eq ??? H2)) in H; #H
     644          @(ex_intro ?? id) lapply (proj2 ?? Hl) #H2
     645          >(pair_eq1 ?????? (pair_eq1 ?????? H2)) >(pair_eq2 ?????? (pair_eq1 ?????? H2))
     646          >H @refl
     647      ]
     648    ]
     649  ]
     650| (* jump_in_policy *)
     651  #i #Hi cases (le_to_or_lt_eq … Hi) -Hi;
     652  [ >append_length <commutative_plus #Hi normalize in Hi;
     653    >(nth_append_first ?? prefix ??(le_S_S_to_le ?? Hi)) @conj
     654    [ #Hj lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i (le_S_S_to_le … Hi))
     655      #Hacc elim (proj1 ?? Hacc Hj) #h #n elim n -n #n #H elim H -H #j #Hj
     656      @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?))) whd in match (snd ???);
     657      >lookup_opt_insert_miss [ @Hj |  @bitvector_of_nat_abs ]
     658      [3: @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
     659      |1: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
     660      ]
     661      @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
     662      @le_S_S @le_plus_n_r
     663    | lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i (le_S_S_to_le … Hi)) #Hacc
     664      #H elim H -H; #h #H elim H -H; #n #H elim H -H #j
    537665      #Hl @(proj2 ?? Hacc) @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?)))
    538       [ <Hl @sym_eq cases z #z1 #z2 whd in match (snd ???); @lookup_opt_insert_miss @bitvector_of_nat_abs
    539         [3: @lt_to_not_eq @(le_S_S_to_le … Hi)
    540         |1: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
    541         ]
    542         @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    543         @le_S_S @le_plus_n_r
    544       | @Hl
    545       ]
    546     ]
    547   | #Hi >(injective_S … Hi) >(nth_append_second ? ? prefix ? ? (le_n (|prefix|)))
    548      <minus_n_n whd in match (nth ????); whd in match (add_instr); cases instr
    549      [1: #pi | 2,3: #x | 4,5: #id | 6: #x #y] @conj normalize nodelta
     666      <Hl @sym_eq @lookup_opt_insert_miss @bitvector_of_nat_abs
     667      [3: @lt_to_not_eq @(le_S_S_to_le … Hi)
     668      |1: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
     669      ]
     670      @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
     671      @le_S_S @le_plus_n_r
     672    ]
     673  | >append_length <commutative_plus #Hi normalize in Hi; >(injective_S … Hi)
     674    >(nth_append_second ?? prefix ?? (le_n (|prefix|)))
     675     <minus_n_n whd in match (nth ????); normalize nodelta in p4; cases instr in p4;
     676     [1: #pi | 2,3: #x | 4,5: #id | 6: #x #y] #Hinstr @conj normalize nodelta
    550677     [3,5,11: #H @⊥ @H (* instr is not a jump *)
    551      |4,6,12: #H elim H -H; #h #H elim H -H #n #H elim H -H #j cases (lookup ??? old_policy ?)
    552        #x #y normalize nodelta >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
    553        [1,3,5: #H destruct (H)]
    554        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    555        @le_S_S @le_plus_n_r
    556      |7,9: (* instr is a jump *) #_ cases (lookup ??? old_policy ?) #x cases x #h #n #j
    557        whd in match (snd ???); @(ex_intro ?? pc)
    558        [ @(ex_intro ?? (\fst (select_jump_length labels pc id)))
    559          @(ex_intro ?? (max_length j (\snd (select_jump_length labels pc id))))
    560          cases (select_jump_length labels pc id)
    561        | @(ex_intro ?? (\fst (select_call_length labels pc id)))
    562          @(ex_intro ?? (max_length j (\snd (select_call_length labels pc id))))
    563          cases (select_call_length labels pc id)
    564        ] #z1 #z2 normalize nodelta @lookup_opt_insert_hit
    565      |8,10: #_ //
    566      |1,2: cases pi
    567        [35,36,37: #H @⊥ @H
    568        |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #H @⊥ @H
    569        |1,2,3,6,7,33,34: #x #y #H @⊥ @H
    570        |9,10,14,15: #id #_ cases (lookup ??? old_policy ?) #x cases x #h #n #j
    571          whd in match (snd ???); @(ex_intro ?? pc)
    572          @(ex_intro ?? (\fst (select_reljump_length labels pc id)))
    573          @(ex_intro ?? (max_length j (\snd (select_reljump_length labels pc id))))
    574          normalize nodelta cases (select_reljump_length labels pc id) #z1 #z2 normalize nodelta
     678     |4,6,12: normalize nodelta in Hinstr; lapply (jmeq_to_eq ??? Hinstr)
     679      #H destruct (H)
     680     |7,9: (* instr is a jump *) #_ @(ex_intro ?? pc)
     681       @(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai))
     682       @lookup_opt_insert_hit
     683     |8,10: #_ / by I/
     684     |1,2: cases pi in Hinstr;
     685       [35,36,37: #Hinstr #H @⊥ @H
     686       |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #Hinstr #H @⊥ @H
     687       |1,2,3,6,7,33,34: #x #y #Hinstr #H @⊥ @H
     688       |9,10,14,15: #id #Hinstr #_
     689         @(ex_intro ?? pc) @(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai))
    575690         @lookup_opt_insert_hit
    576        |11,12,13,16,17: #x #id #_ cases (lookup ??? old_policy ?) #x cases x #h #n #j
    577          whd in match (snd ???); @(ex_intro ?? pc)
    578          @(ex_intro ?? (\fst (select_reljump_length labels pc id)))
    579          @(ex_intro ?? (max_length j (\snd (select_reljump_length labels pc id))))
    580          normalize nodelta cases (select_reljump_length labels pc id) #z1 #z2 normalize nodelta
     691       |11,12,13,16,17: #x #id #Hinstr #_
     692         @(ex_intro ?? pc) @(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai))
    581693         @lookup_opt_insert_hit
    582        |72,73,74: #H elim H -H; #h #H elim H -H #n #H elim H -H #j cases (lookup ??? old_policy ?)
    583         #z cases z -z #x #y #z normalize nodelta
    584         >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
    585         [1,3,5: #H destruct (H)]
    586         @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    587         @le_S_S @le_plus_n_r     
    588        |41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69: #x
    589         #H elim H -H; #h #H elim H -H #n #H elim H -H #j cases (lookup ??? old_policy ?)
    590         #z cases z -z #x #y #z normalize nodelta
    591         >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
    592         [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35: #H destruct (H)]
    593         @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    594         @le_S_S @le_plus_n_r
    595        |38,39,40,43,44,70,71: #x #y #H elim H -H; #h #H elim H -H #n #H elim H -H #j
    596         cases (lookup ??? old_policy ?) #z cases z -z #x #y #z normalize nodelta
    597         >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
    598         [1,3,5,7,9,11,13: #H destruct (H)]
    599         @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    600         @le_S_S @le_plus_n_r             
    601        |46,47,51,52: #id #_ //
    602        |48,49,50,53,54: #x #id #_ //
     694       |72,73,74: #Hinstr lapply (jmeq_to_eq ??? Hinstr) #H normalize in H; destruct (H)
     695       |41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69: #x #Hinstr
     696        lapply (jmeq_to_eq ??? Hinstr) #H normalize in H; destruct (H)
     697       |38,39,40,43,44,70,71: #x #y #Hinstr lapply (jmeq_to_eq ??? Hinstr) #H
     698         normalize in H; destruct (H)
     699       |46,47,51,52: #id #Hinstr #_ / by I/
     700       |48,49,50,53,54: #x #id #Hinstr #_ / by I/
    603701       ]
    604702     ]
    605703   ]
    606   ]
    607 | lapply (refl ? add_instr) cases add_instr in ⊢ (???% → %);
    608   [ #Ha #i >append_length >commutative_plus #Hi normalize in Hi;
    609     cases (le_to_or_lt_eq … Hi) -Hi; #Hi
    610     [ cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,0,short_jump〉)
    611       #x #y @((proj2 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
    612     | normalize nodelta >(injective_S … Hi)
    613       >lookup_opt_lookup_miss
    614       [ >lookup_opt_lookup_miss
    615         [ //
    616         | cases (lookup ?? (bitvector_of_nat ? (|prefix|)) old_policy 〈0,0,short_jump〉)
    617           #x #y normalize nodelta
    618           >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
    619           [ //
    620           | @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    621             @le_S_S @le_plus_n_r
    622           ]
     704 ]
     705| (* policy increase *)
     706  #i >append_length >commutative_plus #Hi normalize in Hi;
     707  cases (le_to_or_lt_eq … Hi) -Hi; #Hi
     708  [ >lookup_insert_miss
     709    [ @(proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)) i (le_S_S_to_le … Hi))
     710    | @bitvector_of_nat_abs
     711      [3: @lt_to_not_eq @(le_S_S_to_le … Hi)
     712      |1: @(transitive_lt ??? (le_S_S_to_le … Hi))
     713      ]
     714      @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
     715      @le_S_S @le_plus_n_r
     716    ]
     717  | >(injective_S … Hi) >p3 >lookup_insert_hit normalize nodelta
     718    @pair_elim #x #y #_ @jmpleq_max_length
     719  ]
     720 ]
     721| (* policy_safe *)
     722  @lookup_forall #x cases x -x #x cases x -x #p #a #j #n normalize nodelta #Hl
     723  elim (insert_lookup_opt ?? 〈p,a,j〉 ???? Hl) -Hl #Hl
     724  [ @(forall_lookup … (proj2 ?? (proj1 ?? Hpolicy)) ? n Hl)
     725  | normalize nodelta in p4; cases instr in p4;
     726    [2,3: #x #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
     727    |6: #x #y #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
     728    |1: #pi cases pi normalize nodelta
     729     [35,36,37: #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
     730     |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32:
     731       #x #abs @⊥ normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
     732     |1,2,3,6,7,33,34: #x #y #abs @⊥ normalize in abs; lapply (jmeq_to_eq ??? abs) #H
     733       destruct (H)
     734     |9,10,14,15: #id >p5 whd in match (jump_expansion_step_instruction ???);
     735       whd in match (select_reljump_length ???);
     736       cases (lookup_def ?? labels id 〈0,pc〉) #q1 #q2 normalize nodelta
     737       >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
     738       >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb pc q2))
     739       cases (leb pc q2) in ⊢ (???% → %); #Hle1
     740       [1,3,5,7: lapply (refl ? (leb (q2-pc) 126)) cases (leb (q2-pc) 126) in ⊢ (???% → %);
     741       |2,4,6,8: lapply (refl ? (leb (pc-q2) 129)) cases (leb (pc-q2) 129) in ⊢ (???% → %);
     742       ]
     743       #Hle2 normalize nodelta #Hli
     744       <(pair_eq1 ?????? (Some_eq ??? Hli)) >Hle1
     745       >(pair_eq2 ?????? (proj2 ?? Hl)) <(pair_eq2 ?????? (Some_eq ??? Hli))
     746       cases old_length
     747       [1,7,13,19,25,31,37,43: @(leb_true_to_le … Hle2)
     748       ] normalize @I (* much faster than / by I/, strangely enough *)
     749     |11,12,13,16,17: #x #id >p5 whd in match (jump_expansion_step_instruction ???);
     750       whd in match (select_reljump_length ???);
     751       cases (lookup_def ?? labels id 〈0,pc〉) #q1 #q2 normalize nodelta
     752       >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
     753       >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb pc q2))
     754       cases (leb pc q2) in ⊢ (???% → %); #Hle1
     755       [1,3,5,7,9: lapply (refl ? (leb (q2-pc) 126)) cases (leb (q2-pc) 126) in ⊢ (???% → %);
     756       |2,4,6,8,10: lapply (refl ? (leb (pc-q2) 129)) cases (leb (pc-q2) 129) in ⊢ (???% → %);
     757       ]
     758       #Hle2 normalize nodelta #Hli
     759       <(pair_eq1 ?????? (Some_eq ??? Hli)) >Hle1 >(pair_eq2 ?????? (proj2 ?? Hl))
     760       <(pair_eq2 ?????? (Some_eq ??? Hli))
     761       cases old_length
     762       [1,7,13,19,25,31,37,43,49,55: @(leb_true_to_le … Hle2)
     763       ] normalize @I (* vide supra *)
     764     ]
     765    |4,5: #id >p5 normalize nodelta whd in match (select_jump_length ???);
     766      whd in match (select_call_length ???); cases (lookup_def ?? labels id 〈0,pc〉)
     767      #q1 #q2 normalize nodelta
     768      >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
     769      >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
     770      [1: lapply (refl ? (leb pc q2)) cases (leb pc q2) in ⊢ (???% → %); #Hle1
     771        [ lapply (refl ? (leb (q2-pc) 126)) cases (leb (q2-pc) 126) in ⊢ (???% → %);
     772        | lapply (refl ? (leb (pc-q2) 129)) cases (leb (pc-q2) 129) in ⊢ (???% → %);
    623773        ]
    624       | >(proj1 ?? (jump_not_in_policy (pi1 … program) old_policy (|prefix|) ?))
    625         [ //
    626         | >prf >p1 >nth_append_second [ <minus_n_n
    627         generalize in match Ha; normalize nodelta cases instr normalize nodelta
    628         [1: #pi cases pi
    629          [1,2,3,6,7,33,34: #x #y #H normalize /2 by nmk/
    630          |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #H normalize /2 by nmk/
    631          |35,36,37: #H normalize /2 by nmk/
    632          |9,10,14,15: #id whd in match (jump_expansion_step_instruction ???);
    633            #H destruct (H)
    634          |11,12,13,16,17: #x #id whd in match (jump_expansion_step_instruction ???);
    635            #H destruct (H)
    636          ]
    637         |2,3: #x #H normalize /2 by nmk/
    638         |6: #x #y #H normalize /2 by nmk/
    639         |4,5: #id #H destruct (H)
    640         ] | @le_n ]
    641         | >prf >append_length normalize <plus_n_Sm @le_plus_n_r
    642         ]
    643       ]
    644     ]
    645   | #x cases x -x #x1 #x2 #Ha #i >append_length >commutative_plus #Hi normalize in Hi;
    646     cases (le_to_or_lt_eq … Hi) -Hi; #Hi
    647     [ cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,0,short_jump〉)
    648       #y cases y -y #y1 #y2 #z whd in match (snd ???); normalize nodelta >lookup_insert_miss
    649       [ @((proj2 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
    650       | @bitvector_of_nat_abs
     774       #Hle2 normalize nodelta
     775      ]
     776      [2,4,5: lapply (refl ? (split ? 5 11 (bitvector_of_nat ? q2)))
     777        cases (split ??? (bitvector_of_nat ? q2)) in ⊢ (???% → %); #x1 #x2 #Hle3
     778        lapply (refl ? (split ? 5 11 (bitvector_of_nat ? pc)))
     779        cases (split ??? (bitvector_of_nat ? pc)) in ⊢ (???% → %); #y1 #y2 #Hle4
     780        normalize nodelta lapply (refl ? (eq_bv 5 x1 y1))
     781        cases (eq_bv 5 x1 y1) in ⊢ (???% → %); #Hle5
     782      ]
     783      #Hli <(pair_eq1 ?????? (Some_eq ??? Hli)) >(pair_eq2 ?????? (proj2 ?? Hl))
     784      <(pair_eq2 ?????? (Some_eq ??? Hli))
     785      cases old_length
     786      [2,8,14: >Hle3 @Hle5
     787      |19,22: >Hle1 @(leb_true_to_le … Hle2)
     788      ] normalize @I (* here too *)
     789    ]
     790  ]
     791 ]
     792| (* changed *)
     793  cases (dec_eq_jump_length (max_length old_length ai) old_length) normalize nodelta
     794  [ #Hml #Hc #i #Hi cases (le_to_or_lt_eq … Hi) -Hi >append_length >commutative_plus #Hi
     795    normalize in Hi;
     796    [ >lookup_insert_miss
     797      [ @((proj2 ?? Hpolicy) Hc i (le_S_S_to_le … Hi))
     798      | @bitvector_of_nat_abs
    651799        [3: @lt_to_not_eq @(le_S_S_to_le … Hi)
    652800        |1: @(transitive_lt ??? (le_S_S_to_le … Hi))
     
    655803        @le_S_S @le_plus_n_r
    656804      ]
    657     | >(injective_S … Hi) elim (proj1 ?? (proj2 ?? (pi2 ?? old_policy) (|prefix|) ?) ?)
    658       [ #a #H elim H -H; #b #H elim H -H #c #H >H >(lookup_opt_lookup_hit … 〈a,b,c〉 H)
    659         normalize nodelta >lookup_insert_hit @jmpleq_max_length
    660       | >prf >p1 >nth_append_second
    661         [ <minus_n_n generalize in match Ha; normalize nodelta cases instr normalize nodelta
    662           [1: #pi cases pi
    663            [1,2,3,6,7,33,34: #x #y #H normalize in H; destruct (H)
    664            |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #H normalize in H; destruct (H)
    665            |35,36,37: #H normalize in H; destruct (H)
    666            |9,10,14,15: #id #H //
    667            |11,12,13,16,17: #x #id #H //
    668            ]
    669           |2,3: #x #H normalize in H; destruct (H)
    670           |6: #x #y #H normalize in H; destruct (H)
    671           |4,5: #id #H //
     805    | >(injective_S … Hi) >p3 >lookup_insert_hit normalize nodelta
     806      @pair_elim #x #y #_ @(sym_eq ??? Hml)
     807    ]
     808  | #_ #H destruct (H)
     809  ]
     810 ]
     811| (* Case where add_instr = None *) normalize nodelta lapply (pi2 ?? acc) >p >p1
     812  normalize nodelta #Hpolicy
     813  @conj [ @conj [ @conj [ @conj [ @conj
     814[ (* out_of_program_none *) #i >append_length >commutative_plus #Hi normalize in Hi;
     815  #Hi2 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_to_le ?? Hi) Hi2)
     816| (* labels_okay *) @lookup_forall #x cases x -x #x cases x #p #a #j #lbl #Hl normalize nodelta
     817  elim (forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) ? lbl Hl)
     818  #id #Hid @(ex_intro … id Hid)
     819 ]
     820| (* jump_in_policy *) #i >append_length >commutative_plus #Hi normalize in Hi;
     821  elim (le_to_or_lt_eq … Hi) -Hi #Hi
     822  [ >(nth_append_first ?? prefix ?? (le_S_S_to_le ?? Hi))
     823    @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i (le_S_S_to_le ?? Hi))
     824  | >(injective_S … Hi) @conj
     825    [ >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n whd in match (nth ????);
     826      normalize nodelta in p4; cases instr in p4;
     827      [ #pi cases pi
     828        [1,2,3,6,7,33,34: #x #y #_ #H @⊥ @H
     829        |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #_ #H @⊥ @H
     830        |9,10,14,15: #id (* normalize segfaults here *) normalize nodelta
     831          whd in match (jump_expansion_step_instruction ???);
     832          #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
     833        |11,12,13,16,17: #x #id normalize nodelta
     834          whd in match (jump_expansion_step_instruction ???);
     835          #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
     836        |35,36,37: #_ #H @⊥ @H
     837        ]
     838      |2,3: #x #_ #H @⊥ @H
     839      |4,5: #id normalize nodelta #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
     840      |6: #x #id #_ #H @⊥ @H
     841      ]
     842    | #H elim H -H #p #H elim H -H #a #H elim H -H #j #H
     843      >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) (|prefix|) (le_n (|prefix|)) ?) in H;
     844      [ #H destruct (H)
     845      | @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
     846        @le_S_S @le_plus_n_r
     847      ]
     848    ]
     849  ]
     850 ]
     851| (* policy_increase *) #i >append_length >commutative_plus #Hi normalize in Hi;
     852  elim (le_to_or_lt_eq … Hi) -Hi #Hi
     853  [ @(proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)) i (le_S_S_to_le … Hi))
     854  | >(injective_S … Hi) >lookup_opt_lookup_miss
     855    [ >lookup_opt_lookup_miss
     856      [ normalize nodelta %2 @refl
     857      | @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) (|prefix|) (le_n (|prefix|)) ?)
     858        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
     859        @le_S_S @le_plus_n_r
     860      ]
     861    | @(proj1 ?? (jump_not_in_policy (pi1 … program) old_policy (|prefix|) ?)) >prf
     862      [ >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r
     863      | >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n >p2
     864        whd in match (nth ????); normalize nodelta in p4; cases instr in p4;
     865        [ #pi cases pi
     866          [1,2,3,6,7,33,34: #x #y #_ normalize /2 by nmk/
     867          |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #_ normalize /2 by nmk/
     868          |9,10,14,15: #id (* normalize segfaults here *) normalize nodelta
     869            whd in match (jump_expansion_step_instruction ???);
     870            #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
     871          |11,12,13,16,17: #x #id normalize nodelta
     872            whd in match (jump_expansion_step_instruction ???);
     873            #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
     874          |35,36,37: #_ normalize /2 by nmk/
    672875          ]
    673         | @le_n ]
    674       | >prf >append_length normalize <plus_n_Sm @le_plus_n_r
    675       ]
    676     ]
    677   ] ]
    678 | @conj [ @conj
     876        |2,3: #x #_ normalize /2 by nmk/
     877        |4,5: #id normalize nodelta #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
     878        |6: #x #id #_ normalize /2 by nmk/
     879        ]
     880      ]
     881    ]
     882  ]
     883 ]
     884| (* policy_safe *) @lookup_forall #x cases x -x #x cases x -x #p #a #j #n #Hl
     885  @(forall_lookup … (proj2 ?? (proj1 ?? Hpolicy)) ? n Hl)
     886 ]
     887| (* changed *) #Hc #i >append_length >commutative_plus #Hi normalize in Hi;
     888  elim (le_to_or_lt_eq … Hi) -Hi #Hi
     889  [ @((proj2 ?? Hpolicy) Hc i (le_S_S_to_le … Hi))
     890  | >(injective_S … Hi) >lookup_opt_lookup_miss
     891    [ >lookup_opt_lookup_miss
     892      [ normalize nodelta @refl
     893      | @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) (|prefix|) (le_n (|prefix|)) ?)
     894        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
     895        @le_S_S @le_plus_n_r
     896      ]
     897    | @(proj1 ?? (jump_not_in_policy (pi1 … program) old_policy (|prefix|) ?)) >prf
     898      [ >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r
     899      | >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n >p2
     900        whd in match (nth ????); normalize nodelta in p4; cases instr in p4;
     901        [ #pi cases pi
     902          [1,2,3,6,7,33,34: #x #y #_ normalize /2 by nmk/
     903          |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #_ normalize /2 by nmk/
     904          |9,10,14,15: #id (* normalize segfaults here *) normalize nodelta
     905            whd in match (jump_expansion_step_instruction ???);
     906            #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
     907          |11,12,13,16,17: #x #id normalize nodelta
     908            whd in match (jump_expansion_step_instruction ???);
     909            #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
     910          |35,36,37: #_ normalize /2 by nmk/
     911          ]
     912        |2,3: #x #_ normalize /2 by nmk/
     913        |4,5: #id normalize nodelta #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
     914        |6: #x #id #_ normalize /2 by nmk/
     915        ]
     916      ]
     917    ]
     918  ]
     919 ]       
     920| @conj [ @conj [ @conj [ @conj [ @conj
    679921  [ #i #Hi //
     922  | //
     923  ]
    680924  | #i #Hi @conj [ >nth_nil #H @⊥ @H | #H elim H #x #H1 elim H1 #y #H2 elim H2 #z #H3
    681925                   normalize in H3; destruct (H3) ]
    682926  ]                 
    683927  | #i #Hi @⊥ @(absurd (i<0)) [ @Hi | @(not_le_Sn_O) ]
     928  ]
     929  | //
     930  ]
     931  | #_ #i #Hi @⊥ @(absurd (i < 0)) [ @Hi | @not_le_Sn_O ]
     932  ]
     933qed.
     934
     935(* this might be replaced by a coercion: (∀x.A x → B x) → Σx.A x → Σx.B x *)
     936(* definition weaken_policy:
     937  ∀program,op.
     938  option (Σp:jump_expansion_policy.
     939    And (And (And (And (out_of_program_none program p)
     940    (labels_okay (create_label_map program op) p))
     941    (jump_in_policy program p)) (policy_increase program op p))
     942    (policy_safe p)) →
     943  option (Σp:jump_expansion_policy.And (out_of_program_none program p)
     944    (jump_in_policy program p)) ≝
     945 λprogram.λop.λx.
     946 match x return λ_.option (Σp.And (out_of_program_none program p) (jump_in_policy program p)) with
     947 [ None ⇒ None ?
     948 | Some z ⇒ Some ? (mk_Sig ?? (pi1 ?? z) ?)
     949 ].
     950@conj
     951[ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? z)))))
     952| @(proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? z))))
    684953]
     954qed. *)
     955
     956(* This function executes n steps from the starting point. *)
     957let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (|l|) 2^16)
     958  (n: ℕ) on n:(Σx:ℕ × (option jump_expansion_policy).
     959    let 〈pc,y〉 ≝ x in
     960    match y with
     961    [ None ⇒ pc > 2^16
     962    | Some p ⇒ And (out_of_program_none program p) (jump_in_policy program p)
     963    ]) ≝
     964  match n with
     965  [ O   ⇒ 〈0,Some ? (pi1 … (jump_expansion_start program))〉
     966  | S m ⇒ let 〈ch,pc,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in
     967          match z return λx. z=x → Σa:ℕ × (option jump_expansion_policy).? with
     968          [ None    ⇒ λp2.〈pc,None ?〉
     969          | Some op ⇒ λp2.pi1 … (jump_expansion_step program (create_label_map program op) «op,?»)
     970          ] (refl … z)
     971  ].
     972[ normalize nodelta @(proj1 ?? (pi2 ?? (jump_expansion_start program)))
     973| normalize nodelta lapply (pi2 ?? (jump_expansion_internal program m))
     974    <p1 >p2 / by /
     975|4: cases (jump_expansion_step program (create_label_map program op) «op,?»)
     976    #p cases p #q #r cases r normalize nodelta
     977    [ / by /
     978    | #j #H @conj
     979      [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
     980      | @(proj2 ?? (proj1 ?? (proj1 ?? H)))
     981      ]
     982    ]
     983| lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 / by /
     984]
    685985qed.
    686986 
    687 let rec jump_expansion_internal (program: Σl:list labelled_instruction.|l| < 2^16)
    688   (n: ℕ) on n: (Σpolicy:jump_expansion_policy.
    689     And
    690     (∀i:ℕ.i ≥ |program| → i < 2^16 → lookup_opt ? 16 (bitvector_of_nat ? i) policy = None ?)
    691     (jump_in_policy program policy)) ≝
    692   match n with
    693   [ O   ⇒ jump_expansion_start program
    694   | S m ⇒ let old_policy ≝ jump_expansion_internal program m in
    695     jump_expansion_step program (create_label_map program old_policy) old_policy
     987lemma pe_int_refl: ∀program.reflexive ? (policy_equal_int program).
     988#program whd #x whd #n #Hn
     989cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉)
     990#y cases y -y #y #z normalize nodelta @refl
     991qed.
     992
     993lemma pe_int_sym: ∀program.symmetric ? (policy_equal_int program).
     994#program whd #x #y #Hxy whd #n #Hn
     995lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉)
     996#z cases z -z #x1 #x2 #x3
     997cases (bvt_lookup … (bitvector_of_nat ? n) y 〈0,0,short_jump〉)
     998#z cases z -z #y1 #y2 #y3 normalize nodelta //
     999qed.
     1000 
     1001lemma pe_int_trans: ∀program.transitive ? (policy_equal_int program).
     1002#program whd #x #y #z whd in match (policy_equal_int ???); whd in match (policy_equal_int ?y ?);
     1003whd in match (policy_equal_int ? x z); #Hxy #Hyz #n #Hn lapply (Hxy n Hn) -Hxy
     1004lapply (Hyz n Hn) -Hyz cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉)
     1005#z cases z -z #x1 #x2 #x3
     1006cases (bvt_lookup … (bitvector_of_nat ? n) y 〈0,0,short_jump〉) #z cases z -z 
     1007#y1 #y2 #y3
     1008cases (bvt_lookup … (bitvector_of_nat ? n) z 〈0,0,short_jump〉) #z cases z -z 
     1009#z1 #z2 #z3 normalize nodelta //
     1010qed.
     1011
     1012definition policy_equal ≝
     1013  λprogram:list labelled_instruction.λp1,p2:option jump_expansion_policy.
     1014  match p1 with
     1015  [ Some x1 ⇒ match p2 with
     1016              [ Some x2 ⇒ policy_equal_int program x1 x2
     1017              | _       ⇒ False
     1018              ]
     1019  | None    ⇒ p2 = None ?
    6961020  ].
    697 [ @(proj1 ?? (pi2 ?? (jump_expansion_start program)))
    698 | @(proj1 ?? (pi2 ?? (jump_expansion_step program (create_label_map program old_policy) old_policy)))
     1021
     1022lemma pe_refl: ∀program.reflexive ? (policy_equal program).
     1023#program whd #x whd cases x
     1024[ //
     1025| #y @pe_int_refl
    6991026]
    7001027qed.
    7011028
    702 definition policy_equal ≝
    703   λprogram:list labelled_instruction.λp1,p2:jump_expansion_policy.
    704   ∀n:ℕ.n < |program| →
    705     let 〈i1,i2,j1〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) p1 〈0,0,short_jump〉 in
    706     let 〈i3,i4,j2〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) p2 〈0,0,short_jump〉 in
    707     j1 = j2.
    708 
    709 lemma pe_refl:
    710   ∀program.reflexive ? (policy_equal program).
    711  #program whd #x whd #n #Hn cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉)
    712  #y cases y -y #y #z normalize nodelta @refl
    713 qed.
    714 
    715 lemma pe_sym:
    716   ∀program.symmetric ? (policy_equal program).
    717  #program whd #x #y #Hxy whd #n #Hn
    718  lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉)
    719  #z cases z -z #x1 #x2 #x3 cases (bvt_lookup … (bitvector_of_nat ? n) y 〈0,0,short_jump〉)
    720  #z cases z -z #y1 #y2 #y3 normalize nodelta //
    721 qed.
    722 
    723 lemma pe_trans:
    724   ∀program.transitive ? (policy_equal program).
    725  #program whd #x #y #z whd in match (policy_equal ???); whd in match (policy_equal ?y ?);
    726  whd in match (policy_equal ? x z); #Hxy #Hyz #n #Hn
    727  lapply (Hxy n Hn) -Hxy lapply (Hyz n Hn) -Hyz
    728  cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉) #z cases z -z #x1 #x2 #x3
    729  cases (bvt_lookup … (bitvector_of_nat ? n) y 〈0,0,short_jump〉) #z cases z -z #y1 #y2 #y3
    730  cases (bvt_lookup … (bitvector_of_nat ? n) z 〈0,0,short_jump〉) #z cases z -z #z1 #z2 #z3
    731  normalize nodelta //
     1029lemma pe_sym: ∀program.symmetric ? (policy_equal program).
     1030#program whd #x #y #Hxy whd cases y in Hxy;
     1031[ cases x
     1032  [ //
     1033  | #x' #H @⊥ @(absurd ? H) /2 by nmk/
     1034  ]
     1035| #y' cases x
     1036  [ #H @⊥ @(absurd ? H) whd in match (policy_equal ???); @nmk #H destruct (H)
     1037  | #x' #H @pe_int_sym @H
     1038  ]
     1039]
     1040qed.
     1041
     1042lemma pe_trans: ∀program.transitive ? (policy_equal program).
     1043#program whd #x #y #z cases x
     1044[ #Hxy #Hyz >Hxy in Hyz; //
     1045| #x' cases y
     1046  [ #H @⊥ @(absurd ? H) /2 by nmk/
     1047  | #y' cases z
     1048    [ #_ #H @⊥ @(absurd ? H) /2 by nmk/
     1049    | #z' @pe_int_trans
     1050    ]
     1051  ]
     1052]
     1053qed.
     1054
     1055definition step_none: ∀program.∀n.
     1056  (\snd (pi1 ?? (jump_expansion_internal program n))) = None ? →
     1057  ∀k.(\snd (pi1 ?? (jump_expansion_internal program (n+k)))) = None ?.
     1058#program #n lapply (refl ? (jump_expansion_internal program n))
     1059 cases (jump_expansion_internal program n) in ⊢ (???% → %);
     1060 #x1 cases x1 #p1 #j1 -x1; #H1 #Heqj #Hj #k elim k
     1061[ <plus_n_O >Heqj @Hj
     1062| #k' -k <plus_n_Sm lapply (refl ? (jump_expansion_internal program (n+k')))
     1063  cases (jump_expansion_internal program (n+k')) in ⊢ (???% → % → %);
     1064  #x2 cases x2 #p2 #j2 -x2; normalize nodelta #H #Heqj2
     1065  cases j2 in H Heqj2;
     1066  [ #H #Heqj2 #_ whd in match (jump_expansion_internal ??);
     1067    >Heqj2 normalize nodelta @refl
     1068  | #x #H #Heqj2 #abs destruct (abs)
     1069  ]
     1070]
    7321071qed.
    7331072
    7341073lemma pe_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
    735  ∀p1,p2:Σpolicy.
    736  (∀i:ℕ.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) policy = None ?)
    737  ∧jump_in_policy program policy.
    738   policy_equal program p1 p2 →
    739   policy_equal program (jump_expansion_step program (create_label_map program p1) p1)
    740     (jump_expansion_step program (create_label_map program p2) p2).
    741  #program #p1 #p2 #Heq whd #n #Hn lapply (Heq n Hn) #H
    742  lapply (refl ? (lookup_opt … (bitvector_of_nat ? n) p1))
    743  cases (lookup_opt … (bitvector_of_nat ? n) p1) in ⊢ (???% → ?);
    744  [ #Hl lapply ((proj2 ?? (jump_not_in_policy program p1 n Hn)) Hl)
    745    #Hnotjmp >lookup_opt_lookup_miss
    746    [ >lookup_opt_lookup_miss
    747      [ @refl
    748      | @(proj1 ?? (jump_not_in_policy program (pi1 … (jump_expansion_step program (create_label_map program p2) p2)) n Hn))
    749        [ @(proj1 ?? (pi2 … (jump_expansion_step program (create_label_map program p2) p2)))
    750        | @Hnotjmp
    751        ]
    752      ]
    753    | @(proj1 ?? (jump_not_in_policy program (pi1 … (jump_expansion_step program (create_label_map program p1) p1)) n Hn))
    754      [ @(proj1 ?? (pi2 ?? (jump_expansion_step program (create_label_map program p1) p1)))
    755      | @Hnotjmp
    756      ]
    757    ]
    758  | #x #Hl cases daemon (* XXX *)
    759  ]
     1074  ∀n.policy_equal program (\snd (pi1 ?? (jump_expansion_internal program n)))
     1075   (\snd (pi1 ?? (jump_expansion_internal program (S n)))) →
     1076  policy_equal program (\snd (pi1 ?? (jump_expansion_internal program (S n))))
     1077    (\snd (pi1 ?? (jump_expansion_internal program (S (S n))))).
     1078#program #n #Heq
     1079cases daemon (* XXX *)
    7601080qed.
    7611081
     
    7631083theorem plus_Sn_m1: ∀n,m:nat. S m + n = m + S n.
    7641084  #n (elim n) normalize /2 by S_pred/ qed.
    765 
     1085 
    7661086lemma equal_remains_equal: ∀program:(Σl:list labelled_instruction.|l| < 2^16).∀n:ℕ.
    767   policy_equal program (jump_expansion_internal program n) (jump_expansion_internal program (S n)) →
    768   ∀k.k ≥ n → policy_equal program (jump_expansion_internal program n) (jump_expansion_internal program k).
    769  #program #n #Heq #k #Hk elim (le_plus_k … Hk); #z #H >H -H -Hk -k;
    770  lapply Heq -Heq; lapply n -n; elim z -z;
    771  [ #n #Heq <plus_n_O @pe_refl 
    772  | #z #Hind #n #Heq <plus_Sn_m1 whd in match (plus (S n) z); @(pe_trans … (jump_expansion_internal program (S n)))
    773    [ @Heq
    774    | @pe_step @Hind @Heq
    775    ]
    776  ]
    777 qed.
    778 
    779 lemma thingie:
    780   ∀A:Prop.(A + ¬A) → (¬¬A) → A.
    781  #A #Adec #nnA cases Adec
    782  [ //
    783  | #H @⊥ @(absurd (¬A) H nnA)
    784  ]
    785 qed.
    786  
    787 lemma policy_not_equal_incr: ∀program:(Σl:list labelled_instruction.|l|<2^16).
    788  ∀policy:(Σp:jump_expansion_policy.
    789     (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
    790     jump_in_policy program p).
    791   ¬policy_equal program policy (jump_expansion_step program (create_label_map program policy) policy) →
    792   ∃n:ℕ.n < (|program|) ∧ jmple
    793     (\snd (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,0,short_jump〉))
    794     (\snd (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉)).
    795  #program #policy #Hp
    796  cases (dec_bounded_exists (λn.jmple
    797    (\snd (bvt_lookup ?? (bitvector_of_nat ? n) policy 〈0,0,short_jump〉))
    798    (\snd (bvt_lookup ?? (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉))) ? (|program|))
    799  [ #H elim H; -H #i #Hi @(ex_intro ?? i) @Hi
    800  | #abs @⊥ @(absurd ?? Hp) #n #Hn
    801    lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) n Hn)
    802    lapply (refl ? (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,0,short_jump〉))
    803    cases (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,0,short_jump〉) in ⊢ (???% → %);
    804    #z cases z -z #x1 #x2 #x3 #Hx
    805    lapply (refl ? (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉))
    806    cases (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉) in ⊢ (???% → %);
    807    #z cases z -z #y1 #y2 #y3 #Hy
    808    normalize nodelta #Hj cases Hj
    809    [ #Hj @⊥ @(absurd ?? abs) @(ex_intro ?? n) @conj [ @Hn | >Hx >Hy @Hj ]
    810    | //
    811    ]
    812  | #n @dec_jmple
    813  ]
    814 qed.
    815 
    816 lemma stupid:
    817   ∀program,n.
    818   pi1 … (jump_expansion_step program (create_label_map program (jump_expansion_internal program n)) (jump_expansion_internal program n)) =
    819   pi1 … (jump_expansion_internal program (S n)).
    820  //
    821 qed.
    822 
     1087  policy_equal program (\snd (pi1 … (jump_expansion_internal program n)))
     1088   (\snd (pi1 … (jump_expansion_internal program (S n)))) →
     1089  ∀k.k ≥ n → policy_equal program (\snd (pi1 … (jump_expansion_internal program n)))
     1090   (\snd (pi1 … (jump_expansion_internal program k))).
     1091#program #n #Heq #k #Hk elim (le_plus_k … Hk); #z #H >H -H -Hk -k;
     1092lapply Heq -Heq; lapply n -n; elim z -z;
     1093[ #n #Heq <plus_n_O @pe_refl
     1094| #z #Hind #n #Heq <plus_Sn_m1 whd in match (plus (S n) z);
     1095  @(pe_trans … (\snd (pi1 … (jump_expansion_internal program (S n)))))
     1096  [ @Heq
     1097  | @Hind @pe_step @Heq
     1098  ]
     1099]
     1100qed.
     1101
     1102(* this number monotonically increases over iterations, maximum 2*|program| *)
    8231103let rec measure_int (program: list labelled_instruction) (policy: jump_expansion_policy) (acc: ℕ)
    8241104 on program: ℕ ≝
    8251105 match program with
    8261106 [ nil      ⇒ acc
    827  | cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) with
     1107 | cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,00
     1108,short_jump〉)) with
    8281109   [ long_jump   ⇒ measure_int t policy (acc + 2)
    8291110   | medium_jump ⇒ measure_int t policy (acc + 1)
     
    8321113 ].
    8331114
    834 (* definition measure ≝
    835   λprogram.λpolicy.measure_int program policy 0. *)
    836  
    8371115lemma measure_plus: ∀program.∀policy.∀x,d:ℕ.
    838   measure_int program policy (x+d) = measure_int program policy x + d.
    839  #program #policy #x #d generalize in match x; -x elim d
    840  [ //
    841  | -d; #d #Hind elim program
    842    [ //
    843    | #h #t #Hd #x whd in match (measure_int ???); whd in match (measure_int ?? x);
    844      cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉))
    845      [ normalize nodelta @Hd
    846      |2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus
    847        @Hd
    848      ]
    849    ]
    850  ]
    851 qed.
    852    
     1116 measure_int program policy (x+d) = measure_int program policy x + d.
     1117#program #policy #x #d generalize in match x; -x elim d
     1118[ //
     1119| -d; #d #Hind elim program
     1120  [ / by refl/
     1121  | #h #t #Hd #x whd in match (measure_int ???); whd in match (measure_int ?? x);
     1122    cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉))
     1123    [ normalize nodelta @Hd
     1124    |2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus
     1125      @Hd
     1126    ]
     1127  ]
     1128]
     1129qed.
     1130
     1131lemma measure_le: ∀program.∀policy.
     1132  measure_int program policy 0 ≤ 2*|program|.
     1133#program #policy elim program
     1134[ normalize @le_n
     1135| #h #t #Hind whd in match (measure_int ???);
     1136  cases (\snd (lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉))
     1137  [ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/
     1138  |2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?)
     1139    @le_plus [1,3: @Hind |2,4: // ]
     1140  ]
     1141]
     1142qed.
     1143
    8531144lemma measure_incr_or_equal: ∀program:Σl:list labelled_instruction.|l|<2^16.
    8541145  ∀policy:Σp:jump_expansion_policy.
    855     (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
    856     jump_in_policy program p.∀l.|l| ≤ |program| → ∀acc:ℕ.
    857   measure_int l policy acc ≤ measure_int l (jump_expansion_step program (create_label_map program policy) policy) acc.
     1146    out_of_program_none program p ∧ jump_in_policy program p.
     1147  ∀l.|l| ≤ |program| → ∀acc:ℕ.
     1148  match \snd (jump_expansion_step program (create_label_map program policy) policy) with
     1149  [ None   ⇒ True
     1150  | Some p ⇒ measure_int l policy acc ≤ measure_int l p acc
     1151  ].
    8581152#program #policy #l elim l -l;
    859   [ #Hp #acc normalize @le_n
    860   | #h #t #Hind #Hp #acc
    861     lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) (|t|) Hp)
    862     whd in match (measure_int ???); whd in match (measure_int ?(jump_expansion_step ???)?);
    863     cases (bvt_lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉) #z cases z -z #x1 #x2 #x3
    864     cases (bvt_lookup … (bitvector_of_nat ? (|t|)) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉) #z cases z -z #y1 #y2 #y3
     1153[ #Hp #acc cases (jump_expansion_step ???) #pi1 cases pi1 #p #q -pi1; cases q [ // | #x #_ @le_n ]
     1154| #h #t #Hind #Hp #acc
     1155  lapply (refl ? (jump_expansion_step program (create_label_map program policy) policy))
     1156  cases (jump_expansion_step ???) in ⊢ (???% → %); #pi1 cases pi1 #p #q -pi1; cases q
     1157  [ //
     1158  | #x #Hx #Hjeq normalize nodelta lapply (proj2 ?? (proj1 ?? Hx) (|t|) Hp)
     1159    whd in match (measure_int ???); whd in match (measure_int ? x ?);
     1160    cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)
     1161    #z cases z -z #x1 #x2 #x3
     1162    cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) x 〈0,0,short_jump〉)
     1163    #z cases z -z #y1 #y2 #y3
    8651164    normalize nodelta #Hj cases Hj
    8661165    [ cases x3 cases y3
    8671166      [1,4,5,7,8,9: #H @⊥ @H
    8681167      |2,3,6: #_ normalize nodelta
    869         [1,2: @(transitive_le ? (measure_int t (jump_expansion_step program (create_label_map program policy) policy) acc))
    870         |3: @(transitive_le ? (measure_int t (jump_expansion_step program (create_label_map program policy) policy) (acc+1)))
     1168        [1,2: @(transitive_le ? (measure_int t x acc))
     1169        |3: @(transitive_le ? (measure_int t x (acc+1)))
    8711170        ]
    872         [1,3,5: @Hind @(transitive_le … Hp) @le_n_Sn
    873         |2,4,6: >measure_plus [1,2: @le_plus_n_r] >measure_plus @le_plus [ @le_n | //]
    874         ]
    875       ]
    876     | #Heq >Heq cases y3 normalize nodelta @Hind @(transitive_le … Hp) @le_n_Sn
    877     ]
    878   ]
    879 qed.
    880 
    881 lemma measure_le: ∀program.∀policy.
    882   measure_int program policy 0 ≤ 2*|program|.
    883  #program #policy elim program
    884  [ normalize @le_n
    885  | #h #t #Hind whd in match (measure_int ???);
    886    cases (\snd (lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉))
    887    [ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/
    888    |2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?)
    889      @le_plus [1,3: @Hind |2,4: // ]
    890    ]
    891  ]
     1171        [2,4,5,6: >measure_plus [1,2: @le_plus_n_r] >measure_plus @le_plus //]
     1172        >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn
     1173        ]
     1174    | #Heq >Heq cases y3 normalize nodelta
     1175      [2,3: >measure_plus >measure_plus @le_plus //]
     1176      >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn
     1177    ]
     1178  ]
     1179]
    8921180qed.
    8931181
     
    8951183lemma bla: ∀a,b:ℕ.a + a = b + b → a = b.
    8961184 #a elim a
    897  [ normalize #b // 
     1185 [ normalize #b //
    8981186 | -a #a #Hind #b cases b [ /2 by le_n_O_to_eq/ | -b #b normalize
    8991187   <plus_n_Sm <plus_n_Sm #H
     
    9061194 [ // | #y // ]
    9071195qed.
    908 
     1196 
    9091197lemma measure_full: ∀program.∀policy.
    9101198  measure_int program policy 0 = 2*|program| → ∀i.i<|program| →
    9111199  (\snd (bvt_lookup ?? (bitvector_of_nat ? i) policy 〈0,0,short_jump〉)) = long_jump.
    912  #program #policy elim program
    913  [ #Hm #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    914  | #h #t #Hind #Hm #i #Hi cut (measure_int t policy 0 = 2*|t|)
    915    [ whd in match (measure_int ???) in Hm;
    916      cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) in Hm;
    917      normalize nodelta
    918      [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/
    919      | >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy))
    920        <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize
    921        >(commutative_plus (|t|) 0) <plus_O_n <minus_n_O
    922        >plus_n_Sm @le_n
    923      | >measure_plus <times_n_Sm >commutative_plus #H lapply (injective_plus_r … H) //
    924      ]
    925    | #Hmt cases (le_to_or_lt_eq … Hi) -Hi;
    926    [ #Hi @(Hind Hmt i (le_S_S_to_le … Hi))
    927    | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm;
    928      cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) in Hm;
    929      normalize nodelta
    930      [ >Hmt normalize <plus_n_O >(commutative_plus (|t|) (S (|t|)))
    931        >plus_n_Sm #H @⊥ @(absurd ? (bla ?? H)) @sth_not_s
    932      | >measure_plus >Hmt normalize <plus_n_O >commutative_plus normalize
    933        #H @⊥ @(absurd ? (injective_plus_r … (injective_S ?? H))) @sth_not_s
    934      | #_ //
    935      ]
    936    ]]
    937  ]
     1200#program #policy elim program
     1201[ #Hm #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
     1202| #h #t #Hind #Hm #i #Hi cut (measure_int t policy 0 = 2*|t|)
     1203  [ whd in match (measure_int ???) in Hm;
     1204    cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) in Hm;
     1205    normalize nodelta
     1206    [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/
     1207    | >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy))
     1208      <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize
     1209      >(commutative_plus (|t|) 0) <plus_O_n <minus_n_O
     1210      >plus_n_Sm @le_n
     1211    | >measure_plus <times_n_Sm >commutative_plus #H lapply (injective_plus_r … H) //
     1212    ]
     1213  | #Hmt cases (le_to_or_lt_eq … Hi) -Hi;
     1214  [ #Hi @(Hind Hmt i (le_S_S_to_le … Hi))
     1215  | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm;
     1216    cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) in Hm;
     1217    normalize nodelta
     1218    [ >Hmt normalize <plus_n_O >(commutative_plus (|t|) (S (|t|)))
     1219      >plus_n_Sm #H @⊥ @(absurd ? (bla ?? H)) @sth_not_s
     1220    | >measure_plus >Hmt normalize <plus_n_O >commutative_plus normalize
     1221      #H @⊥ @(absurd ? (injective_plus_r … (injective_S ?? H))) @sth_not_s
     1222    | #_ //
     1223    ]
     1224  ]]
     1225]
    9381226qed.
    9391227
    9401228lemma measure_special: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
    9411229  ∀policy:Σp:jump_expansion_policy.
    942     (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
    943     jump_in_policy program p.
    944   measure_int program policy 0 = measure_int program (jump_expansion_step program (create_label_map program policy) policy) 0 →
    945   policy_equal program policy (jump_expansion_step program (create_label_map program policy) policy).
    946 #program #policy lapply (le_n (|program|)) @(list_ind ?
    947   (λx.|x| ≤ |program| → measure_int x (pi1 … policy) 0 = measure_int x (pi1 … (jump_expansion_step program (create_label_map program policy) policy)) 0 →
    948       policy_equal x (pi1 … policy) (pi1 … (jump_expansion_step program (create_label_map program policy) policy)))
    949    ?? program)
    950  [ #Hp #Hm #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O
     1230    out_of_program_none program p ∧ jump_in_policy program p.
     1231  match (\snd (pi1 ?? (jump_expansion_step program (create_label_map program policy) policy))) with
     1232  [ None ⇒ True
     1233  | Some p ⇒ measure_int program policy 0 = measure_int program p 0 → policy_equal_int program policy p ].
     1234#program #policy lapply (refl ? (pi1 ?? (jump_expansion_step program (create_label_map program policy) policy)))
     1235cases (jump_expansion_step program (create_label_map program policy) policy) in ⊢ (???% → %);
     1236#p cases p #pc #pol normalize nodelta cases pol
     1237[ //
     1238| #p normalize nodelta #Hpol #eqpol lapply (le_n (|program|))
     1239  @(list_ind ?  (λx.|x| ≤ |pi1 ?? program| →
     1240      measure_int x policy 0 = measure_int x p 0 →
     1241      policy_equal_int x policy p) ?? (pi1 ?? program))
     1242 [ #_ #_ #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O
    9511243 | #h #t #Hind #Hp #Hm #i #Hi cases (le_to_or_lt_eq … Hi) -Hi;
    9521244   [ #Hi @Hind
    9531245     [ @(transitive_le … Hp) //
    954      | whd in match (measure_int ???) in Hm; whd in match (measure_int ?(jump_expansion_step ???)?) in Hm;
    955        lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) (|t|) ?)
    956        [ @(lt_to_le_to_lt … (|h::t|)) [ // | @Hp ]
    957        | cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉) in Hm;
    958          #x cases x -x #x1 #x2 #x3
    959          cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉);
    960          #y cases y -y #y1 #y2 #y3
    961          normalize nodelta cases x3 cases y3 normalize nodelta
    962          [1: #H #_ @H
    963          |2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
    964            @measure_incr_or_equal @(transitive_le … Hp) @le_n_Sn
    965          |4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 |2,4,6: destruct (H2) ]
    966          |5: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 1)
    967            #H #_ @(injective_plus_r … H)
    968          |6: >measure_plus >measure_plus
    969             change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???))
    970             #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l
    971             @measure_incr_or_equal @(transitive_le … Hp) @le_n_Sn
    972          |9: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 2)
    973            #H #_ @(injective_plus_r … H)
    974          ]
     1246     | whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm;
     1247       lapply (proj2 ?? (proj1 ?? Hpol) (|t|) Hp)
     1248       cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉) in Hm;
     1249       #x cases x -x #x1 #x2 #x3
     1250       cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉);
     1251       #y cases y -y #y1 #y2 #y3
     1252       cases x3 cases y3 normalize nodelta
     1253       [1: #H #_ @H
     1254       |2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
     1255         lapply (measure_incr_or_equal program policy t ? 0)
     1256         [1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol //
     1257       |4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 |2,4,6: destruct (H2) ]
     1258       |5: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 1)
     1259         #H #_ @(injective_plus_r … H)
     1260       |6: >measure_plus >measure_plus
     1261          change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???))
     1262          #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l
     1263          lapply (measure_incr_or_equal program policy t ? 0)
     1264          [ @(transitive_le … Hp) @le_n_Sn ] >eqpol //
     1265       |9: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 2)
     1266         #H #_ @(injective_plus_r … H)
    9751267       ]
    9761268     | @(le_S_S_to_le … Hi)
    9771269     ]
    978    | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm; 
    979      whd in match (measure_int ?(jump_expansion_step ???)?) in Hm;
    980      lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) (|t|) ?)
    981      [ @(lt_to_le_to_lt … (|h::t|)) [ // | @Hp ]
    982      | cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉) in Hm;
    983        #x cases x -x #x1 #x2 #x3
    984        cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉);
    985        #y cases y -y #y1 #y2 #y3
    986        normalize nodelta cases x3 cases y3 normalize nodelta
    987        [1,5,9: #_ #_ //
    988        |4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 |2,4,6: destruct (H2) ]
    989        |2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
    990          @measure_incr_or_equal @(transitive_le … Hp) @le_n_Sn
    991        |6: >measure_plus >measure_plus
    992           change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???))
    993           #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l
    994           @measure_incr_or_equal @(transitive_le … Hp) @le_n_Sn
    995        ]
     1270   | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm;
     1271     whd in match (measure_int ? p ?) in Hm;
     1272     lapply (proj2 ?? (proj1 ?? Hpol) (|t|) Hp)
     1273     cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉) in   
     1274Hm;
     1275     #x cases x -x #x1 #x2 #x3
     1276     cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉);
     1277     #y cases y -y #y1 #y2 #y3
     1278     normalize nodelta cases x3 cases y3 normalize nodelta
     1279     [1,5,9: #_ #_ //
     1280     |4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 |2,4,6: destruct (H2) ]
     1281     |2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
     1282       lapply (measure_incr_or_equal program policy t ? 0)
     1283       [1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
     1284     |6: >measure_plus >measure_plus
     1285        change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???))
     1286        #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l
     1287        lapply (measure_incr_or_equal program policy t ? 0)
     1288        [ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
    9961289     ]
    9971290   ]
    998  ] 
     1291 ]
     1292qed.
     1293
     1294lemma le_to_eq_plus: ∀n,z.
     1295  n ≤ z → ∃k.z = n + k.
     1296 #n #z elim z
     1297 [ #H cases (le_to_or_lt_eq … H)
     1298   [ #H2 @⊥ @(absurd … H2) @not_le_Sn_O
     1299   | #H2 @(ex_intro … 0) >H2 //
     1300   ]
     1301 | #z' #Hind #H cases (le_to_or_lt_eq … H)
     1302   [ #H' elim (Hind (le_S_S_to_le … H')) #k' #H2 @(ex_intro … (S k'))
     1303     >H2 >plus_n_Sm //
     1304   | #H' @(ex_intro … 0) >H' //
     1305   ]
     1306 ]
    9991307qed.
    10001308
    10011309lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction.|l| < 2^16.
    1002   |l| ≤ |program| → measure_int l (jump_expansion_internal program 0) 0 = 0.
    1003  #l #program elim l 
     1310  |l| ≤ |program| → measure_int l (jump_expansion_start program) 0 = 0.
     1311 #l #program elim l
    10041312 [ //
    10051313 | #h #t #Hind #Hp whd in match (measure_int ???);
     
    10081316     [ normalize nodelta @Hind @le_S_to_le ]
    10091317     @Hp
    1010    | >(lookup_opt_lookup_miss … (proj1 ?? (jump_not_in_policy program (jump_expansion_internal program 0) (|t|) ?) Hj) 〈0,0,short_jump〉)
    1011      [ normalize nodelta @Hind @le_S_to_le ]
    1012      @Hp
    1013    ]
    1014  ]
    1015 qed.
    1016  
    1017 definition je_fixpoint: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
    1018   Σp:jump_expansion_policy.∃n.∀k.n < k → policy_equal program (jump_expansion_internal program k) p.
    1019  #program @(mk_Sig … (jump_expansion_internal program (2*|program|)))
    1020  @(ex_intro … (2*|program|)) #k #Hk
    1021  cases (dec_bounded_exists (λk.policy_equal program (jump_expansion_internal program k)
    1022    (jump_expansion_internal program (S k))) ? (2*|program|))
    1023  [ #H elim H -H #x #Hx @pe_trans
    1024    [ @(jump_expansion_internal program x)
    1025    | @pe_sym @equal_remains_equal
    1026      [ @(proj2 ?? Hx)
    1027      | @(transitive_le ? (2*|program|))
    1028        [ @le_S_S_to_le @le_S @(proj1 ?? Hx)
    1029        | @le_S_S_to_le @le_S @Hk
     1318   | >(lookup_opt_lookup_miss … (proj1 ?? (jump_not_in_policy program (pi1 ?? (jump_expansion_start program)) (|t|) ?) Hj) 〈0,0,short_jump〉)
     1319     [ normalize nodelta @Hind @le_S_to_le @Hp
     1320     | @Hp
     1321     | %
     1322       [ @(proj1 ?? (proj1 ?? (pi2 ?? (jump_expansion_start program))))
     1323       | @(proj2 ?? (proj1 ?? (pi2 ?? (jump_expansion_start program))))
    10301324       ]
    10311325     ]
    1032    | @equal_remains_equal
    1033      [ @(proj2 ?? Hx)
    1034      | @le_S_S_to_le @le_S @(proj1 ?? Hx)
    1035      ]
    1036    ]
    1037  | #Hnex lapply (not_exists_forall … Hnex) -Hnex; #Hfa @pe_sym @equal_remains_equal
    1038    [ lapply (measure_full program (jump_expansion_internal program (2*|program|)))
    1039      #Hfull #i #Hi
    1040      lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program (jump_expansion_internal program (2*|program|))) (jump_expansion_internal program (2*|program|)))) i Hi)
    1041      lapply (Hfull ? i Hi)
    1042      [ -i @le_to_le_to_eq
    1043        [ @measure_le
    1044        | lapply (le_n (2*|program|)) elim (2*|program|) in ⊢ (?%? → %);
    1045          [ #_ >measure_zero @le_n
    1046          | #x #Hind #Hx
    1047            cut (measure_int program (jump_expansion_internal program x) 0 <
    1048                 measure_int program (jump_expansion_internal program (S x)) 0)
    1049            [ elim (le_to_or_lt_eq …
    1050                (measure_incr_or_equal program (jump_expansion_internal program x) program (le_n (|program|)) 0))
    1051              [ //
    1052              | #H @⊥ @(absurd ?? (Hfa x Hx)) @measure_special @H
    1053              ]
    1054            | #H lapply (Hind (le_S_to_le … Hx)) #H2 @(le_to_lt_to_lt … H) @H2
    1055            ]
    1056          ]
    1057        ]
    1058      | -Hfull cases (bvt_lookup ?? (bitvector_of_nat 16 i) (jump_expansion_internal program (2*|program|)) 〈0,0,short_jump〉)
    1059        #x cases x -x #x1 #x2 #x3 normalize nodelta #Hfull
    1060        >Hfull cases (bvt_lookup ?? (bitvector_of_nat ? i) ? 〈0,0,short_jump〉)
    1061        #y cases y -y #y1 #y2 #y3 normalize nodelta cases y3 normalize nodelta 
    1062        [1,2: #H elim H #H2 [1,3: @⊥ @H2 |2,4: destruct (H2) ]
    1063        | #_ //
    1064        ]
    1065      ]
    1066    | @le_S_to_le @Hk
    1067    ]
    1068  | #n @dec_bounded_forall #m
    1069    cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,0,short_jump〉)
    1070    #x cases x -x #x1 #x2 #x3
    1071    cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,0,short_jump〉)
    1072    #y cases y -y #y1 #y2 #y3 normalize nodelta
    1073    @dec_eq_jump_length
    1074  ]
    1075 qed.
    1076 
     1326   ]
     1327 ]
     1328qed.
     1329
     1330(* the actual computation of the fixpoint *)
     1331definition je_fixpoint: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
     1332  Σp:option jump_expansion_policy.∃n.∀k.n < k →
     1333    policy_equal program (\snd (pi1 ?? (jump_expansion_internal program k))) p.
     1334#program @(\snd (pi1 ?? (jump_expansion_internal program (2*|program|))))
     1335(*@(ex_intro … (2*|program|)) #k #Hk*)
     1336cases (dec_bounded_exists (λk.policy_equal (pi1 ?? program)
     1337   (\snd (pi1 ?? (jump_expansion_internal program k)))
     1338   (\snd (pi1 ?? (jump_expansion_internal program (S k))))) ? (2*|program|))
     1339[ #Hex elim Hex -Hex #x #Hx @(ex_intro … x) #k @pe_trans
     1340  [ @(\snd (pi1 ?? (jump_expansion_internal program x)))
     1341  | @pe_sym @equal_remains_equal
     1342    [ @(proj2 ?? Hx)
     1343    | @(transitive_le ? (2*|program|))
     1344      [ @le_S_S_to_le @le_S @(proj1 ?? Hx)
     1345      | @le_S_S_to_le @le_S @Hk
     1346      ]
     1347    ]
     1348  | @equal_remains_equal
     1349    [ @(proj2 ?? Hx)
     1350    | @le_S_S_to_le @le_S @(proj1 ?? Hx)
     1351    ]   
     1352  ]
     1353| #Hnex lapply (not_exists_forall … Hnex) -Hnex; #Hfa @pe_sym @equal_remains_equal
     1354  [ lapply (refl ? (jump_expansion_internal program (2*|program|)))
     1355    cases (jump_expansion_internal program (2*|program|)) in ⊢ (???% → %);
     1356    #jep cases jep #pc #x -jep cases x normalize nodelta
     1357    [ #Hjep #Heqx >Heqx lapply (step_none program (2*|pi1 ?? program|) ? 1)
     1358      [ >Heqx // | <plus_n_Sm <plus_n_O #H >H // ]
     1359    | #pol_2prog #H2prog #Heq2prog lapply (measure_full (pi1 ?? program) pol_2prog) #Hfull
     1360      whd in match (policy_equal ???); lapply Heq2prog -Heq2prog;
     1361      lapply (refl ? (jump_expansion_internal program (2*|program|)))
     1362      cases (jump_expansion_internal program (2*|program|)) in ⊢ (???% → % → %);
     1363      #z cases z #fpc #pol -z cases pol normalize nodelta
     1364      [ #Heq2prog #Hjep #Hploq destruct (Hploq)
     1365      | #p #Heq2prog #Hjep #Hploq whd in match (jump_expansion_internal ??);
     1366        >Hjep normalize nodelta
     1367        lapply (refl ? (jump_expansion_step program (create_label_map program p) «p,?»))
     1368        [2: cases (jump_expansion_step program (create_label_map program p) «p,?») in ⊢ (???% → %);
     1369        #x cases x #Spc #Spol -x cases Spol normalize nodelta
     1370        [ #Hy #Hgnarf cases daemon (* XXX *)
     1371        | #y #Hy #Hgnarf #i #Hi lapply (proj2 ?? (proj1 ?? Hy) i Hi)
     1372          lapply (Hfull ? i Hi)
     1373          [2: lapply (sym_eq ??? (proj1 ?? Hpy)) #Hblp >(Some_eq ??? Hblp)
     1374                >(Some_eq ??? (pair_eq2 ?????? (pi1_eq ???? Hploq)))
     1375                cases (bvt_lookup ?? (bitvector_of_nat 16 i) pol_2prog 〈0,0,short_jump〉)
     1376                #blp cases blp #a #b #c -blp #EQ >EQ normalize nodelta
     1377                cases (bvt_lookup ?? (bitvector_of_nat 16 i) y 〈0,0,short_jump〉)
     1378                #blp cases blp #d #e #f -blp normalize nodelta cases f
     1379                [1,2: #H elim H #H2 [1,3: @⊥ @H2 |2,4: destruct (H2) ]
     1380                | #_ //
     1381                ]
     1382            | @le_to_le_to_eq
     1383              [ @measure_le
     1384              | cut (∀x.x ≤ (2*|pi1 ?? program|) →
     1385                  ∃p.(\snd (pi1 ?? (jump_expansion_internal program x)) = Some ? p ∧
     1386                      x ≤ measure_int program p 0))
     1387                [ #n elim n
     1388                  [ #_ whd in match (jump_expansion_internal program 0);
     1389                    @(ex_intro … (jump_expansion_start program)) % [ @refl |
     1390                    >measure_zero @le_n ]
     1391                  | -n #n' #Hind #Hn' elim (le_to_or_lt_eq … Hn')
     1392                    [ #H2n' elim (Hind ?)
     1393                      [ -Hgnarf #pn' lapply (refl ? (jump_expansion_internal program (S n')))
     1394                        cases (jump_expansion_internal program (S n')) in ⊢ (???% → %);
     1395                        #x cases x -x #npc #npol cases npol normalize nodelta
     1396                        [ #Hbla #Hnone #Hsome lapply (step_none program (S n'))
     1397                          >Hnone normalize nodelta #Ht elim (le_to_eq_plus ?? Hn')
     1398                          #k #Hk lapply (Ht ? k) [ // | <Hk >Hjep #H destruct (H) ]
     1399                        | #Spol #Hbla #HSpol #H3 @(ex_intro ?? Spol) @conj [ @refl |
     1400                          lapply (measure_incr_or_equal program pn' program)
     1401                          lapply (pi2 ?? (jump_expansion_internal program n'))
     1402                          >(proj1 ?? H3)
     1403                          lapply (refl ? (jump_expansion_internal program n'))
     1404                          lapply H3 -H3
     1405                          cases (jump_expansion_internal program n') in ⊢ (% → ???% → %);
     1406                          #x cases x -x #npc #npol normalize nodelta #Hbli #H3 #EQ
     1407                          >(proj1 ?? H3) in Hbli EQ; #Hbli #EQ
     1408                          whd in match (jump_expansion_internal program (S n')) in HSpol;
     1409                          >EQ in HSpol; normalize nodelta
     1410                        ] ]                       
     1411                       
     1412                       
     1413                       
     1414                      |
     1415                      ]
     1416                     |
     1417                     ]
     1418                   ]
     1419                   
     1420                | #gloeirks elim (gloeirks (2*|program|) (le_n ?)) #q
     1421                  >Hjep >(Some_eq ??? (pair_eq2 ?????? (pi1_eq ???? Hploq)))
     1422                  #H >(Some_eq ??? (proj1 ?? H)) @(proj2 ?? H)
     1423                ]
     1424              ]
     1425            ]
     1426          ]
     1427        ]]
     1428      ]
     1429    ]
     1430  | @le_S_to_le @Hk
     1431  ]
     1432| (* TO BE CHANGED *)
     1433  #n cases (jump_expansion_internal program n) cases (jump_expansion_internal program (S n))
     1434  [ %1 //
     1435  |2,3: #x %2 @nmk whd in match (policy_equal ???); [2: //]
     1436    whd in match (eject_policy_opt ???); #H destruct (H)
     1437  |4: #p1 #p2 whd in match (policy_equal ???); @dec_bounded_forall #m
     1438      cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,0,short_jump〉)
     1439      #x cases x -x #x1 #x2 #x3
     1440      cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,0,short_jump〉)
     1441      #y cases y -y #y1 #y2 #y3 normalize nodelta
     1442      @dec_eq_jump_length 
     1443  ]
     1444]
     1445
     1446(* Take a policy of 〈pc, addr, jump_length〉 tuples, and transform it into
     1447 * a map from pc to jump_length. This cannot be done earlier because the pc
     1448 * changes between iterations. *)
    10771449let rec transform_policy (n: nat) policy (acc: BitVectorTrie jump_length 16) on n:
    10781450  BitVectorTrie jump_length 16 ≝
     
    10871459  ].
    10881460
     1461(* The glue between Policy and Assembly. *)
    10891462definition jump_expansion':
    10901463 ∀program:preamble × (Σl:list labelled_instruction.|l| < 2^16).
Note: See TracChangeset for help on using the changeset viewer.