Changeset 1931 for src/ASM/Policy.ma


Ignore:
Timestamp:
May 9, 2012, 7:23:37 PM (8 years ago)
Author:
boender
Message:
  • added latest bvt alias
  • temporary "cases daemon" commit of new policy type
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r1886 r1931  
    33include "ASM/Fetch.ma".
    44include "ASM/Status.ma".
    5 include alias "basics/logic.ma".
    6 include alias "arithmetics/nat.ma".
    75include "utilities/extralib.ma".
    86include "ASM/Assembly.ma".
    97
     8(*include alias "common/Identifiers.ma".
     9include alias "ASM/BitVector.ma".*)
     10include alias "basics/lists/list.ma".
     11include alias "arithmetics/nat.ma".
     12include alias "basics/logic.ma".
     13
    1014(* Internal types *)
    1115
    12 (* label_map: identifier ↦ 〈instruction number, address〉 *)
    13 definition label_map ≝ identifier_map ASMTag (ℕ × ℕ).
    14 
    15 (* jump_expansion_policy: instruction number ↦ 〈pc, [addr, jump_length]〉 *)
    16 definition jump_expansion_policy ≝ ℕ × (BitVectorTrie (ℕ × ℕ × jump_length) 16).
     16(* label_map: identifier ↦ pseudo program counter *)
     17definition label_map ≝ identifier_map ASMTag .
     18
     19(* ppc_pc_map: program length × (pseudo program counter ↦ 〈pc, jump_length〉) *)
     20definition ppc_pc_map ≝ ℕ × (BitVectorTrie (ℕ × (option jump_length)) 16).
    1721
    1822(* The different properties that we want/need to prove at some point *)
    1923(* Anything that's not in the program doesn't end up in the policy *)
    20 definition out_of_program_none: list labelled_instruction → jump_expansion_policy → Prop ≝
    21   λprefix.λpolicy.
    22   ∀i.i ≥ |prefix| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) (\snd policy) = None ?.
     24definition out_of_program_none: list labelled_instruction → ppc_pc_map → Prop ≝
     25  λprefix.λsigma.
     26  ∀i:ℕ.i ≥ |prefix| → i < 2^16 → bvt_lookup_opt … (bitvector_of_nat 16 i) (\snd sigma) = None ?.
    2327
    2428(* If instruction i is a jump, then there will be something in the policy at
     
    4953  ].
    5054
    51 definition jump_in_policy: list labelled_instruction → jump_expansion_policy → Prop ≝
    52   λprefix.λpolicy.
     55definition is_jump_to ≝
     56  λx:pseudo_instruction.λd:Identifier.
     57  match x with
     58  [ Instruction i ⇒ match i with
     59    [ JC j ⇒ d = j
     60    | JNC j ⇒ d = j
     61    | JZ j ⇒ d = j
     62    | JNZ j ⇒ d = j
     63    | JB _ j ⇒ d = j
     64    | JNB _ j ⇒ d = j
     65    | CJNE _ j ⇒ d = j
     66    | DJNZ _ j ⇒ d = j
     67    | _ ⇒ False
     68    ]
     69  | Call c ⇒ d = c
     70  | Jmp j ⇒ d = j
     71  | _ ⇒ False
     72  ].
     73 
     74definition jump_in_policy: list labelled_instruction → ppc_pc_map → Prop ≝
     75  λprefix.λsigma.
    5376  ∀i:ℕ.i < |prefix| →
    5477  iff (is_jump (nth i ? prefix 〈None ?, Comment []〉))
    55    (∃p:ℕ.∃a:ℕ.∃j:jump_length.
    56      lookup_opt … (bitvector_of_nat 16 i) (\snd policy) = Some ? 〈p,a,j〉).
    57 
    58 definition labels_okay: label_map → jump_expansion_policy → Prop ≝
    59   λlabels.λpolicy.
    60   bvt_forall ?? (\snd policy) (λn.λx.
    61    let 〈pc,addr_nat,j〉 ≝ x in
    62    ∃id:Identifier.\snd (lookup_def … labels id 〈0,pc〉) = addr_nat
    63   ).
     78   (∃x:jump_length.
     79   \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,None ?〉) = Some ? x).
     80
     81(* if the instruction 〈p,a〉 is a jump to label l, then label l is at address a *)
     82(* definition labels_okay: label_map → ppc_pc_map → Prop ≝
     83  λlabels.λsigma.
     84  bvt_forall ?? (\snd sigma) (λn.λx.
     85   let 〈pc,addr_nat〉 ≝ x in
     86   ∃id:Identifier.lookup_def … labels id 0 = addr_nat
     87  ). *)
    6488 
    6589(* Between two policies, jumps cannot decrease *)
     
    83107  λj1.λj2.jmple j1 j2 ∨ j1 = j2.
    84108 
    85 definition policy_increase: list labelled_instruction → jump_expansion_policy
    86   jump_expansion_policy → Prop ≝
     109definition policy_increase: list labelled_instruction → ppc_pc_map
     110  ppc_pc_map → Prop ≝
    87111 λprogram.λop.λp.
    88   (∀i:ℕ.i < |program| →
    89     let 〈pc1,i1,oj〉 ≝ bvt_lookup ?? (bitvector_of_nat ? i) (\snd op) 〈0,0,short_jump〉 in
    90     let 〈pc2,i2,j〉 ≝ bvt_lookup ?? (bitvector_of_nat ? i) (\snd p) 〈0,0,short_jump〉 in
    91     jmpleq oj j
    92   ).
     112 ∀i.i < |program| →
     113   let 〈opc,ox〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd op) 〈0,None ?〉 in
     114   let 〈pc,x〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,None ?〉 in
     115     opc ≤ pc ∧
     116     match ox with
     117     [ Some oj ⇒
     118       match x with
     119       [ Some j ⇒ jmpleq oj j
     120       | _ ⇒ True
     121       ]
     122     | _ ⇒ True
     123     ].
    93124
    94125(* Policy safety *)
    95 definition policy_safe: jump_expansion_policy → Prop ≝
    96  λpolicy.
    97  bvt_forall ?? (\snd policy) (λn.λx.let 〈pc_nat,addr_nat,jmp_len〉 ≝ x in
    98    match jmp_len with
    99    [ short_jump  ⇒ if leb pc_nat addr_nat
    100       then le (addr_nat - pc_nat) 126
    101       else le (pc_nat - addr_nat) 129
    102    | medium_jump ⇒   
    103       let addr ≝ bitvector_of_nat 16 addr_nat in
    104       let pc ≝ bitvector_of_nat 16 pc_nat in
    105       let 〈fst_5_addr, rest_addr〉 ≝ split bool 5 11 addr in
    106       let 〈fst_5_pc, rest_pc〉 ≝ split bool 5 11 pc in
    107       eq_bv 5 fst_5_addr fst_5_pc = true
    108    | long_jump   ⇒ True
    109    ]
    110  ).
     126definition policy_safe: list labelled_instruction → label_map → ppc_pc_map → Prop ≝
     127 λprogram.λlabels.λsigma.
     128 ∀i.i < |program| →
     129 let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,None ?〉 in
     130 let 〈label,instr〉 ≝ nth i ? program 〈None ?, Comment [ ]〉 in
     131 ∀dest.is_jump_to instr dest →
     132   let paddr ≝ lookup_def … labels dest 0 in
     133   let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd sigma) 〈0,None ?〉) in
     134   match j with
     135   [ None ⇒ True
     136   | Some j ⇒ match j with
     137     [ short_jump  ⇒
     138        if leb pc addr
     139        then le (addr - pc) 126
     140        else le (pc - addr) 129
     141     | medium_jump ⇒   
     142        let a ≝ bitvector_of_nat 16 addr in
     143        let p ≝ bitvector_of_nat 16 pc in
     144        let 〈fst_5_addr, rest_addr〉 ≝ split bool 5 11 a in
     145        let 〈fst_5_pc, rest_pc〉 ≝ split bool 5 11 p in
     146        eq_bv 5 fst_5_addr fst_5_pc = true
     147     | long_jump   ⇒ True
     148     ]
     149   ].
     150
     151(* this is the instruction size as determined by the distance from origin to destination *)
     152definition instruction_size_sigma: label_map → ppc_pc_map → Word → pseudo_instruction → ℕ ≝
     153 λlabels.λsigma.λpc.λi.
     154 \fst (assembly_1_pseudoinstruction
     155   (λid.bitvector_of_nat 16 (lookup_def … labels id 0))
     156   (λi.bitvector_of_nat 16 (\fst (bvt_lookup ?? i (\snd sigma) 〈0,None ?〉))) pc
     157   (λx.zero 16) i).
     158 
     159(* this is the instruction size as determined by the jump length given *)
     160definition expand_relative_jump_internal_unsafe:
     161  jump_length → ([[relative]] → preinstruction [[relative]]) → list instruction ≝
     162  λjmp_len:jump_length.λi.
     163  match jmp_len with
     164  [ short_jump ⇒ [ RealInstruction (i (RELATIVE (zero 8))) ]
     165  | medium_jump ⇒ [ ] (* XXX this should not happen *)
     166  | long_jump ⇒
     167    [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2)));
     168      SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *)
     169      LJMP (ADDR16 (zero 16))
     170    ]
     171  ].
     172 @I
     173qed.
     174
     175definition expand_relative_jump_unsafe:
     176  jump_length → preinstruction Identifier → list instruction ≝
     177  λjmp_len:jump_length.λi.
     178  match i with
     179  [ JC jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JC ?)
     180  | JNC jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNC ?)
     181  | JB baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JB ? baddr)
     182  | JZ jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JZ ?)
     183  | JNZ jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNZ ?)
     184  | JBC baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JBC ? baddr)
     185  | JNB baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNB ? baddr)
     186  | CJNE addr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (CJNE ? addr)
     187  | DJNZ addr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (DJNZ ? addr)
     188  | ADD arg1 arg2 ⇒ [ ADD ? arg1 arg2 ]
     189  | ADDC arg1 arg2 ⇒ [ ADDC ? arg1 arg2 ]
     190  | SUBB arg1 arg2 ⇒ [ SUBB ? arg1 arg2 ]
     191  | INC arg ⇒ [ INC ? arg ]
     192  | DEC arg ⇒ [ DEC ? arg ]
     193  | MUL arg1 arg2 ⇒ [ MUL ? arg1 arg2 ]
     194  | DIV arg1 arg2 ⇒ [ DIV ? arg1 arg2 ]
     195  | DA arg ⇒ [ DA ? arg ]
     196  | ANL arg ⇒ [ ANL ? arg ]
     197  | ORL arg ⇒ [ ORL ? arg ]
     198  | XRL arg ⇒ [ XRL ? arg ]
     199  | CLR arg ⇒ [ CLR ? arg ]
     200  | CPL arg ⇒ [ CPL ? arg ]
     201  | RL arg ⇒ [ RL ? arg ]
     202  | RR arg ⇒ [ RR ? arg ]
     203  | RLC arg ⇒ [ RLC ? arg ]
     204  | RRC arg ⇒ [ RRC ? arg ]
     205  | SWAP arg ⇒ [ SWAP ? arg ]
     206  | MOV arg ⇒ [ MOV ? arg ]
     207  | MOVX arg ⇒ [ MOVX ? arg ]
     208  | SETB arg ⇒ [ SETB ? arg ]
     209  | PUSH arg ⇒ [ PUSH ? arg ]
     210  | POP arg ⇒ [ POP ? arg ]
     211  | XCH arg1 arg2 ⇒ [ XCH ? arg1 arg2 ]
     212  | XCHD arg1 arg2 ⇒ [ XCHD ? arg1 arg2 ]
     213  | RET ⇒ [ RET ? ]
     214  | RETI ⇒ [ RETI ? ]
     215  | NOP ⇒ [ RealInstruction (NOP ?) ]
     216  ].
     217
     218definition instruction_size_jmplen:
     219 jump_length → pseudo_instruction → ℕ ≝
     220  λjmp_len.
     221  λi.
     222  let pseudos ≝ match i with
     223  [ Cost cost ⇒ [ ]
     224  | Comment comment ⇒ [ ]
     225  | Call call ⇒
     226    match jmp_len with
     227    [ short_jump ⇒ [ ] (* XXX this should not happen *)
     228    | medium_jump ⇒ [ ACALL (ADDR11 (zero 11)) ]
     229    | long_jump ⇒ [ LCALL (ADDR16 (zero 16)) ]
     230    ]
     231  | Mov d trgt ⇒
     232     [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, DATA16 (zero 16)〉))))]
     233  | Instruction instr ⇒ expand_relative_jump_unsafe jmp_len instr
     234  | Jmp jmp ⇒
     235    match jmp_len with
     236    [ short_jump ⇒ [ SJMP (RELATIVE (zero 8)) ]
     237    | medium_jump ⇒ [ AJMP (ADDR11 (zero 11)) ]
     238    | long_jump ⇒ [ LJMP (ADDR16 (zero 16)) ]
     239    ]
     240  ] in
     241  let mapped ≝ map ? ? assembly1 pseudos in
     242  let flattened ≝ flatten ? mapped in
     243  let pc_len ≝ length ? flattened in
     244    pc_len.
     245 @I.
     246qed.
     247
     248(* new safety condition: policy corresponds to program and resulting program is compact *)
     249definition policy_compact: list labelled_instruction → label_map → ppc_pc_map → Prop ≝
     250 λprogram.λlabels.λsigma.
     251 ∀n:ℕ.S n < |program| →
     252  match bvt_lookup_opt … (bitvector_of_nat ? n) (\snd sigma) with
     253  [ None ⇒ False
     254  | Some x ⇒ let 〈pc,j〉 ≝ x in
     255    match bvt_lookup_opt … (bitvector_of_nat ? (S n)) (\snd sigma) with
     256    [ None ⇒ False
     257    | Some x1 ⇒ let 〈pc1,j1〉 ≝ x1 in
     258       pc1 = instruction_size_sigma labels sigma (bitvector_of_nat ? pc) (\snd (nth n ? program 〈None ?, Comment []〉))
     259    ]
     260  ].
    111261 
    112262(* Definitions and theorems for the jump_length type (itself defined in Assembly) *)
     
    127277  ].
    128278
    129 lemma dec_jmple: ∀x,y:jump_length.jmple x y + ¬(jmple x y).
     279lemma dec_jmple: ∀x,y:jump_length.Sum (jmple x y) (¬(jmple x y)).
    130280 #x #y cases x cases y /3 by inl, inr, nmk, I/
    131281qed.
     
    137287qed.
    138288
    139 lemma dec_eq_jump_length: ∀a,b:jump_length.(a = b) + (a ≠ b).
     289lemma dec_eq_jump_length: ∀a,b:jump_length.Sum (a = b) (a ≠ b).
    140290  #a #b cases a cases b /2/
    141291  %2 @nmk #H destruct (H)
     
    155305  is_label (nth i ? p 〈None ?, Comment [ ]〉) l → does_not_occur ?? l p = false.
    156306 #i #p #l generalize in match i; elim p
    157  [ #i >nth_nil #H @⊥ @H
     307 [ #i >nth_nil #H cases H
    158308 | #h #t #IH #i cases i -i
    159309   [ cases h #hi #hp cases hi
    160      [ normalize #H @⊥ @H
     310     [ normalize #H cases H
    161311     | #l' #Heq whd in ⊢ (??%?); change with (eq_identifier ? l' l) in match (instruction_matches_identifier ????);
    162312       whd in Heq; >Heq
     
    175325 ]
    176326qed.
    177 
    178 definition expand_relative_jump_internal_unsafe:
    179   jump_length → ([[relative]] → preinstruction [[relative]]) → option (list instruction) ≝
    180   λjmp_len:jump_length.λi.
    181   match jmp_len with
    182   [ short_jump ⇒ Some ? [ RealInstruction (i (RELATIVE (zero 8))) ]
    183   | medium_jump ⇒ None …
    184   | long_jump ⇒ Some ?
    185     [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2)));
    186       SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *)
    187       LJMP (ADDR16 (zero 16))
    188     ]
    189   ].
    190  @I
    191 qed.
    192 
    193 definition expand_relative_jump_unsafe:
    194   jump_length → preinstruction Identifier → option (list instruction) ≝
    195   λjmp_len:jump_length.λi.
    196   match i with
    197   [ JC jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JC ?)
    198   | JNC jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNC ?)
    199   | JB baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JB ? baddr)
    200   | JZ jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JZ ?)
    201   | JNZ jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNZ ?)
    202   | JBC baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JBC ? baddr)
    203   | JNB baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNB ? baddr)
    204   | CJNE addr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (CJNE ? addr)
    205   | DJNZ addr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (DJNZ ? addr)
    206   | ADD arg1 arg2 ⇒ Some … [ ADD ? arg1 arg2 ]
    207   | ADDC arg1 arg2 ⇒ Some … [ ADDC ? arg1 arg2 ]
    208   | SUBB arg1 arg2 ⇒ Some … [ SUBB ? arg1 arg2 ]
    209   | INC arg ⇒ Some … [ INC ? arg ]
    210   | DEC arg ⇒ Some … [ DEC ? arg ]
    211   | MUL arg1 arg2 ⇒ Some … [ MUL ? arg1 arg2 ]
    212   | DIV arg1 arg2 ⇒  Some … [ DIV ? arg1 arg2 ]
    213   | DA arg ⇒ Some … [ DA ? arg ]
    214   | ANL arg ⇒ Some … [ ANL ? arg ]
    215   | ORL arg ⇒ Some … [ ORL ? arg ]
    216   | XRL arg ⇒ Some … [ XRL ? arg ]
    217   | CLR arg ⇒ Some … [ CLR ? arg ]
    218   | CPL arg ⇒ Some … [ CPL ? arg ]
    219   | RL arg ⇒ Some … [ RL ? arg ]
    220   | RR arg ⇒ Some … [ RR ? arg ]
    221   | RLC arg ⇒ Some … [ RLC ? arg ]
    222   | RRC arg ⇒ Some … [ RRC ? arg ]
    223   | SWAP arg ⇒ Some … [ SWAP ? arg ]
    224   | MOV arg ⇒ Some … [ MOV ? arg ]
    225   | MOVX arg ⇒ Some … [ MOVX ? arg ]
    226   | SETB arg ⇒ Some … [ SETB ? arg ]
    227   | PUSH arg ⇒ Some … [ PUSH ? arg ]
    228   | POP arg ⇒ Some … [ POP ? arg ]
    229   | XCH arg1 arg2 ⇒ Some … [ XCH ? arg1 arg2 ]
    230   | XCHD arg1 arg2 ⇒ Some … [ XCHD ? arg1 arg2 ]
    231   | RET ⇒ Some … [ RET ? ]
    232   | RETI ⇒ Some … [ RETI ? ]
    233   | NOP ⇒ Some … [ RealInstruction (NOP ?) ]
    234   ].
    235 
    236 definition expand_pseudo_instruction_unsafe:
    237  jump_length → pseudo_instruction → option (list instruction) ≝
    238   λjmp_len.
    239   λi.
    240   match i with
    241   [ Cost cost ⇒ Some ? [ ]
    242   | Comment comment ⇒ Some ? [ ]
    243   | Call call ⇒
    244     match jmp_len with
    245     [ short_jump ⇒ None ?
    246     | medium_jump ⇒ Some ? [ ACALL (ADDR11 (zero 11)) ]
    247     | long_jump ⇒ Some ? [ LCALL (ADDR16 (zero 16)) ]
    248     ]
    249   | Mov d trgt ⇒
    250       Some ? [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, DATA16 (zero 16)〉))))]
    251   | Instruction instr ⇒ expand_relative_jump_unsafe jmp_len instr
    252   | Jmp jmp ⇒
    253     match jmp_len with
    254     [ short_jump ⇒ Some ? [ SJMP (RELATIVE (zero 8)) ]
    255     | medium_jump ⇒ Some ? ([ AJMP (ADDR11 (zero 11)) ])
    256     | long_jump ⇒ Some ? [ LJMP (ADDR16 (zero 16)) ]
    257     ]
    258   ].
    259  @I
    260 qed.
    261 
    262 definition instruction_size: (* ℕ → *) jump_length → pseudo_instruction → ℕ ≝
    263   λjmp_len.λinstr.
    264   let ilist ≝ expand_pseudo_instruction_unsafe jmp_len instr in
    265   let bv: list (BitVector 8) ≝ match ilist with
    266     [ None   ⇒ (* this shouldn't happen *) [ ]
    267     | Some l ⇒ flatten … (map … assembly1 l)
    268     ] in
    269   |bv|.
    270327 
    271328definition policy_isize_sum ≝
    272   λprefix:list labelled_instruction.λpolicy:jump_expansion_policy.
    273   (\fst policy) = foldl_strong (option Identifier × pseudo_instruction)
     329  λprefix:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map.
     330  (\fst sigma) = foldl_strong (option Identifier × pseudo_instruction)
    274331  (λacc.ℕ)
    275332  prefix
    276333  (λhd.λx.λtl.λp.λacc.
    277     let 〈i1,i2,jl〉 ≝ bvt_lookup … (bitvector_of_nat ? (|hd|)) (\snd policy) 〈0,0,short_jump〉 in
    278     acc + (instruction_size jl (\snd x)))
     334    acc + (instruction_size_sigma labels sigma (bitvector_of_nat 16 (\fst sigma)) (\snd x)))
    279335  0.
    280336
    281337(* The function that creates the label-to-address map *)
    282338definition create_label_map: ∀program:list labelled_instruction.
    283   ∀policy:jump_expansion_policy.
    284339  (Σlabels:label_map.
    285340    ∀i:ℕ.lt i (|program|) →
    286341    ∀l.occurs_exactly_once ?? l program →
    287342    is_label (nth i ? program 〈None ?, Comment [ ]〉) l →
    288     ∃a.lookup … labels l = Some ? 〈i,a〉
     343    lookup ?? labels l = Some ? i
    289344  ) ≝
    290   λprogram.λpolicy.
    291   let 〈final_pc, final_labels〉 ≝
    292     foldl_strong (option Identifier × pseudo_instruction)
    293     (λprefix.ℕ × (Σlabels.
    294       ∀i:ℕ.lt i (|prefix|) →
    295       ∀l.occurs_exactly_once ?? l prefix →
    296       is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l →
    297       ∃a.lookup … labels l = Some ? 〈i,a〉)
    298     )
    299     program
    300     (λprefix.λx.λtl.λprf.λacc.
    301      let 〈pc,labels〉 ≝ acc in
    302      let 〈label,instr〉 ≝ x in
    303        let new_labels ≝
    304        match label with
    305        [ None   ⇒ labels
    306        | Some l ⇒ add ? (ℕ×ℕ) labels l 〈|prefix|, pc〉
    307        ] in
    308      let 〈i1,i2,jmp_len〉 ≝
    309        bvt_lookup ?? (bitvector_of_nat 16 (|prefix|)) (\snd policy) 〈0,0,short_jump〉 in
    310        〈pc + (instruction_size jmp_len instr), new_labels〉
    311     ) 〈0, empty_map …〉 in
    312     final_labels.
    313 [#i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
    314   [ #Hi #l normalize nodelta; cases label normalize nodelta
    315     [ >occurs_exactly_once_None #Hocc >(nth_append_first ? ? prefix ? ? (le_S_S_to_le ? ? Hi)) #Hl
    316       lapply (pi2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #addr #Haddr 
    317       % [ @addr | @Haddr ]
    318     | #l' #Hocc #Hl lapply (occurs_exactly_once_Some_stronger ?????? Hocc) -Hocc;
    319       @eq_identifier_elim #Heq #Hocc
    320       [ normalize in Hocc;
    321         >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; #Hl 
    322         @⊥ @(absurd … Hocc)
    323       | normalize nodelta lapply (pi2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc ?)
    324         [ #addr #Haddr % [ @addr | <Haddr @lookup_add_miss /2/ ]
    325         | >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; / by /
     345  λprogram.
     346  foldl_strong (option Identifier × pseudo_instruction)
     347  (λprefix.Σlabels:label_map.
     348    ∀i:ℕ.lt i (|prefix|) →
     349    ∀l.occurs_exactly_once ?? l prefix →
     350    is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l →
     351    lookup … labels l = Some ? i
     352  )
     353  program
     354  (λprefix.λx.λtl.λprf.λlabels.
     355   let 〈label,instr〉 ≝ x in
     356     match label with
     357     [ None   ⇒ labels
     358     | Some l ⇒ add … labels l (|prefix|)
     359     ]
     360   ) (empty_map …).
     361[1,2: #i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi;
     362  [ #Hi #lbl #Hocc #Hlbl lapply (occurs_exactly_once_Some_stronger ?????? Hocc) -Hocc
     363    @eq_identifier_elim
     364    [ #Heq #Hocc normalize in Hocc; >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) in Hlbl; #Hl
     365      @⊥ @(absurd … Hocc) >(label_does_not_occur i … Hl) normalize nodelta /2 by nmk/
     366    | #Heq #Hocc normalize in Hocc; >lookup_add_miss
     367      [ @(pi2 … labels i (le_S_S_to_le … Hi))
     368        [ @Hocc
     369        | >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hlbl; / by /
    326370        ]
    327       ]
    328       >(label_does_not_occur i … Hl) normalize nodelta @nmk / by /
    329     ]
    330   | #Hi #l #Hocc >(injective_S … Hi) >nth_append_second
    331     [ <minus_n_n #Hl normalize in Hl; normalize nodelta cases label in Hl;
    332       [ normalize nodelta #H @⊥ @H
    333       | #l' normalize nodelta #Heq % [ @pc | <Heq normalize nodelta @lookup_add_hit ]
    334       ]
     371      | @sym_neq @Heq
     372      ]
     373    ]
     374  | #Hi #lbl #Hocc >(injective_S … Hi) >nth_append_second
     375    [ <minus_n_n #Hl normalize in Hl; >Hl @lookup_add_hit
    335376    | @le_n
    336377    ]
    337   ]
    338 | #i #Hi #l #Hl @⊥ @Hl
     378  | #Hi #lbl >occurs_exactly_once_None #Hocc #Hlbl
     379    @(pi2 … labels i (le_S_S_to_le … Hi))
     380    [ @Hocc
     381    | >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hlbl; / by /
     382    ]
     383  | #Hi #lbl #Hocc >(injective_S … Hi) >nth_append_second
     384    [ <minus_n_n #Hl cases Hl
     385    | @le_n
     386    ]
     387  ]
     388| #i #Hi #l #Hl cases Hl
    339389]
    340390qed.
    341391
    342 definition select_reljump_length: label_map → ℕ → Identifier → ℕ ×jump_length ≝
    343   λlabels.λpc.λlbl.
    344   let 〈n, addr〉 ≝ lookup_def … labels lbl 〈0, pc〉 in
    345   if leb pc addr (* forward jump *)
    346   then if leb (addr - pc) 126
    347        then 〈addr, short_jump〉
    348        else 〈addr, long_jump〉
    349   else if leb (pc - addr) 129
    350        then 〈addr, short_jump〉
    351        else 〈addr, long_jump〉.
    352 
    353 definition select_call_length: label_map → ℕ → Identifier → ℕ × jump_length ≝
    354   λlabels.λpc_nat.λlbl.
    355   let pc ≝ bitvector_of_nat 16 pc_nat in
    356   let addr_nat ≝ (\snd (lookup_def ? ? labels lbl 〈0, pc_nat〉)) in
    357   let addr ≝ bitvector_of_nat 16 addr_nat in
    358   let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 addr in
    359   let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
     392definition select_reljump_length: label_map → ppc_pc_map → ppc_pc_map → ℕ →  ℕ →
     393  Identifier → jump_length ≝
     394  λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl.
     395  let paddr ≝ lookup_def … labels lbl 0 in
     396  if leb ppc paddr (* forward jump *)
     397  then
     398    let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,None ?〉)
     399                    + added in
     400    if leb (addr - \fst inc_sigma) 126
     401    then short_jump
     402    else long_jump
     403  else
     404    let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,None ?〉) in
     405    if leb (\fst inc_sigma - addr) 129
     406    then short_jump
     407    else long_jump.
     408
     409definition select_call_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → ℕ →
     410  Identifier → jump_length ≝
     411  λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl.
     412  let paddr ≝ lookup_def ? ? labels lbl 0 in
     413  let addr ≝
     414    if leb ppc paddr (* forward jump *)
     415    then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,None ?〉)
     416            + added
     417    else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,None ?〉) in
     418  let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 (bitvector_of_nat ? addr) in
     419  let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 (bitvector_of_nat ? (\fst inc_sigma)) in
    360420  if eq_bv ? fst_5_addr fst_5_pc
    361   then 〈addr_nat, medium_jump〉
    362   else 〈addr_nat, long_jump〉.
     421  then medium_jump
     422  else long_jump.
    363423 
    364 definition select_jump_length: label_map → ℕ → Identifier → ℕ × jump_length ≝
    365   λlabels.λpc.λlbl.
    366   let 〈n, addr〉 ≝ lookup_def … labels lbl 〈0, pc〉 in
    367   if leb pc addr
    368   then if leb (addr - pc) 126
    369        then 〈addr, short_jump〉
    370        else select_call_length labels pc lbl
    371   else if leb (pc - addr) 129
    372        then 〈addr, short_jump〉
    373        else select_call_length labels pc lbl.
     424definition select_jump_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → ℕ →
     425  Identifier → jump_length ≝
     426  λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl.
     427  let paddr ≝ lookup_def … labels lbl 0 in
     428  if leb ppc paddr (* forward jump *)
     429  then
     430    let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,None ?〉)
     431              + added in
     432    if leb (addr - \fst inc_sigma) 126
     433    then short_jump
     434    else select_call_length labels old_sigma inc_sigma added ppc lbl
     435  else
     436    let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,None ?〉) in
     437    if leb (\fst inc_sigma - addr) 129
     438    then short_jump
     439    else select_call_length labels old_sigma inc_sigma added ppc lbl.
    374440 
    375 definition jump_expansion_step_instruction: label_map →
    376   preinstruction Identifier → option (ℕ × jump_length)
    377   λlabels.λpc.λi.
     441definition jump_expansion_step_instruction: label_map → ppc_pc_map → ppc_pc_map
     442  ℕ → ℕ → preinstruction Identifier → option jump_length
     443  λlabels.λold_sigma.λinc_sigma.λadded.λppc.λi.
    378444  match i with
    379   [ JC j     ⇒ Some ? (select_reljump_length labels pc j)
    380   | JNC j    ⇒ Some ? (select_reljump_length labels pc j)
    381   | JZ j     ⇒ Some ? (select_reljump_length labels pc j)
    382   | JNZ j    ⇒ Some ? (select_reljump_length labels pc j)
    383   | JB _ j   ⇒ Some ? (select_reljump_length labels pc j)
    384   | JBC _ j  ⇒ Some ? (select_reljump_length labels pc j)
    385   | JNB _ j  ⇒ Some ? (select_reljump_length labels pc j)
    386   | CJNE _ j ⇒ Some ? (select_reljump_length labels pc j)
    387   | DJNZ _ j ⇒ Some ? (select_reljump_length labels pc j)
     445  [ JC j     ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
     446  | JNC j    ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
     447  | JZ j     ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
     448  | JNZ j    ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
     449  | JB _ j   ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
     450  | JBC _ j  ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
     451  | JNB _ j  ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
     452  | CJNE _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
     453  | DJNZ _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
    388454  | _        ⇒ None ?
    389455  ].
    390456
    391 lemma dec_is_jump: ∀x.(is_jump x) + (¬is_jump x).
     457lemma dec_is_jump: ∀x.Sum (is_jump x) (¬is_jump x).
    392458#x cases x #l #i cases i
    393459[#id cases id
     
    407473
    408474lemma jump_not_in_policy: ∀prefix:list labelled_instruction.
    409  ∀policy:(Σp:jump_expansion_policy.
     475 ∀policy:(Σp:ppc_pc_map.
    410476 out_of_program_none prefix p ∧ jump_in_policy prefix p).
    411477  ∀i:ℕ.i < |prefix| →
    412478  iff (¬is_jump (nth i ? prefix 〈None ?, Comment []〉))
    413   (lookup_opt … (bitvector_of_nat 16 i) (\snd policy) = None ?).
     479  (\snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd policy) 〈0,None ?〉) = None ?).
    414480 #prefix #policy #i #Hi @conj
    415 [ #Hnotjmp lapply (refl ? (lookup_opt … (bitvector_of_nat 16 i) (\snd policy)))
    416   cases (lookup_opt … (bitvector_of_nat 16 i) (\snd policy)) in ⊢ (???% → ?);
    417   [ #H @H
    418   | #x cases x -x #x cases x -x #x #y #z #H @⊥ @(absurd ? ? Hnotjmp) @(proj2 ?? (proj2 ?? (pi2 ?? policy) i Hi))
    419     @(ex_intro ?? x (ex_intro ?? y (ex_intro ?? z H)))
     481[ #Hnotjmp lapply (refl ? (bvt_lookup … (bitvector_of_nat 16 i) (\snd policy) 〈0,None ?〉))
     482  cases (bvt_lookup … (bitvector_of_nat 16 i) (\snd policy) 〈0,None ?〉) in ⊢ (???% → ?);
     483  #pc #j cases j
     484  [ #H >H @refl
     485  | #x #H >H @⊥ @(absurd ? ? Hnotjmp) @(proj2 ?? (proj2 ?? (pi2 ?? policy) i Hi))
     486    >H @(ex_intro ?? x ?) / by /
    420487  ]
    421488| #Hnone @nmk #Hj lapply (proj1 ?? (proj2 ?? (pi2 ?? policy) i Hi) Hj)
    422   #H elim H -H; #x #H elim H -H; #y #H elim H -H #z #H >H in Hnone; #abs destruct (abs)
     489  #H elim H -H; #x #H >H in Hnone; #abs destruct (abs)
    423490
    424491qed.
     
    440507definition jump_expansion_start:
    441508  ∀program:(Σl:list labelled_instruction.|l| < 2^16).
    442   Σpolicy:jump_expansion_policy.
    443     And (And (out_of_program_none (pi1 ?? program) policy)
    444     (jump_in_policy (pi1 ?? program) policy))
    445     (∀i.i < |pi1 ?? program| → is_jump (nth i ? (pi1 ?? program) 〈None ?, Comment []〉) →
    446      lookup_opt … (bitvector_of_nat 16 i) (\snd policy) = Some ? 〈0,0,short_jump〉) ≝
    447   λprogram.
     509  ∀labels:label_map.
     510  Σpolicy:ppc_pc_map.
     511    And (out_of_program_none (pi1 ?? program) policy)
     512    (jump_in_policy (pi1 ?? program) policy) ≝
     513  λprogram.λlabels.
    448514  foldl_strong (option Identifier × pseudo_instruction)
    449   (λprefix.Σpolicy:jump_expansion_policy.
    450     And (And (out_of_program_none prefix policy)
    451     (jump_in_policy prefix policy))
    452     (∀i.i < |prefix| → is_jump (nth i ? prefix 〈None ?, Comment []〉) →
    453       lookup_opt … (bitvector_of_nat 16 i) (\snd policy) = Some ? 〈0,0,short_jump〉))
     515  (λprefix.Σpolicy:ppc_pc_map.
     516    (And (out_of_program_none prefix policy)
     517    (jump_in_policy prefix policy)))
    454518  program
    455519  (λprefix.λx.λtl.λprf.λp.
    456    let 〈pc,policy〉 ≝ p in
     520   let 〈pc,sigma〉 ≝ p in
    457521   let 〈label,instr〉 ≝ x in
    458    〈pc + instruction_size short_jump instr,match instr with
     522   let isize ≝ instruction_size_jmplen short_jump instr in
     523   〈pc + isize,
     524   match instr with
    459525   [ Instruction i ⇒ match i with
    460      [ JC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
    461      | JNC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
    462      | JZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
    463      | JNZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
    464      | JB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
    465      | JNB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
    466      | JBC _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
    467      | CJNE _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
    468      | DJNZ _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
    469      | _ ⇒ policy
     526     [ JC jmp ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,Some ? short_jump〉 sigma
     527     | JNC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,Some ? short_jump〉 sigma
     528     | JZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,Some ? short_jump〉 sigma
     529     | JNZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,Some ? short_jump〉 sigma
     530     | JB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,Some ? short_jump〉 sigma
     531     | JNB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,Some ? short_jump〉 sigma
     532     | JBC _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,Some ? short_jump〉 sigma
     533     | CJNE _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,Some ? short_jump〉 sigma
     534     | DJNZ _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,Some ? short_jump〉 sigma
     535     | _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,None ?〉 sigma
    470536     ]
    471    | Call c ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
    472    | Jmp j  ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
    473    | _      ⇒ policy
     537   | Call c ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,Some ? short_jump〉 sigma
     538   | Jmp j  ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,Some ? short_jump〉 sigma
     539   | _      ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,None ?〉 sigma
    474540   ]〉
    475541  ) 〈0, Stub ? ?〉.
    476 [ @conj
    477   [ @conj
    478     #i >append_length <commutative_plus #Hi normalize in Hi;
    479     [ #Hi2 cases (le_to_or_lt_eq … Hi) -Hi #Hi
    480       cases p -p #p cases p -p #pc #p #Hp cases x -x #l #pi cases pi
     542[ @conj #i >append_length <commutative_plus #Hi normalize in Hi;
     543  [ #Hi2
     544    cases (le_to_or_lt_eq … Hi) -Hi #Hi
     545    cases p -p #p cases p -p #pc #p #Hp cases x -x #l #pi cases pi
    481546      [1,7: #id cases id normalize nodelta
    482547        [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:
    483548          [1,2,3,6,7,24,25: #x #y
    484           |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    485           @(proj1 ?? (proj1 ?? Hp) i ? Hi2) @le_S_to_le @le_S_to_le @Hi
     549          |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] >lookup_opt_insert_miss
     550          [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:
     551            @bitvector_of_nat_abs
     552            [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:
     553              @Hi2
     554            |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:
     555              @(transitive_lt … Hi2) @le_S_to_le @Hi
     556            |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:
     557              @sym_neq @lt_to_not_eq @le_S_to_le @Hi
     558            ]
     559          ]
     560          @(proj1 ?? Hp i ? Hi2) @le_S_to_le @le_S_to_le @Hi
    486561        |38,39,40,41,42,43,44,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74:
    487562          [1,2,3,6,7,24,25: #x #y
    488563          |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    489           <Hi @(proj1 ?? (proj1 ?? Hp) (S (|prefix|)) (le_S ?? (le_n (|prefix|))) ?)
     564          >lookup_opt_insert_miss
     565          [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:
     566            @bitvector_of_nat_abs
     567            [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:
     568               @Hi2
     569            |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:
     570              @(transitive_lt … Hi2) <Hi @le_n
     571            |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:
     572              @sym_neq @lt_to_not_eq <Hi @le_n
     573            ]
     574          ]
     575          <Hi @(proj1 ?? Hp (S (|prefix|)) (le_S ?? (le_n (|prefix|))) ?)
    490576          >Hi @Hi2
    491577        |9,10,11,12,13,14,15,16,17:
     
    497583            ]
    498584          |1,3,5,7,9,11,13,15,17:
    499             @(proj1 ?? (proj1 ?? Hp) i ? Hi2) @le_S_to_le @le_S_to_le @Hi
     585            @(proj1 ?? Hp i ? Hi2) @le_S_to_le @le_S_to_le @Hi
    500586          ]
    501587        |46,47,48,49,50,51,52,53,54:
     
    507593            ]
    508594          |1,3,5,7,9,11,13,15,17:
    509             @(proj1 ?? (proj1 ?? Hp) i ? Hi2) <Hi @le_S @le_n
     595            @(proj1 ?? Hp i ? Hi2) <Hi @le_S @le_n
    510596          ]
    511597        ]
    512       |2,3,6,8,9,12: [3,6: #w] #z normalize nodelta
    513         [1,3,4: @(proj1 ?? (proj1 ?? Hp) i ? Hi2) @le_S_to_le @le_S_to_le @Hi
     598      |2,3,6,8,9,12: [3,6: #w] #z >lookup_opt_insert_miss
     599        [2,4,6,8,10,12: @bitvector_of_nat_abs
     600          [1,4,7,10,13,16: @Hi2
     601          |2,8,11: @(transitive_lt … Hi2) @le_S_to_le @Hi
     602          |5,14,17: @(transitive_lt … Hi2) <Hi @le_n
     603          |3,9,12: @sym_neq @lt_to_not_eq @le_S_to_le @Hi
     604          |6,15,18: <Hi @sym_neq @lt_to_not_eq @le_n
     605          ]
     606        ]
     607        [1,3,4: @(proj1 ?? Hp i ? Hi2) @le_S_to_le @le_S_to_le @Hi
    514608        |2,5,6:
    515           <Hi @(proj1 ?? (proj1 ?? Hp) (S (|prefix|)) (le_S ?? (le_n (|prefix|))) ?)
     609          <Hi @(proj1 ?? Hp (S (|prefix|)) (le_S ?? (le_n (|prefix|))) ?)
    516610          >Hi @Hi2
    517611        ]
     
    524618          |9,12: @sym_neq @lt_to_not_eq <Hi @le_n
    525619          ]         
    526         |1,3: @(proj1 ?? (proj1 ?? Hp) i ? Hi2) @le_S_to_le @le_S_to_le @Hi
    527         |5,7: @(proj1 ?? (proj1 ?? Hp) i ? Hi2) <Hi @le_S @le_n
     620        |1,3: @(proj1 ?? Hp i ? Hi2) @le_S_to_le @le_S_to_le @Hi
     621        |5,7: @(proj1 ?? Hp i ? Hi2) <Hi @le_S @le_n
    528622        ]
    529623      ]
    530624    | cases (le_to_or_lt_eq … Hi) -Hi #Hi
    531625      [ >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) @conj
    532         [ #Hj @(ex_intro ?? 0 (ex_intro ?? 0 (ex_intro ?? short_jump ?)))
    533           cases p -p #p cases p #pc #pol #Hp cases x #l #ins cases ins normalize nodelta
     626        [ #Hj cases p -p #p cases p #pc #pol #Hp cases x #l #ins cases ins normalize nodelta
    534627          [1: #pi cases pi normalize nodelta
    535             [1,2,3,6,7,33,34: #x #y
    536             |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x
     628            [1,2,3,6,7,33,34,35,36,37: [1,2,3,4,5,6,7: #x #y] >lookup_insert_miss
     629              [2,4,6,8,10,12,14,16,18,20: @bitvector_of_nat_abs
     630               [1,4,7,10,13,16,19,22,25,28: @(transitive_lt … (pi2 ?? program)) >prf
     631                 >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)
     632                 @le_S_S_to_le @le_plus_n_r
     633               |2,5,8,11,14,17,20,23,26,29: @(transitive_lt … (pi2 ?? program)) >prf
     634                 >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r
     635               |3,6,9,12,15,18,21,24,27,30: @lt_to_not_eq @(le_S_S_to_le … Hi)
     636               ]
     637              ]
     638            |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x >lookup_insert_miss
     639              [2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36: @bitvector_of_nat_abs
     640               [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52:
     641                 @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm
     642                 @le_S_to_le @(transitive_le … Hi) @le_S_S_to_le @le_plus_n_r
     643               |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53:
     644                 @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm
     645                 @le_S_S_to_le @le_plus_n_r
     646               |3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54:
     647                 @lt_to_not_eq @(le_S_S_to_le … Hi)
     648               ]
     649              ]
    537650            |9,10,11,12,13,14,15,16,17:
    538               [1,2,6,7: #x | 3,4,5,8,9: #x #id] >lookup_opt_insert_miss
     651              [1,2,6,7: #x | 3,4,5,8,9: #x #id] >lookup_insert_miss
    539652              [2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
    540653               [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf
     
    546659               ]
    547660              ]
     661             ]
     662          |2,3: #x >lookup_insert_miss
     663            [2,4: @bitvector_of_nat_abs
     664              [1,4: @(transitive_lt … (pi2 ?? program)) >prf
     665                >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)
     666                @le_S_S_to_le @le_plus_n_r
     667              |2,5: @(transitive_lt … (pi2 ?? program)) >prf
     668                 >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r
     669              |3,6: @lt_to_not_eq @(le_S_S_to_le … Hi)
     670              ]
    548671            ]
    549           |2,3: #x
    550           |4,5: #id >lookup_opt_insert_miss
     672          |4,5: #id >lookup_insert_miss
    551673            [2,4: @bitvector_of_nat_abs
    552674              [1,4: @(transitive_lt … (pi2 ?? program)) >prf
     
    558680              ]
    559681            ]
    560           |6: #x #id
     682          |6: #x #id >lookup_insert_miss
     683            [2: @bitvector_of_nat_abs
     684              [ @(transitive_lt … (pi2 ?? program)) >prf
     685                >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)
     686                @le_S_S_to_le @le_plus_n_r
     687              | @(transitive_lt … (pi2 ?? program)) >prf
     688                >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r
     689              | @lt_to_not_eq @(le_S_S_to_le … Hi)
     690              ]
     691            ]
    561692          ]
    562           @((proj2 ?? Hp) i (le_S_S_to_le … Hi) Hj)
    563         | #H @(proj2 ?? (proj2 ?? (proj1 ?? (pi2 ?? p)) i ?))
    564           [ @(le_S_S_to_le … Hi)
    565           | cases p in H; -p #p cases p #pc #pol #Hp cases x #l #ins cases ins normalize nodelta
    566             [1: #id cases id
    567               [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
    568                 [1,2,3,6,7,24,25: #x #y
    569                 |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    570                 normalize nodelta / by /
    571               |9,10,11,12,13,14,15,16,17: [1,2,6,7: #x |3,4,5,8,9: #x #id]
    572                 normalize nodelta >lookup_opt_insert_miss
    573                 [1,3,5,7,9,11,13,15,17: / by /
    574                 |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
    575                   [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf
    576                     >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)
    577                     @le_S_S_to_le @le_plus_n_r
    578                   |2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf
    579                     >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r 
    580                   |3,6,9,12,15,18,21,24,27: @lt_to_not_eq @(le_S_S_to_le … Hi)
    581                   ]
     693          @(proj1 ?? (proj2 ?? Hp i (le_S_S_to_le … Hi)) Hj)
     694        | #H @(proj2 ?? (proj2 ?? (pi2 ?? p) i (le_S_S_to_le … Hi)))
     695          cases p in H; -p #p cases p #pc #pol #Hp cases x #l #ins cases ins normalize nodelta
     696          [1: #id cases id
     697            [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:
     698              [1,2,3,6,7,24,25: #x #y
     699              |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
     700              normalize nodelta >lookup_insert_miss
     701              [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:
     702                @bitvector_of_nat_abs
     703                [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:
     704                 @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm
     705                 @le_S_to_le @(transitive_le … Hi) @le_S_S_to_le @le_plus_n_r
     706               |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:
     707                 @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm
     708                 @le_S_S_to_le @le_plus_n_r
     709               |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:
     710                 @lt_to_not_eq @(le_S_S_to_le … Hi)
     711               ]
     712             ] / by /
     713            |9,10,11,12,13,14,15,16,17: [1,2,6,7: #x |3,4,5,8,9: #x #id]
     714              normalize nodelta >lookup_insert_miss
     715              [1,3,5,7,9,11,13,15,17: / by /
     716              |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
     717                [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf
     718                  >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)
     719                  @le_S_S_to_le @le_plus_n_r
     720                |2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf
     721                  >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r 
     722                |3,6,9,12,15,18,21,24,27: @lt_to_not_eq @(le_S_S_to_le … Hi)
    582723                ]
    583724              ]
    584             |2,3: #x / by /
    585             |4,5: #id >lookup_opt_insert_miss
    586               [2,4: @bitvector_of_nat_abs
    587                 [1,4: @(transitive_lt … (pi2 ?? program)) >prf
    588                    >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)
    589                    @le_S_S_to_le @le_plus_n_r
    590                 |2,5: @(transitive_lt … (pi2 ?? program)) >prf
    591                    >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r
    592                 |3,6: @lt_to_not_eq @(le_S_S_to_le … Hi)
    593                 ]
     725            ]
     726          |2,3: #x >lookup_insert_miss
     727            [2,4: @bitvector_of_nat_abs
     728              [1,4: @(transitive_lt … (pi2 ?? program)) >prf
     729                 >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)
     730                 @le_S_S_to_le @le_plus_n_r
     731              |2,5: @(transitive_lt … (pi2 ?? program)) >prf
     732                 >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r
     733              |3,6: @lt_to_not_eq @(le_S_S_to_le … Hi)
     734              ]
    594735              |1,3: / by /
     736            ]
     737          |4,5: #id >lookup_insert_miss
     738            [2,4: @bitvector_of_nat_abs
     739              [1,4: @(transitive_lt … (pi2 ?? program)) >prf
     740                 >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)
     741                 @le_S_S_to_le @le_plus_n_r
     742              |2,5: @(transitive_lt … (pi2 ?? program)) >prf
     743                 >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r
     744              |3,6: @lt_to_not_eq @(le_S_S_to_le … Hi)
    595745              ]
    596             |6: #x #id / by /
     746            |1,3: / by /
    597747            ]
     748          |6: #x #id >lookup_insert_miss
     749            [2: @bitvector_of_nat_abs
     750              [@(transitive_lt … (pi2 ?? program)) >prf
     751               >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)
     752               @le_S_S_to_le @le_plus_n_r
     753              |@(transitive_lt … (pi2 ?? program)) >prf
     754               >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r
     755              |@lt_to_not_eq @(le_S_S_to_le … Hi)
     756              ]
     757            ]
     758            / by /
    598759          ]
    599760        ]
    600       | >(injective_S … Hi) >(nth_append_second ?? prefix ?? (le_n (|prefix|)))
    601         <minus_n_n whd in match (nth ????);
    602         cases x #l #ins cases ins
    603         [1: #pi cases pi
    604           [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
    605             [1,2,3,6,7,24,25: #x #y
    606             |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    607             @conj
    608             [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55:
    609               #H @⊥ @H
    610             |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
    611               cases p -p #p cases p -p #pc #pol #Hp #H elim H -H #p #H elim H -H #a #H elim H -H #j
    612               normalize nodelta >(proj1 ?? (proj1 ?? Hp) (|prefix|) (le_n (|prefix|)) ?)
    613               [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55:
    614                 #H destruct (H)
    615               |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
    616                 @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm
    617                 @le_S_S_to_le @le_plus_n_r
    618               ]
    619             ]
    620           |9,10,11,12,13,14,15,16,17: [1,2,6,7: #x | 3,4,5,8,9: #x #id]
    621             @conj
    622             [1,3,5,7,9,11,13,15,17:
    623               #_ @(ex_intro ?? 0 (ex_intro ?? 0 (ex_intro ?? short_jump ?)))
    624               cases p -p #p cases p -p #pc #pol #Hp @lookup_opt_insert_hit
    625             |2,4,6,8,10,12,14,16,18:
    626               #_ / by I/
    627             ]
     761    | >(injective_S … Hi) >(nth_append_second ?? prefix ?? (le_n (|prefix|)))
     762      <minus_n_n whd in match (nth ????); cases x #l #ins cases ins
     763      [1: #pi cases pi
     764        [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:
     765          [1,2,3,6,7,24,25: #x #y
     766          |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
     767          @conj
     768          [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:
     769            #H cases H in ⊢ ?;
     770          |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:
     771            cases p -p #p cases p -p #pc #pol #Hp #H elim H -H #p
     772            normalize nodelta >lookup_insert_hit #H destruct (H)
    628773          ]
    629         |2,3,6: #x [3: #id] @conj
    630           [1,3,5: #H @⊥ @H
    631           |2,4,6:
    632             cases p -p #p cases p -p #pc #pol #Hp #H elim H -H #p #H elim H -H #a #H elim H -H #j
    633             normalize nodelta >(proj1 ?? (proj1 ?? Hp) (|prefix|) (le_n (|prefix|)) ?)
    634             [1,3,5: #H destruct (H)
    635             |2,4,6: @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm
    636               @le_S_S_to_le @le_plus_n_r
    637             ]
     774        |9,10,11,12,13,14,15,16,17: [1,2,6,7: #x | 3,4,5,8,9: #x #id]
     775          @conj normalize nodelta
     776          [(*1: #_ @(ex_intro ?? (zero ?) (ex_intro ?? (bitvector_of_nat ? (lookup_def … labels x 0)) ?))*)
     777          1,3,5,7,9,11,13,15,17: #_ @(ex_intro ?? short_jump ?)
     778          |2,4,6,8,10,12,14,16,18: #_ / by I/
    638779          ]
    639         |4,5: #x @conj
    640           [1,3: #_ @(ex_intro ?? 0 (ex_intro ?? 0 (ex_intro ?? short_jump ?)))
    641             cases p -p #p cases p -p #pc #pol #Hp @lookup_opt_insert_hit
    642           |2,4: #_ / by I/
     780          cases p -p #p cases p -p #pc #pol #Hp >lookup_insert_hit @refl
    643781        ]
    644       ]
    645     ]
    646   ]
    647 | #i >append_length <commutative_plus #Hi normalize in Hi;
    648   elim (le_to_or_lt_eq … Hi) -Hi #Hi
    649   [ >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) #H
    650     cases p -p #p cases p #pc #pol #Hp cases x #l #ins cases ins normalize nodelta
    651     [1: #pi cases pi
    652       [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
    653         [1,2,3,6,7,24,25: #x #y
    654         |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    655         normalize nodelta
    656         @((proj2 ?? Hp) i (le_S_S_to_le … Hi) H)
    657       |9,10,11,12,13,14,15,16,17: [1,2,6,7: #x | 3,4,5,8,9: #x #id]
    658         normalize nodelta >lookup_opt_insert_miss
    659         [1,3,5,7,9,11,13,15,17: @((proj2 ?? Hp) i (le_S_S_to_le … Hi) H)
    660         |2,4,6,8,10,12,14,16,18,20: @bitvector_of_nat_abs
    661           [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf
    662             >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)
     782      |2,3,6: #x [3: #id] @conj
     783        [1,3,5: #H @⊥ @H
     784        |2,4,6:
     785          cases p -p #p cases p -p #pc #pol #Hp #H elim H -H #p
     786          normalize nodelta >lookup_insert_hit #H destruct (H)
     787          (* [1,3,5: #_ #H destruct (H)
     788          |2,4,6: @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm
    663789            @le_S_S_to_le @le_plus_n_r
    664           |2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf
    665             >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r
    666           |3,6,9,12,15,18,21,24,27: @lt_to_not_eq @(le_S_S_to_le … Hi)
    667           ]
     790          ] *)
    668791        ]
    669       ]
    670     |2,3,6: #x [3: #id]
    671       normalize nodelta @((proj2 ?? Hp) i (le_S_S_to_le … Hi) H)
    672     |4,5: #x >lookup_opt_insert_miss
    673       [1,3: @((proj2 ?? Hp) i (le_S_S_to_le … Hi) H)
    674       |2,4: @bitvector_of_nat_abs
    675         [1,4: @(transitive_lt … (pi2 ?? program)) >prf
    676           >append_length <plus_n_Sm @le_S_to_le @(transitive_le … Hi)
    677           @le_S_S_to_le @le_plus_n_r
    678         |2,5: @(transitive_lt … (pi2 ?? program)) >prf
    679           >append_length <plus_n_Sm @le_S_S_to_le @le_plus_n_r
    680         |3,6: @lt_to_not_eq @(le_S_S_to_le … Hi)
     792      |4,5: #x @conj
     793        [1,3: #_ @(ex_intro ?? (short_jump) ?)
     794          cases p -p #p cases p -p #pc #pol #Hp normalize nodelta >lookup_insert_hit @refl
     795        |2,4: #_ / by I/
    681796        ]
    682797      ]
    683798    ]
    684   | >(injective_S … Hi) >(nth_append_second ?? prefix ?? (le_n (|prefix|)))
    685     <minus_n_n whd in match (nth ????); cases x #l #ins cases ins
    686     [1: #pi cases pi
    687       [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37:
    688         [1,2,3,6,7,24,25: #x #y
    689         |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    690         #H @⊥ @H
    691       |9,10,11,12,13,14,15,16,17: [1,2,6,7: #x | 3,4,5,8,9: #x #id]
    692         #_ cases p -p #p cases p -p #pc #pol #Hp >lookup_opt_insert_hit / by /
    693       ]
    694     |2,3,6: #x [3: #id] #H @⊥ @H
    695     |4,5: #id #_ cases p -p #p cases p -p #pc #pol #Hp >lookup_opt_insert_hit / by /
     799  ]
     800| @conj
     801  [ #i #_ #Hi2 / by refl/
     802  | #i #_ @conj
     803    [ >nth_nil #H @⊥ @H
     804    | #H elim H -H #p >lookup_stub #H destruct (H)
    696805    ]
    697806  ]
    698807]
    699 | @conj
    700   [ @conj
    701     [ #i #_ #Hi2 / by refl/
    702     | #i #_ @conj
    703       [ >nth_nil #H @⊥ @H
    704       | #H elim H -H #p #H elim H -H #a #H elim H -H #j #H normalize in H; destruct (H)
    705       ]
    706     ]
    707   | #i #Hi >nth_nil #H @⊥ @H
    708   ]
    709 ]
    710 qed.
    711 
    712 definition policy_equal_int ≝
    713   λprogram:list labelled_instruction.λp1,p2:jump_expansion_policy.
    714   ∀n:ℕ.n < |program| →
    715     let 〈pc1,i1,j1〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,0,short_jump〉 in
    716     let 〈pc2,i2,j2〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,0,short_jump〉 in
    717     j1 = j2.
     808qed.
     809
     810definition policy_equal ≝
     811  λprogram:list labelled_instruction.λp1,p2:ppc_pc_map.
     812  (* \fst p1 = \fst p2 ∧ *)
     813  (∀n:ℕ.n < |program| →
     814    let pc1 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,None ?〉 in
     815    let pc2 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,None ?〉 in
     816    pc1 = pc2).
    718817   
    719 definition nec_plus_ultra ≝
    720   λprogram:list labelled_instruction.λp:jump_expansion_policy.
    721   ¬(∀i.i < |program| → \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,0,short_jump〉) = long_jump).
     818(*definition nec_plus_ultra ≝
     819  λprogram:list labelled_instruction.λp:ppc_pc_mapjump_expansion_policy.
     820  ¬(∀i.i < |program| → \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,0,short_jump〉) = long_jump). *)
    722821 
    723822lemma geb_to_leb: ∀a,b:ℕ.geb a b = leb b a.
     
    725824qed.
    726825
    727 (*lemma foldl_strong_eq:
    728   ∀A: Type[0].
    729   ∀P: list A → Type[0].
    730   ∀l: list A.
    731   ∀H: ∀prefix. ∀hd. ∀tl. l = prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]).
    732   ∀acc: P [ ].
    733     foldl_strong_internal A P l H [ ] l acc (refl …).*)
     826include alias "common/Identifiers.ma".
     827include alias "ASM/BitVector.ma".
     828include alias "basics/lists/list.ma".
     829include alias "arithmetics/nat.ma".
     830include alias "basics/logic.ma".
    734831
    735832
    736833(* One step in the search for a jump expansion fixpoint. *)
     834(* Takes a horrible amount of time to typecheck. I suspect disambiguation problems. *)
    737835definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
    738   ∀labels:(Σlm:label_map.∀i:ℕ.lt i (|pi1 ?? program|) →
    739     ∀l.occurs_exactly_once ?? l (pi1 ?? program) →
    740     is_label (nth i ? (pi1 ?? program) 〈None ?, Comment [ ]〉) l →
    741     ∃a.lookup … lm l = Some ? 〈i,a〉).
    742   ∀old_policy:(Σpolicy:jump_expansion_policy.
    743     out_of_program_none (pi1 ?? program) policy ∧
    744     jump_in_policy (pi1 ?? program) policy ∧ (\fst policy < 2^16) ∧
    745     policy_isize_sum (pi1 ?? program) policy).
    746   (Σx:bool × (option jump_expansion_policy).
    747     let 〈ch,y〉 ≝ x in
     836  ∀labels:(Σlm:label_map. ∀i:ℕ.lt i (|program|) →
     837    ∀l.occurs_exactly_once ?? l program →
     838    is_label (nth i ? program 〈None ?, Comment [ ]〉) l →
     839    lookup … lm l = Some ? i).
     840  ∀old_policy:(Σpolicy:ppc_pc_map.
     841    And (And (And (out_of_program_none program policy)
     842    (jump_in_policy program policy))
     843    (policy_isize_sum program labels policy))
     844    (\fst policy < 2^16)).
     845  (Σx:bool × (option ppc_pc_map).
     846    let 〈no_ch,y〉 ≝ x in
    748847    match y with
    749     [ None ⇒ nec_plus_ultra program old_policy
    750     | Some p ⇒ out_of_program_none (pi1 ?? program) p ∧ labels_okay labels p ∧
    751         jump_in_policy (pi1 ?? program) p ∧
    752         policy_increase (pi1 ?? program) old_policy p ∧ policy_safe p ∧
    753         (ch = false → policy_equal_int (pi1 ?? program) old_policy p) ∧
    754         policy_isize_sum (pi1 ?? program) p ∧ \fst p < 2^16
     848    [ None ⇒ (* nec_plus_ultra program old_policy *) True
     849    | Some p ⇒ And (And (And (And (And (And (And (out_of_program_none (pi1 ?? program) p) (* labels_okay labels p ∧*)
     850       (jump_in_policy program p))
     851       (policy_isize_sum program labels p))
     852       (policy_increase program old_policy p))
     853       (policy_safe program labels p))
     854       (policy_compact program labels p))
     855       (no_ch = true → policy_equal program old_policy p))
     856       (\fst p < 2^16)
    755857    ])
    756     ≝ 
    757   λprogram.λlabels.λold_policy.
    758   let 〈final_changed, final_policy〉 ≝
     858    ≝
     859  λprogram.λlabels.λold_sigma.
     860  let 〈final_added, final_policy〉 ≝
    759861    foldl_strong (option Identifier × pseudo_instruction)
    760     (λprefix.Σx:bool × jump_expansion_policy.
    761         let 〈changed,policy〉 ≝ x in
    762         out_of_program_none prefix policy ∧ labels_okay labels policy ∧
    763         jump_in_policy prefix policy ∧
    764         policy_increase prefix old_policy policy ∧
    765         policy_safe policy ∧
    766         (changed = false → policy_equal_int prefix old_policy policy) ∧
    767         policy_isize_sum prefix policy)
     862    (λprefix.Σx:ℕ × ppc_pc_map.
     863      let 〈added,policy〉 ≝ x in
     864      And (And (And (And (And (And (out_of_program_none prefix policy)
     865      (jump_in_policy prefix policy))
     866      (policy_isize_sum prefix labels policy))
     867      (policy_increase prefix old_sigma policy))
     868      (policy_safe prefix labels policy))
     869      (policy_compact prefix labels policy))
     870      (added = 0 → policy_equal prefix old_sigma policy))
    768871    program
    769872    (λprefix.λx.λtl.λprf.λacc.
    770       let 〈changed, pol〉 ≝ acc in
    771       (* let 〈pc,pol〉 ≝ p in *)
     873      let 〈inc_added, inc_pc_sigma〉 ≝ (pi1 ?? acc) in
    772874      let 〈label,instr〉 ≝ x in
    773       let add_instr ≝
    774         match instr with
    775         [ Instruction i ⇒ jump_expansion_step_instruction labels (\fst pol) i
    776         | Call c        ⇒ Some ? (select_call_length labels (\fst pol) c)
    777         | Jmp j         ⇒ Some ? (select_jump_length labels (\fst pol) j)
    778         | _             ⇒ None ?
     875      (* Now, we must add the current ppc and its pc translation.
     876       * Three possibilities:
     877       *   - Instruction is not a jump; i.e. constant size whatever the sigma we use;
     878       *   - Instruction is a backward jump; we can use the sigma we're constructing,
     879       *     since it will already know the translation of its destination;
     880       *   - Instruction is a forward jump; we must use the old sigma (the new sigma
     881       *     does not know the translation yet), but compensate for the jumps we
     882       *     have lengthened.
     883       *)
     884      let add_instr ≝ match instr with
     885      [ Jmp  j        ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
     886      | Call c        ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
     887      | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (|prefix|) i
     888      | _             ⇒ None ?
     889      ] in
     890      let 〈inc_pc, inc_sigma〉 ≝ inc_pc_sigma in
     891      let 〈old_pc, old_length〉 ≝ bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,None ?〉 in
     892      match add_instr with
     893      [ None ⇒
     894        let isize ≝ instruction_size_jmplen short_jump instr in
     895        (* instruction is not a jump: nothing changes *)
     896        〈inc_added, 〈plus inc_pc isize, bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈inc_pc, None ?〉 inc_sigma〉〉   
     897      | Some proj_length ⇒
     898        let x ≝ match old_length with
     899        [ None ⇒ (* this should not happen! *) short_jump
     900        | Some y ⇒ y
    779901        ] in
    780       let old_length ≝ \snd (bvt_lookup … (bitvector_of_nat 16 (|prefix|)) (\snd old_policy) 〈0,0,short_jump〉) in
    781       match add_instr with
    782       [ None    ⇒ (* i.e. it's not a jump *)
    783         let isize ≝ instruction_size short_jump instr in
    784         〈changed, 〈(\fst pol) + isize, (\snd pol)〉〉
    785       | Some z ⇒ let 〈addr,ai〉 ≝ z in
    786         let new_length ≝ max_length old_length ai in
    787         let isize ≝ instruction_size new_length instr in
    788         〈match dec_eq_jump_length new_length old_length with
    789          [ inl _ ⇒ changed
    790          | inr _ ⇒ true], 〈(\fst pol) + isize,
    791          insert … (bitvector_of_nat 16 (|prefix|)) 〈(\fst pol), addr, new_length〉 (\snd pol)〉〉
    792       ]
    793     ) 〈false, 〈0, Stub ? ?〉〉 in
     902        let new_length ≝ max_length x proj_length in
     903        let old_size ≝ instruction_size_jmplen x instr in
     904        let isize ≝ instruction_size_jmplen new_length instr in
     905        〈plus inc_added (minus isize old_size), 〈plus inc_pc isize,
     906         bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈inc_pc, Some ? new_length〉 inc_sigma〉〉
     907      ]
     908    ) 〈0, 〈0, Stub ??〉〉 in
    794909    if geb (\fst final_policy) 2^16 then
    795       〈final_changed,None ?〉
     910      〈eqb final_added 0, None ?〉
    796911    else
    797       〈final_changed,Some ? final_policy〉.
    798 [ @pair_elim #fch #x #Heq <(pair_eq2 ?????? Heq) normalize nodelta
    799   @nmk #Hfull lapply p generalize in match (foldl_strong ?????); * #x #H #H2
    800   >H2 in H; normalize nodelta -H2 -x #H
    801   @(absurd ((\fst final_policy) ≥ 2^16))
    802   [ @leb_true_to_le <geb_to_leb @p1
    803   | @lt_to_not_le @(le_to_lt_to_lt … (proj2 ?? (proj1 ?? (pi2 ?? old_policy))))
    804     >(proj2 ?? H) >(proj2 ?? (pi2 ?? old_policy)) cases daemon (* XXX *)
    805   ]
     912      〈eqb final_added 0, Some ? final_policy〉.
     913[ / by I/
    806914| normalize nodelta lapply p generalize in match (foldl_strong ?????); * #x #H #H2
    807   >H2 in H; normalize nodelta #H @conj
    808   [ @H
     915  >H2 in H; normalize nodelta -H2 -x #H @conj
     916  [ @conj
     917    [ @(proj1 ?? H)
     918    | #H2 @(proj2 ?? H) @eqb_true_to_eq @H2
     919    ]
    809920  | @not_le_to_lt @leb_false_to_not_le <geb_to_leb @p1
    810921  ]
    811 | lapply (pi2 ?? acc) >p #Hpolicy normalize nodelta in Hpolicy;
     922| (* XXX complicated proof *) cases daemon 
     923| normalize nodelta @conj [ @conj [ @conj [ @conj [ @conj [ @conj
     924  [ #i #Hi / by refl/
     925  | #i #Hi @conj [ >nth_nil #H @⊥ @H | #H elim H #x -H #H
     926                   normalize in Hi; @⊥ @(absurd ? Hi) @not_le_Sn_O ]
     927  ]
     928  | / by refl/
     929  ]]]]]
     930  [4: #_]
     931  #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O
     932]
     933qed.
     934     
     935(* old proof | lapply (pi2 ?? acc) >p #Hpolicy normalize nodelta in Hpolicy;
    812936  cases (dec_eq_jump_length new_length old_length) #Hlength normalize nodelta
    813937  @conj [1,3: @conj [1,3: @conj [1,3: @conj [1,3: @conj [1,3: @conj
     
    11791303  ]
    11801304]
    1181 qed.
     1305qed.*)
    11821306
    11831307(* this might be replaced by a coercion: (∀x.A x → B x) → Σx.A x → Σx.B x *)
     
    12201344
    12211345let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (length ? l) 2^16) (n: ℕ)
    1222   on n:(Σx:bool × (option jump_expansion_policy).
     1346  on n:(Σx:bool × (option ppc_pc_map).
    12231347    let 〈c,pol〉 ≝ x in
    12241348    match pol with
    12251349    [ None ⇒ True
    1226     | Some x ⇒ And (And (And (out_of_program_none program x) (jump_in_policy program x)) (\fst x < 2^16)) (policy_isize_sum program x)
     1350    | Some x ⇒
     1351      And (And (And
     1352        (out_of_program_none program x)
     1353        (jump_in_policy program x))
     1354        (policy_isize_sum program (create_label_map program) x))
     1355        (\fst x < 2^16)
    12271356    ]) ≝
     1357  let labels ≝ create_label_map program in
    12281358  match n with
    1229   [ O   ⇒ 〈true,Some ? (pi1 ?? (jump_expansion_start program))〉
     1359  [ O   ⇒ 〈true,Some ? (pi1 ?? (jump_expansion_start program labels))〉
    12301360  | S m ⇒ let 〈ch,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in
    1231           match z return λx. z=x → Σa:bool × (option jump_expansion_policy).? with
     1361          match z return λx. z=x → Σa:bool × (option ppc_pc_map).? with
    12321362          [ None    ⇒ λp2.〈false,None ?〉
    12331363          | Some op ⇒ λp2.if ch
    1234             then pi1 ?? (jump_expansion_step program (create_label_map program op) «op,?»)
     1364            then pi1 ?? (jump_expansion_step program labels «op,?»)
    12351365            else (jump_expansion_internal program m)
    12361366          ] (refl … z)
     
    12381368[ normalize nodelta @conj
    12391369  [ @conj
    1240     [ @(proj1 ?? (pi2 ?? (jump_expansion_start program)))
     1370    [ @(pi2 ?? (jump_expansion_start program (create_label_map program)))
    12411371    | (* XXX *) cases daemon
    12421372    ]
     
    12451375| lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta / by /
    12461376| lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta / by /
    1247 | normalize nodelta cases (jump_expansion_step program (create_label_map program op) «op,?»)
     1377| normalize nodelta cases (jump_expansion_step program labels «op,?»)
    12481378  #p cases p -p #p #r cases r normalize nodelta
    12491379  [ #H / by I/
     
    12521382      [ @conj
    12531383        [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))))
    1254         | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))))
     1384        | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))))
    12551385        ]
    1256       | @(proj2 ?? H)
    1257       ]
    1258     | @(proj2 ?? (proj1 ?? H))
     1386      | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))))
     1387      ]
     1388    | @(proj2 ?? H)
    12591389    ]
    12601390  ]
     
    12621392qed.
    12631393
    1264 lemma pe_int_refl: ∀program.reflexive ? (policy_equal_int program).
     1394lemma pe_int_refl: ∀program.reflexive ? (policy_equal program).
    12651395#program whd #x whd #n #Hn
    1266 cases (bvt_lookup … (bitvector_of_nat 16 n) (\snd x) 〈0,0,short_jump〉)
    1267 #y cases y -y #y #z normalize nodelta @refl
    1268 qed.
    1269 
    1270 lemma pe_int_sym: ∀program.symmetric ? (policy_equal_int program).
     1396cases (bvt_lookup … (bitvector_of_nat 16 n) (\snd x) 〈0,None ?〉)
     1397#y #z normalize nodelta @refl
     1398qed.
     1399
     1400lemma pe_int_sym: ∀program.symmetric ? (policy_equal program).
    12711401#program whd #x #y #Hxy whd #n #Hn
    1272 lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,0,short_jump〉)
    1273 #z cases z -z #x1 #x2 #x3
    1274 cases (bvt_lookup … (bitvector_of_nat ? n) (\snd y) 〈0,0,short_jump〉)
    1275 #z cases z -z #y1 #y2 #y3 normalize nodelta //
     1402lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,None ?〉)
     1403#x1 #x2
     1404cases (bvt_lookup … (bitvector_of_nat ? n) (\snd y) 〈0,None ?〉)
     1405#y1 #y2 normalize nodelta //
    12761406qed.
    12771407 
    1278 lemma pe_int_trans: ∀program.transitive ? (policy_equal_int program).
    1279 #program whd #x #y #z whd in match (policy_equal_int ???); whd in match (policy_equal_int ?y ?);
    1280 whd in match (policy_equal_int ? x z); #Hxy #Hyz #n #Hn lapply (Hxy n Hn) -Hxy
    1281 lapply (Hyz n Hn) -Hyz cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,0,short_jump〉)
    1282 #z cases z -z #x1 #x2 #x3
    1283 cases (bvt_lookup … (bitvector_of_nat ? n) (\snd y) 〈0,0,short_jump〉) #z cases z -z 
    1284 #y1 #y2 #y3
    1285 cases (bvt_lookup … (bitvector_of_nat ? n) (\snd z) 〈0,0,short_jump〉) #z cases z -z 
    1286 #z1 #z2 #z3 normalize nodelta //
    1287 qed.
    1288 
    1289 definition policy_equal ≝
    1290   λprogram:list labelled_instruction.λp1,p2:option jump_expansion_policy.
     1408lemma pe_int_trans: ∀program.transitive ? (policy_equal program).
     1409#program whd #x #y #z whd in match (policy_equal ???); whd in match (policy_equal ?y ?);
     1410whd in match (policy_equal ? x z); #Hxy #Hyz #n #Hn lapply (Hxy n Hn) -Hxy
     1411lapply (Hyz n Hn) -Hyz cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,None ?〉)
     1412#x1 #x2
     1413cases (bvt_lookup … (bitvector_of_nat ? n) (\snd y) 〈0,None ?〉) #y1 #y2
     1414cases (bvt_lookup … (bitvector_of_nat ? n) (\snd z) 〈0,None ?〉) #z1 #z2
     1415normalize nodelta //
     1416qed.
     1417
     1418definition policy_equal_opt ≝
     1419  λprogram:list labelled_instruction.λp1,p2:option ppc_pc_map.
    12911420  match p1 with
    12921421  [ Some x1 ⇒ match p2 with
    1293               [ Some x2 ⇒ policy_equal_int program x1 x2
     1422              [ Some x2 ⇒ policy_equal program x1 x2
    12941423              | _       ⇒ False
    12951424              ]
     
    12971426  ].
    12981427
    1299 lemma pe_refl: ∀program.reflexive ? (policy_equal program).
     1428lemma pe_refl: ∀program.reflexive ? (policy_equal_opt program).
    13001429#program whd #x whd cases x
    13011430[ //
     
    13041433qed.
    13051434
    1306 lemma pe_sym: ∀program.symmetric ? (policy_equal program).
     1435lemma pe_sym: ∀program.symmetric ? (policy_equal_opt program).
    13071436#program whd #x #y #Hxy whd cases y in Hxy;
    13081437[ cases x
     
    13111440  ]
    13121441| #y' cases x
    1313   [ #H @⊥ @(absurd ? H) whd in match (policy_equal ???); @nmk #H destruct (H)
     1442  [ #H @⊥ @(absurd ? H) whd in match (policy_equal_opt ???); @nmk #H destruct (H)
    13141443  | #x' #H @pe_int_sym @H
    13151444  ]
     
    13171446qed.
    13181447
    1319 lemma pe_trans: ∀program.transitive ? (policy_equal program).
     1448lemma pe_trans: ∀program.transitive ? (policy_equal_opt program).
    13201449#program whd #x #y #z cases x
    13211450[ #Hxy #Hyz >Hxy in Hyz; //
     
    13501479
    13511480lemma pe_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
    1352   ∀n.policy_equal program (\snd (pi1 ?? (jump_expansion_internal program n)))
     1481  ∀n.policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program n)))
    13531482   (\snd (pi1 ?? (jump_expansion_internal program (S n)))) →
    1354   policy_equal program (\snd (pi1 ?? (jump_expansion_internal program (S n))))
     1483  policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program (S n))))
    13551484    (\snd (pi1 ?? (jump_expansion_internal program (S (S n))))).
    13561485#program #n #Heq
     
    13631492 
    13641493lemma equal_remains_equal: ∀program:(Σl:list labelled_instruction.|l| < 2^16).∀n:ℕ.
    1365   policy_equal program (\snd (pi1 … (jump_expansion_internal program n)))
     1494  policy_equal_opt program (\snd (pi1 … (jump_expansion_internal program n)))
    13661495   (\snd (pi1 … (jump_expansion_internal program (S n)))) →
    1367   ∀k.k ≥ n → policy_equal program (\snd (pi1 … (jump_expansion_internal program n)))
     1496  ∀k.k ≥ n → policy_equal_opt program (\snd (pi1 … (jump_expansion_internal program n)))
    13681497   (\snd (pi1 … (jump_expansion_internal program k))).
    13691498#program #n #Heq #k #Hk elim (le_plus_k … Hk); #z #H >H -H -Hk -k;
     
    13791508
    13801509(* this number monotonically increases over iterations, maximum 2*|program| *)
    1381 let rec measure_int (program: list labelled_instruction) (policy: jump_expansion_policy) (acc: ℕ)
     1510let rec measure_int (program: list labelled_instruction) (policy: ppc_pc_map) (acc: ℕ)
    13821511 on program: ℕ ≝
    13831512 match program with
    13841513 [ nil      ⇒ acc
    1385  | cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,00
    1386 ,short_jump〉)) with
    1387    [ long_jump   ⇒ measure_int t policy (acc + 2)
    1388    | medium_jump ⇒ measure_int t policy (acc + 1)
    1389    | _           ⇒ measure_int t policy acc
     1514 | cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,None ?〉)) with
     1515   [ None ⇒ measure_int t policy acc
     1516   | Some j ⇒ match j with
     1517     [ long_jump   ⇒ measure_int t policy (acc + 2)
     1518     | medium_jump ⇒ measure_int t policy (acc + 1)
     1519     | _           ⇒ measure_int t policy acc
     1520     ]
    13901521   ]
    13911522 ].
     
    13981529  [ / by refl/
    13991530  | #h #t #Hd #x whd in match (measure_int ???); whd in match (measure_int ?? x);
    1400     cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,0,short_jump〉))
     1531    cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,None ?〉))
    14011532    [ normalize nodelta @Hd
    1402     |2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus
    1403       @Hd
     1533    | #x cases x
     1534      [ normalize nodelta @Hd
     1535      |2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus
     1536        @Hd
     1537      ]
    14041538    ]
    14051539  ]
     
    14121546[ normalize @le_n
    14131547| #h #t #Hind whd in match (measure_int ???);
    1414   cases (\snd (lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,0,short_jump〉))
     1548  cases (\snd (lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,None ?〉))
    14151549  [ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/
    1416   |2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?)
    1417     @le_plus [1,3: @Hind |2,4: / by le_n/ ]
     1550  | #x cases x
     1551    [ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/
     1552    |2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?)
     1553      @le_plus [1,3: @Hind |2,4: / by le_n/ ]
     1554    ]
    14181555  ]
    14191556]
     
    14211558
    14221559lemma measure_incr_or_equal: ∀program:Σl:list labelled_instruction.|l|<2^16.
    1423   ∀policy:Σp:jump_expansion_policy.
    1424     out_of_program_none program p ∧ jump_in_policy program p ∧ \fst p < 2^16 ∧ policy_isize_sum program p.
     1560  ∀policy:Σp:ppc_pc_map.
     1561    out_of_program_none program p ∧ jump_in_policy program p ∧
     1562    policy_isize_sum program (create_label_map program) p ∧ \fst p < 2^16.
    14251563  ∀l.|l| ≤ |program| → ∀acc:ℕ.
    1426   match \snd (jump_expansion_step program (create_label_map program policy) policy) with
     1564  match \snd (jump_expansion_step program (create_label_map program) policy) with
    14271565  [ None   ⇒ True
    14281566  | Some p ⇒ measure_int l policy acc ≤ measure_int l p acc
     
    14311569[ #Hp #acc cases (jump_expansion_step ???) #pi1 cases pi1 #p #q -pi1; cases q [ // | #x #_ @le_n ]
    14321570| #h #t #Hind #Hp #acc
    1433   lapply (refl ? (jump_expansion_step program (create_label_map program policy) policy))
     1571  lapply (refl ? (jump_expansion_step program (create_label_map program) policy))
    14341572  cases (jump_expansion_step ???) in ⊢ (???% → %); #pi1 cases pi1 -pi1 #c #r cases r
    14351573  [ / by I/
    14361574  | #x normalize nodelta #Hx #Hjeq lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx)))) (|t|) Hp)
    14371575    whd in match (measure_int ???); whd in match (measure_int ? x ?);
    1438     cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,0,short_jump〉)
    1439     #z cases z -z #x1 #x2 #x3
    1440     cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd x) 〈0,0,short_jump〉)
    1441     #z cases z -z #y1 #y2 #y3
    1442     normalize nodelta #Hj cases Hj
    1443     [ cases x3 cases y3
    1444       [1,4,5,7,8,9: #H @⊥ @H
    1445       |2,3,6: #_ normalize nodelta
    1446         [1,2: @(transitive_le ? (measure_int t x acc))
    1447         |3: @(transitive_le ? (measure_int t x (acc+1)))
    1448         ]
    1449         [2,4,5,6: >measure_plus [1,2: @le_plus_n_r] >measure_plus @le_plus / by le_n/]
    1450         >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn
    1451         ]
    1452     | #Heq >Heq cases y3 normalize nodelta
    1453       [2,3: >measure_plus >measure_plus @le_plus / by le_n/]
    1454       >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn
    1455     ]
    1456   ]
    1457 ]
     1576    cases (dec_is_jump (nth (|t|) ? program 〈None ?, Comment []〉))
     1577    [ #Hj
     1578      elim (proj1 ?? (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx)))))) (|t|) ?) Hj)
     1579      [ #j2 elim (proj1 ?? (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? policy))) (|t|) ?) Hj)
     1580        [ #j1 normalize nodelta
     1581         cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,None ?〉)
     1582         #x1 #x2
     1583         cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd x) 〈0,None ?〉)
     1584         #y1 #y2 normalize nodelta #Hx #Hy >Hx >Hy normalize nodelta
     1585         #Hblerp cases (proj2 ?? Hblerp) cases j1 cases j2
     1586         [1,4,5,7,8,9: #H cases H
     1587         |2,3,6: #_ normalize nodelta
     1588           [1,2: @(transitive_le ? (measure_int t x acc))
     1589           |3: @(transitive_le ? (measure_int t x (acc+1)))
     1590           ]
     1591           [2,4,5,6: >measure_plus [1,2: @le_plus_n_r] >measure_plus @le_plus / by le_n/]
     1592           >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn
     1593         |11,12,13,15,16,17: #H destruct (H)
     1594         |10,14,18: normalize nodelta #_ >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn
     1595         ]
     1596       | @(transitive_le … Hp) @le_n
     1597       ]
     1598     | @(transitive_le … Hp) @le_n
     1599     ]
     1600   | #Hnj   
     1601     lapply (proj1 ?? (jump_not_in_policy (pi1 ?? program) (pi1 ?? policy) (|t|) ?) Hnj)
     1602     [3: lapply (proj1 ?? (jump_not_in_policy (pi1 ?? program) x (|t|) ?) Hnj)
     1603       [3: cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,None ?〉)
     1604          #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd x) 〈0,None ?〉)
     1605          #y1 #y2 #Hy #Hx >Hx >Hy normalize nodelta
     1606          #_ >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn
     1607       |1: @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx))))))
     1608       |2: @(transitive_le … Hp) @le_n
     1609       ]
     1610     |1: @(proj1 ?? (proj1 ?? (pi2 ?? policy)))
     1611     |2: @(transitive_le … Hp) @le_n
     1612     ]
     1613   ]
     1614 ]
    14581615qed.
    14591616
     
    14751632lemma measure_full: ∀program.∀policy.
    14761633  measure_int program policy 0 = 2*|program| → ∀i.i<|program| →
    1477   (\snd (bvt_lookup ?? (bitvector_of_nat ? i) (\snd policy) 〈0,0,short_jump〉)) = long_jump.
    1478 #program #policy elim program
     1634  (\snd (bvt_lookup ?? (bitvector_of_nat ? i) (\snd policy) 〈0,None ?〉)) = None ? ∨
     1635  (\snd (bvt_lookup ?? (bitvector_of_nat ? i) (\snd policy) 〈0,None ?〉)) = Some ? long_jump.
     1636#program #policy elim program
    14791637[ #Hm #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    14801638| #h #t #Hind #Hm #i #Hi cut (measure_int t policy 0 = 2*|t|)
    14811639  [ whd in match (measure_int ???) in Hm;
    1482     cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,0,short_jump〉)) in Hm;
     1640    cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,None ?〉)) in Hm;
    14831641    normalize nodelta
    14841642    [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/
    1485     | >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy))
    1486       <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize
    1487       >(commutative_plus (|t|) 0) <plus_O_n <minus_n_O
    1488       >plus_n_Sm @le_n
    1489     | >measure_plus <times_n_Sm >commutative_plus #H lapply (injective_plus_r … H) //
     1643    | #j cases j normalize nodelta
     1644      [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/
     1645      | >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy))
     1646        <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize
     1647        >(commutative_plus (|t|) 0) <plus_O_n <minus_n_O
     1648        >plus_n_Sm @le_n
     1649      | >measure_plus <times_n_Sm >commutative_plus #H lapply (injective_plus_r … H) //
     1650      ]
    14901651    ]
    14911652  | #Hmt cases (le_to_or_lt_eq … Hi) -Hi;
    14921653  [ #Hi @(Hind Hmt i (le_S_S_to_le … Hi))
    14931654  | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm;
    1494     cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,0,short_jump〉)) in Hm;
     1655    cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,None ?〉)) in Hm;
    14951656    normalize nodelta
    1496     [ >Hmt normalize <plus_n_O >(commutative_plus (|t|) (S (|t|)))
    1497       >plus_n_Sm #H @⊥ @(absurd ? (bla ?? H)) @sth_not_s
    1498     | >measure_plus >Hmt normalize <plus_n_O >commutative_plus normalize
    1499       #H @⊥ @(absurd ? (injective_plus_r … (injective_S ?? H))) @sth_not_s
    1500     | #_ //
     1657    [ #_ %1 @refl
     1658    | #j cases j normalize nodelta
     1659      [ >Hmt normalize <plus_n_O >(commutative_plus (|t|) (S (|t|)))
     1660        >plus_n_Sm #H @⊥ @(absurd ? (bla ?? H)) @sth_not_s
     1661      | >measure_plus >Hmt normalize <plus_n_O >commutative_plus normalize
     1662        #H @⊥ @(absurd ? (injective_plus_r … (injective_S ?? H))) @sth_not_s
     1663      | #_ %2 @refl
     1664      ]
    15011665    ]
    15021666  ]]
     
    15051669
    15061670lemma measure_special: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
    1507   ∀policy:Σp:jump_expansion_policy.
    1508     out_of_program_none program p ∧ jump_in_policy program p ∧ \fst p < 2^16 ∧ policy_isize_sum program p.
    1509   match (\snd (pi1 ?? (jump_expansion_step program (create_label_map program policy) policy))) with
     1671  ∀policy:Σp:ppc_pc_map.
     1672    out_of_program_none program p ∧ jump_in_policy program p ∧ policy_isize_sum program (create_label_map program) p ∧ \fst p < 2^16.
     1673  match (\snd (pi1 ?? (jump_expansion_step program (create_label_map program) policy))) with
    15101674  [ None ⇒ True
    1511   | Some p ⇒ measure_int program policy 0 = measure_int program p 0 → policy_equal_int program policy p ].
    1512 #program #policy lapply (refl ? (pi1 ?? (jump_expansion_step program (create_label_map program policy) policy)))
    1513 cases (jump_expansion_step program (create_label_map program policy) policy) in ⊢ (???% → %);
     1675  | Some p ⇒ measure_int program policy 0 = measure_int program p 0 → policy_equal program policy p ].
     1676#program #policy lapply (refl ? (pi1 ?? (jump_expansion_step program (create_label_map program) policy)))
     1677cases (jump_expansion_step program (create_label_map program) policy) in ⊢ (???% → %);
    15141678#p cases p -p #ch #pol normalize nodelta cases pol
    15151679[ / by I/
     
    15171681  @(list_ind ?  (λx.|x| ≤ |pi1 ?? program| →
    15181682      measure_int x policy 0 = measure_int x p 0 →
    1519       policy_equal_int x policy p) ?? (pi1 ?? program))
     1683      policy_equal x policy p) ?? (pi1 ?? program))
    15201684 [ #_ #_ #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O
    15211685 | #h #t #Hind #Hp #Hm #i #Hi cases (le_to_or_lt_eq … Hi) -Hi;
     
    15231687     [ @(transitive_le … Hp) / by /
    15241688     | whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm;
    1525        lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (|t|) Hp)
    1526        cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉) in Hm;
    1527        #x cases x -x #x1 #x2 #x3
    1528        cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉);
    1529        #y cases y -y #y1 #y2 #y3
    1530        cases x3 cases y3 normalize nodelta
    1531        [1: #H #_ @H
    1532        |2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
    1533          lapply (measure_incr_or_equal program policy t ? 0)
    1534          [1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
    1535        |4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 |2,4,6: destruct (H2) ]
    1536        |5: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 1)
    1537          #H #_ @(injective_plus_r … H)
    1538        |6: >measure_plus >measure_plus
    1539           change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???))
    1540           #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l
    1541           lapply (measure_incr_or_equal program policy t ? 0)
    1542           [ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
    1543        |9: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 2)
    1544          #H #_ @(injective_plus_r … H)
    1545        ]
    1546      | @(le_S_S_to_le … Hi)
     1689       lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (|t|) Hp) #Hinc
     1690       cases (dec_is_jump (nth (|t|) ? program 〈None ?, Comment []〉))
     1691       [ #Hj elim (proj1 ?? (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))))) (|t|) ?) Hj)
     1692         [ #j2 elim (proj1 ?? (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? policy))) (|t|) ?) Hj)
     1693           [ #j1 normalize nodelta
     1694             cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,None ?〉) in Hm Hinc; #x1 #x2
     1695             cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,None ?〉); #y1 #y2
     1696             #Hm #Hinc #Hx #Hy lapply Hm -Hm; lapply Hinc -Hinc; >Hx >Hy normalize nodelta
     1697             cases j1 cases j2 normalize nodelta
     1698             [1: / by /
     1699             |2,3: >measure_plus #_ #H @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
     1700               lapply (measure_incr_or_equal program policy t ? 0)
     1701               [1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
     1702             |4,7,8: #H elim (proj2 ?? H) #H2 [1,3,5: cases H2 |2,4,6: destruct (H2) ]
     1703             |5: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 1)
     1704               #_ #H @(injective_plus_r … H)
     1705             |6: >measure_plus >measure_plus
     1706               change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???))
     1707               #_ #H @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l
     1708               lapply (measure_incr_or_equal program policy t ? 0)
     1709               [ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
     1710             |9: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 2)
     1711               #_ #H @(injective_plus_r … H)
     1712             ]
     1713           | @(transitive_le … Hp) @le_n
     1714           ]
     1715         | @(transitive_le … Hp) @le_n
     1716         ]
     1717       | #Hnj lapply (proj1 ?? (jump_not_in_policy (pi1 ?? program) (pi1 ?? policy) (|t|) ?) Hnj)
     1718         [3: lapply (proj1 ?? (jump_not_in_policy (pi1 ?? program) p (|t|) ?) Hnj)
     1719           [3: cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,None ?〉) in Hm Hinc;
     1720               #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd p) 〈0,None ?〉)
     1721               #y1 #y2 #Hm #Hinc #Hy #Hx lapply Hm -Hm; lapply Hinc -Hinc; >Hx >Hy normalize nodelta
     1722               #_ / by /
     1723           |1: @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol))))))
     1724           |2: @(transitive_le … Hp) @le_n
     1725           ]
     1726        |1: @(proj1 ?? (proj1 ?? (pi2 ?? policy)))
     1727        |2: @(transitive_le … Hp) @le_n
     1728        ]
     1729      ]
     1730      | @(le_S_S_to_le … Hi)
    15471731     ]
    15481732   | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm;
    15491733     whd in match (measure_int ? p ?) in Hm;
    15501734     lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol)))) (|t|) Hp)
     1735     (* XXX *) cases daemon
     1736     (* change proof for not_jump
    15511737     cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉) in   
    15521738Hm;
     
    15641750        #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l
    15651751        lapply (measure_incr_or_equal program policy t ? 0)
    1566         [ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
    1567      ]
     1752        [ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by / 
     1753     ] *)
    15681754   ]
    15691755 ]
     
    15861772
    15871773lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction.|l| < 2^16.
    1588   |l| ≤ |program| → measure_int l (jump_expansion_start program) 0 = 0.
     1774  |l| ≤ |program| → measure_int l (jump_expansion_start program (create_label_map program)) 0 = 0.
    15891775 #l #program elim l
    15901776 [ //
    1591  | #h #t #Hind #Hp whd in match (measure_int ???);
     1777 | #h #t #Hind #Hp cases daemon
     1778 
     1779 (* old proof whd in match (measure_int ???);
     1780   cases daemo
    15921781   cases (dec_is_jump (nth (|t|) ? program 〈None ?, Comment []〉)) #Hj
    1593    [ >(lookup_opt_lookup_hit … (proj2 ?? (pi2 ?? (jump_expansion_start program)) (|t|) ? Hj) 〈0,0,short_jump〉)
     1782   [ lapply
     1783       (proj1 ?? (pi2 ??
     1784          (jump_expansion_start program (create_label_map program))))) 〈0,None ?〉)
    15941785     [ normalize nodelta @Hind @le_S_to_le ]
    15951786     @Hp
     
    16021793       ]
    16031794     ]
    1604    ]
     1795   ]*)
    16051796 ]
    16061797qed.
     
    16081799(* the actual computation of the fixpoint *)
    16091800definition je_fixpoint: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
    1610   Σp:option jump_expansion_policy.∃n.∀k.n < k →
    1611     policy_equal program (\snd (pi1 ?? (jump_expansion_internal program k))) p.
     1801  Σp:option ppc_pc_map.∃n.∀k.n < k →
     1802    policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program k))) p.
    16121803#program @(\snd (pi1 ?? (jump_expansion_internal program (2*|program|))))
     1804
     1805cases daemon
     1806
     1807(* old proof
    16131808cases (dec_bounded_exists (λk.policy_equal (pi1 ?? program)
    16141809   (\snd (pi1 ?? (jump_expansion_internal program k)))
    16151810   (\snd (pi1 ?? (jump_expansion_internal program (S k))))) ? (2*|program|))
     1811 cases daemon
    16161812[ #Hex elim Hex -Hex #x #Hx @(ex_intro … x) #k #Hk
    16171813  @pe_trans
     
    17361932      @dec_eq_jump_length 
    17371933  ]
    1738 ]
    1739 qed.
    1740 
    1741 (* Take a policy of 〈pc, addr, jump_length〉 tuples, and transform it into
    1742  * a map from pc to jump_length. This cannot be done earlier because the pc
    1743  * changes between iterations. *)
    1744 let rec transform_policy (n: nat) (policy: jump_expansion_policy) (acc: BitVectorTrie jump_length 16) on n:
    1745   BitVectorTrie jump_length 16 ≝
    1746   match n with
    1747   [ O    ⇒ acc
    1748   | S n' ⇒
    1749     match lookup_opt … (bitvector_of_nat 16 n') (\snd policy) with
    1750     [ None   ⇒ transform_policy n' policy acc
    1751     | Some x ⇒ let 〈pc,addr,length〉 ≝ x in
    1752       transform_policy n' policy (insert … (bitvector_of_nat 16 pc) length acc)
    1753     ]
    1754   ].
     1934] *)
     1935qed.
    17551936
    17561937(* The glue between Policy and Assembly. *)
    17571938definition jump_expansion':
    17581939 ∀program:preamble × (Σl:list labelled_instruction.|l| < 2^16).
    1759  ∀lookup_labels.policy_type lookup_labels
    1760  λprogram.λlookup_labels.λpc.
    1761   let policy ≝
    1762     transform_policy (|\snd program|) (pi1 … (je_fixpoint (\snd program))) (Stub ??) in
    1763   «bvt_lookup ? ? pc policy long_jump,?».
    1764   cases daemon (* XXX later *)
    1765 qed.
     1940 ℕ → ℕ × (option jump_length)
     1941 λprogram.λppc:ℕ.
     1942  let policy ≝ pi1 … (je_fixpoint (\snd program)) in
     1943  match policy with
     1944  [ None ⇒ 〈0, Some ? long_jump〉
     1945  | Some x ⇒ bvt_lookup ?? (bitvector_of_nat 16 ppc) (\snd x) 〈0,Some ? long_jump〉
     1946  ].
Note: See TracChangeset for help on using the changeset viewer.