Changeset 1609


Ignore:
Timestamp:
Dec 14, 2011, 2:44:42 PM (8 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
Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r1607 r1609  
    55include alias "basics/logic.ma".
    66include alias "arithmetics/nat.ma".
     7include "utilities/extralib.ma".
    78
    89definition assembly_preinstruction ≝
     
    462463
    463464 
    464 (* jump_expansion_policy: instruction number ↦ 〈pc, jump_length〉 *)
    465 definition jump_expansion_policy ≝ BitVectorTrie (ℕ × jump_length) 16.
     465(* jump_expansion_policy: instruction number ↦ 〈pc, addr, jump_length〉 *)
     466definition jump_expansion_policy ≝ BitVectorTrie (ℕ × ℕ × jump_length) 16.
    466467
    467468definition expand_relative_jump_internal:
     
    667668     let 〈pc,labels〉 ≝ acc in
    668669     let 〈label,instr〉 ≝ x in
    669           let new_labels ≝
    670           match label with
    671           [ None   ⇒ labels
    672           | Some l ⇒ add … labels l 〈|prefix|, pc〉
    673           ] in
    674           let jmp_len ≝ \snd (bvt_lookup ?? (bitvector_of_nat 16 (|prefix|)) policy 〈pc, long_jump〉) in
    675           〈add_instruction_size pc jmp_len instr, new_labels〉
     670       let new_labels ≝
     671       match label with
     672       [ None   ⇒ labels
     673       | Some l ⇒ add … labels l 〈|prefix|, pc〉
     674       ] in
     675     let 〈i1,i2,jmp_len〉 ≝ bvt_lookup ?? (bitvector_of_nat 16 (|prefix|)) policy 〈0, 0, long_jump〉 in
     676       〈add_instruction_size pc jmp_len instr, new_labels〉
    676677    ) 〈0, empty_map …〉 in
    677678    final_labels.
     
    705706qed.
    706707
    707 definition select_reljump_length: label_map → ℕ → Identifier → jump_length ≝
     708definition select_reljump_length: label_map → ℕ → Identifier → ℕ ×jump_length ≝
    708709  λlabels.λpc.λlbl.
    709710  let 〈n, addr〉 ≝ lookup_def … labels lbl 〈0, pc〉 in
    710711  if leb pc addr (* forward jump *)
    711712  then if leb (addr - pc) 126
    712        then short_jump
    713        else long_jump
     713       then 〈addr, short_jump〉
     714       else 〈addr, long_jump〉
    714715  else if leb (pc - addr) 129
    715        then short_jump
    716        else long_jump.
    717 
    718 definition select_call_length: label_map → ℕ → Identifier → jump_length ≝
     716       then 〈addr, short_jump〉
     717       else 〈addr, long_jump〉.
     718
     719definition select_call_length: label_map → ℕ → Identifier → ℕ × jump_length ≝
    719720  λlabels.λpc_nat.λlbl.
    720721  let pc ≝ bitvector_of_nat 16 pc_nat in
    721   let addr ≝ bitvector_of_nat 16 (\snd (lookup_def ? ? labels lbl 〈0, pc_nat〉)) in
     722  let addr_nat ≝ (\snd (lookup_def ? ? labels lbl 〈0, pc_nat〉)) in
     723  let addr ≝ bitvector_of_nat 16 addr_nat in
    722724  let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 addr in
    723725  let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
    724726  if eq_bv ? fst_5_addr fst_5_pc
    725   then medium_jump
    726   else long_jump.
     727  then 〈addr_nat, medium_jump〉
     728  else 〈addr_nat, long_jump〉.
    727729 
    728 definition select_jump_length: label_map → ℕ → Identifier → jump_length ≝
     730definition select_jump_length: label_map → ℕ → Identifier → ℕ × jump_length ≝
    729731  λlabels.λpc.λlbl.
    730732  let 〈n, addr〉 ≝ lookup_def … labels lbl 〈0, pc〉 in
    731733  if leb pc addr
    732734  then if leb (addr - pc) 126
    733        then short_jump
     735       then 〈addr, short_jump〉
    734736       else select_call_length labels pc lbl
    735737  else if leb (pc - addr) 129
    736        then short_jump
     738       then 〈addr, short_jump〉
    737739       else select_call_length labels pc lbl.
    738740 
    739741definition jump_expansion_step_instruction: label_map → ℕ →
    740   preinstruction Identifier → option jump_length
     742  preinstruction Identifier → option (ℕ × jump_length)
    741743  λlabels.λpc.λi.
    742744  match i with
     
    800802  ∀i:ℕ.i < |prefix| →
    801803  (is_jump (nth i ? prefix 〈None ?, Comment []〉) ↔
    802    ∃p,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,j〉).
     804   ∃p,a,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,a,j〉).
    803805
    804806(* these should be moved to BitVector at some point *) 
     
    826828 jump_in_policy prefix p).
    827829  ∀i:ℕ.i < |prefix| →
    828   ¬is_jump (nth i ? prefix 〈None ?, Comment []〉) ↔
    829   lookup_opt … (bitvector_of_nat 16 i) policy = None ?.
     830  iff (¬is_jump (nth i ? prefix 〈None ?, Comment []〉))
     831  (lookup_opt … (bitvector_of_nat 16 i) policy = None ?).
    830832 #prefix #policy #i #Hi @conj
    831833 [ #Hnotjmp lapply (refl ? (lookup_opt … (bitvector_of_nat 16 i) policy))
    832834   cases (lookup_opt … (bitvector_of_nat 16 i) policy) in ⊢ (???% → ?);
    833835   [ #H @H
    834    | #x cases x #y #z #H @⊥ @(absurd ? ? Hnotjmp) @(proj2 ?? (proj2 ?? (pi2 ?? policy) i Hi))
    835      @(ex_intro … y (ex_intro … z H))
     836   | #x cases x -x #x #z cases x -x #x #y #H @⊥ @(absurd ? ? Hnotjmp) @(proj2 ?? (proj2 ?? (pi2 ?? policy) i Hi))
     837     @(ex_intro ?? x (ex_intro ?? y (ex_intro ?? z H)))
    836838   ]
    837839 | #Hnone @nmk #Hj lapply (proj1 ?? (proj2 ?? (pi2 ?? policy) i Hi) Hj)
    838    #H elim H -H; #x #H elim H -H; #y #H >H in Hnone; #abs destruct (abs)
     840   #H elim H -H; #x #H elim H -H; #y #H elim H -H; #z #H >H in Hnone; #abs destruct (abs)
    839841 ] 
    840842qed.
    841  
     843
    842844definition jump_expansion_start:
    843845  ∀program:(Σl:list labelled_instruction.|l| < 2^16).
     
    846848    jump_in_policy program policy ∧
    847849    ∀i.i < |program| → is_jump (nth i ? program 〈None ?, Comment []〉) →
    848      lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈0,short_jump〉 ≝
     850     lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈0,0,short_jump〉 ≝
    849851  λprogram.
    850852  foldl_strong (option Identifier × pseudo_instruction)
     
    853855    jump_in_policy prefix policy ∧
    854856    ∀i.i < |prefix| → is_jump (nth i ? prefix 〈None ?, Comment []〉) →
    855       lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈0,short_jump〉)
     857      lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈0,0,short_jump〉)
    856858  program
    857859  (λprefix.λx.λtl.λprf.λpolicy.
     
    859861   match instr with
    860862   [ Instruction i ⇒ match i with
    861      [ JC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
    862      | JNC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
    863      | JZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
    864      | JNZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
    865      | JB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
    866      | JNB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
    867      | JBC _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
    868      | CJNE _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
    869      | DJNZ _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
     863     [ JC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
     864     | JNC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
     865     | JZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
     866     | JNZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
     867     | JB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
     868     | JNB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
     869     | JBC _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
     870     | CJNE _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
     871     | DJNZ _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
    870872     | _ ⇒ (pi1 … policy)
    871873     ]
    872    | Call c ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
    873    | Jmp j  ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
    874    | _      ⇒ (pi1 policy)
     874   | Call c ⇒ bvt_insert (ℕ×ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
     875   | Jmp j  ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,0,short_jump〉 policy
     876   | _      ⇒ (pi1 ?? policy)
    875877   ]
    876878  ) (Stub ? ?).
     
    901903    >(nth_append_second ? ? prefix ? ? (le_n (|prefix|))) <minus_n_n #H @⊥ @H
    902904   ]
    903    #H elim H; -H; #t1 #H elim H; -H #t2 #H
     905   #H elim H; -H; #t1 #H elim H; -H #t2 #H elim H; -H; #t3 #H
    904906   >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?) in H;
    905907   [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:
     
    950952   >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n //
    951953  ]
    952   @(ex_intro ?? 0 (ex_intro ?? short_jump (lookup_opt_insert_hit ?? 16 ? policy)))
     954  @(ex_intro ?? 0 (ex_intro ?? 0 (ex_intro ?? short_jump (lookup_opt_insert_hit ?? 16 ? policy))))
    953955 ]
    954956 #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
     
    980982 λprogram.λop.λp.
    981983  (∀i:ℕ.i < |program| →
    982     jmpleq
    983       (\snd (bvt_lookup … (bitvector_of_nat ? i) op 〈0,short_jump〉))
    984       (\snd (bvt_lookup … (bitvector_of_nat ? i) p 〈0,short_jump〉))).
    985    
     984    let 〈i1,i2,oj〉 ≝ bvt_lookup ?? (bitvector_of_nat ? i) op 〈0,0,short_jump〉 in
     985    let 〈i3,i4,j〉 ≝ bvt_lookup ?? (bitvector_of_nat ? i) p 〈0,0,short_jump〉 in
     986    jmpleq oj j).
     987
     988definition policy_safe: (*label_map → *)jump_expansion_policy → Prop ≝
     989 (*λlabels.*)λpolicy.
     990 bvt_forall (ℕ×ℕ×jump_length) 16 policy (λn.λx.let 〈pc_nat,addr_nat,jmp_len〉 ≝ x in
     991    match jmp_len with
     992    [ short_jump  ⇒ if leb pc_nat addr_nat
     993       then le (addr_nat - pc_nat) 126
     994       else le (pc_nat - addr_nat) 129
     995    | medium_jump ⇒
     996       let addr ≝ bitvector_of_nat 16 addr_nat in
     997       let pc ≝ bitvector_of_nat 16 pc_nat in
     998       let 〈fst_5_addr, rest_addr〉 ≝ split bool 5 11 addr in
     999       let 〈fst_5_pc, rest_pc〉 ≝ split bool 5 11 pc in
     1000       eq_bv 5 fst_5_addr fst_5_pc = true
     1001    | long_jump   ⇒ True
     1002    ]
     1003  ).
     1004 
    9861005definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
     1006  ∀labels:(Σlm:label_map.∀i:ℕ.lt i (|program|) →
     1007    ∀l.occurs_exactly_once l program →
     1008    is_label (nth i ? program 〈None ?, Comment [ ]〉) l →
     1009    ∃a.lookup … lm l = Some ? 〈i,a〉).
    9871010  ∀old_policy:(Σpolicy.
    9881011    (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat 16 i) policy = None ?) ∧
     
    9931016    policy_increase program old_policy policy)
    9941017    ≝
    995   λprogram.λold_policy.
    996   let labels ≝ create_label_map program old_policy in
     1018  λprogram.λlabels.λold_policy.
    9971019  let 〈final_pc, final_policy〉 ≝
    9981020    foldl_strong (option Identifier × pseudo_instruction)
     
    10151037        ] in
    10161038      let 〈new_pc, new_policy〉 ≝
    1017         let 〈ignore,old_length〉 ≝ lookup … (bitvector_of_nat 16 (|prefix|)) old_policy 〈0, short_jump〉 in
     1039        let 〈ignore,old_length〉 ≝ bvt_lookup … (bitvector_of_nat 16 (|prefix|)) old_policy 〈0, 0, short_jump〉 in
    10181040        match add_instr with
    10191041        [ None    ⇒ (* i.e. it's not a jump *)
    10201042          〈add_instruction_size pc long_jump instr, policy〉
    1021         | Some ai ⇒
     1043        | Some z ⇒ let 〈addr,ai〉 ≝ z in
    10221044          let new_length ≝ max_length old_length ai in
    1023           〈add_instruction_size pc new_length instr, insert … (bitvector_of_nat 16 (|prefix|)) 〈pc, new_length〉 policy〉
     1045          〈add_instruction_size pc new_length instr, insert … (bitvector_of_nat 16 (|prefix|)) 〈pc, addr, new_length〉 policy〉
    10241046        ] in
    10251047      〈new_pc, new_policy〉
     
    10291051[ #Hi2 cases (lookup ??? old_policy ?) #h #n cases add_instr
    10301052  [ @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2)
    1031   | #z normalize nodelta >lookup_opt_insert_miss
     1053  | #z cases z -z #z1 #z2 whd in match (snd ???); >lookup_opt_insert_miss
    10321054    [ @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2)
    10331055    | >eq_bv_sym @bitvector_of_nat_abs
     
    10441066      cases add_instr cases (lookup ??? old_policy ?) normalize nodelta #x #y
    10451067      [ @(proj1 ?? Hacc Hj)
    1046       | #z elim (proj1 ?? Hacc Hj) #h #n elim n -n #n #Hn
    1047         % [ @h | % [ @n | <Hn @lookup_opt_insert_miss @bitvector_of_nat_abs
     1068      | #z cases z -z #z1 #z2 elim (proj1 ?? Hacc Hj) #h #n elim n -n #n #H elim H -H #j #Hj
     1069        @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?))) whd in match (snd ???);
     1070        >lookup_opt_insert_miss [ @Hj |  @bitvector_of_nat_abs ]
    10481071        [3: @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
    10491072        |1: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
     
    10511074        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    10521075        @le_S_S @le_plus_n_r
    1053         ] ]
    10541076      ]
    10551077    | lapply (proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc
    1056       #H elim H -H; #h #H elim H -H; #n cases add_instr cases (lookup ??? old_policy ?)
     1078      #H elim H -H; #h #H elim H -H; #n #H elim H -H #j cases add_instr cases (lookup ??? old_policy ?)
    10571079      normalize nodelta #x #y [2: #z]
    1058       #Hl @(proj2 ?? Hacc) @(ex_intro ?? h (ex_intro ?? n ?))
    1059       [ <Hl @sym_eq @lookup_opt_insert_miss @bitvector_of_nat_abs
     1080      #Hl @(proj2 ?? Hacc) @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?)))
     1081      [ <Hl @sym_eq cases z #z1 #z2 whd in match (snd ???); @lookup_opt_insert_miss @bitvector_of_nat_abs
    10601082        [3: @lt_to_not_eq @(le_S_S_to_le … Hi)
    10611083        |1: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
     
    10701092     [1: #pi | 2,3: #x | 4,5: #id | 6: #x #y] @conj normalize nodelta
    10711093     [3,5,11: #H @⊥ @H (* instr is not a jump *)
    1072      |4,6,12: #H elim H -H; #h #H elim H -H #n cases (lookup ??? old_policy ?)
     1094     |4,6,12: #H elim H -H; #h #H elim H -H #n #H elim H -H #j cases (lookup ??? old_policy ?)
    10731095       #x #y normalize nodelta >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
    10741096       [1,3,5: #H destruct (H)]
    10751097       @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    10761098       @le_S_S @le_plus_n_r
    1077      |7,9: (* instr is a jump *) #_ cases (lookup ??? old_policy ?) #h #n
     1099     |7,9: (* instr is a jump *) #_ cases (lookup ??? old_policy ?) #x cases x #h #n #j
    10781100       whd in match (snd ???); @(ex_intro ?? pc)
    1079        [ @(ex_intro ?? (max_length n (select_jump_length (create_label_map program old_policy) pc id)))
    1080        | @(ex_intro ?? (max_length n (select_call_length (create_label_map program old_policy) pc id)))
    1081        ] @lookup_opt_insert_hit
     1101       [ @(ex_intro ?? (\fst (select_jump_length labels pc id)))
     1102         @(ex_intro ?? (max_length j (\snd (select_jump_length labels pc id))))
     1103         cases (select_jump_length labels pc id)
     1104       | @(ex_intro ?? (\fst (select_call_length labels pc id)))
     1105         @(ex_intro ?? (max_length j (\snd (select_call_length labels pc id))))
     1106         cases (select_call_length labels pc id)
     1107       ] #z1 #z2 normalize nodelta @lookup_opt_insert_hit
    10821108     |8,10: #_ //
    10831109     |1,2: cases pi
     
    10851111       |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #H @⊥ @H
    10861112       |1,2,3,6,7,33,34: #x #y #H @⊥ @H
    1087        |9,10,14,15: #id #_ cases (lookup ??? old_policy ?) #h #n
    1088          whd in match (snd ???);
    1089          @(ex_intro ?? pc (ex_intro ?? (max_length n (select_reljump_length (create_label_map program old_policy) pc id)) ?))
     1113       |9,10,14,15: #id #_ cases (lookup ??? old_policy ?) #x cases x #h #n #j
     1114         whd in match (snd ???); @(ex_intro ?? pc)
     1115         @(ex_intro ?? (\fst (select_reljump_length labels pc id)))
     1116         @(ex_intro ?? (max_length j (\snd (select_reljump_length labels pc id))))
     1117         normalize nodelta cases (select_reljump_length labels pc id) #z1 #z2 normalize nodelta
    10901118         @lookup_opt_insert_hit
    1091        |11,12,13,16,17: #x #id #_ cases (lookup ??? old_policy ?) #h #n
    1092          whd in match (snd ???);
    1093          @(ex_intro ?? pc (ex_intro ?? (max_length n (select_reljump_length (create_label_map program old_policy) pc id)) ?))
     1119       |11,12,13,16,17: #x #id #_ cases (lookup ??? old_policy ?) #x cases x #h #n #j
     1120         whd in match (snd ???); @(ex_intro ?? pc)
     1121         @(ex_intro ?? (\fst (select_reljump_length labels pc id)))
     1122         @(ex_intro ?? (max_length j (\snd (select_reljump_length labels pc id))))
     1123         normalize nodelta cases (select_reljump_length labels pc id) #z1 #z2 normalize nodelta
    10941124         @lookup_opt_insert_hit
    1095        |72,73,74: #H elim H -H; #h #H elim H -H #n cases (lookup ??? old_policy ?)
    1096         #x #y normalize nodelta
     1125       |72,73,74: #H elim H -H; #h #H elim H -H #n #H elim H -H #j cases (lookup ??? old_policy ?)
     1126        #z cases z -z #x #y #z normalize nodelta
    10971127        >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
    10981128        [1,3,5: #H destruct (H)]
     
    11001130        @le_S_S @le_plus_n_r     
    11011131       |41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69: #x
    1102         #H elim H -H; #h #H elim H -H #n cases (lookup ??? old_policy ?)
    1103         #x #y normalize nodelta
     1132        #H elim H -H; #h #H elim H -H #n #H elim H -H #j cases (lookup ??? old_policy ?)
     1133        #z cases z -z #x #y #z normalize nodelta
    11041134        >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
    11051135        [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35: #H destruct (H)]
    11061136        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    11071137        @le_S_S @le_plus_n_r
    1108        |38,39,40,43,44,70,71: #x #y #H elim H -H; #h #H elim H -H #n
    1109         cases (lookup ??? old_policy ?) #x #y normalize nodelta
     1138       |38,39,40,43,44,70,71: #x #y #H elim H -H; #h #H elim H -H #n #H elim H -H #j
     1139        cases (lookup ??? old_policy ?) #z cases z -z #x #y #z normalize nodelta
    11101140        >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
    11111141        [1,3,5,7,9,11,13: #H destruct (H)]
     
    11211151  [ #Ha #i >append_length >commutative_plus #Hi normalize in Hi;
    11221152    cases (le_to_or_lt_eq … Hi) -Hi; #Hi
    1123     [ cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉)
     1153    [ cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,0,short_jump〉)
    11241154      #x #y @((proj2 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
    11251155    | normalize nodelta >(injective_S … Hi)
     
    11271157      [ >lookup_opt_lookup_miss
    11281158        [ //
    1129         | cases (lookup ?? (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉)
     1159        | cases (lookup ?? (bitvector_of_nat ? (|prefix|)) old_policy 〈0,0,short_jump〉)
    11301160          #x #y normalize nodelta
    11311161          >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
     
    11561186      ]
    11571187    ]
    1158   | #x #Ha #i >append_length >commutative_plus #Hi normalize in Hi;
     1188  | #x cases x -x #x1 #x2 #Ha #i >append_length >commutative_plus #Hi normalize in Hi;
    11591189    cases (le_to_or_lt_eq … Hi) -Hi; #Hi
    1160     [ cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉)
    1161       #y #z normalize nodelta normalize nodelta >lookup_insert_miss
     1190    [ cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,0,short_jump〉)
     1191      #y cases y -y #y1 #y2 #z whd in match (snd ???); normalize nodelta >lookup_insert_miss
    11621192      [ @((proj2 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
    11631193      | @bitvector_of_nat_abs
     
    11691199      ]
    11701200    | >(injective_S … Hi) elim (proj1 ?? (proj2 ?? (pi2 ?? old_policy) (|prefix|) ?) ?)
    1171       [ #a #H elim H -H; #b #H >H >(lookup_opt_lookup_hit … 〈a,b〉 H)
     1201      [ #a #H elim H -H; #b #H elim H -H #c #H >H >(lookup_opt_lookup_hit … 〈a,b,c〉 H)
    11721202        normalize nodelta >lookup_insert_hit @jmpleq_max_length
    11731203      | >prf >p1 >nth_append_second
     
    11911221| @conj [ @conj
    11921222  [ #i #Hi //
    1193   | #i #Hi @conj [ >nth_nil #H @⊥ @H | #H elim H #x #H1 elim H1 #y #H2
    1194                    normalize in H2; destruct (H2) ]
     1223  | #i #Hi @conj [ >nth_nil #H @⊥ @H | #H elim H #x #H1 elim H1 #y #H2 elim H2 #z #H3
     1224                   normalize in H3; destruct (H3) ]
    11951225  ]                 
    11961226  | #i #Hi @⊥ @(absurd (i<0)) [ @Hi | @(not_le_Sn_O) ]
     
    12051235  match n with
    12061236  [ O   ⇒ jump_expansion_start program
    1207   | S m ⇒ jump_expansion_step program (jump_expansion_internal program m)
     1237  | S m ⇒ let old_policy ≝ jump_expansion_internal program m in
     1238    jump_expansion_step program (create_label_map program old_policy) old_policy
    12081239  ].
    12091240[ @(proj1 ?? (pi2 ?? (jump_expansion_start program)))
    1210 | @(proj1 ?? (pi2 ?? (jump_expansion_step program (jump_expansion_internal program m))))
     1241| @(proj1 ?? (pi2 ?? (jump_expansion_step program (create_label_map program old_policy) old_policy)))
    12111242]
    12121243qed.
     
    12151246  λprogram:list labelled_instruction.λp1,p2:jump_expansion_policy.
    12161247  ∀n:ℕ.n < |program| →
    1217     (\snd (bvt_lookup … (bitvector_of_nat 16 n) p1 〈0,short_jump〉)) =
    1218     (\snd (bvt_lookup … (bitvector_of_nat 16 n) p2 〈0,short_jump〉)).
     1248    let 〈i1,i2,j1〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) p1 〈0,0,short_jump〉 in
     1249    let 〈i3,i4,j2〉 ≝ bvt_lookup … (bitvector_of_nat 16 n) p2 〈0,0,short_jump〉 in
     1250    j1 = j2.
    12191251
    12201252lemma pe_refl:
    12211253  ∀program.reflexive ? (policy_equal program).
    1222  #program whd #x whd #n #Hn @refl
     1254 #program whd #x whd #n #Hn cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉)
     1255 #y cases y -y #y #z normalize nodelta @refl
    12231256qed.
    12241257
     
    12261259  ∀program.symmetric ? (policy_equal program).
    12271260 #program whd #x #y #Hxy whd #n #Hn
    1228  >(Hxy n Hn) @refl
     1261 lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉)
     1262 #z cases z -z #x1 #x2 #x3 cases (bvt_lookup … (bitvector_of_nat ? n) y 〈0,0,short_jump〉)
     1263 #z cases z -z #y1 #y2 #y3 normalize nodelta //
    12291264qed.
    12301265
    12311266lemma pe_trans:
    12321267  ∀program.transitive ? (policy_equal program).
    1233  #program whd #x #y #z #Hxy #Hyz whd #n #Hn
    1234  >(Hxy n Hn) @(Hyz n Hn)
     1268 #program whd #x #y #z whd in match (policy_equal ???); whd in match (policy_equal ?y ?);
     1269 whd in match (policy_equal ? x z); #Hxy #Hyz #n #Hn
     1270 lapply (Hxy n Hn) -Hxy lapply (Hyz n Hn) -Hyz
     1271 cases (bvt_lookup … (bitvector_of_nat ? n) x 〈0,0,short_jump〉) #z cases z -z #x1 #x2 #x3
     1272 cases (bvt_lookup … (bitvector_of_nat ? n) y 〈0,0,short_jump〉) #z cases z -z #y1 #y2 #y3
     1273 cases (bvt_lookup … (bitvector_of_nat ? n) z 〈0,0,short_jump〉) #z cases z -z #z1 #z2 #z3
     1274 normalize nodelta //
    12351275qed.
    12361276
     
    12401280 ∧jump_in_policy program policy.
    12411281  policy_equal program p1 p2 →
    1242   policy_equal program (jump_expansion_step program p1) (jump_expansion_step program p2).
     1282  policy_equal program (jump_expansion_step program (create_label_map program p1) p1)
     1283    (jump_expansion_step program (create_label_map program p2) p2).
    12431284 #program #p1 #p2 #Heq whd #n #Hn lapply (Heq n Hn) #H
    12441285 lapply (refl ? (lookup_opt … (bitvector_of_nat ? n) p1))
     
    12481289   [ >lookup_opt_lookup_miss
    12491290     [ @refl
    1250      | @(proj1 ?? (jump_not_in_policy program (pi1 … (jump_expansion_step program p2)) n Hn))
    1251        [ @(proj1 ?? (pi2 … (jump_expansion_step program p2)))
     1291     | @(proj1 ?? (jump_not_in_policy program (pi1 … (jump_expansion_step program (create_label_map program p2) p2)) n Hn))
     1292       [ @(proj1 ?? (pi2 … (jump_expansion_step program (create_label_map program p2) p2)))
    12521293       | @Hnotjmp
    12531294       ]
    12541295     ]
    1255    | @(proj1 ?? (jump_not_in_policy program (pi1 … (jump_expansion_step program p1)) n Hn))
    1256      [ @(proj1 ?? (pi2 ?? (jump_expansion_step program p1)))
     1296   | @(proj1 ?? (jump_not_in_policy program (pi1 … (jump_expansion_step program (create_label_map program p1) p1)) n Hn))
     1297     [ @(proj1 ?? (pi2 ?? (jump_expansion_step program (create_label_map program p1) p1)))
    12571298     | @Hnotjmp
    12581299     ]
    12591300   ]
    1260  | #x #Hl cases daemon
     1301 | #x #Hl cases daemon (* XXX *)
    12611302 ]
    12621303qed.
     
    12871328qed.
    12881329 
    1289 include "utilities/extralib.ma".
    1290 
    12911330lemma policy_not_equal_incr: ∀program:(Σl:list labelled_instruction.|l|<2^16).
    12921331 ∀policy:(Σp:jump_expansion_policy.
    12931332    (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
    12941333    jump_in_policy program p).
    1295   ¬policy_equal program policy (jump_expansion_step program policy) →
     1334  ¬policy_equal program policy (jump_expansion_step program (create_label_map program policy) policy) →
    12961335  ∃n:ℕ.n < (|program|) ∧ jmple
    1297     (\snd (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,short_jump〉))
    1298     (\snd (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program policy) 〈0,short_jump〉)).
     1336    (\snd (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,0,short_jump〉))
     1337    (\snd (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉)).
    12991338 #program #policy #Hp
    13001339 cases (dec_bounded_exists (λn.jmple
    1301    (\snd (bvt_lookup ?? (bitvector_of_nat ? n) policy 〈0,short_jump〉))
    1302    (\snd (bvt_lookup ?? (bitvector_of_nat ? n) (jump_expansion_step program policy) 〈0,short_jump〉))) ? (|program|))
     1340   (\snd (bvt_lookup ?? (bitvector_of_nat ? n) policy 〈0,0,short_jump〉))
     1341   (\snd (bvt_lookup ?? (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉))) ? (|program|))
    13031342 [ #H elim H; -H #i #Hi @(ex_intro ?? i) @Hi
    1304  | #abs @⊥ @(absurd ?? Hp) #n #Hn cases (proj2 ?? (pi2 ?? (jump_expansion_step program policy)) n Hn)
    1305    [ #Hj @⊥ @(absurd ?? abs) @(ex_intro ?? n) @conj [ @Hn | @Hj ]
    1306    | #H @H
     1343 | #abs @⊥ @(absurd ?? Hp) #n #Hn
     1344   lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) n Hn)
     1345   lapply (refl ? (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,0,short_jump〉))
     1346   cases (bvt_lookup … (bitvector_of_nat ? n) policy 〈0,0,short_jump〉) in ⊢ (???% → %);
     1347   #z cases z -z #x1 #x2 #x3 #Hx
     1348   lapply (refl ? (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉))
     1349   cases (bvt_lookup … (bitvector_of_nat ? n) (jump_expansion_step program (create_label_map program policy) policy) 〈0,0,short_jump〉) in ⊢ (???% → %);
     1350   #z cases z -z #y1 #y2 #y3 #Hy
     1351   normalize nodelta #Hj cases Hj
     1352   [ #Hj @⊥ @(absurd ?? abs) @(ex_intro ?? n) @conj [ @Hn | >Hx >Hy @Hj ]
     1353   | //
    13071354   ]
    13081355 | #n @dec_jmple
     
    13121359lemma stupid:
    13131360  ∀program,n.
    1314   pi1 … (jump_expansion_step program (jump_expansion_internal program n)) =
     1361  pi1 … (jump_expansion_step program (create_label_map program (jump_expansion_internal program n)) (jump_expansion_internal program n)) =
    13151362  pi1 … (jump_expansion_internal program (S n)).
    13161363 //
     
    13211368 match program with
    13221369 [ nil      ⇒ acc
    1323  | cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,short_jump〉)) with
     1370 | cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) with
    13241371   [ long_jump   ⇒ measure_int t policy (acc + 2)
    13251372   | medium_jump ⇒ measure_int t policy (acc + 1)
     
    13281375 ].
    13291376
    1330 definition measure ≝
    1331   λprogram.λpolicy.measure_int program policy 0.
     1377(* definition measure ≝
     1378  λprogram.λpolicy.measure_int program policy 0. *)
    13321379 
    13331380lemma measure_plus: ∀program.∀policy.∀x,d:ℕ.
     
    13381385   [ //
    13391386   | #h #t #Hd #x whd in match (measure_int ???); whd in match (measure_int ?? x);
    1340      cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,short_jump〉))
     1387     cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉))
    13411388     [ normalize nodelta @Hd
    13421389     |2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus
     
    13511398    (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
    13521399    jump_in_policy program p.∀l.|l| ≤ |program| → ∀acc:ℕ.
    1353   measure_int l policy acc ≤ measure_int l (jump_expansion_step program policy) acc.
     1400  measure_int l policy acc ≤ measure_int l (jump_expansion_step program (create_label_map program policy) policy) acc.
    13541401#program #policy #l elim l -l;
    13551402  [ #Hp #acc normalize @le_n
    13561403  | #h #t #Hind #Hp #acc
    1357     cases (proj2 ?? (pi2 ?? (jump_expansion_step program policy)) (|t|) ?)
    1358     [ whd in match (measure_int ???); whd in match (measure_int ?(jump_expansion_step ??)?);
    1359       cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,short_jump〉))
    1360       cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (jump_expansion_step program policy) 〈0,short_jump〉))
     1404    lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) (|t|) Hp)
     1405    whd in match (measure_int ???); whd in match (measure_int ?(jump_expansion_step ???)?);
     1406    cases (bvt_lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉) #z cases z -z #x1 #x2 #x3
     1407    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
     1408    normalize nodelta #Hj cases Hj
     1409    [ cases x3 cases y3
    13611410      [1,4,5,7,8,9: #H @⊥ @H
    13621411      |2,3,6: #_ normalize nodelta
    1363         [1,2: @(transitive_le ? (measure_int t (jump_expansion_step program policy) acc))
    1364         |3: @(transitive_le ? (measure_int t (jump_expansion_step program policy) (acc+1)))
     1412        [1,2: @(transitive_le ? (measure_int t (jump_expansion_step program (create_label_map program policy) policy) acc))
     1413        |3: @(transitive_le ? (measure_int t (jump_expansion_step program (create_label_map program policy) policy) (acc+1)))
    13651414        ]
    13661415        [1,3,5: @Hind @(transitive_le … Hp) @le_n_Sn
     
    13681417        ]
    13691418      ]
    1370     | #Heq whd in match (measure_int ???); whd in match (measure_int ?(jump_expansion_step ??)?);
    1371       >Heq cases (\snd (lookup … (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉))
    1372       [ normalize nodelta @Hind @(transitive_le … Hp) @le_n_Sn
    1373       | normalize nodelta @Hind @(transitive_le … Hp) @le_n_Sn
    1374       | normalize nodelta @Hind @(transitive_le … Hp) @le_n_Sn
    1375       ]
    1376     | @Hp
     1419    | #Heq >Heq cases y3 normalize nodelta @Hind @(transitive_le … Hp) @le_n_Sn
    13771420    ]
    13781421  ]
     
    13841427 [ normalize @le_n
    13851428 | #h #t #Hind whd in match (measure_int ???);
    1386    cases (\snd (lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,short_jump〉))
     1429   cases (\snd (lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉))
    13871430   [ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/
    13881431   |2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?)
     
    14091452lemma measure_full: ∀program.∀policy.
    14101453  measure_int program policy 0 = 2*|program| → ∀i.i<|program| →
    1411   (\snd (bvt_lookup ?? (bitvector_of_nat ? i) policy 〈0,short_jump〉)) = long_jump.
     1454  (\snd (bvt_lookup ?? (bitvector_of_nat ? i) policy 〈0,0,short_jump〉)) = long_jump.
    14121455 #program #policy elim program
    14131456 [ #Hm #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    14141457 | #h #t #Hind #Hm #i #Hi cut (measure_int t policy 0 = 2*|t|)
    14151458   [ whd in match (measure_int ???) in Hm;
    1416      cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,short_jump〉)) in Hm;
     1459     cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) in Hm;
    14171460     normalize nodelta
    14181461     [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/
     
    14261469   [ #Hi @(Hind Hmt i (le_S_S_to_le … Hi))
    14271470   | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm;
    1428      cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,short_jump〉)) in Hm;
     1471     cases (\snd (lookup … (bitvector_of_nat ? (|t|)) policy 〈0,0,short_jump〉)) in Hm;
    14291472     normalize nodelta
    14301473     [ >Hmt normalize <plus_n_O >(commutative_plus (|t|) (S (|t|)))
     
    14421485    (∀i.i ≥ |program| → i < 2^16 → lookup_opt … (bitvector_of_nat ? i) p = None ?) ∧
    14431486    jump_in_policy program p.
    1444   measure_int program policy 0 = measure_int program (jump_expansion_step program policy) 0 →
    1445   policy_equal program policy (jump_expansion_step program policy).
     1487  measure_int program policy 0 = measure_int program (jump_expansion_step program (create_label_map program policy) policy) 0 →
     1488  policy_equal program policy (jump_expansion_step program (create_label_map program policy) policy).
    14461489#program #policy lapply (le_n (|program|)) @(list_ind ?
    1447   (λx.|x| ≤ |program| → measure_int x (pi1 … policy) 0 = measure_int x (pi1 … (jump_expansion_step program policy)) 0 →
    1448       policy_equal x (pi1 … policy) (pi1 … (jump_expansion_step program policy)))
     1490  (λx.|x| ≤ |program| → measure_int x (pi1 … policy) 0 = measure_int x (pi1 … (jump_expansion_step program (create_label_map program policy) policy)) 0 →
     1491      policy_equal x (pi1 … policy) (pi1 … (jump_expansion_step program (create_label_map program policy) policy)))
    14491492   ?? program)
    14501493 [ #Hp #Hm #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O
     
    14521495   [ #Hi @Hind
    14531496     [ @(transitive_le … Hp) //
    1454      | whd in match (measure_int ???) in Hm; whd in match (measure_int ?(jump_expansion_step ??)?) in Hm;
    1455        lapply (proj2 ?? (pi2 ?? (jump_expansion_step program policy)) (|t|) ?)
     1497     | whd in match (measure_int ???) in Hm; whd in match (measure_int ?(jump_expansion_step ???)?) in Hm;
     1498       lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) (|t|) ?)
    14561499       [ @(lt_to_le_to_lt … (|h::t|)) [ // | @Hp ]
    1457        | cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,short_jump〉)) in Hm;
    1458          cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (jump_expansion_step program policy) 〈0,short_jump〉));
    1459          normalize nodelta
     1500       | cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉) in Hm;
     1501         #x cases x -x #x1 #x2 #x3
     1502         cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉);
     1503         #y cases y -y #y1 #y2 #y3
     1504         normalize nodelta cases x3 cases y3 normalize nodelta
    14601505         [1: #H #_ @H
    14611506         |2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
     
    14751520     ]
    14761521   | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm; 
    1477      whd in match (measure_int ?(jump_expansion_step ??)?) in Hm;
    1478      lapply (proj2 ?? (pi2 ?? (jump_expansion_step program policy)) (|t|) ?)
     1522     whd in match (measure_int ?(jump_expansion_step ???)?) in Hm;
     1523     lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (create_label_map program policy) policy)) (|t|) ?)
    14791524     [ @(lt_to_le_to_lt … (|h::t|)) [ // | @Hp ]
    1480      | cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,short_jump〉)) in Hm;
    1481        cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (jump_expansion_step program policy) 〈0,short_jump〉));
    1482        normalize nodelta
     1525     | cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉) in Hm;
     1526       #x cases x -x #x1 #x2 #x3
     1527       cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,0,short_jump〉);
     1528       #y cases y -y #y1 #y2 #y3
     1529       normalize nodelta cases x3 cases y3 normalize nodelta
    14831530       [1,5,9: #_ #_ //
    14841531       |4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 |2,4,6: destruct (H2) ]
     
    15011548 | #h #t #Hind #Hp whd in match (measure_int ???);
    15021549   cases (dec_is_jump (nth (|t|) ? program 〈None ?, Comment []〉)) #Hj
    1503    [ >(lookup_opt_lookup_hit … (proj2 ?? (pi2 ?? (jump_expansion_start program)) (|t|) ? Hj) 〈0,short_jump〉)
     1550   [ >(lookup_opt_lookup_hit … (proj2 ?? (pi2 ?? (jump_expansion_start program)) (|t|) ? Hj) 〈0,0,short_jump〉)
    15041551     [ normalize nodelta @Hind @le_S_to_le ]
    15051552     @Hp
    1506    | >(lookup_opt_lookup_miss … (proj1 ?? (jump_not_in_policy program (jump_expansion_internal program 0) (|t|) ?) Hj) 〈0,short_jump〉)
     1553   | >(lookup_opt_lookup_miss … (proj1 ?? (jump_not_in_policy program (jump_expansion_internal program 0) (|t|) ?) Hj) 〈0,0,short_jump〉)
    15071554     [ normalize nodelta @Hind @le_S_to_le ]
    15081555     @Hp
     
    15131560definition je_fixpoint: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
    15141561  Σp:jump_expansion_policy.∃n.∀k.n < k → policy_equal program (jump_expansion_internal program k) p.
    1515  #program @(mk_Sig …(jump_expansion_internal program (2*|program|)))
     1562 #program @(mk_Sig … (jump_expansion_internal program (2*|program|)))
    15161563 @(ex_intro … (2*|program|)) #k #Hk
    15171564 cases (dec_bounded_exists (λk.policy_equal program (jump_expansion_internal program k)
     
    15341581   [ lapply (measure_full program (jump_expansion_internal program (2*|program|)))
    15351582     #Hfull #i #Hi
    1536      lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (jump_expansion_internal program (2*|program|)))) i Hi)
    1537      >(Hfull ? i Hi)
    1538      [ cases (\snd (bvt_lookup ?? (bitvector_of_nat 16 i) (jump_expansion_step program (jump_expansion_internal program (2*|program|))) 〈0,short_jump〉))
    1539        [1,2: #H elim H #H2 [1,3: @⊥ @H2 |2,4: destruct (H2) ]
    1540        | #_ //
    1541        ]
    1542      | -i @le_to_le_to_eq
     1583     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)
     1584     lapply (Hfull ? i Hi)
     1585     [ -i @le_to_le_to_eq
    15431586       [ @measure_le
    15441587       | lapply (le_n (2*|program|)) elim (2*|program|) in ⊢ (?%? → %);
     
    15561599         ]
    15571600       ]
     1601     | -Hfull cases (bvt_lookup ?? (bitvector_of_nat 16 i) (jump_expansion_internal program (2*|program|)) 〈0,0,short_jump〉)
     1602       #x cases x -x #x1 #x2 #x3 normalize nodelta #Hfull
     1603       >Hfull cases (bvt_lookup ?? (bitvector_of_nat ? i) ? 〈0,0,short_jump〉)
     1604       #y cases y -y #y1 #y2 #y3 normalize nodelta cases y3 normalize nodelta 
     1605       [1,2: #H elim H #H2 [1,3: @⊥ @H2 |2,4: destruct (H2) ]
     1606       | #_ //
     1607       ]
    15581608     ]
    15591609   | @le_S_to_le @Hk
    15601610   ]
    1561  | #n @dec_bounded_forall #m @dec_eq_jump_length
     1611 | #n @dec_bounded_forall #m
     1612   cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,0,short_jump〉)
     1613   #x cases x -x #x1 #x2 #x3
     1614   cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,0,short_jump〉)
     1615   #y cases y -y #y1 #y2 #y3 normalize nodelta
     1616   @dec_eq_jump_length
    15621617 ]
    15631618qed.
     
    17541809 generalize in match (policy_ok_prefix_ok 〈preamble,instr_list〉 pol suffix
    17551810  (prefix@[hd]) EQ1) in ⊢ ?; >sigma00_append <EQ2 whd in ⊢ (?(??%?) → ?);
    1756  @pair_elim' #ppc #pc_map #EQ3 normalize nodelta
    1757  @pair_elim' #pc #map #EQ4 normalize nodelta
    1758  @pair_elim' #l' #i' #EQ5 normalize nodelta
     1811 @pair_elim #ppc #pc_map #EQ3 normalize nodelta
     1812 @pair_elim #pc #map #EQ4 normalize nodelta
     1813 @pair_elim #l' #i' #EQ5 normalize nodelta
    17591814 cases (construct_costs_safe ??????) normalize
    17601815  [* #abs @⊥ @abs % | #X #_ % #abs destruct(abs)]
  • src/ASM/BitVectorTrie.ma

    r1600 r1609  
    8989 ]
    9090qed.
    91   
     91 
    9292definition forall
    9393 ≝
    9494  λA.λn.λt:BitVectorTrie A n.λP.fold ? ? ? (λk.λa.λacc.(P k a) ∧ acc) t True.
    95  
     95
     96alias id "bvt_forall" = "cic:/matita/cerco/ASM/BitVectorTrie/forall.def(4)".
     97
    9698lemma forall_nodel:
    9799  ∀A:Type[0].
  • src/common/Errors.ma

    r1608 r1609  
    1818include "basics/lists/list.ma".
    1919include "common/PreIdentifiers.ma".
    20 include "basics/lists/list.ma".
    2120include "basics/russell.ma".
    2221
Note: See TracChangeset for help on using the changeset viewer.