Context Navigation

← Previous Change
Next Change →

Assembly.ma

Timestamp:

Dec 14, 2011, 2:44:42 PM (9 years ago)

Author:

boender

Message:

added alias to ASM/BitVectorTrie
removed double include from common/Errors
externalised label generation in ASM/Assembly, plus stuff to make it compile

File:

: 1 edited

src/ASM/Assembly.ma (modified) (48 diffs)

Legend:

: Unmodified
: Added
: Removed

src/ASM/Assembly.ma

-                      r1607
+                      r1609
 include alias "basics/logic.ma".
 include alias "arithmetics/nat.ma".
+include "utilities/extralib.ma".
 definition assembly_preinstruction ≝
 …
 (* jump_expansion_policy: instruction number ↦ 〈pc, jump_length〉 *)
 definition jump_expansion_policy ≝ BitVectorTrie (ℕ × jump_length) 16.
+(* jump_expansion_policy: instruction number ↦ 〈pc, addr, jump_length〉 *)
+definition jump_expansion_policy ≝ BitVectorTrie (ℕ × ℕ × jump_length) 16.
 definition expand_relative_jump_internal:
 …
      let 〈pc,labels〉 ≝ acc in
      let 〈label,instr〉 ≝ x in
           let new_labels ≝
           match label with
           [ None   ⇒ labels
           | Some l ⇒ add … labels l 〈|prefix|, pc〉
           ] in
           let jmp_len ≝ \snd (bvt_lookup ?? (bitvector_of_nat 16 (|prefix|)) policy 〈pc, long_jump〉) in
           〈add_instruction_size pc jmp_len instr, new_labels〉
+       let new_labels ≝
+       match label with
+       [ None   ⇒ labels
+       | Some l ⇒ add … labels l 〈|prefix|, pc〉
+       ] in
+     let 〈i1,i2,jmp_len〉 ≝ bvt_lookup ?? (bitvector_of_nat 16 (|prefix|)) policy 〈0, 0, long_jump〉 in
+       〈add_instruction_size pc jmp_len instr, new_labels〉
     ) 〈0, empty_map …〉 in
     final_labels.
 …
 qed.
 definition select_reljump_length: label_map → ℕ → Identifier → jump_length ≝
+definition select_reljump_length: label_map → ℕ → Identifier → ℕ ×jump_length ≝
   λlabels.λpc.λlbl.
   let 〈n, addr〉 ≝ lookup_def … labels lbl 〈0, pc〉 in
   if leb pc addr (* forward jump *)
   then if leb (addr - pc) 126
        then short_jump
        else long_jump
+       then 〈addr, short_jump〉
+       else 〈addr, long_jump〉
   else if leb (pc - addr) 129
        then short_jump
        else long_jump.
 definition select_call_length: label_map → ℕ → Identifier → jump_length ≝
+       then 〈addr, short_jump〉
+       else 〈addr, long_jump〉.
+definition select_call_length: label_map → ℕ → Identifier → ℕ × jump_length ≝
   λlabels.λpc_nat.λlbl.
   let pc ≝ bitvector_of_nat 16 pc_nat in
+  let addr ≝ bitvector_of_nat 16 (\snd (lookup_def ? ? labels lbl 〈0, pc_nat〉)) in
+  let addr_nat ≝ (\snd (lookup_def ? ? labels lbl 〈0, pc_nat〉)) in
+  let addr ≝ bitvector_of_nat 16 addr_nat in
   let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 addr in
   let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
   if eq_bv ? fst_5_addr fst_5_pc
   then medium_jump
   else long_jump.
+  then 〈addr_nat, medium_jump〉
+  else 〈addr_nat, long_jump〉.
 definition select_jump_length: label_map → ℕ → Identifier → jump_length ≝
+definition select_jump_length: label_map → ℕ → Identifier → ℕ × jump_length ≝
   λlabels.λpc.λlbl.
   let 〈n, addr〉 ≝ lookup_def … labels lbl 〈0, pc〉 in
   if leb pc addr
   then if leb (addr - pc) 126
        then short_jump
+       then 〈addr, short_jump〉
        else select_call_length labels pc lbl
   else if leb (pc - addr) 129
        then short_jump
+       then 〈addr, short_jump〉
        else select_call_length labels pc lbl.
 definition jump_expansion_step_instruction: label_map → ℕ →
   preinstruction Identifier → option jump_length ≝
+  preinstruction Identifier → option (ℕ × jump_length) ≝
   λlabels.λpc.λi.
   match i with
 …
   ∀i:ℕ.i < |prefix| →
   (is_jump (nth i ? prefix 〈None ?, Comment []〉) ↔
    ∃p,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,j〉).
+   ∃p,a,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,a,j〉).
 (* these should be moved to BitVector at some point *)
 …
  jump_in_policy prefix p).
   ∀i:ℕ.i < |prefix| →
   ¬is_jump (nth i ? prefix 〈None ?, Comment []〉) ↔
   lookup_opt … (bitvector_of_nat 16 i) policy = None ?.
+  iff (¬is_jump (nth i ? prefix 〈None ?, Comment []〉))
+  (lookup_opt … (bitvector_of_nat 16 i) policy = None ?).
  #prefix #policy #i #Hi @conj
  [ #Hnotjmp lapply (refl ? (lookup_opt … (bitvector_of_nat 16 i) policy))
    cases (lookup_opt … (bitvector_of_nat 16 i) policy) in ⊢ (???% → ?);
    [ #H @H
    | #x cases x #y #z #H @⊥ @(absurd ? ? Hnotjmp) @(proj2 ?? (proj2 ?? (pi2 ?? policy) i Hi))
      @(ex_intro … y (ex_intro … z H))
+   | #x cases x -x #x #z cases x -x #x #y #H @⊥ @(absurd ? ? Hnotjmp) @(proj2 ?? (proj2 ?? (pi2 ?? policy) i Hi))
+     @(ex_intro ?? x (ex_intro ?? y (ex_intro ?? z H)))
+   ]
  | #Hnone @nmk #Hj lapply (proj1 ?? (proj2 ?? (pi2 ?? policy) i Hi) Hj)
    #H elim H -H; #x #H elim H -H; #y #H >H in Hnone; #abs destruct (abs)
+   #H elim H -H; #x #H elim H -H; #y #H elim H -H; #z #H >H in Hnone; #abs destruct (abs)
+ ]
 qed.
 definition jump_expansion_start:
   ∀program:(Σl:list labelled_instruction.|l| < 2^16).
 …
     jump_in_policy program policy ∧
     ∀i.i < |program| → is_jump (nth i ? program 〈None ?, Comment []〉) →
      lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈0,short_jump〉 ≝
+     lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈0,0,short_jump〉 ≝
   λprogram.
   foldl_strong (option Identifier × pseudo_instruction)
 …
     jump_in_policy prefix policy ∧
     ∀i.i < |prefix| → is_jump (nth i ? prefix 〈None ?, Comment []〉) →
       lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈0,short_jump〉)
+      lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈0,0,short_jump〉)
   program
   (λprefix.λx.λtl.λprf.λpolicy.
 …
    match instr with
    [ Instruction i ⇒ match i with
      [ JC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
      | JNC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
      | JZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
      | JNZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
      | JB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
      | JNB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
      | JBC _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
      | CJNE _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
      | DJNZ _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
+     [ JC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
+     | JNC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
+     | JZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
+     | JNZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
+     | JB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
+     | JNB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
+     | JBC _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
+     | CJNE _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
+     | DJNZ _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
      | _ ⇒ (pi1 … policy)
+     ]
    | Call c ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
    | Jmp j  ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
    | _      ⇒ (pi1 … policy)
+   | Call c ⇒ bvt_insert (ℕ×ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
+   | Jmp j  ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
+   | _      ⇒ (pi1 ?? policy)
+   ]
   ) (Stub ? ?).
 …
     >(nth_append_second ? ? prefix ? ? (le_n (|prefix|))) <minus_n_n #H @⊥ @H
+   ]
    #H elim H; -H; #t1 #H elim H; -H #t2 #H
+   #H elim H; -H; #t1 #H elim H; -H #t2 #H elim H; -H; #t3 #H
    >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?) in H;
    [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61:
 …
    >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n //
+  ]
   @(ex_intro ?? 0 (ex_intro ?? short_jump (lookup_opt_insert_hit ?? 16 ? policy)))
+  @(ex_intro ?? 0 (ex_intro ?? 0 (ex_intro ?? short_jump (lookup_opt_insert_hit ?? 16 ? policy))))
+ ]
  #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
 …
  λprogram.λop.λp.
   (∀i:ℕ.i < |program| →
+    jmpleq
+      (\snd (bvt_lookup … (bitvector_of_nat ? i) op 〈0,short_jump〉))
+      (\snd (bvt_lookup … (bitvector_of_nat ? i) p 〈0,short_jump〉))).
+    let 〈i1,i2,oj〉 ≝ bvt_lookup ?? (bitvector_of_nat ? i) op 〈0,0,short_jump〉 in
+    let 〈i3,i4,j〉 ≝ bvt_lookup ?? (bitvector_of_nat ? i) p 〈0,0,short_jump〉 in
+    jmpleq oj j).
+definition policy_safe: (*label_map → *)jump_expansion_policy → Prop ≝
+ (*λlabels.*)λpolicy.
+ bvt_forall (ℕ×ℕ×jump_length) 16 policy (λn.λx.let 〈pc_nat,addr_nat,jmp_len〉 ≝ x in
+    match jmp_len with
+    [ short_jump  ⇒ if leb pc_nat addr_nat
+       then le (addr_nat - pc_nat) 126
+       else le (pc_nat - addr_nat) 129
+    | medium_jump ⇒
+       let addr ≝ bitvector_of_nat 16 addr_nat in
+       let pc ≝ bitvector_of_nat 16 pc_nat in
+       let 〈fst_5_addr, rest_addr〉 ≝ split bool 5 11 addr in
+       let 〈fst_5_pc, rest_pc〉 ≝ split bool 5 11 pc in
+       eq_bv 5 fst_5_addr fst_5_pc = true
+    | long_jump   ⇒ True
+    ]
+  ).
 definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
+  ∀labels:(Σlm:label_map.∀i:ℕ.lt i (|program|) →
+    ∀l.occurs_exactly_once l program →
+    is_label (nth i ? program 〈None ?, Comment [ ]〉) l →
+    ∃a.lookup … lm l = Some ? 〈i,a〉).
   ∀old_policy:(Σpolicy.
     (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
 …
     policy_increase program old_policy policy)
     ≝
+  λprogram.λold_policy.
+  let labels ≝ create_label_map program old_policy in
+  λprogram.λlabels.λold_policy.
   let 〈final_pc, final_policy〉 ≝
     foldl_strong (option Identifier × pseudo_instruction)
 …
         ] in
       let 〈new_pc, new_policy〉 ≝
         let 〈ignore,old_length〉 ≝ lookup … (bitvector_of_nat 16 (|prefix|)) old_policy 〈0, short_jump〉 in
+        let 〈ignore,old_length〉 ≝ bvt_lookup … (bitvector_of_nat 16 (|prefix|)) old_policy 〈0, 0, short_jump〉 in
         match add_instr with
         [ None    ⇒ (* i.e. it's not a jump *)
           〈add_instruction_size pc long_jump instr, policy〉
         | Some ai ⇒
+        | Some z ⇒ let 〈addr,ai〉 ≝ z in
           let new_length ≝ max_length old_length ai in
           〈add_instruction_size pc new_length instr, insert … (bitvector_of_nat 16 (|prefix|)) 〈pc, new_length〉 policy〉
+          〈add_instruction_size pc new_length instr, insert … (bitvector_of_nat 16 (|prefix|)) 〈pc, addr, new_length〉 policy〉
         ] in
       〈new_pc, new_policy〉
 …
 [ #Hi2 cases (lookup ??? old_policy ?) #h #n cases add_instr
   [ @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2)
   | #z normalize nodelta >lookup_opt_insert_miss
+  | #z cases z -z #z1 #z2 whd in match (snd ???); >lookup_opt_insert_miss
     [ @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2)
     | >eq_bv_sym @bitvector_of_nat_abs
 …
       cases add_instr cases (lookup ??? old_policy ?) normalize nodelta #x #y
       [ @(proj1 ?? Hacc Hj)
+      | #z elim (proj1 ?? Hacc Hj) #h #n elim n -n #n #Hn
+        % [ @h | % [ @n | <Hn @lookup_opt_insert_miss @bitvector_of_nat_abs
+      | #z cases z -z #z1 #z2 elim (proj1 ?? Hacc Hj) #h #n elim n -n #n #H elim H -H #j #Hj
+        @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?))) whd in match (snd ???);
+        >lookup_opt_insert_miss [ @Hj |  @bitvector_of_nat_abs ]
         [3: @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
         |1: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
 …
         @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
         @le_S_S @le_plus_n_r
-        ] ]
+      ]
     | lapply (proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc
       #H elim H -H; #h #H elim H -H; #n cases add_instr cases (lookup ??? old_policy ?)
+      #H elim H -H; #h #H elim H -H; #n #H elim H -H #j cases add_instr cases (lookup ??? old_policy ?)
       normalize nodelta #x #y [2: #z]
       #Hl @(proj2 ?? Hacc) @(ex_intro ?? h (ex_intro ?? n ?))
       [ <Hl @sym_eq @lookup_opt_insert_miss @bitvector_of_nat_abs
+      #Hl @(proj2 ?? Hacc) @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?)))
+      [ <Hl @sym_eq cases z #z1 #z2 whd in match (snd ???); @lookup_opt_insert_miss @bitvector_of_nat_abs
         [3: @lt_to_not_eq @(le_S_S_to_le … Hi)
         |1: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
 …
      [1: #pi | 2,3: #x | 4,5: #id | 6: #x #y] @conj normalize nodelta
      [3,5,11: #H @⊥ @H (* instr is not a jump *)
      |4,6,12: #H elim H -H; #h #H elim H -H #n cases (lookup ??? old_policy ?)
+     |4,6,12: #H elim H -H; #h #H elim H -H #n #H elim H -H #j cases (lookup ??? old_policy ?)
        #x #y normalize nodelta >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
        [1,3,5: #H destruct (H)]
        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
        @le_S_S @le_plus_n_r
      |7,9: (* instr is a jump *) #_ cases (lookup ??? old_policy ?) #h #n
+     |7,9: (* instr is a jump *) #_ cases (lookup ??? old_policy ?) #x cases x #h #n #j
        whd in match (snd ???); @(ex_intro ?? pc)
+       [ @(ex_intro ?? (max_length n (select_jump_length (create_label_map program old_policy) pc id)))
+       | @(ex_intro ?? (max_length n (select_call_length (create_label_map program old_policy) pc id)))
+       ] @lookup_opt_insert_hit
+       [ @(ex_intro ?? (\fst (select_jump_length labels pc id)))
+         @(ex_intro ?? (max_length j (\snd (select_jump_length labels pc id))))
+         cases (select_jump_length labels pc id)
+       | @(ex_intro ?? (\fst (select_call_length labels pc id)))
+         @(ex_intro ?? (max_length j (\snd (select_call_length labels pc id))))
+         cases (select_call_length labels pc id)
+       ] #z1 #z2 normalize nodelta @lookup_opt_insert_hit
      |8,10: #_ //
      |1,2: cases pi
 …
        |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #H @⊥ @H
        |1,2,3,6,7,33,34: #x #y #H @⊥ @H
+       |9,10,14,15: #id #_ cases (lookup ??? old_policy ?) #h #n
+         whd in match (snd ???);
+         @(ex_intro ?? pc (ex_intro ?? (max_length n (select_reljump_length (create_label_map program old_policy) pc id)) ?))
+       |9,10,14,15: #id #_ cases (lookup ??? old_policy ?) #x cases x #h #n #j
+         whd in match (snd ???); @(ex_intro ?? pc)
+         @(ex_intro ?? (\fst (select_reljump_length labels pc id)))
+         @(ex_intro ?? (max_length j (\snd (select_reljump_length labels pc id))))
+         normalize nodelta cases (select_reljump_length labels pc id) #z1 #z2 normalize nodelta
          @lookup_opt_insert_hit
+       |11,12,13,16,17: #x #id #_ cases (lookup ??? old_policy ?) #h #n
+         whd in match (snd ???);
+         @(ex_intro ?? pc (ex_intro ?? (max_length n (select_reljump_length (create_label_map program old_policy) pc id)) ?))
+       |11,12,13,16,17: #x #id #_ cases (lookup ??? old_policy ?) #x cases x #h #n #j
+         whd in match (snd ???); @(ex_intro ?? pc)
+         @(ex_intro ?? (\fst (select_reljump_length labels pc id)))
+         @(ex_intro ?? (max_length j (\snd (select_reljump_length labels pc id))))
+         normalize nodelta cases (select_reljump_length labels pc id) #z1 #z2 normalize nodelta
          @lookup_opt_insert_hit
        |72,73,74: #H elim H -H; #h #H elim H -H #n cases (lookup ??? old_policy ?)
         #x #y normalize nodelta
+       |72,73,74: #H elim H -H; #h #H elim H -H #n #H elim H -H #j cases (lookup ??? old_policy ?)
+        #z cases z -z #x #y #z normalize nodelta
         >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
         [1,3,5: #H destruct (H)]
 …
         @le_S_S @le_plus_n_r
        |41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69: #x
         #H elim H -H; #h #H elim H -H #n cases (lookup ??? old_policy ?)
         #x #y normalize nodelta
+        #H elim H -H; #h #H elim H -H #n #H elim H -H #j cases (lookup ??? old_policy ?)
+        #z cases z -z #x #y #z normalize nodelta
         >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
         [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35: #H destruct (H)]
         @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
         @le_S_S @le_plus_n_r
        |38,39,40,43,44,70,71: #x #y #H elim H -H; #h #H elim H -H #n
         cases (lookup ??? old_policy ?) #x #y normalize nodelta
+       |38,39,40,43,44,70,71: #x #y #H elim H -H; #h #H elim H -H #n #H elim H -H #j
+        cases (lookup ??? old_policy ?) #z cases z -z #x #y #z normalize nodelta
         >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
         [1,3,5,7,9,11,13: #H destruct (H)]
 …
   [ #Ha #i >append_length >commutative_plus #Hi normalize in Hi;
     cases (le_to_or_lt_eq … Hi) -Hi; #Hi
     [ cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉)
+    [ cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,0,short_jump〉)
       #x #y @((proj2 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
     | normalize nodelta >(injective_S … Hi)
 …
       [ >lookup_opt_lookup_miss
         [ //
         | cases (lookup ?? (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉)
+        | cases (lookup ?? (bitvector_of_nat ? (|prefix|)) old_policy 〈0,0,short_jump〉)
           #x #y normalize nodelta
           >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
 …
+      ]
+    ]
   | #x #Ha #i >append_length >commutative_plus #Hi normalize in Hi;
+  | #x cases x -x #x1 #x2 #Ha #i >append_length >commutative_plus #Hi normalize in Hi;
     cases (le_to_or_lt_eq … Hi) -Hi; #Hi
     [ cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉)
       #y #z normalize nodelta normalize nodelta >lookup_insert_miss
+    [ cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,0,short_jump〉)
+      #y cases y -y #y1 #y2 #z whd in match (snd ???); normalize nodelta >lookup_insert_miss
       [ @((proj2 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
       | @bitvector_of_nat_abs
 …
+      ]
     | >(injective_S … Hi) elim (proj1 ?? (proj2 ?? (pi2 ?? old_policy) (|prefix|) ?) ?)
       [ #a #H elim H -H; #b #H >H >(lookup_opt_lookup_hit … 〈a,b〉 H)
+      [ #a #H elim H -H; #b #H elim H -H #c #H >H >(lookup_opt_lookup_hit … 〈a,b,c〉 H)
         normalize nodelta >lookup_insert_hit @jmpleq_max_length
       | >prf >p1 >nth_append_second
 …
 | @conj [ @conj
   [ #i #Hi //
   | #i #Hi @conj [ >nth_nil #H @⊥ @H | #H elim H #x #H1 elim H1 #y #H2
                    normalize in H2; destruct (H2) ]
+  | #i #Hi @conj [ >nth_nil #H @⊥ @H | #H elim H #x #H1 elim H1 #y #H2 elim H2 #z #H3
+                   normalize in H3; destruct (H3) ]
+  ]
   | #i #Hi @⊥ @(absurd (i<0)) [ @Hi | @(not_le_Sn_O) ]
 …
   match n with
   [ O   ⇒ jump_expansion_start program
+  | S m ⇒ jump_expansion_step program (jump_expansion_internal program m)
+  | S m ⇒ let old_policy ≝ jump_expansion_internal program m in
+    jump_expansion_step program (create_label_map program old_policy) old_policy
   ].
 [ @(proj1 ?? (pi2 ?? (jump_expansion_start program)))
 | @(proj1 ?? (pi2 ?? (jump_expansion_step program (jump_expansion_internal program m))))
+| @(proj1 ?? (pi2 ?? (jump_expansion_step program (create_label_map program old_policy) old_policy)))
+]
 qed.
 …
   λprogram:list labelled_instruction.λp1,p2:jump_expansion_policy.
   ∀n:ℕ.n < |program| →
+    (\snd (bvt_lookup … (bitvector_of_nat 16 n) p1 〈0,short_jump〉)) =
+    (\snd (bvt_lookup … (bitvector_of_nat 16 n) p2 〈0,short_jump〉)).
+    let 〈i1,i2,j1〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) p1 〈0,0,short_jump〉 in
+    let 〈i3,i4,j2〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) p2 〈0,0,short_jump〉 in
+    j1 = j2.
 lemma pe_refl:
   ∀program.reflexive ? (policy_equal program).
+ #program whd #x whd #n #Hn @refl
+ #program whd #x whd #n #Hn cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉)
+ #y cases y -y #y #z normalize nodelta @refl
 qed.
 …
   ∀program.symmetric ? (policy_equal program).
  #program whd #x #y #Hxy whd #n #Hn
+ >(Hxy n Hn) @refl
+ lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉)
+ #z cases z -z #x1 #x2 #x3 cases (bvt_lookup … (bitvector_of_nat ? n) y 〈0,0,short_jump〉)
+ #z cases z -z #y1 #y2 #y3 normalize nodelta //
 qed.
 lemma pe_trans:
   ∀program.transitive ? (policy_equal program).
+ #program whd #x #y #z #Hxy #Hyz whd #n #Hn
+ >(Hxy n Hn) @(Hyz n Hn)
+ #program whd #x #y #z whd in match (policy_equal ???); whd in match (policy_equal ?y ?);
+ whd in match (policy_equal ? x z); #Hxy #Hyz #n #Hn
+ lapply (Hxy n Hn) -Hxy lapply (Hyz n Hn) -Hyz
+ cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉) #z cases z -z #x1 #x2 #x3
+ cases (bvt_lookup … (bitvector_of_nat ? n) y 〈0,0,short_jump〉) #z cases z -z #y1 #y2 #y3
+ cases (bvt_lookup … (bitvector_of_nat ? n) z 〈0,0,short_jump〉) #z cases z -z #z1 #z2 #z3
+ normalize nodelta //
 qed.
 …
  ∧jump_in_policy program policy.
   policy_equal program p1 p2 →
+  policy_equal program (jump_expansion_step program p1) (jump_expansion_step program p2).
+  policy_equal program (jump_expansion_step program (create_label_map program p1) p1)
+    (jump_expansion_step program (create_label_map program p2) p2).
  #program #p1 #p2 #Heq whd #n #Hn lapply (Heq n Hn) #H
  lapply (refl ? (lookup_opt … (bitvector_of_nat ? n) p1))
 …
    [ >lookup_opt_lookup_miss
      [ @refl
      | @(proj1 ?? (jump_not_in_policy program (pi1 … (jump_expansion_step program p2)) n Hn))
        [ @(proj1 ?? (pi2 … (jump_expansion_step program p2)))
+     | @(proj1 ?? (jump_not_in_policy program (pi1 … (jump_expansion_step program (create_label_map program p2) p2)) n Hn))
+       [ @(proj1 ?? (pi2 … (jump_expansion_step program (create_label_map program p2) p2)))
        | @Hnotjmp
+       ]
+     ]
    | @(proj1 ?? (jump_not_in_policy program (pi1 … (jump_expansion_step program p1)) n Hn))
      [ @(proj1 ?? (pi2 ?? (jump_expansion_step program p1)))
+   | @(proj1 ?? (jump_not_in_policy program (pi1 … (jump_expansion_step program (create_label_map program p1) p1)) n Hn))
+     [ @(proj1 ?? (pi2 ?? (jump_expansion_step program (create_label_map program p1) p1)))
      | @Hnotjmp
+     ]
+   ]
  | #x #Hl cases daemon
+ | #x #Hl cases daemon (* XXX *)
+ ]
 qed.
 …
 qed.
-include "utilities/extralib.ma".
 lemma policy_not_equal_incr: ∀program:(Σl:list labelled_instruction.|l|<2^16).
  ∀policy:(Σp:jump_expansion_policy.
     (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
     jump_in_policy program p).
   ¬policy_equal program policy (jump_expansion_step program policy) →
+  ¬policy_equal program policy (jump_expansion_step program (create_label_map program policy) policy) →
   ∃n:ℕ.n < (|program|) ∧ jmple
     (\snd (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,short_jump〉))
     (\snd (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program policy) 〈0,short_jump〉)).
+    (\snd (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,0,short_jump〉))
+    (\snd (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉)).
  #program #policy #Hp
  cases (dec_bounded_exists (λn.jmple
    (\snd (bvt_lookup ?? (bitvector_of_nat ? n) policy 〈0,short_jump〉))
    (\snd (bvt_lookup ?? (bitvector_of_nat ? n) (jump_expansion_step program policy) 〈0,short_jump〉))) ? (|program|))
+   (\snd (bvt_lookup ?? (bitvector_of_nat ? n) policy 〈0,0,short_jump〉))
+   (\snd (bvt_lookup ?? (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉))) ? (|program|))
  [ #H elim H; -H #i #Hi @(ex_intro ?? i) @Hi
+ | #abs @⊥ @(absurd ?? Hp) #n #Hn cases (proj2 ?? (pi2 ?? (jump_expansion_step program policy)) n Hn)
+   [ #Hj @⊥ @(absurd ?? abs) @(ex_intro ?? n) @conj [ @Hn | @Hj ]
+   | #H @H
+ | #abs @⊥ @(absurd ?? Hp) #n #Hn
+   lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) n Hn)
+   lapply (refl ? (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,0,short_jump〉))
+   cases (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,0,short_jump〉) in ⊢ (???% → %);
+   #z cases z -z #x1 #x2 #x3 #Hx
+   lapply (refl ? (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉))
+   cases (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉) in ⊢ (???% → %);
+   #z cases z -z #y1 #y2 #y3 #Hy
+   normalize nodelta #Hj cases Hj
+   [ #Hj @⊥ @(absurd ?? abs) @(ex_intro ?? n) @conj [ @Hn | >Hx >Hy @Hj ]
+   | //
+   ]
  | #n @dec_jmple
 …
 lemma stupid:
   ∀program,n.
   pi1 … (jump_expansion_step program (jump_expansion_internal program n)) =
+  pi1 … (jump_expansion_step program (create_label_map program (jump_expansion_internal program n)) (jump_expansion_internal program n)) =
   pi1 … (jump_expansion_internal program (S n)).
  //
 …
  match program with
  [ nil      ⇒ acc
  | cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,short_jump〉)) with
+ | cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) with
    [ long_jump   ⇒ measure_int t policy (acc + 2)
    | medium_jump ⇒ measure_int t policy (acc + 1)
 …
  ].
 definition measure ≝
   λprogram.λpolicy.measure_int program policy 0.
+(* definition measure ≝
+  λprogram.λpolicy.measure_int program policy 0. *)
 lemma measure_plus: ∀program.∀policy.∀x,d:ℕ.
 …
    [ //
    | #h #t #Hd #x whd in match (measure_int ???); whd in match (measure_int ?? x);
      cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,short_jump〉))
+     cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉))
      [ normalize nodelta @Hd
      |2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus
 …
     (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
     jump_in_policy program p.∀l.|l| ≤ |program| → ∀acc:ℕ.
   measure_int l policy acc ≤ measure_int l (jump_expansion_step program policy) acc.
+  measure_int l policy acc ≤ measure_int l (jump_expansion_step program (create_label_map program policy) policy) acc.
 #program #policy #l elim l -l;
   [ #Hp #acc normalize @le_n
   | #h #t #Hind #Hp #acc
+    cases (proj2 ?? (pi2 ?? (jump_expansion_step program policy)) (|t|) ?)
+    [ whd in match (measure_int ???); whd in match (measure_int ?(jump_expansion_step ??)?);
+      cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,short_jump〉))
+      cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (jump_expansion_step program policy) 〈0,short_jump〉))
+    lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) (|t|) Hp)
+    whd in match (measure_int ???); whd in match (measure_int ?(jump_expansion_step ???)?);
+    cases (bvt_lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉) #z cases z -z #x1 #x2 #x3
+    cases (bvt_lookup … (bitvector_of_nat ? (|t|)) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉) #z cases z -z #y1 #y2 #y3
+    normalize nodelta #Hj cases Hj
+    [ cases x3 cases y3
       [1,4,5,7,8,9: #H @⊥ @H
       |2,3,6: #_ normalize nodelta
         [1,2: @(transitive_le ? (measure_int t (jump_expansion_step program policy) acc))
         |3: @(transitive_le ? (measure_int t (jump_expansion_step program policy) (acc+1)))
+        [1,2: @(transitive_le ? (measure_int t (jump_expansion_step program (create_label_map program policy) policy) acc))
+        |3: @(transitive_le ? (measure_int t (jump_expansion_step program (create_label_map program policy) policy) (acc+1)))
+        ]
         [1,3,5: @Hind @(transitive_le … Hp) @le_n_Sn
 …
+        ]
+      ]
+    | #Heq whd in match (measure_int ???); whd in match (measure_int ?(jump_expansion_step ??)?);
+      >Heq cases (\snd (lookup … (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉))
+      [ normalize nodelta @Hind @(transitive_le … Hp) @le_n_Sn
+      | normalize nodelta @Hind @(transitive_le … Hp) @le_n_Sn
+      | normalize nodelta @Hind @(transitive_le … Hp) @le_n_Sn
+      ]
+    | @Hp
+    | #Heq >Heq cases y3 normalize nodelta @Hind @(transitive_le … Hp) @le_n_Sn
+    ]
+  ]
 …
  [ normalize @le_n
  | #h #t #Hind whd in match (measure_int ???);
    cases (\snd (lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,short_jump〉))
+   cases (\snd (lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉))
    [ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/
    |2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?)
 …
 lemma measure_full: ∀program.∀policy.
   measure_int program policy 0 = 2*|program| → ∀i.i<|program| →
   (\snd (bvt_lookup ?? (bitvector_of_nat ? i) policy 〈0,short_jump〉)) = long_jump.
+  (\snd (bvt_lookup ?? (bitvector_of_nat ? i) policy 〈0,0,short_jump〉)) = long_jump.
  #program #policy elim program
  [ #Hm #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
  | #h #t #Hind #Hm #i #Hi cut (measure_int t policy 0 = 2*|t|)
    [ whd in match (measure_int ???) in Hm;
      cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,short_jump〉)) in Hm;
+     cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) in Hm;
      normalize nodelta
      [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/
 …
    [ #Hi @(Hind Hmt i (le_S_S_to_le … Hi))
    | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm;
      cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,short_jump〉)) in Hm;
+     cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) in Hm;
      normalize nodelta
      [ >Hmt normalize <plus_n_O >(commutative_plus (|t|) (S (|t|)))
 …
     (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
     jump_in_policy program p.
   measure_int program policy 0 = measure_int program (jump_expansion_step program policy) 0 →
   policy_equal program policy (jump_expansion_step program policy).
+  measure_int program policy 0 = measure_int program (jump_expansion_step program (create_label_map program policy) policy) 0 →
+  policy_equal program policy (jump_expansion_step program (create_label_map program policy) policy).
 #program #policy lapply (le_n (|program|)) @(list_ind ?
   (λx.|x| ≤ |program| → measure_int x (pi1 … policy) 0 = measure_int x (pi1 … (jump_expansion_step program policy)) 0 →
       policy_equal x (pi1 … policy) (pi1 … (jump_expansion_step program policy)))
+  (λx.|x| ≤ |program| → measure_int x (pi1 … policy) 0 = measure_int x (pi1 … (jump_expansion_step program (create_label_map program policy) policy)) 0 →
+      policy_equal x (pi1 … policy) (pi1 … (jump_expansion_step program (create_label_map program policy) policy)))
    ?? program)
  [ #Hp #Hm #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O
 …
    [ #Hi @Hind
      [ @(transitive_le … Hp) //
      | whd in match (measure_int ???) in Hm; whd in match (measure_int ?(jump_expansion_step ??)?) in Hm;
        lapply (proj2 ?? (pi2 ?? (jump_expansion_step program policy)) (|t|) ?)
+     | whd in match (measure_int ???) in Hm; whd in match (measure_int ?(jump_expansion_step ???)?) in Hm;
+       lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) (|t|) ?)
        [ @(lt_to_le_to_lt … (|h::t|)) [ // | @Hp ]
+       | cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,short_jump〉)) in Hm;
+         cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (jump_expansion_step program policy) 〈0,short_jump〉));
+         normalize nodelta
+       | cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉) in Hm;
+         #x cases x -x #x1 #x2 #x3
+         cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉);
+         #y cases y -y #y1 #y2 #y3
+         normalize nodelta cases x3 cases y3 normalize nodelta
          [1: #H #_ @H
          |2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
 …
+     ]
    | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm;
      whd in match (measure_int ?(jump_expansion_step ??)?) in Hm;
      lapply (proj2 ?? (pi2 ?? (jump_expansion_step program policy)) (|t|) ?)
+     whd in match (measure_int ?(jump_expansion_step ???)?) in Hm;
+     lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) (|t|) ?)
      [ @(lt_to_le_to_lt … (|h::t|)) [ // | @Hp ]
+     | cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,short_jump〉)) in Hm;
+       cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (jump_expansion_step program policy) 〈0,short_jump〉));
+       normalize nodelta
+     | cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉) in Hm;
+       #x cases x -x #x1 #x2 #x3
+       cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉);
+       #y cases y -y #y1 #y2 #y3
+       normalize nodelta cases x3 cases y3 normalize nodelta
        [1,5,9: #_ #_ //
        |4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 |2,4,6: destruct (H2) ]
 …
  | #h #t #Hind #Hp whd in match (measure_int ???);
    cases (dec_is_jump (nth (|t|) ? program 〈None ?, Comment []〉)) #Hj
    [ >(lookup_opt_lookup_hit … (proj2 ?? (pi2 ?? (jump_expansion_start program)) (|t|) ? Hj) 〈0,short_jump〉)
+   [ >(lookup_opt_lookup_hit … (proj2 ?? (pi2 ?? (jump_expansion_start program)) (|t|) ? Hj) 〈0,0,short_jump〉)
      [ normalize nodelta @Hind @le_S_to_le ]
      @Hp
    | >(lookup_opt_lookup_miss … (proj1 ?? (jump_not_in_policy program (jump_expansion_internal program 0) (|t|) ?) Hj) 〈0,short_jump〉)
+   | >(lookup_opt_lookup_miss … (proj1 ?? (jump_not_in_policy program (jump_expansion_internal program 0) (|t|) ?) Hj) 〈0,0,short_jump〉)
      [ normalize nodelta @Hind @le_S_to_le ]
      @Hp
 …
 definition je_fixpoint: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
   Σp:jump_expansion_policy.∃n.∀k.n < k → policy_equal program (jump_expansion_internal program k) p.
  #program @(mk_Sig …(jump_expansion_internal program (2*|program|)))
+ #program @(mk_Sig … (jump_expansion_internal program (2*|program|)))
  @(ex_intro … (2*|program|)) #k #Hk
  cases (dec_bounded_exists (λk.policy_equal program (jump_expansion_internal program k)
 …
    [ lapply (measure_full program (jump_expansion_internal program (2*|program|)))
      #Hfull #i #Hi
+     lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (jump_expansion_internal program (2*|program|)))) i Hi)
+     >(Hfull ? i Hi)
+     [ cases (\snd (bvt_lookup ?? (bitvector_of_nat 16 i) (jump_expansion_step program (jump_expansion_internal program (2*|program|))) 〈0,short_jump〉))
+       [1,2: #H elim H #H2 [1,3: @⊥ @H2 |2,4: destruct (H2) ]
+       | #_ //
+       ]
+     | -i @le_to_le_to_eq
+     lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program (jump_expansion_internal program (2*|program|))) (jump_expansion_internal program (2*|program|)))) i Hi)
+     lapply (Hfull ? i Hi)
+     [ -i @le_to_le_to_eq
        [ @measure_le
        | lapply (le_n (2*|program|)) elim (2*|program|) in ⊢ (?%? → %);
 …
+         ]
+       ]
+     | -Hfull cases (bvt_lookup ?? (bitvector_of_nat 16 i) (jump_expansion_internal program (2*|program|)) 〈0,0,short_jump〉)
+       #x cases x -x #x1 #x2 #x3 normalize nodelta #Hfull
+       >Hfull cases (bvt_lookup ?? (bitvector_of_nat ? i) ? 〈0,0,short_jump〉)
+       #y cases y -y #y1 #y2 #y3 normalize nodelta cases y3 normalize nodelta
+       [1,2: #H elim H #H2 [1,3: @⊥ @H2 |2,4: destruct (H2) ]
+       | #_ //
+       ]
+     ]
    | @le_S_to_le @Hk
+   ]
+ | #n @dec_bounded_forall #m @dec_eq_jump_length
+ | #n @dec_bounded_forall #m
+   cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,0,short_jump〉)
+   #x cases x -x #x1 #x2 #x3
+   cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,0,short_jump〉)
+   #y cases y -y #y1 #y2 #y3 normalize nodelta
+   @dec_eq_jump_length
+ ]
 qed.
 …
  generalize in match (policy_ok_prefix_ok 〈preamble,instr_list〉 pol suffix
   (prefix@[hd]) EQ1) in ⊢ ?; >sigma00_append <EQ2 whd in ⊢ (?(??%?) → ?);
  @pair_elim' #ppc #pc_map #EQ3 normalize nodelta
  @pair_elim' #pc #map #EQ4 normalize nodelta
  @pair_elim' #l' #i' #EQ5 normalize nodelta
+ @pair_elim #ppc #pc_map #EQ3 normalize nodelta
+ @pair_elim #pc #map #EQ4 normalize nodelta
+ @pair_elim #l' #i' #EQ5 normalize nodelta
  cases (construct_costs_safe ??????) normalize
   [* #abs @⊥ @abs % | #X #_ % #abs destruct(abs)]

Note: See TracChangeset for help on using the changeset viewer.

Context Navigation

Changeset 1609 for src/ASM/Assembly.ma

Legend:

src/ASM/Assembly.ma

Download in other formats: