Changeset 2034


Ignore:
Timestamp:
Jun 8, 2012, 5:16:22 PM (5 years ago)
Author:
boender
Message:
  • split Policy into three separate files for ease (and indeed possibility) of compilation
Location:
src/ASM
Files:
2 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r2032 r2034  
    1 include "ASM/ASM.ma".
    2 include "ASM/Arithmetic.ma".
    3 include "ASM/Fetch.ma".
    4 include "ASM/Status.ma".
    5 include "utilities/extralib.ma".
    6 include "ASM/Assembly.ma".
     1include "ASM/PolicyStep.ma".
    72
    83include alias "basics/lists/list.ma".
     
    105include alias "basics/logic.ma".
    116
    12 (* Internal types *)
    13 
    14 (* ppc_pc_map: program length × (pseudo program counter ↦ 〈pc, jump_length〉) *)
    15 definition ppc_pc_map ≝ ℕ × (BitVectorTrie (ℕ × jump_length) 16).
    16 
    17 (* The different properties that we want/need to prove at some point *)
    18 (* Anything that's not in the program doesn't end up in the policy *)
    19 definition out_of_program_none: list labelled_instruction → ppc_pc_map → Prop ≝
    20   λprefix.λsigma.
    21   ∀i:ℕ.i > |prefix| → i < 2^16 → bvt_lookup_opt … (bitvector_of_nat 16 i) (\snd sigma) = None ?.
    22 
    23 (* If instruction i is a jump, then there will be something in the policy at
    24  * position i *)
    25 definition is_jump' ≝
    26   λx:preinstruction Identifier.
    27   match x with
    28   [ JC _ ⇒ True
    29   | JNC _ ⇒ True
    30   | JZ _ ⇒ True
    31   | JNZ _ ⇒ True
    32   | JB _ _ ⇒ True
    33   | JNB _ _ ⇒ True
    34   | JBC _ _ ⇒ True
    35   | CJNE _ _ ⇒ True
    36   | DJNZ _ _ ⇒ True
    37   | _ ⇒ False
    38   ].
    39  
    40 definition is_jump ≝
    41   λinstr:pseudo_instruction.
    42   match instr with
    43   [ Instruction i   ⇒ is_jump' i
    44   | Call _ ⇒ True
    45   | Jmp _ ⇒ True
    46   | _ ⇒ False
    47   ].
    48 
    49 definition is_jump_to ≝
    50   λx:pseudo_instruction.λd:Identifier.
    51   match x with
    52   [ Instruction i ⇒ match i with
    53     [ JC j ⇒ d = j
    54     | JNC j ⇒ d = j
    55     | JZ j ⇒ d = j
    56     | JNZ j ⇒ d = j
    57     | JB _ j ⇒ d = j
    58     | JNB _ j ⇒ d = j
    59     | CJNE _ j ⇒ d = j
    60     | DJNZ _ j ⇒ d = j
    61     | _ ⇒ False
    62     ]
    63   | Call c ⇒ d = c
    64   | Jmp j ⇒ d = j
    65   | _ ⇒ False
    66   ].
    67  
    68 definition jump_not_in_policy: list labelled_instruction → ppc_pc_map → Prop ≝
    69   λprefix.λsigma.
    70   ∀i:ℕ.i < |prefix| →
    71   ¬is_jump (\snd (nth i ? prefix 〈None ?, Comment []〉)) →
    72   \snd (bvt_lookup … (bitvector_of_nat 16 (S i)) (\snd sigma) 〈0,short_jump〉) = short_jump.
    73 
    74 (* if the instruction 〈p,a〉 is a jump to label l, then label l is at address a *)
    75 (* definition labels_okay: label_map → ppc_pc_map → Prop ≝
    76   λlabels.λsigma.
    77   bvt_forall ?? (\snd sigma) (λn.λx.
    78    let 〈pc,addr_nat〉 ≝ x in
    79    ∃id:Identifier.lookup_def … labels id 0 = addr_nat
    80   ). *)
    81  
    82 (* Between two policies, jumps cannot decrease *)
    83 definition jmpeqb: jump_length → jump_length → bool ≝
    84   λj1.λj2.
    85   match j1 with
    86   [ short_jump ⇒ match j2 with [ short_jump ⇒ true | _ ⇒ false ]
    87   | medium_jump ⇒ match j2 with [ medium_jump ⇒ true | _ ⇒ false ]
    88   | long_jump ⇒ match j2 with [ long_jump ⇒ true | _ ⇒ false ]
    89   ].
    90 
    91 lemma jmpeqb_to_eq: ∀j1,j2.jmpeqb j1 j2 → j1 = j2.
    92  #j1 #j2 cases j1 cases j2
    93  [1,5,9: / by /]
    94  #H cases H
    95 qed.
    96 
    97 definition jmple: jump_length → jump_length → Prop ≝
    98   λj1.λj2.
    99   match j1 with
    100   [ short_jump  ⇒
    101     match j2 with
    102     [ short_jump ⇒ False
    103     | _          ⇒ True
    104     ]
    105   | medium_jump ⇒
    106     match j2 with
    107     [ long_jump ⇒ True
    108     | _         ⇒ False
    109     ]
    110   | long_jump   ⇒ False
    111   ].
    112 
    113 definition jmpleq: jump_length → jump_length → Prop ≝
    114   λj1.λj2.jmple j1 j2 ∨ j1 = j2.
    115  
    116 definition policy_increase: list labelled_instruction → ppc_pc_map →
    117   ppc_pc_map → Prop ≝
    118  λprogram.λop.λp.
    119  ∀i.i < |program| →
    120    let 〈opc,oj〉 ≝ bvt_lookup … (bitvector_of_nat 16 (S i)) (\snd op) 〈0,short_jump〉 in
    121    let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat 16 (S i)) (\snd p) 〈0,short_jump〉 in
    122      (*opc ≤ pc ∧*) jmpleq oj j.
    123 
    124 (* Policy safety *)
    125 (*definition policy_safe: list labelled_instruction → label_map → ppc_pc_map → Prop ≝
    126  λprogram.λlabels.λsigma.
    127  ∀i.i < |program| →
    128  let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,false〉 in
    129  let 〈label,instr〉 ≝ nth i ? program 〈None ?, Comment [ ]〉 in
    130  ∀dest.is_jump_to instr dest →
    131    let paddr ≝ lookup_def … labels dest 0 in
    132    let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd sigma) 〈0,false〉) in
    133    match j with
    134    [ None ⇒ True
    135    | Some j ⇒ match j with
    136      [ short_jump  ⇒
    137         if leb pc addr
    138         then le (addr - pc) 126
    139         else le (pc - addr) 129
    140      | medium_jump ⇒   
    141         let a ≝ bitvector_of_nat 16 addr in
    142         let p ≝ bitvector_of_nat 16 pc in
    143         let 〈fst_5_addr, rest_addr〉 ≝ vsplit bool 5 11 a in
    144         let 〈fst_5_pc, rest_pc〉 ≝ vsplit bool 5 11 p in
    145         eq_bv 5 fst_5_addr fst_5_pc = true
    146      | long_jump   ⇒ True
    147      ]
    148    ].*)
    149 
    150 (* this is the instruction size as determined by the distance from origin to destination *)
    151 (*definition instruction_size_sigma: label_map → ppc_pc_map → Word → pseudo_instruction → ℕ ≝
    152  λlabels.λsigma.λpc.λi.
    153  \fst (assembly_1_pseudoinstruction
    154    (λid.bitvector_of_nat 16 (lookup_def … labels id 0))
    155    (λi.bitvector_of_nat 16 (\fst (bvt_lookup ?? i (\snd sigma) 〈0,false〉))) pc
    156    (λx.zero 16) i).*)
    157  
    158 (* this is the instruction size as determined by the jump length given *)
    159 definition expand_relative_jump_internal_unsafe:
    160   jump_length → ([[relative]] → preinstruction [[relative]]) → list instruction ≝
    161   λjmp_len:jump_length.λi.
    162   match jmp_len with
    163   [ short_jump ⇒ [ RealInstruction (i (RELATIVE (zero 8))) ]
    164   | medium_jump ⇒ [ ] (* this should not happen *)
    165   | long_jump ⇒
    166     [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2)));
    167       SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *)
    168       LJMP (ADDR16 (zero 16))
    169     ]
    170   ].
    171  @I
    172 qed.
    173 
    174 definition expand_relative_jump_unsafe:
    175   jump_length → preinstruction Identifier → list instruction ≝
    176   λjmp_len:jump_length.λi.
    177   match i with
    178   [ JC jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JC ?)
    179   | JNC jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNC ?)
    180   | JB baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JB ? baddr)
    181   | JZ jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JZ ?)
    182   | JNZ jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNZ ?)
    183   | JBC baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JBC ? baddr)
    184   | JNB baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNB ? baddr)
    185   | CJNE addr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (CJNE ? addr)
    186   | DJNZ addr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (DJNZ ? addr)
    187   | ADD arg1 arg2 ⇒ [ ADD ? arg1 arg2 ]
    188   | ADDC arg1 arg2 ⇒ [ ADDC ? arg1 arg2 ]
    189   | SUBB arg1 arg2 ⇒ [ SUBB ? arg1 arg2 ]
    190   | INC arg ⇒ [ INC ? arg ]
    191   | DEC arg ⇒ [ DEC ? arg ]
    192   | MUL arg1 arg2 ⇒ [ MUL ? arg1 arg2 ]
    193   | DIV arg1 arg2 ⇒ [ DIV ? arg1 arg2 ]
    194   | DA arg ⇒ [ DA ? arg ]
    195   | ANL arg ⇒ [ ANL ? arg ]
    196   | ORL arg ⇒ [ ORL ? arg ]
    197   | XRL arg ⇒ [ XRL ? arg ]
    198   | CLR arg ⇒ [ CLR ? arg ]
    199   | CPL arg ⇒ [ CPL ? arg ]
    200   | RL arg ⇒ [ RL ? arg ]
    201   | RR arg ⇒ [ RR ? arg ]
    202   | RLC arg ⇒ [ RLC ? arg ]
    203   | RRC arg ⇒ [ RRC ? arg ]
    204   | SWAP arg ⇒ [ SWAP ? arg ]
    205   | MOV arg ⇒ [ MOV ? arg ]
    206   | MOVX arg ⇒ [ MOVX ? arg ]
    207   | SETB arg ⇒ [ SETB ? arg ]
    208   | PUSH arg ⇒ [ PUSH ? arg ]
    209   | POP arg ⇒ [ POP ? arg ]
    210   | XCH arg1 arg2 ⇒ [ XCH ? arg1 arg2 ]
    211   | XCHD arg1 arg2 ⇒ [ XCHD ? arg1 arg2 ]
    212   | RET ⇒ [ RET ? ]
    213   | RETI ⇒ [ RETI ? ]
    214   | NOP ⇒ [ RealInstruction (NOP ?) ]
    215   ].
    216 
    217 definition instruction_size_jmplen:
    218  jump_length → pseudo_instruction → ℕ ≝
    219   λjmp_len.
    220   λi.
    221   let pseudos ≝ match i with
    222   [ Cost cost ⇒ [ ]
    223   | Comment comment ⇒ [ ]
    224   | Call call ⇒
    225     match jmp_len with
    226     [ short_jump ⇒ [ ] (* this should not happen *)
    227     | medium_jump ⇒ [ ACALL (ADDR11 (zero 11)) ]
    228     | long_jump ⇒ [ LCALL (ADDR16 (zero 16)) ]
    229     ]
    230   | Mov d trgt ⇒
    231      [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, DATA16 (zero 16)〉))))]
    232   | Instruction instr ⇒ expand_relative_jump_unsafe jmp_len instr
    233   | Jmp jmp ⇒
    234     match jmp_len with
    235     [ short_jump ⇒ [ SJMP (RELATIVE (zero 8)) ]
    236     | medium_jump ⇒ [ AJMP (ADDR11 (zero 11)) ]
    237     | long_jump ⇒ [ LJMP (ADDR16 (zero 16)) ]
    238     ]
    239   ] in
    240   let mapped ≝ map ? ? assembly1 pseudos in
    241   let flattened ≝ flatten ? mapped in
    242   let pc_len ≝ length ? flattened in
    243     pc_len.
    244  @I.
    245 qed.
    246 
    247 definition policy_compact_unsafe: list labelled_instruction → label_map → ppc_pc_map → Prop ≝
    248  λprogram.λlabels.λsigma.
    249  ∀n:ℕ.n < |program| →
    250   match bvt_lookup_opt … (bitvector_of_nat ? n) (\snd sigma) with
    251   [ None ⇒ False
    252   | Some x ⇒ let 〈pc,j〉 ≝ x in
    253     match bvt_lookup_opt … (bitvector_of_nat ? (S n)) (\snd sigma) with
    254     [ None ⇒ False
    255     | Some x1 ⇒ let 〈pc1,j1〉 ≝ x1 in
    256        pc1 = pc + instruction_size_jmplen j (\snd (nth n ? program 〈None ?, Comment []〉))
    257     ]
    258   ].
    259    
    260 (* new safety condition: policy corresponds to program and resulting program is compact *)
    261 definition policy_compact: list labelled_instruction → label_map → ppc_pc_map → Prop ≝
    262  λprogram.λlabels.λsigma.
    263  ∀n:ℕ.n < |program| →
    264   match bvt_lookup_opt … (bitvector_of_nat ? n) (\snd sigma) with
    265   [ None ⇒ False
    266   | Some x ⇒ let 〈pc,j〉 ≝ x in
    267     match bvt_lookup_opt … (bitvector_of_nat ? (S n)) (\snd sigma) with
    268     [ None ⇒ False
    269     | Some x1 ⇒ let 〈pc1,j1〉 ≝ x1 in
    270        pc1 = pc + instruction_size (λid.bitvector_of_nat ? (lookup_def ?? labels id 0))
    271          (λppc.bitvector_of_nat ? (\fst (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉)))
    272          (λppc.jmpeqb long_jump (\snd (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉)))
    273          (bitvector_of_nat ? n) (\snd (nth n ? program 〈None ?, Comment []〉))
    274     ]
    275   ].
    276  
    277 (* Definitions and theorems for the jump_length type (itself defined in Assembly) *)
    278 definition max_length: jump_length → jump_length → jump_length ≝
    279   λj1.λj2.
    280   match j1 with
    281   [ long_jump   ⇒ long_jump
    282   | medium_jump ⇒
    283     match j2 with
    284     [ medium_jump ⇒ medium_jump
    285     | _           ⇒ long_jump
    286     ]
    287   | short_jump  ⇒
    288     match j2 with
    289     [ short_jump ⇒ short_jump
    290     | _          ⇒ long_jump
    291     ]
    292   ].
    293 
    294 lemma dec_jmple: ∀x,y:jump_length.Sum (jmple x y) (¬(jmple x y)).
    295  #x #y cases x cases y /3 by inl, inr, nmk, I/
    296 qed.
    297  
    298 lemma jmpleq_max_length: ∀ol,nl.
    299   jmpleq ol (max_length ol nl).
    300  #ol #nl cases ol cases nl
    301  /2 by or_introl, or_intror, I/
    302 qed.
    303 
    304 lemma dec_eq_jump_length: ∀a,b:jump_length.Sum (a = b) (a ≠ b).
    305   #a #b cases a cases b /2/
    306   %2 @nmk #H destruct (H)
    307 qed.
    308  
    309 (* definition policy_isize_sum ≝
    310   λprefix:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map.
    311   (\fst sigma) = foldl_strong (option Identifier × pseudo_instruction)
    312   (λacc.ℕ)
    313   prefix
    314   (λhd.λx.λtl.λp.λacc.
    315     acc + (instruction_size (λid.bitvector_of_nat ? (lookup_def ?? labels id 0))
    316     (λppc.bitvector_of_nat ? (\fst (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉)))
    317     (λppc.jmpeqb long_jump (\snd (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉)))
    318     (bitvector_of_nat 16 (\fst sigma)) (\snd x)))
    319   0. *)
    320  
    321 (* The function that creates the label-to-address map *)
    322 definition create_label_map: ∀program:list labelled_instruction.
    323   (Σlabels:label_map.
    324     ∀l.occurs_exactly_once ?? l program →
    325     bitvector_of_nat ? (lookup_def ?? labels l 0) =
    326      address_of_word_labels_code_mem program l
    327   ) ≝
    328  λprogram.
    329    \fst (create_label_cost_map program).
    330  #l #Hl lapply (pi2 ?? (create_label_cost_map0 program)) @pair_elim
    331  #labels #costs #EQ normalize nodelta #H whd in match create_label_cost_map;
    332  normalize nodelta >EQ @(H l Hl)
    333 qed.
    334 
    335 definition select_reljump_length: label_map → ppc_pc_map → ppc_pc_map → ℕ →  ℕ →
    336   Identifier → jump_length ≝
    337   λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl.
    338   let paddr ≝ lookup_def … labels lbl 0 in
    339   if leb ppc paddr (* forward jump *)
    340   then
    341     let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉)
    342                     + added in
    343     if leb (addr - \fst inc_sigma) 129
    344     then short_jump
    345     else long_jump
    346   else
    347     let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉) in
    348     if leb (\fst inc_sigma - addr) 125
    349     then short_jump
    350     else long_jump.
    351 
    352 definition select_call_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → ℕ →
    353   Identifier → jump_length ≝
    354   λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl.
    355   let paddr ≝ lookup_def ? ? labels lbl 0 in
    356   let addr ≝
    357     if leb ppc paddr (* forward jump *)
    358     then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉)
    359             + added
    360     else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉) in
    361   let 〈fst_5_addr, rest_addr〉 ≝ vsplit ? 5 11 (bitvector_of_nat ? addr) in
    362   let 〈fst_5_pc, rest_pc〉 ≝ vsplit ? 5 11 (bitvector_of_nat ? (\fst inc_sigma)) in
    363   if eq_bv ? fst_5_addr fst_5_pc
    364   then medium_jump
    365   else long_jump.
    366  
    367 definition select_jump_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → ℕ →
    368   Identifier → jump_length ≝
    369   λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl.
    370   let paddr ≝ lookup_def … labels lbl 0 in
    371   if leb ppc paddr (* forward jump *)
    372   then
    373     let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉)
    374               + added in
    375     if leb (addr - \fst inc_sigma) 126
    376     then short_jump
    377     else select_call_length labels old_sigma inc_sigma added ppc lbl
    378   else
    379     let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉) in
    380     if leb (\fst inc_sigma - addr) 129
    381     then short_jump
    382     else select_call_length labels old_sigma inc_sigma added ppc lbl.
    383  
    384 definition jump_expansion_step_instruction: label_map → ppc_pc_map → ppc_pc_map →
    385   ℕ → ℕ → preinstruction Identifier → option jump_length ≝
    386   λlabels.λold_sigma.λinc_sigma.λadded.λppc.λi.
    387   match i with
    388   [ JC j     ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
    389   | JNC j    ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
    390   | JZ j     ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
    391   | JNZ j    ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
    392   | JB _ j   ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
    393   | JBC _ j  ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
    394   | JNB _ j  ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
    395   | CJNE _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
    396   | DJNZ _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
    397   | _        ⇒ None ?
    398   ].
    399 
    400 lemma dec_is_jump: ∀x.Sum (is_jump x) (¬is_jump x).
    401 #i cases i
    402 [#id cases id
    403  [1,2,3,6,7,33,34:
    404   #x #y %2 whd in match (is_jump ?); /2 by nmk/
    405  |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32:
    406   #x %2 whd in match (is_jump ?); /2 by nmk/
    407  |35,36,37: %2 whd in match (is_jump ?); /2 by nmk/
    408  |9,10,14,15: #x %1 / by I/
    409  |11,12,13,16,17: #x #y %1 / by I/
    410  ]
    411 |2,3: #x %2 /2 by nmk/
    412 |4,5: #x %1 / by I/
    413 |6: #x #y %2 /2 by nmk/
    414 ]
    415 qed.
    416 
    417 lemma geb_to_leb: ∀a,b:ℕ.geb a b = leb b a.
    418   #a #b / by refl/
    419 qed.
    420 
    421 lemma nth_last: ∀A,a,l.
    422   nth (|l|) A l a = a.
    423  #A #a #l elim l
    424  [ / by /
    425  | #h #t #Hind whd in match (nth ????); whd in match (tail ??); @Hind
    426  ]
    427 qed.
    428 
    429 (* The first step of the jump expansion: everything to short. *)
    430 definition jump_expansion_start:
    431   ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16).
    432   ∀labels:label_map.
    433   Σpolicy:option ppc_pc_map.
    434     match policy with
    435     [ None ⇒ True
    436     | Some p ⇒
    437        And (And (And (And (And (And (out_of_program_none (pi1 ?? program) p)
    438        (jump_not_in_policy (pi1 ?? program) p))
    439        (policy_compact_unsafe program labels p))
    440        (bvt_lookup_opt … (bitvector_of_nat ? 0) (\snd p) = Some ? 〈0,short_jump〉))
    441        (∀i.i ≤ |program| → ∃pc.
    442          bvt_lookup_opt … (bitvector_of_nat ? i) (\snd p) = Some ? 〈pc,short_jump〉))
    443        (bvt_lookup_opt … (bitvector_of_nat ? (|program|)) (\snd p) =
    444          Some ? 〈\fst p,short_jump〉))
    445        (\fst p < 2^16)
    446     ] ≝
    447   λprogram.λlabels.
    448   let final_policy ≝ foldl_strong (option Identifier × pseudo_instruction)
    449   (λprefix.Σpolicy:ppc_pc_map.
    450     And (And (And (And (And (out_of_program_none prefix policy)
    451     (jump_not_in_policy prefix policy))
    452     (policy_compact_unsafe prefix labels policy))
    453     (bvt_lookup_opt … (bitvector_of_nat ? 0) (\snd policy) = Some ? 〈0,short_jump〉))
    454     (∀i.i ≤ |prefix| → ∃pc.
    455       bvt_lookup_opt … (bitvector_of_nat ? i) (\snd policy) = Some ? 〈pc,short_jump〉))
    456     (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd policy) =
    457       Some ? 〈\fst policy,short_jump〉))
    458   program
    459   (λprefix.λx.λtl.λprf.λp.
    460    let 〈pc,sigma〉 ≝ pi1 ?? p in
    461    let 〈label,instr〉 ≝ x in
    462    let isize ≝ instruction_size_jmplen short_jump instr in
    463    〈pc + isize, bvt_insert … (bitvector_of_nat 16 (S (|prefix|))) 〈pc+isize,short_jump〉 sigma〉
    464   ) 〈0, bvt_insert ?? (bitvector_of_nat 16 0) 〈0,short_jump〉 (Stub ??)〉 in
    465   if geb (\fst (pi1 ?? final_policy)) 2^16 then
    466     None ?
    467   else
    468     Some ? (pi1 ?? final_policy).
    469 [ / by I/
    470 | lapply p -p generalize in match (foldl_strong ?????); * #p #Hp #hg
    471   @conj [ @Hp | @not_le_to_lt @leb_false_to_not_le <geb_to_leb @hg ]
    472 | @conj [ @conj [ @conj [ @conj [ @conj
    473   [ (* out_of_program_none *)
    474     #i >append_length <commutative_plus #Hi normalize in Hi; #Hi2
    475     cases (le_to_or_lt_eq … Hi) -Hi #Hi
    476     cases p -p #p cases p -p #pc #p #Hp cases x -x #l #pi
    477     [ >lookup_opt_insert_miss
    478       [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i ? Hi2)
    479         @le_S_to_le @le_S_to_le @Hi
    480       | @bitvector_of_nat_abs
    481         [ @Hi2
    482         | @(transitive_lt … Hi2) @le_S_to_le @Hi
    483         | @sym_neq @lt_to_not_eq @le_S_to_le @Hi
    484         ]
    485       ]
    486     | >lookup_opt_insert_miss
    487       [ <Hi @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) (S (S (|prefix|))) ?)
    488         [ @le_S @le_n
    489         | >Hi @Hi2
    490         ]
    491       | @bitvector_of_nat_abs
    492         [ @Hi2
    493         | @(transitive_lt … Hi2) <Hi @le_n
    494         | @sym_neq @lt_to_not_eq <Hi @le_n
    495         ]
    496       ]
    497     ]
    498   | (* jump_not_in_policy *) cases p -p #p cases p -p #pc #sigma #Hp
    499     cases x in prf; #lbl #ins #prf #i >append_length <commutative_plus #Hi
    500     normalize in Hi; normalize nodelta cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    501     [ >lookup_insert_miss
    502       [ lapply ((proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) i ?)
    503         [ @Hi
    504         | >nth_append_first
    505           [ #H #H2 @H @H2
    506           | @Hi
    507           ]
    508         ]
    509       | @bitvector_of_nat_abs
    510         [ @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length <commutative_plus @le_S
    511           @le_plus_a @Hi
    512         | @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length <plus_n_Sm @le_S_S
    513           @le_plus_n_r
    514         | @lt_to_not_eq @le_S_S @Hi
    515         ]
    516       ]
    517     | >Hi >lookup_insert_hit #_ @refl
    518     ]
    519   ]
    520   | (* policy_compact_unsafe *) #i >append_length <commutative_plus #Hi normalize in Hi;
    521     cases p -p #p cases p -p #fpc #sigma #Hp cases x #lbl #instr normalize nodelta
    522     cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    523     [ >lookup_opt_insert_miss
    524       [ >lookup_opt_insert_miss
    525         [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))) i Hi)
    526           lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? i) sigma))
    527           cases (bvt_lookup_opt … (bitvector_of_nat ? i) sigma) in ⊢ (???% → %);
    528           [ #_ normalize nodelta / by /
    529           | #x cases x -x #pci #ji #EQi
    530             lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) sigma))
    531             cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) sigma) in ⊢ (???% → %);
    532             [ #_ normalize nodelta / by /
    533             | #x cases x -x #pcSi #jSi #EQSi normalize nodelta >nth_append_first
    534               [ / by /
    535               | @Hi
    536               ]
    537             ]
    538           ]
    539         ]
    540       ]
    541       [2: lapply (le_S_to_le … Hi) -Hi #Hi]
    542       @bitvector_of_nat_abs
    543       [1,4: @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length <commutative_plus
    544         @le_plus_a @Hi
    545       |2,5: @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length <plus_n_Sm
    546         @le_S_S @le_plus_n_r
    547       |3,6: @lt_to_not_eq @le_S_S @Hi
    548       ]
    549     | >lookup_opt_insert_miss
    550       [ >Hi >lookup_opt_insert_hit normalize nodelta
    551         >(proj2 ?? Hp) normalize nodelta >nth_append_second
    552         [ <minus_n_n whd in match (nth ????); @refl
    553         | @le_n
    554         ]
    555       | @bitvector_of_nat_abs
    556         [ @(transitive_lt … (pi2 ?? program)) >Hi >prf @le_S_S >append_length <commutative_plus
    557           @le_plus_a @le_n
    558         | @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length <plus_n_Sm
    559           @le_S_S @le_plus_n_r
    560         | @lt_to_not_eq @le_S_S >Hi @le_n
    561         ]
    562       ]
    563     ]
    564   ]
    565   | (* lookup 0 = 0 *)
    566     cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta
    567     >lookup_opt_insert_miss
    568     [ @(proj2 ?? (proj1 ?? (proj1 ?? Hp)))
    569     | @bitvector_of_nat_abs
    570       [ / by /
    571       | @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm
    572         @le_S_S @le_plus_n_r
    573       | @lt_to_not_eq / by /
    574       ]
    575     ]
    576   ]
    577   | (* lookup = short_jump *) #i >append_length <commutative_plus #Hi normalize in Hi;
    578     cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta
    579     cases (le_to_or_lt_eq … Hi) -Hi #Hi
    580     [ >lookup_opt_insert_miss
    581       [ @(proj2 ?? (proj1 ?? Hp) i (le_S_S_to_le … Hi))
    582       | @bitvector_of_nat_abs
    583         [ @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S >commutative_plus
    584           @le_plus_a @le_S_S_to_le @Hi
    585         | @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S
    586           @le_S_S @le_plus_n_r
    587         | @lt_to_not_eq @Hi
    588         ]
    589       ]
    590     | >Hi >lookup_opt_insert_hit @(ex_intro ?? (pc+instruction_size_jmplen short_jump instr))
    591       @refl
    592     ]
    593   ]
    594   | (* lookup at the end *) cases p -p #p cases p -p #pc #sigma #Hp cases x
    595     #lbl #instr >append_length <plus_n_Sm <plus_n_O >lookup_opt_insert_hit
    596     / by refl/
    597   ]
    598 | @conj [ @conj [ @conj [ @conj [ @conj
    599   [ #i cases i
    600     [ #Hi @⊥ @(absurd ? Hi) @le_to_not_lt / by /
    601     | -i #i #Hi #Hi2 >lookup_opt_insert_miss
    602       [ / by refl/
    603       | @bitvector_of_nat_abs
    604         [ @Hi2
    605         | / by /
    606         | @sym_neq @lt_to_not_eq / by /
    607         ]
    608       ]
    609     ]
    610   | #i cases i
    611     [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    612     | -i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O
    613     ]
    614   ]
    615   | #i cases i
    616     [ #Hi @⊥ @(absurd … Hi) @le_to_not_lt @le_n
    617     | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    618     ]
    619   ]
    620   | >lookup_opt_insert_hit @refl
    621   ]
    622   | #i cases i
    623     [ #Hi >lookup_opt_insert_hit @(ex_intro ?? 0) @refl
    624     | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    625     ]
    626   ]
    627   | >lookup_opt_insert_hit @refl
    628   ]
    629 ]
    630 qed.
    631 
    632 definition policy_equal ≝
    633   λprogram:list labelled_instruction.λp1,p2:ppc_pc_map.
    634   (* \fst p1 = \fst p2 ∧ *)
    635   (∀n:ℕ.n ≤ |program| →
    636     let pc1 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉 in
    637     let pc2 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉 in
    638     \snd pc1 = \snd pc2).
    639    
    640 definition nec_plus_ultra ≝
    641   λprogram:list labelled_instruction.λp:ppc_pc_map.
    642   ¬(∀i.i < |program| → is_jump (\snd (nth i ? program 〈None ?, Comment []〉)) →
    643   \snd (bvt_lookup … (bitvector_of_nat 16 (S i)) (\snd p) 〈0,short_jump〉) = long_jump).
    644  
    645 (*include alias "common/Identifiers.ma".*)
    646 include alias "ASM/BitVector.ma".
    647 include alias "basics/lists/list.ma".
    648 include alias "arithmetics/nat.ma".
    649 include alias "basics/logic.ma".
    650 
    651 lemma blerpque: ∀a,b,i.
    652   is_jump i → instruction_size_jmplen (max_length a b) i = instruction_size_jmplen a i →
    653   (max_length a b) = a.
    654  #a #b #i cases i
    655  [1: #pi cases pi
    656    [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
    657      try (#x #y #H #_) try (#x #H #_) try (#H #_) cases H
    658    |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #_ try (#_ %)
    659      try (#abs normalize in abs; destruct (abs) @I)
    660      cases a; cases b; try (#_ %) try (#abs normalize in abs; destruct(abs) @I)
    661      try (@(subaddressing_mode_elim … x) #w #abs normalize in abs; destruct (abs) @I)
    662      cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w
    663      try ( #abs normalize in abs; destruct (abs) @I)
    664      @(subaddressing_mode_elim … a1) #w2 #abs normalize in abs; destruct (abs)
    665    ]
    666   |2,3,6: #x [3: #y] #H cases H
    667   |4,5: #id #_ cases a cases b
    668     [2,3,4,6,11,12,13,15: normalize #H destruct (H)
    669     |1,5,7,8,9,10,14,16,17,18: #H / by refl/
    670     ]
    671   ]
    672 qed.
    673 
    674 lemma etblorp: ∀a,b,i.is_jump i →
    675   instruction_size_jmplen a i ≤ instruction_size_jmplen (max_length a b) i.
    676  #a #b #i cases i
    677  [2,3,6: #x [3: #y] #H cases H
    678  |4,5: #id #_ cases a cases b / by le_n/
    679  |1: #pi cases pi
    680    [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
    681      [1,2,3,6,7,24,25: #x #y
    682      |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    683      #H cases H
    684    |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
    685      #_ cases a cases b
    686      [2,3: cases x #ad cases ad
    687        [15,34: #b #Hb / by le_n/
    688        |1,2,3,4,8,9,16,17,18,19,20,21,22,23,27,28,35,36,37,38: #b] #Hb cases Hb
    689      |1,4,5,6,7,8,9: / by le_n/
    690      |11,12: cases x #ad cases ad
    691        [15,34: #b #Hb / by le_n/
    692        |1,2,3,4,8,9,16,17,18,19,20,21,22,23,27,28,35,36,37,38: #b] #Hb cases Hb
    693      |10,13,14,15,16,17,18: / by le_n/
    694      |20,21: cases x #ad cases ad
    695        [15,34: #b #Hb / by le_n/
    696        |1,2,3,4,8,9,16,17,18,19,20,21,22,23,27,28,35,36,37,38: #b] #Hb cases Hb
    697      |19,22,23,24,25,26,27: / by le_n/
    698      |29,30: cases x #ad cases ad #a1 #a2
    699        [1,3: cases a2 #ad2 cases ad2
    700          [1,8,20,27: #b #Hb / by le_n/
    701          |2,3,4,9,15,16,17,18,19,21,22,23,28,34,35,36,37,38: #b] #Hb cases Hb
    702        |2,4: cases a1 #ad1 cases ad1
    703          [2,4,21,23: #b #Hb / by le_n/
    704          |1,3,8,9,15,16,17,18,19,20,22,27,28,34,35,36,37,38: #b] #Hb cases Hb
    705        ]
    706      |28,31,32,33,34,35,36: / by le_n/
    707      |38,39: cases x #ad cases ad
    708        [1,4,20,23: #b #Hb / by le_n/
    709        |2,3,8,9,15,16,17,18,19,21,22,27,28,34,35,36,37,38: #b] #Hb cases Hb
    710      |37,40,41,42,43,44,45: / by le_n/
    711      |46,47,48,49,50,51,52,53,54: / by le_n/
    712      |55,56,57,58,59,60,61,62,63: / by le_n/
    713      |64,65,66,67,68,69,70,71,72: / by le_n/
    714      |73,74,75,76,77,78,79,80,81: / by le_n/
    715      ]
    716    ]
    717  ]
    718 qed.
    719 
    720 lemma minus_zero_to_le: ∀n,m:ℕ.n - m = 0 → n ≤ m.
    721  #n
    722  elim n
    723  [ #m #_ @le_O_n
    724  | #n' #Hind #m cases m
    725    [ #H -n whd in match (minus ??) in H; >H @le_n
    726    | #m' -m #H whd in match (minus ??) in H; @le_S_S @Hind @H
    727    ]
    728  ]
    729 qed.
    730 
    731 lemma plus_zero_zero: ∀n,m:ℕ.n + m = 0 → m = 0.
    732  #n #m #Hn @sym_eq @le_n_O_to_eq <Hn >commutative_plus @le_plus_n_r
    733 qed.
    734 
    735 (* One step in the search for a jump expansion fixpoint. *)
    736 definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16).
    737   ∀labels:(Σlm:label_map.∀l.
    738     occurs_exactly_once ?? l program →
    739     bitvector_of_nat ? (lookup_def … lm l 0) =
    740     address_of_word_labels_code_mem program l).
    741   ∀old_policy:(Σpolicy:ppc_pc_map.
    742     And (And (And (out_of_program_none program policy)
    743     (jump_not_in_policy program policy))
    744     (bvt_lookup_opt … (bitvector_of_nat ? 0) (\snd policy) = Some ? 〈0,short_jump〉))
    745     (\fst policy < 2^16)).
    746   (Σx:bool × (option ppc_pc_map).
    747     let 〈no_ch,y〉 ≝ x in
    748     match y with
    749     [ None ⇒ nec_plus_ultra program old_policy
    750     | Some p ⇒ And (And (And (And (And (And (out_of_program_none program p)
    751        (jump_not_in_policy program p))
    752        (policy_increase program old_policy p))
    753        (policy_compact program labels p))
    754        (bvt_lookup_opt … (bitvector_of_nat ? 0) (\snd p) = Some ? 〈0,short_jump〉))
    755        (no_ch = true → policy_equal program old_policy p))
    756        (\fst p < 2^16)
    757     ])
    758     ≝
    759   λprogram.λlabels.λold_sigma.
    760   let 〈final_added, final_policy〉 ≝
    761     pi1 ?? (foldl_strong (option Identifier × pseudo_instruction)
    762     (λprefix.Σx:ℕ × ppc_pc_map.
    763       let 〈added,policy〉 ≝ x in
    764       And (And (And (And (And (out_of_program_none prefix policy)
    765       (jump_not_in_policy prefix policy))
    766       (policy_increase prefix old_sigma policy))
    767       (policy_compact_unsafe prefix labels policy))
    768       (bvt_lookup_opt … (bitvector_of_nat ? 0) (\snd policy) = Some ? 〈0,short_jump〉))
    769       (added = 0 → policy_equal prefix old_sigma policy))
    770     program
    771     (λprefix.λx.λtl.λprf.λacc.
    772       let 〈inc_added, inc_pc_sigma〉 ≝ (pi1 ?? acc) in
    773       let 〈label,instr〉 ≝ x in
    774       (* Now, we must add the current ppc and its pc translation.
    775        * Three possibilities:
    776        *   - Instruction is not a jump; i.e. constant size whatever the sigma we use;
    777        *   - Instruction is a backward jump; we can use the sigma we're constructing,
    778        *     since it will already know the translation of its destination;
    779        *   - Instruction is a forward jump; we must use the old sigma (the new sigma
    780        *     does not know the translation yet), but compensate for the jumps we
    781        *     have lengthened.
    782        *)
    783       let add_instr ≝ match instr with
    784       [ Jmp  j        ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
    785       | Call c        ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
    786       | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (|prefix|) i
    787       | _             ⇒ None ?
    788       ] in
    789       let 〈inc_pc, inc_sigma〉 ≝ inc_pc_sigma in
    790       let 〈old_pc,old_length〉 ≝
    791         bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉 in
    792       let old_size ≝ instruction_size_jmplen old_length instr in
    793       let 〈new_length, isize〉 ≝ match add_instr with
    794       [ None    ⇒ 〈short_jump, instruction_size_jmplen short_jump instr〉
    795       | Some pl ⇒ 〈max_length old_length pl, instruction_size_jmplen (max_length old_length pl) instr〉
    796       ] in
    797       let new_added ≝ match add_instr with
    798       [ None   ⇒ inc_added
    799       | Some x ⇒ plus inc_added (minus isize old_size)
    800       ] in
    801       〈new_added, 〈plus inc_pc isize,
    802        bvt_insert … (bitvector_of_nat ? (S (|prefix|))) 〈inc_pc+isize, new_length〉 inc_sigma〉〉
    803     ) 〈0, 〈0, bvt_insert … (bitvector_of_nat 16 0) 〈0, short_jump〉 (Stub ??)〉〉) in
    804     if geb (\fst final_policy) 2^16 then
    805       〈eqb final_added 0, None ?〉
    806     else
    807       〈eqb final_added 0, Some ? final_policy〉.
    808 [ normalize nodelta cases daemon (* XXX nec_plus_ultra *)
    809 | normalize nodelta lapply p generalize in match (foldl_strong ?????); * #x #H #H2
    810   >H2 in H; normalize nodelta -H2 -x #H @conj
    811   [ @conj
    812     [ @conj
    813       [ @conj
    814         [ @(proj1 ?? (proj1 ?? (proj1 ?? H)))
    815         | cases daemon (* XXX policy_compact_unsafe → policy_compact *)
    816         ]
    817       | @(proj2 ?? (proj1 ?? H))
    818       ]
    819     | #H2 @(proj2 ?? H) @eqb_true_to_eq @H2
    820     ]
    821   | @not_le_to_lt @leb_false_to_not_le <geb_to_leb @p1
    822   ]
    823 |4: lapply (pi2 ?? acc) >p cases inc_pc_sigma #inc_pc #inc_sigma
    824   lapply (refl ? (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉))
    825   cases (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in ⊢ (???% → %);
    826   #old_pc #old_length #Holdeq #Hpolicy @pair_elim #added #policy normalize nodelta
    827   @pair_elim #new_length #isize normalize nodelta #Heq1 #Heq2
    828   @conj [ @conj [ @conj [ @conj [ @conj
    829   [ (* out_of_program_none *) #i >append_length <commutative_plus #Hi normalize in Hi; #Hi2
    830     cases instr in Heq2; normalize nodelta
    831     #x [6: #y] #H <(proj2 ?? (pair_destruct ?????? H)) >lookup_opt_insert_miss
    832     [1,3,5,7,9,11: @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i ? Hi2)
    833       @le_S_to_le @Hi
    834     |2,4,6,8,10,12: @bitvector_of_nat_abs
    835       [1,4,7,10,13,16: @Hi2
    836       |2,5,8,11,14,17: @(transitive_lt … Hi2) @Hi
    837       |3,6,9,12,15,18: @sym_neq @lt_to_not_eq @Hi
    838       ]
    839     ]
    840   | (* jump_not_in_policy *) #i >append_length <commutative_plus #Hi normalize in Hi;
    841      cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    842      [ <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
    843       [ >(nth_append_first ? i prefix ?? Hi)
    844         @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i Hi)
    845       | @bitvector_of_nat_abs
    846         [ @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length >commutative_plus
    847           @le_plus_a @Hi
    848         | @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm
    849           @le_plus_n_r
    850         | @lt_to_not_eq @le_S_S @Hi
    851         ]
    852       ]
    853      | <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit
    854        cases instr in Heq1;
    855        [2,3,6: #x [3: #y] normalize nodelta #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl
    856        |4,5: #x normalize nodelta #Heq1 #H @⊥ cases H #H @H >nth_append_second
    857          [1,3: <minus_n_n whd in match (nth ????); / by I/
    858          |2,4: @le_n
    859          ]
    860        |1: #pi >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????); cases pi
    861          [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
    862            [1,2,3,6,7,24,25: #x #y
    863            |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] normalize nodelta #Heq1
    864              <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl
    865            |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] normalize nodelta
    866              #_ #H @⊥ cases H #H2 @H2 / by I/
    867            ]
    868          ]
    869        ]
    870      ]
    871   | (* policy_increase *) #i >append_length >commutative_plus #Hi normalize in Hi;
    872     cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi; #Hi
    873     [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i Hi)
    874       <(proj2 ?? (pair_destruct ?????? Heq2))     
    875       @pair_elim #opc #oj #EQ1 >lookup_insert_miss
    876       [ @pair_elim #pc #j #EQ2 / by /
    877       | @bitvector_of_nat_abs
    878         [ @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S >commutative_plus
    879           @le_plus_a @Hi
    880         | @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm @le_plus_n_r
    881         | @lt_to_not_eq @le_S_S @Hi
    882         ]
    883       ]
    884     | >Hi <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_hit
    885       cases (dec_is_jump instr)
    886       [ cases instr in Heq1; normalize nodelta
    887         [ #pi cases pi
    888           [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
    889             [1,2,3,6,7,24,25: #x #y
    890             |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] #_ #Hj cases Hj
    891           |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
    892             whd in match jump_expansion_step_instruction; normalize nodelta #Heq1
    893             <(proj1 ?? (pair_destruct ?????? Heq1)) #_ >Holdeq normalize nodelta
    894             @jmpleq_max_length
    895           ]
    896         |2,3,6: #x [3: #y] #_ #Hj cases Hj
    897         |4,5: #x #Heq1 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) >Holdeq normalize nodelta
    898           @jmpleq_max_length
    899         ]
    900       | lapply Heq1 -Heq1; lapply (refl ? instr); cases instr in ⊢ (???% → %); normalize nodelta
    901         [ #pi cases pi
    902           [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
    903             [1,2,3,6,7,24,25: #x #y
    904             |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    905             whd in match jump_expansion_step_instruction; normalize nodelta #Heqi #Heq1
    906             #Hj <(proj1 ?? (pair_destruct ?????? Heq1))
    907             lapply (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))) (|prefix|) ??)
    908             [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82:
    909               >prf >nth_append_second
    910               [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:
    911                 <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj
    912               |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
    913                 @le_n
    914               ]
    915             |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83:
    916               >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    917             |3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84:
    918               cases (lookup ?? (bitvector_of_nat ? (S (|prefix|))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)
    919               #a #b #H >H normalize nodelta %2 @refl
    920             ]
    921           |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
    922             #_ #_ #abs cases abs #ABS @⊥ @ABS / by I/
    923           ]
    924         |2,3,6: #x [3: #y] #Heqi #Heq1 #Hj <(proj1 ?? (pair_destruct ?????? Heq1))
    925           lapply (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))) (|prefix|) ??)
    926           [1,4,7: >prf >nth_append_second
    927             [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj
    928             |2,4,6: @le_n
    929             ]
    930           |2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    931           |3,6,9: cases (lookup ?? (bitvector_of_nat ? (S (|prefix|))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)
    932             #a #b #H >H normalize nodelta %2 @refl
    933           ]
    934         |4,5: #x #_ #_ #abs cases abs #ABS @⊥ @ABS / by I/
    935         ]
    936       ]
    937     ]
    938   ]
    939   | (* policy_compact_unsafe *) (*XXX*) cases daemon
    940   ]
    941   | (* 0 ↦ 0 *) <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_opt_insert_miss
    942     [ @(proj2 ?? (proj1 ?? Hpolicy))
    943     | @bitvector_of_nat_abs
    944       [ / by /
    945       | @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm
    946         @le_S_S @le_plus_n_r
    947       | @lt_to_not_eq / by /
    948       ]
    949     ]
    950   ]
    951   | (* added = 0 → policy_equal *) lapply (proj2 ?? Hpolicy)
    952     lapply Heq2 -Heq2 lapply Heq1 -Heq1 lapply (refl ? instr)
    953     cases instr in ⊢ (???% → % → % → %); normalize nodelta
    954     [ #pi cases pi normalize nodelta
    955       [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
    956         [1,2,3,6,7,24,25: #x #y
    957         |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    958         #Hins #Heq1 #Heq2 #Hold <(proj1 ?? (pair_destruct ?????? Heq2)) #Hadded
    959         #i >append_length >commutative_plus #Hi normalize in Hi;
    960         cases (le_to_or_lt_eq … Hi) -Hi #Hi
    961         [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:
    962           <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
    963           [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:
    964             @(Hold Hadded i (le_S_S_to_le … Hi))
    965           |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
    966             @bitvector_of_nat_abs
    967             [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82:
    968               @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus
    969               @le_S_S @le_plus_a @le_S_S_to_le @Hi
    970             |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83:
    971               @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm @le_S_S
    972               @le_plus_n_r
    973             |3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84:
    974               @lt_to_not_eq @Hi
    975             ]
    976           ]
    977         |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
    978            <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit
    979            lapply (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))) (|prefix|) ??)
    980            [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82:
    981              >prf >nth_append_second
    982              [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:
    983                <minus_n_n whd in match (nth ????); >p1 >Hins @nmk #H @H
    984              |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
    985                @le_n
    986              ]
    987            |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83:
    988              >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    989            |3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84:
    990              cases (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)
    991              #a #b #H >H <(proj1 ?? (pair_destruct ?????? Heq1)) normalize nodelta @refl
    992            ]
    993          ]
    994        |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Hins #Heq1 #Heq2 #Hold
    995          <(proj1 ?? (pair_destruct ?????? Heq2)) <(proj2 ?? (pair_destruct ?????? Heq1))
    996          #H #i >append_length >commutative_plus #Hi normalize in Hi;
    997          cases (le_to_or_lt_eq … Hi) -Hi #Hi
    998          [1,3,5,7,9,11,13,15,17: <(proj2 ?? (pair_destruct ?????? Heq2))
    999            >lookup_insert_miss
    1000            [1,3,5,7,9,11,13,15,17: @(Hold ? i (le_S_S_to_le … Hi))
    1001              [1,2,3,4,5,6,7,8,9: @sym_eq @le_n_O_to_eq <H @le_plus_n_r]
    1002            ]
    1003            @bitvector_of_nat_abs
    1004            [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf
    1005              >append_length >commutative_plus @le_S_S @le_plus_a @le_S_S_to_le @Hi
    1006            |2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf
    1007              >append_length @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
    1008            |3,6,9,12,15,18,21,24,27: @lt_to_not_eq @Hi
    1009            ]
    1010          |2,4,6,8,10,12,14,16,18: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi
    1011            >lookup_insert_hit <(proj1 ?? (pair_destruct ?????? Heq1))
    1012            >Holdeq normalize nodelta @sym_eq @blerpque
    1013            [3,6,9,12,15,18,21,24,27:
    1014              elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … H)))
    1015              [1,3,5,7,9,11,13,15,17: #H @⊥ @(absurd ? H) @le_to_not_lt @etblorp
    1016              |2,4,6,8,10,12,14,16,18: #H @H
    1017              ]
    1018              / by I/
    1019            |2,5,8,11,14,17,20,23,26: / by I/
    1020            ]
    1021          ]
    1022        ]
    1023      |2,3,6: #x [3: #y] #Hins #Heq1 #Heq2 #Hold <(proj1 ?? (pair_destruct ?????? Heq2))
    1024        #Hadded #i >append_length >commutative_plus #Hi normalize in Hi;
    1025        cases (le_to_or_lt_eq …Hi) -Hi #Hi
    1026        [1,3,5: <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
    1027          [1,3,5: @(Hold Hadded i (le_S_S_to_le … Hi))
    1028          |2,4,6: @bitvector_of_nat_abs
    1029            [1,4,7: @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus
    1030              @le_S_S @le_plus_a @le_S_S_to_le @Hi
    1031            |2,5,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm
    1032              @le_S_S @le_plus_n_r
    1033            |3,6,9: @lt_to_not_eq @Hi
    1034            ]
    1035          ]
    1036        |2,4,6: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit
    1037          lapply (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))) (|prefix|) ??)
    1038          [1,4,7: >prf >nth_append_second
    1039            [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Hins @nmk #H @H
    1040            |2,4,6: @le_n
    1041            ]
    1042          |2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    1043          |3,6,9: cases (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)
    1044            #a #b #H >H <(proj1 ?? (pair_destruct ?????? Heq1)) normalize nodelta @refl
    1045          ]
    1046        ]
    1047      |4,5: #x #Hins #Heq1 #Heq2 #Hold
    1048        <(proj1 ?? (pair_destruct ?????? Heq2)) <(proj2 ?? (pair_destruct ?????? Heq1))
    1049        #H #i >append_length >commutative_plus #Hi normalize in Hi;
    1050        cases (le_to_or_lt_eq … Hi) -Hi #Hi
    1051        [1,3: <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
    1052          [1,3: @(Hold ? i (le_S_S_to_le … Hi))
    1053            [1,2: @sym_eq @le_n_O_to_eq <H @le_plus_n_r]
    1054          ]
    1055          @bitvector_of_nat_abs
    1056          [1,4: @(transitive_lt … (pi2 ?? program)) >prf
    1057            >append_length >commutative_plus @le_S_S @le_plus_a @le_S_S_to_le @Hi
    1058          |2,5: @(transitive_lt … (pi2 ?? program)) >prf
    1059            >append_length @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
    1060          |3,6: @lt_to_not_eq @Hi
    1061          ]
    1062          |2,4: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit
    1063            <(proj1 ?? (pair_destruct ?????? Heq1))>Holdeq normalize nodelta
    1064            @sym_eq @blerpque
    1065            [3,6: elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … H)))
    1066              [1,3: #H @⊥ @(absurd ? H) @le_to_not_lt @etblorp
    1067              |2,4: #H @H
    1068              ]
    1069              / by I/
    1070            |2,5: / by I/
    1071            ]
    1072          ]
    1073        ]
    1074      ]
    1075 | normalize nodelta @conj [ @conj [ @conj [ @conj [ @conj
    1076   [ #i cases i
    1077     [ #Hi @⊥ @(absurd ? Hi) @le_to_not_lt / by /
    1078     | -i #i #Hi #Hi2 >lookup_opt_insert_miss
    1079       [ / by refl/
    1080       | @bitvector_of_nat_abs
    1081         [ @Hi2
    1082         | / by /
    1083         | @sym_neq @lt_to_not_eq / by /
    1084         ]
    1085       ]
    1086     ] 
    1087   | #i cases i
    1088     [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    1089     | -i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O
    1090     ]
    1091   ]
    1092   | #i cases i
    1093     [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    1094     | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    1095     ]
    1096   ]
    1097   | #i cases i
    1098     [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    1099     | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    1100     ]
    1101   ]
    1102   | >lookup_opt_insert_hit @refl
    1103   ]
    1104   | #_ #i cases i
    1105     [ #Hi >lookup_insert_hit
    1106       >(lookup_opt_lookup_hit … (proj2 ?? (proj1 ?? (pi2 ?? old_sigma))) 〈0,short_jump〉)
    1107       @refl
    1108     | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    1109     ]
    1110   ]
    1111 ]
    1112 qed.
    1113    
    11147let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (S (|l|)) 2^16) (n: ℕ)
    11158  on n:(Σx:bool × (option ppc_pc_map).
    11169    let 〈c,pol〉 ≝ x in
    1117     match pol with
     10    And
     11    (match pol with
    111812    [ None ⇒ True
    111913    | Some x ⇒
     
    112216        (jump_not_in_policy program x))
    112317        (n > 0 → policy_compact program (create_label_map program) x))
    1124         (bvt_lookup_opt … (bitvector_of_nat ? 0) (\snd x) = Some ? 〈0,short_jump〉))
     18        (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd x) 〈0,short_jump〉) = 0))
    112519        (\fst x < 2^16)
    1126     ])
     20    ]) (n = 0 → c = true))
    112721  let labels ≝ create_label_map program in
    1128   match n with
    1129   [ O   ⇒ 〈true,pi1 ?? (jump_expansion_start program labels)〉
    1130   | S m ⇒ let 〈ch,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in
     22  match n return λx.n = x → Σa:bool × (option ppc_pc_map).? with
     23  [ O   ⇒ λp.〈true,pi1 ?? (jump_expansion_start program labels)〉
     24  | S m ⇒ λp.let 〈ch,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in
    113125          match z return λx. z=x → Σa:bool × (option ppc_pc_map).? with
    113226          [ None    ⇒ λp2.〈false,None ?〉
    113327          | Some op ⇒ λp2.if ch
    113428            then pi1 ?? (jump_expansion_step program labels «op,?»)
    1135             else (jump_expansion_internal program m)
     29            else pi1 ?? (jump_expansion_internal program m)
    113630          ] (refl … z)
    1137   ].
     31  ] (refl … n).
    113832[ normalize nodelta cases (jump_expansion_start program (create_label_map program))
    1139   #x cases x -x 
    1140   [ / by I/
    1141   | #sigma normalize nodelta #H @conj [ @conj [ @conj
     33  #x cases x -x
     34  [ #H @conj / by I/
     35  | #sigma normalize nodelta #H @conj [ @conj [ @conj [ @conj
    114236    [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
    1143     | #H @⊥ @(absurd ? H) @le_to_not_lt @le_n
     37    | >p #H @⊥ @(absurd ? H) @le_to_not_lt @le_n
    114438    ]
    114539    | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
    114640    ]
    1147     | @(proj2 ?? H) ]
    1148   ]
    1149 | cases daemon
    1150 | lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta / by /
    1151 | lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta
    1152   #H @conj [ @conj [ @(proj1 ?? (proj1 ?? (proj1 ?? H))) |  @(proj2 ?? (proj1 ?? H)) ] | @(proj2 ?? H) ]
    1153 | normalize nodelta cases (jump_expansion_step program labels «op,?»)
     41    | @(proj2 ?? H)
     42    ]
     43    | / by /
     44    ]
     45  ]
     46| normalize nodelta @conj [ / by I/ | >p #H destruct (H) ]
     47| cases ch in p1; #p1
     48  [ normalize nodelta
     49    cases (jump_expansion_step program (create_label_map program) «op,?»)
     50    #x cases x -x #ch2 #z2 cases z2 normalize nodelta
     51    [ #_ @conj [ / by I/ | >p #H2 destruct (H2) ]
     52    | #j2 #H2 @conj [ @conj [ @conj [ @conj
     53      [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))))
     54      | #_ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))
     55      ]
     56      | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))
     57      ]
     58      | @(proj2 ?? H2)
     59      ]
     60      | >p #H3 destruct (H3)
     61      ]
     62    ]
     63  | normalize nodelta lapply (pi2 ?? (jump_expansion_internal program m))
     64    <p1 >p2 normalize nodelta #H @conj [ @conj [ @conj [ @conj
     65    [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
     66    | >p #Hm cases (le_to_or_lt_eq … Hm) -Hm #Hm
     67      [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) @(le_S_S_to_le … Hm)
     68      | lapply ((proj2 ?? H) (sym_eq … (injective_S … Hm))) #H2 destruct (H2)
     69      ]
     70    ]
     71    | @(proj2 ?? (proj1 ?? (proj1 ?? H)))
     72    ]
     73    | @(proj2 ?? (proj1 ?? H))
     74    ]
     75    | >p #H2 destruct (H2)
     76    ]
     77  ]
     78| cases (jump_expansion_internal program m) in p1;
    115479  #p cases p -p #p #r cases r normalize nodelta
    1155   [ #H / by I/
    1156   | #j #H @conj
    1157     [ @conj
    1158       [ @conj
    1159         [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
    1160         | cases daemon
    1161         ]
    1162       | @(proj2 ?? (proj1 ?? (proj1 ?? H)))
    1163       ]
    1164     | @(proj2 ?? H)
     80  [ #_ >p2 #ABS destruct (ABS)
     81  | #map >p2 normalize nodelta
     82    #H #eq destruct (eq) @conj [ @conj
     83    [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
     84    | @(proj2 ?? (proj1 ?? (proj1 ?? H)))
     85    ]
     86    | @(proj2 ?? (proj1 ?? H))
    116587    ]
    116688  ]
     
    1242164 #x1 cases x1 #p1 #j1 -x1; #H1 #Heqj #Hj #k elim k
    1243165[ <plus_n_O >Heqj @Hj
    1244 | #k' -k <plus_n_Sm whd in match (jump_expansion_internal program (S (n+k')));
     166| #k' -k <plus_n_Sm (*whd in match (jump_expansion_internal program (S (n+k')));*)
    1245167  lapply (refl ? (jump_expansion_internal program (n+k')))
    1246   cases (jump_expansion_internal program (n+k')) in ⊢ (???% → % → %);
     168  cases (jump_expansion_internal program (n+k')) in ⊢ (???% → %);
    1247169  #x2 cases x2 -x2 #c2 #p2 normalize nodelta #H #Heqj2
    1248170  cases p2 in H Heqj2;
     
    1288210 match program with
    1289211 [ nil      ⇒ acc
    1290  | cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (S (|t|))) (\snd policy) 〈0,short_jump〉)) with
     212 | cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)) with
    1291213   [ long_jump   ⇒ measure_int t policy (acc + 2)
    1292214   | medium_jump ⇒ measure_int t policy (acc + 1)
     
    1302224  [ / by refl/
    1303225  | #h #t #Hd #x whd in match (measure_int ???); whd in match (measure_int ?? x);
    1304     cases (\snd (bvt_lookup … (bitvector_of_nat ? (S (|t|))) (\snd policy) 〈0,short_jump〉))
     226    cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉))
    1305227    [ normalize nodelta @Hd
    1306228    |2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus
     
    1316238[ normalize @le_n
    1317239| #h #t #Hind whd in match (measure_int ???);
    1318   cases (\snd (lookup ?? (bitvector_of_nat ? (S (|t|))) (\snd policy) 〈0,short_jump〉))
     240  cases (\snd (lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉))
    1319241  [ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/
    1320242  |2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?)
     
    1329251    out_of_program_none program p ∧
    1330252    jump_not_in_policy program p ∧
    1331     lookup_opt … (bitvector_of_nat ? 0) (\snd p) = Some ? 〈0,short_jump〉
     253    \fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0
    1332254    \fst p < 2^16.
    1333255  ∀l.|l| ≤ |program| → ∀acc:ℕ.
     
    1343265  [ / by I/
    1344266  | #x normalize nodelta #Hx #Hjeq
    1345     lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx)))) (|t|) Hp)
     267    lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx))))) (|t|) Hp)
    1346268    whd in match (measure_int ???); whd in match (measure_int ? x ?);
    1347     cases (bvt_lookup ?? (bitvector_of_nat ? (S (|t|))) (\snd (pi1 ?? policy)) 〈0,short_jump〉)
    1348     #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? (S (|t|))) (\snd x) 〈0,short_jump〉)
     269    cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd (pi1 ?? policy)) 〈0,short_jump〉)
     270    #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd x) 〈0,short_jump〉)
    1349271    #y1 #y2 normalize nodelta #Hblerp cases Hblerp cases x2 cases y2
    1350272    [1,4,5,7,8,9: #H cases H
     
    1380302  measure_int program policy 0 = 2*|program| → ∀i.i<|program| →
    1381303  is_jump (\snd (nth i ? program 〈None ?,Comment []〉)) →
    1382   (\snd (bvt_lookup ?? (bitvector_of_nat ? (S i)) (\snd policy) 〈0,short_jump〉)) = long_jump.
     304  (\snd (bvt_lookup ?? (bitvector_of_nat ? i) (\snd policy) 〈0,short_jump〉)) = long_jump.
    1383305#program #policy elim program in ⊢ (% → ∀i.% → ? → %);
    1384306[ #Hm #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
     
    1387309  [ #Hi @Hind
    1388310    [ whd in match (measure_int ???) in Hm;
    1389       cases (\snd (bvt_lookup … (bitvector_of_nat ? (S (|t|))) (\snd policy) 〈0,short_jump〉)) in Hm;
     311      cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)) in Hm;
    1390312      normalize nodelta
    1391313      [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/
     
    1398320    ]
    1399321  | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm;
    1400     cases (\snd (bvt_lookup … (bitvector_of_nat ? (S (|t|))) (\snd policy) 〈0,short_jump〉)) in Hm;
     322    cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)) in Hm;
    1401323    normalize nodelta
    1402324    [ #Hm @⊥ @(absurd ? (measure_le t policy)) >Hm @lt_to_not_le /2 by lt_plus, le_n/
     
    1413335  ∀policy:Σp:ppc_pc_map.
    1414336    out_of_program_none program p ∧ jump_not_in_policy program p ∧
    1415     bvt_lookup_opt … (bitvector_of_nat ? 0) (\snd p) = Some ? 〈0,short_jump〉
     337    \fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0
    1416338    \fst p < 2^16.
    1417339  match (\snd (pi1 ?? (jump_expansion_step program (create_label_map program) policy))) with
     
    1426348      measure_int x policy 0 = measure_int x p 0 →
    1427349      policy_equal x policy p) ?? (pi1 ?? program))
    1428  [ #_ #_ #i #Hi <(le_n_O_to_eq … Hi)
    1429    >(lookup_opt_lookup_hit … 〈0,short_jump〉 (proj2 ?? (proj1 ?? (proj1 ?? Hpol))))
    1430    >(lookup_opt_lookup_hit … 〈0,short_jump〉 (proj2 ?? (proj1 ?? (pi2 ?? policy))))
    1431    / by refl/
    1432  | #h #t #Hind #Hp #Hm #i #Hi cases (le_to_or_lt_eq … Hi) -Hi;
    1433    [ #Hi @Hind
     350 [ #_ #_ #i #Hi @⊥ @(absurd ? Hi) @le_to_not_lt @le_O_n
     351 | #h #t #Hind #Hp #Hm #i #Hi cases (le_to_or_lt_eq … (le_S_S_to_le …  Hi)) -Hi #Hi
     352   [ @Hind
    1434353     [ @(transitive_le … Hp) / by /
    1435354     | whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm;
    1436        lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (|t|) Hp) #Hinc
    1437        cases (bvt_lookup ?? (bitvector_of_nat ? (S (|t|))) ? 〈0,short_jump〉) in Hm Hinc; #x1 #x2
    1438        cases (bvt_lookup ?? (bitvector_of_nat ? (S (|t|))) ? 〈0,short_jump〉); #y1 #y2
     355       lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol))))) (|t|) Hp) #Hinc
     356       cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉) in Hm Hinc; #x1 #x2
     357       cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉); #y1 #y2
    1439358       #Hm #Hinc lapply Hm -Hm; lapply Hinc -Hinc; normalize nodelta
    1440359       cases x2 cases y2 normalize nodelta
     
    1454373         #_ #H @(injective_plus_r … H)
    1455374       ]
    1456      | @(le_S_S_to_le … Hi)
     375     | @Hi
    1457376     ]
    1458    | #Hi >Hi whd in match (measure_int ???) in Hm;
    1459      whd in match (measure_int ? p ?) in Hm;
    1460      lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (|t|) Hp)
    1461      cases (bvt_lookup ?? (bitvector_of_nat ? (S (|t|))) ? 〈0,short_jump〉) in Hm;
     377   | >Hi whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm;
     378     lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol))))) (|t|) Hp)
     379     cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉) in Hm;
    1462380     #x1 #x2
    1463      cases (bvt_lookup ?? (bitvector_of_nat ? (S (|t|))) ? 〈0,short_jump〉);
    1464      #y1 #y2
     381     cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉); #y1 #y2
    1465382     normalize nodelta cases x2 cases y2 normalize nodelta
    1466383     [1,5,9: #_ #_ @refl
     
    1506423   [ / by refl/
    1507424   | #h #t #Hind #Hp whd in match (measure_int ???);
    1508      elim (proj2 ?? (proj1 ?? (proj1 ?? Hpl)) (S (|t|)) Hp)
     425     elim (proj2 ?? (proj1 ?? (proj1 ?? Hpl)) (|t|) (le_S_to_le … Hp))
    1509426     #pc #Hpc >(lookup_opt_lookup_hit … Hpc 〈0,short_jump〉) normalize nodelta @Hind
    1510427     @(transitive_le … Hp) @le_n_Sn
    1511428   ]
    1512  ]   
     429 ]
    1513430qed.
    1514431
     
    1528445    #c #pol #Hp cases pol
    1529446    [ normalize nodelta //
    1530     | #x normalize nodelta #H @conj [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
    1531     | #Hneq @(proj2 ?? (proj1 ?? (proj1 ?? H))) cases (pi1 ?? program) in Hneq;
     447    | #x normalize nodelta #H @conj [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
     448    | #Hneq @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) cases (pi1 ?? program) in Hneq;
    1532449      [ #H cases H #H @⊥ @H @refl
    1533450      | #h #t #_ / by /
     
    1561478      lapply (refl ? (jump_expansion_step program (create_label_map program) «Fp,?»))
    1562479      [ @conj [ @conj
    1563       [ @(proj1 ?? (proj1 ?? (proj1 ?? HFp)))
     480      [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))))
     481      | @(proj2 ?? (proj1 ?? (proj1 ?? HFp))) ]
    1564482      | @(proj2 ?? (proj1 ?? HFp)) ]
    1565       | @(proj2 ?? HFp) ]
    1566483      | lapply (measure_full program Fp ?)
    1567484        [ @le_to_le_to_eq
    1568485          [ @measure_le
    1569486          | cut (∀x:ℕ.x ≤ 2*|program| →
    1570              ∃p.(\snd (pi1 ?? (jump_expansion_internal program x)) = Some ? p ∧       
     487             ∃p.(\snd (pi1 ?? (jump_expansion_internal program x)) = Some ? p ∧
    1571488                x ≤ measure_int program p 0))
    1572489            [ #x elim x
     
    1601518                      #z cases z -z #xch #xpol normalize nodelta #H #H2 >(proj1 ?? H2) in H;
    1602519                      normalize nodelta #H @conj [ @conj
    1603                       [ @(proj1 ?? (proj1 ?? (proj1 ?? H)))
     520                      [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
     521                      | @(proj2 ?? (proj1 ?? (proj1 ?? H))) ]
    1604522                      | @(proj2 ?? (proj1 ?? H)) ]
    1605                       | @(proj2 ?? H) ]
    1606523                    | lapply (Hfa x (le_S_to_le … Hx)) lapply HeqSxpol -HeqSxpol
    1607                       whd in match (jump_expansion_internal program (S x));
    1608524                      lapply (refl ? (jump_expansion_internal program x))
    1609                       lapply Hxpol -Hxpol cases (jump_expansion_internal program x) in ⊢ (% → ???% → %);
     525                      lapply Hxpol -Hxpol
     526                      whd in match (jump_expansion_internal program (S x));
     527                      cases (jump_expansion_internal program x) in ⊢ (% → ???% → %);
    1610528                      #z cases z -z #xch #b normalize nodelta #H #Heq >(proj1 ?? Heq) in H;
    1611                       #H #Heq cases xch in Heq; #Heq normalize nodelta
     529                      #H #Heq2 cases xch in H Heq2; #H #Heq2 normalize nodelta
    1612530                      [ lapply (refl ? (jump_expansion_step program (create_label_map (pi1 ?? program)) «xpol,?»))
    1613531                        [ @conj [ @conj
    1614                           [ @(proj1 ?? (proj1 ?? (proj1 ?? H)))
     532                          [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
     533                          | @(proj2 ?? (proj1 ?? (proj1 ?? H))) ]
    1615534                          | @(proj2 ?? (proj1 ?? H)) ]
    1616                           | @(proj2 ?? H) ]
    1617535                        | cases (jump_expansion_step ???) in ⊢ (???% → %); #z cases z -z #a #c
    1618536                          normalize nodelta cases c normalize nodelta
     
    1621539                            [ / by /
    1622540                            | #H3 lapply (measure_special program «xpol,?»)
    1623                               [ @conj [ @conj
    1624                                 [ @(proj1 ?? (proj1 ?? (proj1 ?? H)))
     541                              [ @conj [ @conj
     542                                [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
     543                                | @(proj2 ?? (proj1 ?? (proj1 ?? H))) ]
    1625544                                | @(proj2 ?? (proj1 ?? H)) ]
    1626                                 | @(proj2 ?? H) ]
    1627545                              | >Heq normalize nodelta #H4 @⊥ @(absurd … (H4 H3)) @Hfull
    1628546                              ]
     
    1632550                      | lapply (refl ? (jump_expansion_step program (create_label_map (pi1 ?? program)) «xpol,?»))
    1633551                        [ @conj [ @conj
    1634                           [ @(proj1 ?? (proj1 ?? (proj1 ?? H)))
     552                          [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
     553                          | @(proj2 ?? (proj1 ?? (proj1 ?? H))) ]
    1635554                          | @(proj2 ?? (proj1 ?? H)) ]
    1636                           | @(proj2 ?? H) ]
    1637555                        | cases (jump_expansion_step ???) in ⊢ (???% → %); #z cases z -z #a #c
    1638556                          normalize nodelta cases c normalize nodelta
     
    1654572          [ #H #EQ2 @⊥ @(absurd ?? H) @Hfull
    1655573          | #Gp #HGp #EQ2 cases Fch
    1656             [ normalize nodelta #i cases i
    1657               [ #_ >(lookup_opt_lookup_hit … (proj2 ?? (proj1 ?? HFp)) 〈0,short_jump〉)
    1658                 >(lookup_opt_lookup_hit … (proj2 ?? (proj1 ?? (proj1 ?? HGp))) 〈0,short_jump〉)
    1659                 / by refl/
    1660               | -i #i #Hi
    1661                 cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉))) #Hj
    1662                 [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))) i Hi)
    1663                   lapply (Hfull i Hi Hj)
    1664                   cases (bvt_lookup … (bitvector_of_nat ? (S i)) (\snd Fp) 〈0,short_jump〉)
    1665                   #fp #fj #Hfj >Hfj normalize nodelta
    1666                   cases (bvt_lookup … (bitvector_of_nat ? (S i)) (\snd Gp) 〈0,short_jump〉)
    1667                   #gp #gj cases gj normalize nodelta
    1668                   [1,2: #H cases H #H2 cases H2 destruct (H2)
    1669                   |3: #_ @refl
    1670                   ]
    1671                 | >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))) i Hi Hj)
    1672                   >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))) i Hi Hj) @refl
     574            [ normalize nodelta #i #Hi
     575              cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉))) #Hj
     576              [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))) i Hi)
     577                lapply (Hfull i Hi Hj)
     578                cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Fp) 〈0,short_jump〉)
     579                #fp #fj #Hfj >Hfj normalize nodelta
     580                cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Gp) 〈0,short_jump〉)
     581                #gp #gj cases gj normalize nodelta
     582                [1,2: #H cases H #H2 cases H2 destruct (H2)
     583                |3: #_ @refl
    1673584                ]
     585              | >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))))) i Hi Hj)
     586                >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp)))) i Hi Hj) @refl
    1674587              ]
    1675588            | normalize nodelta /2 by pe_int_refl/
     
    1688601  |2,3: #x #Hnpol #HSpol %2 @nmk whd in match (policy_equal ???); //
    1689602    #H destruct (H)
    1690   |4: #np #Hnp #Sp #HSp whd in match (policy_equal ???); @dec_bounded_forall #m
    1691     cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,short_jump〉)
    1692     #x1 #x2
    1693     cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,short_jump〉)
    1694     #y1 #y2 normalize nodelta
    1695     @dec_eq_jump_length 
     603  |4: #np #Hnp #Sp #HSp whd in match (policy_equal ???); cases program #p #_ cases p
     604    [ %1 #m #Hm @⊥ @(absurd ? Hm) @le_to_not_lt @le_O_n
     605    | #h #t elim (dec_bounded_forall ?? (|t|))
     606      [1: #Hyp %1 #m #Hm @(Hyp m) @(le_S_S_to_le … Hm)
     607      |2: #Hyp %2 @nmk #H @(absurd ?? Hyp) #m #Hm @(H m) @(le_S_S … Hm)
     608      | #m cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,short_jump〉)
     609        #x1 #x2
     610        cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,short_jump〉)
     611        #y1 #y2 normalize nodelta
     612        @dec_eq_jump_length
     613      ]
     614     
     615    ] 
    1696616  ]
    1697617]
Note: See TracChangeset for help on using the changeset viewer.