Changeset 1965 for src/ASM/Policy.ma


Ignore:
Timestamp:
May 17, 2012, 12:42:14 PM (8 years ago)
Author:
boender
Message:
  • further completed proof, changed jump_expansion' to reflect new type of sigma
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r1956 r1965  
    294294qed.
    295295 
    296 definition policy_isize_sum ≝
     296(* definition policy_isize_sum ≝
    297297  λprefix:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map.
    298298  (\fst sigma) = foldl_strong (option Identifier × pseudo_instruction)
     
    304304    (λppc.jmpeqb long_jump (\snd (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉)))
    305305    (bitvector_of_nat 16 (\fst sigma)) (\snd x)))
    306   0.
     306  0. *)
    307307 
    308308(* The function that creates the label-to-address map *)
     
    406406qed.
    407407
    408 (* The first step of the jump expansion: everything to short.
    409  * The third condition of the dependent type implies jump_in_policy;
    410  * I've left it in for convenience of type-checking. *)
     408(* The first step of the jump expansion: everything to short. *)
    411409definition jump_expansion_start:
    412410  ∀program:(Σl:list labelled_instruction.|l| < 2^16).
     
    416414    [ None ⇒ True
    417415    | Some p ⇒
    418        And (And (out_of_program_none (pi1 ?? program) p)
     416       And (And (And (And (out_of_program_none (pi1 ?? program) p)
    419417       (jump_not_in_policy (pi1 ?? program) p))
     418       (policy_compact program labels p))
     419       (∀i.i < |program| →
     420         \snd (bvt_lookup … (bitvector_of_nat ? i) (\snd p) 〈0,short_jump〉) = short_jump))
    420421       (\fst p < 2^16)
    421422    ] ≝
     
    423424  let final_policy ≝ foldl_strong (option Identifier × pseudo_instruction)
    424425  (λprefix.Σpolicy:ppc_pc_map.
    425     And (out_of_program_none prefix policy)
     426    And (And (And (out_of_program_none prefix policy)
    426427    (jump_not_in_policy prefix policy))
     428    (policy_compact prefix labels policy))
     429    (∀i.i < |prefix| →
     430      \snd (bvt_lookup … (bitvector_of_nat ? i) (\snd policy) 〈0,short_jump〉) = short_jump))
    427431  program
    428432  (λprefix.λx.λtl.λprf.λp.
     
    456460| lapply p -p generalize in match (foldl_strong ?????); * #p #Hp #hg
    457461  @conj [ @Hp | @not_le_to_lt @leb_false_to_not_le <geb_to_leb @hg ]
    458 | @conj
     462| @conj [ @conj [ @conj
    459463  [ (* out_of_program_none *)
    460464    #i >append_length <commutative_plus #Hi normalize in Hi; #Hi2
     
    475479            ]
    476480          ]
    477           @(proj1 ?? Hp i ? Hi2) @le_S_to_le @le_S_to_le @Hi
     481          @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) i ? Hi2) @le_S_to_le @le_S_to_le @Hi
    478482        |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:
    479483          [1,2,3,6,7,24,25: #x #y
     
    490494            ]
    491495          ]
    492           <Hi @(proj1 ?? Hp (S (|prefix|)) (le_S ?? (le_n (|prefix|))) ?)
     496          <Hi @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) (S (|prefix|)) (le_S ?? (le_n (|prefix|))) ?)
    493497          >Hi @Hi2
    494498        |9,10,11,12,13,14,15,16,17:
     
    500504            ]
    501505          |1,3,5,7,9,11,13,15,17:
    502             @(proj1 ?? Hp i ? Hi2) @le_S_to_le @le_S_to_le @Hi
     506            @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) i ? Hi2) @le_S_to_le @le_S_to_le @Hi
    503507          ]
    504508        |46,47,48,49,50,51,52,53,54:
     
    510514            ]
    511515          |1,3,5,7,9,11,13,15,17:
    512             @(proj1 ?? Hp i ? Hi2) <Hi @le_S @le_n
     516            @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) i ? Hi2) <Hi @le_S @le_n
    513517          ]
    514518        ]
     
    522526          ]
    523527        ]
    524         [1,3,4: @(proj1 ?? Hp i ? Hi2) @le_S_to_le @le_S_to_le @Hi
     528        [1,3,4: @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) i ? Hi2) @le_S_to_le @le_S_to_le @Hi
    525529        |2,5,6:
    526           <Hi @(proj1 ?? Hp (S (|prefix|)) (le_S ?? (le_n (|prefix|))) ?)
     530          <Hi @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) (S (|prefix|)) (le_S ?? (le_n (|prefix|))) ?)
    527531          >Hi @Hi2
    528532        ]
     
    535539          |9,12: @sym_neq @lt_to_not_eq <Hi @le_n
    536540          ]         
    537         |1,3: @(proj1 ?? Hp i ? Hi2) @le_S_to_le @le_S_to_le @Hi
    538         |5,7: @(proj1 ?? Hp i ? Hi2) <Hi @le_S @le_n
     541        |1,3: @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) i ? Hi2) @le_S_to_le @le_S_to_le @Hi
     542        |5,7: @(proj1 ?? (proj1 ?? (proj1 ?? Hp)) i ? Hi2) <Hi @le_S @le_n
    539543        ]
    540544      ]
     
    547551        |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] >lookup_insert_miss
    548552        [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:
    549           >(nth_append_first ? i prefix ?? Hi) @((proj2 ?? Hp) i Hi)
     553          >(nth_append_first ? i prefix ?? Hi) @((proj2 ?? (proj1 ?? (proj1 ?? Hp))) i Hi)
    550554        |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:
    551555          @bitvector_of_nat_abs
     
    562566      |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] >lookup_insert_miss
    563567        [1,3,5,7,9,11,13,15,17:
    564           >(nth_append_first ? i prefix ?? Hi) @((proj2 ?? Hp) i Hi)
     568          >(nth_append_first ? i prefix ?? Hi) @((proj2 ?? (proj1 ?? (proj1 ?? Hp))) i Hi)
    565569        |2,4,6,8,10,12,14,16,18:
    566570          @bitvector_of_nat_abs
     
    578582    |2,3,4,5,6: #x [5: #y] >lookup_insert_miss
    579583      [1,3,5,7,9:
    580         >(nth_append_first ? i prefix ?? Hi) @((proj2 ?? Hp) i Hi)
     584        >(nth_append_first ? i prefix ?? Hi) @((proj2 ?? (proj1 ?? (proj1 ?? Hp))) i Hi)
    581585      |2,4,6,8,10:
    582586        @bitvector_of_nat_abs
     
    608612  ]
    609613]
    610 | @conj
     614| (* policy_compact *) cases daemon (*XXX*)
     615]
     616| (* lookup = short_jump *) #i >append_length <commutative_plus #Hi normalize in Hi;
     617 cases p -p #p cases p -p #pc #sigma #Hp cases x
     618  #lbl #instr cases instr normalize nodelta
     619  [ #pi cases pi normalize nodelta
     620    [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:
     621      [1,2,3,6,7,24,25: #x #y
     622      |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
     623      cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     624      [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:
     625        >lookup_insert_miss
     626        [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:
     627          @((proj2 ?? Hp) i Hi)
     628        |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:
     629          @bitvector_of_nat_abs
     630          [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:
     631            @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus
     632            @le_plus_a @Hi
     633          |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:
     634            @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S
     635            @le_plus_n_r
     636          |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:
     637            @lt_to_not_eq @Hi
     638          ]
     639        ]
     640      |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:
     641        >Hi >lookup_insert_hit @refl
     642      ]
     643    |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
     644      cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     645      [1,3,5,7,9,11,13,15,17: >lookup_insert_miss
     646        [1,3,5,7,9,11,13,15,17: @((proj2 ?? Hp) i Hi)
     647        |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
     648          [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf
     649            >append_length >commutative_plus @le_plus_a @Hi
     650          |2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf
     651            >append_length <plus_n_Sm @le_S_S @le_plus_n_r
     652          |3,6,9,12,15,18,21,24,27: @lt_to_not_eq @Hi
     653          ]
     654        ]
     655      |2,4,6,8,10,12,14,16,18: >Hi >lookup_insert_hit @refl
     656      ]
     657    ]
     658  |2,3,4,5,6: #x [5: #y] cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     659    [1,3,5,7,9: >lookup_insert_miss
     660      [1,3,5,7,9: @((proj2 ?? Hp) i Hi)
     661      |2,4,6,8,10: @bitvector_of_nat_abs
     662        [1,4,7,10,13: @(transitive_lt … (pi2 ?? program)) >prf >append_length
     663          >commutative_plus @le_plus_a @Hi
     664        |2,5,8,11,14: @(transitive_lt … (pi2 ?? program)) >prf >append_length
     665          <plus_n_Sm @le_S_S @le_plus_n_r
     666        |3,6,9,12,15: @lt_to_not_eq @Hi
     667        ]
     668      ]
     669    |2,4,6,8,10: >Hi >lookup_insert_hit @refl
     670    ]
     671  ]
     672]
     673| @conj [ @conj [ @conj
    611674  [ #i #_ #Hi2 / by refl/
     675  | #i #H @⊥ @(absurd … H) @not_le_Sn_O
     676  ]
     677  | #i #H @⊥ @(absurd … H) @not_le_Sn_O
     678  ]
    612679  | #i #H @⊥ @(absurd … H) @not_le_Sn_O
    613680  ]
     
    770837     |29,30: cases x #ad cases ad #a1 #a2
    771838       [1,3: cases a2 #ad2 cases ad2
    772          [1,8,20,27: #b #Hb normalize @le_S @le_S @le_S @le_S @le_S @le_n (* auto inexplicably takes a long time here *)
     839         [1,8,20,27: #b #Hb / by le_n/
    773840         |2,3,4,9,15,16,17,18,19,21,22,23,28,34,35,36,37,38: #b] #Hb cases Hb
    774841       |2,4: cases a1 #ad1 cases ad1
    775          [2,4,21,23: #b #Hb normalize @le_S @le_S @le_S @le_S @le_S @le_n
     842         [2,4,21,23: #b #Hb / by le_n/
    776843         |1,3,8,9,15,16,17,18,19,20,22,27,28,34,35,36,37,38: #b] #Hb cases Hb
    777844       ]
     
    807874(* One step in the search for a jump expansion fixpoint. *)
    808875definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
    809   ∀labels:(Σlm:label_map. ∀i:ℕ.lt i (|program|) →
    810     ∀l.occurs_exactly_once ?? l program →
    811     is_label (nth i ? program 〈None ?, Comment [ ]〉) l →
    812     lookup … lm l = Some ? i).
     876  ∀labels:(Σlm:label_map.∀l.
     877    occurs_exactly_once ?? l program →
     878    bitvector_of_nat ? (lookup_def … lm l 0) =
     879    address_of_word_labels_code_mem program l).
    813880  ∀old_policy:(Σpolicy:ppc_pc_map.
    814881    And (And (out_of_program_none program policy)
     
    11321199]
    11331200qed.
    1134 
    1135      
    1136 (* old proof | lapply (pi2 ?? acc) >p #Hpolicy normalize nodelta in Hpolicy;
    1137   cases (dec_eq_jump_length new_length old_length) #Hlength normalize nodelta
    1138   @conj [1,3: @conj [1,3: @conj [1,3: @conj [1,3: @conj [1,3: @conj
    1139 [1,3: (* out_of_policy_none *)
    1140   #i >append_length <commutative_plus #Hi normalize in Hi;
    1141   #Hi2 >lookup_opt_insert_miss
    1142   [1,3: @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i (le_S_to_le … Hi)) @Hi2
    1143   |2,4: >eq_bv_sym @bitvector_of_nat_abs
    1144     [1,4: @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    1145       @le_S_S @le_plus_n_r
    1146     |2,5: @Hi2
    1147     |3,6: @lt_to_not_eq @Hi
    1148     ]
    1149   ]
    1150 |2,4: (* labels_okay *)
    1151   @lookup_forall #i cases i -i #i cases i -i #p #a #j #n #Hl
    1152   elim (insert_lookup_opt ?? 〈p,a,j〉 ???? Hl) -Hl #Hl
    1153   [1,3: elim (forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) ? n Hl)
    1154     #i #Hi @(ex_intro ?? i Hi)
    1155   |2,4: normalize nodelta normalize nodelta in p2; cases instr in p2;
    1156     [2,3,8,9: #x #abs normalize nodelta in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
    1157     |6,12: #x #y #abs normalize nodelta in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
    1158     |1,7: #pi cases pi
    1159       [35,36,37,72,73,74: #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
    1160       |1,2,3,6,7,33,34,38,39,40,43,44,70,71:
    1161         #x #y #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
    1162       |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69:
    1163         #x #abs normalize in abs;lapply (jmeq_to_eq ??? abs) #H destruct (H)
    1164       |9,10,14,15,46,47,51,52:
    1165         #id normalize nodelta whd in match (jump_expansion_step_instruction ???);
    1166         whd in match (select_reljump_length ???); >p3
    1167         lapply (refl ? (lookup_def ?? (pi1 ?? labels) id 〈0,\fst pol〉))
    1168         cases (lookup_def ?? labels id 〈0,\fst pol〉) in ⊢ (???% → %); #q1 #q2
    1169         normalize nodelta #H
    1170         >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
    1171         >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb (\fst pol) q2))
    1172         cases (leb (\fst pol) q2) in ⊢ (???% → %); #Hle1
    1173         [1,3,5,7,9,11,13,15: lapply (refl ? (leb (q2-\fst pol) 126)) cases (leb (q2-\fst pol) 126) in ⊢ (???% → %);
    1174         |2,4,6,8,10,12,14,16: lapply (refl ? (leb (\fst pol-q2) 129)) cases (leb (\fst pol-q2) 129) in ⊢ (???% → %);
    1175         ]
    1176         #Hle2 normalize nodelta #Hli @(ex_intro ?? id) >H
    1177         <(pair_eq1 ?????? (Some_eq ??? Hli)) @refl
    1178       |11,12,13,16,17,48,49,50,53,54:
    1179         #x #id normalize nodelta whd in match (jump_expansion_step_instruction ???);
    1180         whd in match (select_reljump_length ???); >p3
    1181         lapply (refl ? (lookup_def ?? labels id 〈0,\fst pol〉))
    1182         cases (lookup_def ?? labels id 〈0,\fst pol〉) in ⊢ (???% → %); #q1 #q2
    1183         normalize nodelta #H
    1184         >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
    1185         >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb (\fst pol) q2))
    1186         cases (leb (\fst pol) q2) in ⊢ (???% → %); #Hle1
    1187         [1,3,5,7,9,11,13,15,17,19: lapply (refl ? (leb (q2-\fst pol) 126)) cases (leb (q2-\fst pol) 126) in ⊢ (???% → %);
    1188         |2,4,6,8,10,12,14,16,18,20: lapply (refl ? (leb (\fst pol-q2) 129)) cases (leb (\fst pol-q2) 129) in ⊢ (???% → %);
    1189         ]
    1190         #Hle2 normalize nodelta #Hli @(ex_intro ?? id) >H
    1191         <(pair_eq1 ?????? (Some_eq ??? Hli)) @refl
    1192       ]
    1193     |4,5,10,11: #id normalize nodelta whd in match (select_jump_length ???);
    1194       whd in match (select_call_length ???); >p3
    1195       lapply (refl ? (lookup_def ?? labels id 〈0,\fst pol〉))
    1196       cases (lookup_def ?? labels id 〈0,\fst pol〉) in ⊢ (???% → %); #q1 #q2
    1197       normalize nodelta #H
    1198       [1,3: cases (leb (\fst pol) q2)
    1199         [1,3: cases (leb (q2-\fst pol) 126) |2,4: cases (leb (\fst pol-q2) 129) ]
    1200         [1,3,5,7: normalize nodelta #H2 >(pair_eq1 ?????? (Some_eq ??? H2)) in H;
    1201         #Hli @(ex_intro ?? id) lapply (proj2 ?? Hl)
    1202         #H >(pair_eq1 ?????? (pair_eq1 ?????? H))
    1203         >(pair_eq2 ?????? (pair_eq1 ?????? H)) >Hli @refl]
    1204       ]
    1205       cases (split ? 5 11 (bitvector_of_nat 16 q2)) #n1 #n2
    1206       cases (split ? 5 11 (bitvector_of_nat 16 (\fst pol))) #m1 #m2
    1207       normalize nodelta cases (eq_bv ? n1 m1)
    1208       normalize nodelta #H2 >(pair_eq1 ?????? (Some_eq ??? H2)) in H; #H
    1209       @(ex_intro ?? id) lapply (proj2 ?? Hl) #H2
    1210       >(pair_eq1 ?????? (pair_eq1 ?????? H2)) >(pair_eq2 ?????? (pair_eq1 ?????? H2))
    1211       >H @refl
    1212     ]
    1213   ]
    1214  ]
    1215 |2,4: (* jump_in_policy *)
    1216   #i #Hi cases (le_to_or_lt_eq … Hi) -Hi;
    1217   [1,3: >append_length <commutative_plus #Hi normalize in Hi;
    1218     >(nth_append_first ?? prefix ??(le_S_S_to_le ?? Hi)) @conj
    1219     [1,3: #Hj lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_S_to_le … Hi))
    1220       #Hacc elim (proj1 ?? Hacc Hj) #h #n elim n -n #n #H elim H -H #j #Hj
    1221       @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?))) whd in match (snd ???);
    1222       >lookup_opt_insert_miss [1,3: @Hj |2,4:  @bitvector_of_nat_abs ]
    1223       [3,6: @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi)
    1224       |1,4: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
    1225       ]
    1226       @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    1227       @le_S_S @le_plus_n_r
    1228     |2,4: lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_S_to_le … Hi))
    1229       #Hacc #H elim H -H; #h #H elim H -H; #n #H elim H -H #j #Hl
    1230       @(proj2 ?? Hacc) @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?)))
    1231       <Hl @sym_eq @lookup_opt_insert_miss @bitvector_of_nat_abs
    1232       [3,6: @lt_to_not_eq @(le_S_S_to_le … Hi)
    1233       |1,4: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
    1234       ]
    1235       @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    1236       @le_S_S @le_plus_n_r
    1237     ]
    1238   |2,4: >append_length <commutative_plus #Hi normalize in Hi; >(injective_S … Hi)
    1239     >(nth_append_second ?? prefix ?? (le_n (|prefix|)))
    1240      <minus_n_n whd in match (nth ????); normalize nodelta in p2; cases instr in p2;
    1241      [1,7: #pi | 2,3,8,9: #x | 4,5,10,11: #id | 6,12: #x #y] #Hinstr @conj normalize nodelta
    1242      [5,7,9,11,21,23: #H @⊥ @H (* instr is not a jump *)
    1243      |6,8,10,12,22,24: normalize nodelta in Hinstr; lapply (jmeq_to_eq ??? Hinstr)
    1244       #H destruct (H)
    1245      |13,15,17,19: (* instr is a jump *) #_ @(ex_intro ?? (\fst pol))
    1246        @(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai))
    1247        @lookup_opt_insert_hit
    1248      |14,16,18,20: #_ / by I/
    1249      |1,2,3,4: cases pi in Hinstr;
    1250        [35,36,37,109,110,111: #Hinstr #H @⊥ @H
    1251        |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,78,79,82,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106:
    1252          #x #Hinstr #H @⊥ @H
    1253        |1,2,3,6,7,33,34,75,76,77,80,81,107,108: #x #y #Hinstr #H @⊥ @H
    1254        |9,10,14,15,83,84,88,89: #id #Hinstr #_
    1255          @(ex_intro ?? (\fst pol)) @(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai))
    1256          @lookup_opt_insert_hit
    1257        |11,12,13,16,17,85,86,87,90,91: #x #id #Hinstr #_
    1258          @(ex_intro ?? (\fst pol)) @(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai))
    1259          @lookup_opt_insert_hit
    1260        |72,73,74,146,147,148: #Hinstr lapply (jmeq_to_eq ??? Hinstr) #H normalize in H; destruct (H)
    1261        |41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,115,116,119,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143:
    1262         #x #Hinstr lapply (jmeq_to_eq ??? Hinstr) #H normalize in H; destruct (H)
    1263        |38,39,40,43,44,70,71,112,113,114,117,118,144,145: #x #y #Hinstr lapply (jmeq_to_eq ??? Hinstr) #H
    1264          normalize in H; destruct (H)
    1265        |46,47,51,52,120,121,125,126: #id #Hinstr #_ / by I/
    1266        |48,49,50,53,54,122,123,124,127,128: #x #id #Hinstr #_ / by I/
    1267        ]
    1268      ]
    1269    ]
    1270  ]
    1271 |2,4: (* policy increase *)
    1272   #i >append_length >commutative_plus #Hi normalize in Hi;
    1273   cases (le_to_or_lt_eq … Hi) -Hi; #Hi
    1274   [1,3: >lookup_insert_miss
    1275     [1,3: @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i (le_S_S_to_le … Hi))
    1276     |2,4: @bitvector_of_nat_abs
    1277       [3,6: @lt_to_not_eq @(le_S_S_to_le … Hi)
    1278       |1,4: @(transitive_lt ??? (le_S_S_to_le … Hi))
    1279       ]
    1280       @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    1281       @le_S_S @le_plus_n_r
    1282     ]
    1283   |2: >(injective_S … Hi) normalize nodelta in Hlength; >lookup_insert_hit normalize nodelta
    1284     >Hlength @pair_elim #l1 #l2 #Hl @pair_elim #y1 #y2 #Hy
    1285     >Hl %2 @refl
    1286   |4: cases daemon (* XXX get rest of proof done first *)
    1287   ]
    1288  ]
    1289 |2,4: (* policy_safe *)
    1290   @lookup_forall #x cases x -x #x cases x -x #p #a #j #n normalize nodelta #Hl
    1291   elim (insert_lookup_opt ?? 〈p,a,j〉 ???? Hl) -Hl #Hl
    1292   [1,3: @(forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy))) ? n Hl)
    1293   |2,4: normalize nodelta in p2; cases instr in p2;
    1294     [2,3,8,9: #x #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
    1295     |6,12: #x #y #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
    1296     |1,7: #pi cases pi normalize nodelta
    1297      [35,36,37,72,73,74: #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
    1298      |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69:
    1299        #x #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
    1300      |1,2,3,6,7,33,34,38,39,40,43,44,70,71:
    1301        #x #y #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H)
    1302      |9,10,14,15,46,47,51,52: #id >p3 whd in match (jump_expansion_step_instruction ???);
    1303        whd in match (select_reljump_length ???);
    1304        cases (lookup_def ?? labels id 〈0,\fst pol〉) #q1 #q2 normalize nodelta
    1305        >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
    1306        >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb (\fst pol) q2))
    1307        cases (leb (\fst pol) q2) in ⊢ (???% → %); #Hle1
    1308        [1,3,5,7,9,11,13,15: lapply (refl ? (leb (q2-\fst pol) 126)) cases (leb (q2-\fst pol) 126) in ⊢ (???% → %);
    1309        |2,4,6,8,10,12,14,16: lapply (refl ? (leb (\fst pol-q2) 129)) cases (leb (\fst pol-q2) 129) in ⊢ (???% → %);
    1310        ]
    1311        #Hle2 normalize nodelta #Hli
    1312        <(pair_eq1 ?????? (Some_eq ??? Hli)) >Hle1
    1313        >(pair_eq2 ?????? (proj2 ?? Hl)) <(pair_eq2 ?????? (Some_eq ??? Hli))
    1314        cases (\snd (lookup ?? (bitvector_of_nat ? (|prefix|)) (\snd old_policy) ?))
    1315        [1,7,13,19,25,31,37,43,49,55,61,67,73,79,85,91: @(leb_true_to_le … Hle2)
    1316        ] normalize @I (* much faster than / by I/, strangely enough *)
    1317      |11,12,13,16,17,48,49,50,53,54: #x #id >p3 whd in match (jump_expansion_step_instruction ???);
    1318        whd in match (select_reljump_length ???);
    1319        cases (lookup_def ?? labels id 〈0,\fst pol〉) #q1 #q2 normalize nodelta
    1320        >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
    1321        >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb (\fst pol) q2))
    1322        cases (leb (\fst pol) q2) in ⊢ (???% → %); #Hle1
    1323        [1,3,5,7,9,11,13,15,17,19: lapply (refl ? (leb (q2-\fst pol) 126)) cases (leb (q2-\fst pol) 126) in ⊢ (???% → %);
    1324        |2,4,6,8,10,12,14,16,18,20: lapply (refl ? (leb (\fst pol-q2) 129)) cases (leb (\fst pol-q2) 129) in ⊢ (???% → %);
    1325        ]
    1326        #Hle2 normalize nodelta #Hli
    1327        <(pair_eq1 ?????? (Some_eq ??? Hli)) >Hle1 >(pair_eq2 ?????? (proj2 ?? Hl))
    1328        <(pair_eq2 ?????? (Some_eq ??? Hli))
    1329        cases (\snd (lookup ?? (bitvector_of_nat ? (|prefix|)) (\snd old_policy) ?))
    1330        [1,7,13,19,25,31,37,43,49,55,61,67,73,79,85,91,97,103,109,115: @(leb_true_to_le … Hle2)
    1331        ] normalize @I (* vide supra *)
    1332      ]
    1333     |4,5,10,11: #id >p3 normalize nodelta whd in match (select_jump_length ???);
    1334       whd in match (select_call_length ???); cases (lookup_def ?? labels id 〈0,\fst pol〉)
    1335       #q1 #q2 normalize nodelta
    1336       >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
    1337       >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl)))
    1338       [1,3: lapply (refl ? (leb (\fst pol) q2)) cases (leb (\fst pol) q2) in ⊢ (???% → %); #Hle1
    1339         [1,3: lapply (refl ? (leb (q2-\fst pol) 126)) cases (leb (q2-\fst pol) 126) in ⊢ (???% → %);
    1340         |2,4: lapply (refl ? (leb (\fst pol-q2) 129)) cases (leb (\fst pol-q2) 129) in ⊢ (???% → %);
    1341         ]
    1342        #Hle2 normalize nodelta
    1343       ]
    1344       [2,4,6,8,9,10: lapply (refl ? (split ? 5 11 (bitvector_of_nat ? q2)))
    1345         cases (split ??? (bitvector_of_nat ? q2)) in ⊢ (???% → %); #x1 #x2 #Hle3
    1346         lapply (refl ? (split ? 5 11 (bitvector_of_nat ? (\fst pol))))
    1347         cases (split ??? (bitvector_of_nat ? (\fst pol))) in ⊢ (???% → %); #y1 #y2 #Hle4
    1348         normalize nodelta lapply (refl ? (eq_bv 5 x1 y1))
    1349         cases (eq_bv 5 x1 y1) in ⊢ (???% → %); #Hle5
    1350       ]
    1351       #Hli <(pair_eq1 ?????? (Some_eq ??? Hli)) >(pair_eq2 ?????? (proj2 ?? Hl))
    1352       <(pair_eq2 ?????? (Some_eq ??? Hli))
    1353       cases (\snd (lookup ?? (bitvector_of_nat ? (|prefix|)) (\snd old_policy) ?))
    1354       [2,8,14,20,26,32: >Hle3 @Hle5
    1355       |37,40,43,46: >Hle1 @(leb_true_to_le … Hle2)
    1356       ] normalize @I (* here too *)
    1357     ]
    1358   ]
    1359  ]
    1360 |2,4: (* changed *)
    1361   normalize nodelta #Hc [2: destruct (Hc)] #i #Hi cases (le_to_or_lt_eq … Hi) -Hi
    1362   >append_length >commutative_plus #Hi
    1363   normalize in Hi;
    1364   [ >lookup_insert_miss
    1365     [ @(proj2 ?? (proj1 ?? Hpolicy) Hc i (le_S_S_to_le … Hi))
    1366     | @bitvector_of_nat_abs
    1367       [3: @lt_to_not_eq @(le_S_S_to_le … Hi)
    1368       |1: @(transitive_lt ??? (le_S_S_to_le … Hi))
    1369       ]
    1370       @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    1371       @le_S_S @le_plus_n_r
    1372     ]
    1373   | >(injective_S … Hi) >lookup_insert_hit normalize nodelta in Hlength; >Hlength
    1374     normalize nodelta @pair_elim #l1 #l2 #Hl @pair_elim #y1 #y2 #Hy >Hl @refl
    1375   ]
    1376  ]
    1377 |2,4: (* policy_isize_sum XXX *) cases daemon
    1378 ]
    1379 | (* Case where add_instr = None *) normalize nodelta lapply (pi2 ?? acc) >p >p1
    1380   normalize nodelta #Hpolicy
    1381   @conj [ @conj [ @conj [ @conj [ @conj [ @conj
    1382 [ (* out_of_program_none *) #i >append_length >commutative_plus #Hi normalize in Hi;
    1383   #Hi2 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i (le_S_to_le ?? Hi) Hi2)
    1384 | (* labels_okay *) @lookup_forall #x cases x -x #x cases x #p #a #j #lbl #Hl normalize nodelta
    1385   elim (forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) ? lbl Hl)
    1386   #id #Hid @(ex_intro … id Hid)
    1387  ]
    1388 | (* jump_in_policy *) #i >append_length >commutative_plus #Hi normalize in Hi;
    1389   elim (le_to_or_lt_eq … Hi) -Hi #Hi
    1390   [ >(nth_append_first ?? prefix ?? (le_S_S_to_le ?? Hi))
    1391     @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_S_to_le ?? Hi))
    1392   | >(injective_S … Hi) @conj
    1393     [ >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n whd in match (nth ????);
    1394       normalize nodelta in p2; cases instr in p2;
    1395       [ #pi cases pi
    1396         [1,2,3,6,7,33,34: #x #y #_ #H @⊥ @H
    1397         |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #_ #H @⊥ @H
    1398         |9,10,14,15: #id (* normalize segfaults here *) normalize nodelta
    1399           whd in match (jump_expansion_step_instruction ???);
    1400           #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
    1401         |11,12,13,16,17: #x #id normalize nodelta
    1402           whd in match (jump_expansion_step_instruction ???);
    1403           #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
    1404         |35,36,37: #_ #H @⊥ @H
    1405         ]
    1406       |2,3: #x #_ #H @⊥ @H
    1407       |4,5: #id normalize nodelta #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
    1408       |6: #x #id #_ #H @⊥ @H
    1409       ]
    1410     | #H elim H -H #p #H elim H -H #a #H elim H -H #j #H
    1411       >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) (|prefix|) (le_n (|prefix|)) ?) in H;
    1412       [ #H destruct (H)
    1413       | @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    1414         @le_S_S @le_plus_n_r
    1415       ]
    1416     ]
    1417   ]
    1418  ]
    1419 | (* policy_increase *) #i >append_length >commutative_plus #Hi normalize in Hi;
    1420   elim (le_to_or_lt_eq … Hi) -Hi #Hi
    1421   [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i (le_S_S_to_le … Hi))
    1422   | >(injective_S … Hi) >lookup_opt_lookup_miss
    1423     [ >lookup_opt_lookup_miss
    1424       [ normalize nodelta %2 @refl
    1425       | @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) (|prefix|) (le_n (|prefix|)) ?)
    1426         @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    1427         @le_S_S @le_plus_n_r
    1428       ]
    1429     | @(proj1 ?? (jump_not_in_policy (pi1 … program) «pi1 ?? old_policy,proj1 ?? (proj1 ?? (pi2 ?? old_policy))» (|prefix|) ?)) >prf
    1430       [ >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r
    1431       | >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n >p1
    1432         whd in match (nth ????); normalize nodelta in p2; cases instr in p2;
    1433         [ #pi cases pi
    1434           [1,2,3,6,7,33,34: #x #y #_ normalize /2 by nmk/
    1435           |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #_ normalize /2 by nmk/
    1436           |9,10,14,15: #id (* normalize segfaults here *) normalize nodelta
    1437             whd in match (jump_expansion_step_instruction ???);
    1438             #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
    1439           |11,12,13,16,17: #x #id normalize nodelta
    1440             whd in match (jump_expansion_step_instruction ???);
    1441             #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
    1442           |35,36,37: #_ normalize /2 by nmk/
    1443           ]
    1444         |2,3: #x #_ normalize /2 by nmk/
    1445         |4,5: #id normalize nodelta #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
    1446         |6: #x #id #_ normalize /2 by nmk/
    1447         ]
    1448       ]
    1449     ]
    1450   ]
    1451  ]
    1452 | (* policy_safe *) @lookup_forall #x cases x -x #x cases x -x #p #a #j #n #Hl
    1453   @(forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy))) ? n Hl)
    1454  ]
    1455 | (* changed *) #Hc #i >append_length >commutative_plus #Hi normalize in Hi;
    1456   elim (le_to_or_lt_eq … Hi) -Hi #Hi
    1457   [ @(proj2 ?? (proj1 ?? Hpolicy) Hc i (le_S_S_to_le … Hi))
    1458   | >(injective_S … Hi) >lookup_opt_lookup_miss
    1459     [ >lookup_opt_lookup_miss
    1460       [ normalize nodelta @refl
    1461       | @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) (|prefix|) (le_n (|prefix|)) ?)
    1462         @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    1463         @le_S_S @le_plus_n_r
    1464       ]
    1465     | @(proj1 ?? (jump_not_in_policy (pi1 … program) «pi1 ?? old_policy,proj1 ?? (proj1 ?? (pi2 ?? old_policy))» (|prefix|) ?)) >prf
    1466       [ >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r
    1467       | >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n >p1
    1468         whd in match (nth ????); normalize nodelta in p2; cases instr in p2;
    1469         [ #pi cases pi
    1470           [1,2,3,6,7,33,34: #x #y #_ normalize /2 by nmk/
    1471           |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #_ normalize /2 by nmk/
    1472           |9,10,14,15: #id (* normalize segfaults here *) normalize nodelta
    1473             whd in match (jump_expansion_step_instruction ???);
    1474             #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
    1475           |11,12,13,16,17: #x #id normalize nodelta
    1476             whd in match (jump_expansion_step_instruction ???);
    1477             #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
    1478           |35,36,37: #_ normalize /2 by nmk/
    1479           ]
    1480         |2,3: #x #_ normalize /2 by nmk/
    1481         |4,5: #id normalize nodelta #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2)
    1482         |6: #x #id #_ normalize /2 by nmk/
    1483         ]
    1484       ]
    1485     ]
    1486   ]
    1487  ]
    1488 | (* XXX policy_isize_sum *) cases daemon
    1489 ]
    1490 | @conj [ @conj [ @conj [ @conj [ @conj [ @conj
    1491   [ #i #Hi / by refl/
    1492   | / by I/
    1493   ]
    1494   | #i #Hi @conj [ >nth_nil #H @⊥ @H | #H elim H #x #H1 elim H1 #y #H2 elim H2 #z #H3
    1495                    normalize in H3; destruct (H3) ]
    1496   ]                 
    1497   | #i #Hi @⊥ @(absurd (i<0)) [ @Hi | @(not_le_Sn_O) ]
    1498   ]
    1499   | / by I/
    1500   ]
    1501   | #_ #i #Hi @⊥ @(absurd (i < 0)) [ @Hi | @not_le_Sn_O ]
    1502   ]
    1503   | / by refl/
    1504   ]
    1505 ]
    1506 qed.*)
    1507 
    1508 (* this might be replaced by a coercion: (∀x.A x → B x) → Σx.A x → Σx.B x *)
    1509 (* definition weaken_policy:
    1510   ∀program,op.
    1511   option (Σp:jump_expansion_policy.
    1512     And (And (And (And (out_of_program_none program p)
    1513     (labels_okay (create_label_map program op) p))
    1514     (jump_in_policy program p)) (policy_increase program op p))
    1515     (policy_safe p)) →
    1516   option (Σp:jump_expansion_policy.And (out_of_program_none program p)
    1517     (jump_in_policy program p)) ≝
    1518  λprogram.λop.λx.
    1519  match x return λ_.option (Σp.And (out_of_program_none program p) (jump_in_policy program p)) with
    1520  [ None ⇒ None ?
    1521  | Some z ⇒ Some ? (mk_Sig ?? (pi1 ?? z) ?)
    1522  ].
    1523 @conj
    1524 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? z)))))
    1525 | @(proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? z))))
    1526 ]
    1527 qed. *)
    1528 
    1529 (* This function executes n steps from the starting point. *)
    1530 (*let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (|l|) 2^16)
    1531   (n: ℕ) on n:(Σx:bool × ℕ × (option jump_expansion_policy).
    1532     let 〈ch,pc,y〉 ≝ x in
    1533     match y with
    1534     [ None ⇒ pc > 2^16
    1535     | Some p ⇒ And (out_of_program_none program p) (jump_in_policy program p)
    1536     ]) ≝
    1537   match n with
    1538   [ O   ⇒ 〈0,Some ? (pi1 … (jump_expansion_start program))〉
    1539   | S m ⇒ let 〈ch,pc,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in
    1540           match z return λx. z=x → Σa:bool × ℕ × (option jump_expansion_policy).? with
    1541           [ None    ⇒ λp2.〈pc,None ?〉
    1542           | Some op ⇒ λp2.pi1 … (jump_expansion_step program (create_label_map program op) «op,?»)
    1543           ] (refl … z)
    1544   ].*)
    1545  
    1546 
     1201   
    15471202let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (length ? l) 2^16) (n: ℕ)
    15481203  on n:(Σx:bool × (option ppc_pc_map).
     
    15511206    [ None ⇒ True
    15521207    | Some x ⇒
    1553       And (And
     1208      And (And (And
    15541209        (out_of_program_none program x)
    1555         (policy_isize_sum program (create_label_map program) x))
     1210        (jump_not_in_policy program x))
     1211        (policy_compact program (create_label_map program) x))
    15561212        (\fst x < 2^16)
    15571213    ]) ≝
     
    15701226  #p cases p
    15711227  [ / by I/
    1572   | #pm / by I/
     1228  | #pm normalize nodelta #H @conj [ @(proj1 ?? (proj1 ?? H)) | @(proj2 ?? H) ]
    15731229  ]
    15741230| lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta / by /
    1575 | lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta / by /
     1231| lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta
     1232  #H @conj [ @(proj1 ?? (proj1 ?? H)) | @(proj2 ?? H) ]
    15761233| normalize nodelta cases (jump_expansion_step program labels «op,?»)
    15771234  #p cases p -p #p #r cases r normalize nodelta
     
    15791236  | #j #H @conj
    15801237    [ @conj
    1581       [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
    1582       | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
     1238      [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))
     1239      | @(proj2 ?? (proj1 ?? (proj1 ?? H)))
    15831240      ]
    15841241    | @(proj2 ?? H)
     
    17481405  ∀policy:Σp:ppc_pc_map.
    17491406    out_of_program_none program p ∧
    1750     policy_isize_sum program (create_label_map program) p ∧ \fst p < 2^16.
     1407    jump_not_in_policy program p ∧ \fst p < 2^16.
    17511408  ∀l.|l| ≤ |program| → ∀acc:ℕ.
    17521409  match \snd (jump_expansion_step program (create_label_map program) policy) with
     
    17641421    cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)
    17651422    #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd x) 〈0,short_jump〉)
    1766     #y1 #y2 normalize nodelta #Hblerp cases (proj2 ?? Hblerp) cases x2 cases y2
     1423    #y1 #y2 normalize nodelta #Hblerp cases Hblerp cases x2 cases y2
    17671424    [1,4,5,7,8,9: #H cases H
    17681425    |2,3,6: #_ normalize nodelta
     
    17961453lemma measure_full: ∀program.∀policy.
    17971454  measure_int program policy 0 = 2*|program| → ∀i.i<|program| →
    1798   is_jump (nth i ? program 〈None ?,Comment []〉) →
     1455  is_jump (\snd (nth i ? program 〈None ?,Comment []〉)) →
    17991456  (\snd (bvt_lookup ?? (bitvector_of_nat ? i) (\snd policy) 〈0,short_jump〉)) = long_jump.
    18001457#program #policy elim program in ⊢ (% → ∀i.% → ? → %);
     
    18291486lemma measure_special: ∀program:(Σl:list labelled_instruction.|l| < 2^16).
    18301487  ∀policy:Σp:ppc_pc_map.
    1831     out_of_program_none program p ∧ policy_isize_sum program (create_label_map program) p ∧ \fst p < 2^16.
     1488    out_of_program_none program p ∧ jump_not_in_policy program p ∧ \fst p < 2^16.
    18321489  match (\snd (pi1 ?? (jump_expansion_step program (create_label_map program) policy))) with
    18331490  [ None ⇒ True
     
    18551512         lapply (measure_incr_or_equal program policy t ? 0)
    18561513         [1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
    1857        |4,7,8: #H elim (proj2 ?? H) #H2 [1,3,5: cases H2 |2,4,6: destruct (H2) ]
     1514       |4,7,8: #H elim H #H2 [1,3,5: cases H2 |2,4,6: destruct (H2) ]
    18581515       |5: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 1)
    18591516         #_ #H @(injective_plus_r … H)
     
    18711528     whd in match (measure_int ? p ?) in Hm;
    18721529     lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol))) (|t|) Hp)
    1873      cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉) in   
    1874 Hm;
     1530     cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉) in Hm;
    18751531     #x1 #x2
    18761532     cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉);
    18771533     #y1 #y2
    18781534     normalize nodelta cases x2 cases y2 normalize nodelta
    1879      cases daemon
    1880      (* [1,5,9: #_ #_ //
    1881      |4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 |2,4,6: destruct (H2) ]
     1535     [1,5,9: #_ #_ @refl
     1536     |4,7,8: #_ #H elim H #H2 [1,3,5: cases H2 |2,4,6: destruct (H2) ]
    18821537     |2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt
    18831538       lapply (measure_incr_or_equal program policy t ? 0)
     
    18881543        lapply (measure_incr_or_equal program policy t ? 0)
    18891544        [ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by /
    1890      ] *)
     1545     ]
    18911546   ]
    18921547 ]
     
    19081563qed.
    19091564
    1910 (* probably needs some kind of not_jump → short *)
    19111565lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction.|l| < 2^16.
    19121566  match jump_expansion_start program (create_label_map program) with
     
    19201574 | #pl normalize nodelta #Hpl #EQ elim l
    19211575   [ / by refl/
    1922    | #h #t #Hind #Hp
    1923      cases daemon (*
    1924     cases (dec_is_jump (nth (|t|) ? program 〈None ?, Comment []〉)) #Hj
    1925      [ normalize nodelta @Hind @le_S_to_le ]
    1926      @Hp
    1927    | >(lookup_opt_lookup_miss … (proj1 ?? (jump_not_in_policy program (pi1 ?? (jump_expansion_start program)) (|t|) ?) Hj) 〈0,0,short_jump〉)
    1928      [ normalize nodelta @Hind @le_S_to_le @Hp
    1929      | @Hp
    1930      | %
    1931        [ @(proj1 ?? (proj1 ?? (pi2 ?? (jump_expansion_start program))))
    1932        | @(proj2 ?? (proj1 ?? (pi2 ?? (jump_expansion_start program))))
    1933        ]
    1934      ]
    1935    ]*)
    1936  ]
     1576   | #h #t #Hind #Hp whd in match (measure_int ???);
     1577     >(proj2 ?? (proj1 ?? Hpl) (|t|))
     1578     [ normalize nodelta @Hind ]
     1579     @(transitive_le … Hp) [ @le_n_Sn | @ le_n ]
     1580   ]
     1581 ]   
    19371582qed.
    19381583
     
    19421587    And (match p with
    19431588      [ None ⇒ True
    1944       | Some pol ⇒ And (And (
    1945       (out_of_program_none program pol))
    1946       (policy_isize_sum program (create_label_map program) pol))
     1589      | Some pol ⇒ And (out_of_program_none program pol)
    19471590      (policy_compact program (create_label_map program) pol)
    19481591      ])
    19491592    (∃n.∀k.n < k →
    19501593      policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program k))) p).
    1951 #program @(\snd (pi1 ?? (jump_expansion_internal program (2*|program|))))
    1952 cases daemon
    1953 
    1954 (* old proof
    1955 cases (dec_bounded_exists (λk.policy_equal (pi1 ?? program)
     1594#program @(\snd (pi1 ?? (jump_expansion_internal program (2*|program|)))) @conj
     1595[ lapply (pi2 ?? (jump_expansion_internal program (2*|program|)))
     1596    cases (jump_expansion_internal program (2*|program|)) #p cases p -p
     1597    #c #pol #Hp cases pol
     1598    [ normalize nodelta //
     1599    | #x normalize nodelta #H @conj [ @(proj1 ?? (proj1 ?? (proj1 ?? H)))
     1600    | cases daemon ] ]
     1601| cases (dec_bounded_exists (λk.policy_equal_opt (pi1 ?? program)
    19561602   (\snd (pi1 ?? (jump_expansion_internal program k)))
    19571603   (\snd (pi1 ?? (jump_expansion_internal program (S k))))) ? (2*|program|))
    1958  cases daemon
    19591604[ #Hex elim Hex -Hex #x #Hx @(ex_intro … x) #k #Hk
    19601605  @pe_trans
     
    19691614    ]   
    19701615  ]
    1971 | #Hnex lapply (not_exists_forall … Hnex) -Hnex; #Hfa @(ex_intro … (2*|program|)) #k #Hk
    1972   @pe_sym @equal_remains_equal
     1616| #Hnex lapply (not_exists_forall … Hnex) -Hnex; #Hfa
     1617  @(ex_intro … (2*|program|)) #k #Hk @pe_sym @equal_remains_equal
    19731618  [ lapply (refl ? (jump_expansion_internal program (2*|program|)))
    19741619    cases (jump_expansion_internal program (2*|program|)) in ⊢ (???% → %);
     
    19791624    | #Fp #HFp #EQ whd in match (jump_expansion_internal ??);
    19801625      >EQ normalize nodelta
    1981       lapply (refl ? (jump_expansion_step program (create_label_map program Fp) «Fp,?»))
    1982       [ @HFp
     1626      lapply (refl ? (jump_expansion_step program (create_label_map program) «Fp,?»))
     1627      [ @conj [ @(proj1 ?? (proj1 ?? HFp)) | @(proj2 ?? HFp) ]
    19831628      | lapply (measure_full program Fp ?)
    19841629        [ @le_to_le_to_eq
     
    19881633                x ≤ measure_int program p 0))
    19891634            [ #x elim x
    1990               [ #Hx @(ex_intro ?? (jump_expansion_start program)) @conj
    1991                 [ whd in match (jump_expansion_internal ??); @refl
    1992                 | @le_O_n
     1635              [ #Hx lapply (refl ? (jump_expansion_start program (create_label_map program)))
     1636                cases (jump_expansion_start program (create_label_map program)) in ⊢ (???% → %);
     1637                #z cases z -z normalize nodelta
     1638                [ #Waar #Heqn @⊥ elim (le_to_eq_plus ?? Hx) #k #Hk
     1639                  @(absurd … (step_none program 0 ? k))
     1640                  [ whd in match (jump_expansion_internal ??); >Heqn @refl
     1641                  | <Hk >EQ @nmk #H destruct (H)
     1642                  ]
     1643                | #pol #Hpol #Heqpol @(ex_intro ?? pol) @conj
     1644                  [ whd in match (jump_expansion_internal ??); >Heqpol @refl
     1645                  | @le_O_n
     1646                  ]
    19931647                ]
    19941648              | -x #x #Hind #Hx
     
    20081662                    [ cases (jump_expansion_internal program x) in Hxpol;
    20091663                      #z cases z -z #xch #xpol normalize nodelta #H #H2 >(proj1 ?? H2) in H;
    2010                       normalize nodelta / by /
     1664                      normalize nodelta #H @conj [ @(proj1 ?? (proj1 ?? H)) | @(proj2 ?? H) ]
    20111665                    | lapply (Hfa x Hx) lapply HeqSxpol -HeqSxpol
    20121666                      whd in match (jump_expansion_internal program (S x));
     
    20151669                      #z cases z -z #xch #b normalize nodelta #H #Heq >(proj1 ?? Heq) in H;
    20161670                      #H #Heq cases xch in Heq; #Heq normalize nodelta
    2017                       [ lapply (refl ? (jump_expansion_step program (create_label_map (pi1 ?? program) xpol) «xpol,H»))
    2018                         cases (jump_expansion_step ???) in ⊢ (???% → %); #z cases z -z #a #c
    2019                         normalize nodelta cases c normalize nodelta
    2020                         [ #H1 #Heq #H2 destruct (H2)
    2021                         | #d #H1 #Heq #H2 destruct (H2) #Hfull #H2 elim (le_to_or_lt_eq … H2)
    2022                           [ / by /
    2023                           | #H3 lapply (measure_special program «xpol,H») >Heq
    2024                             normalize nodelta #H4 @⊥
    2025                             @(absurd … (H4 H3))
    2026                             @Hfull
     1671                      [ lapply (refl ? (jump_expansion_step program (create_label_map (pi1 ?? program)) «xpol,?»))
     1672                        [ @conj [ @(proj1 ?? (proj1 ?? H)) | @(proj2 ?? H) ]
     1673                        | cases (jump_expansion_step ???) in ⊢ (???% → %); #z cases z -z #a #c
     1674                          normalize nodelta cases c normalize nodelta
     1675                          [ #H1 #Heq #H2 destruct (H2)
     1676                          | #d #H1 #Heq #H2 destruct (H2) #Hfull #H2 elim (le_to_or_lt_eq … H2)
     1677                            [ / by /
     1678                            | #H3 lapply (measure_special program «xpol,?»)
     1679                              [ @conj [ @(proj1 ?? (proj1 ?? H)) | @(proj2 ?? H) ]
     1680                              | >Heq normalize nodelta #H4 @⊥ @(absurd … (H4 H3)) @Hfull
     1681                              ]
     1682                            ]
    20271683                          ]
    20281684                        ]
    2029                       | lapply (refl ? (jump_expansion_step program (create_label_map (pi1 ?? program) xpol) «xpol,H»))
    2030                         cases (jump_expansion_step ???) in ⊢ (???% → %); #z cases z -z #a #c
    2031                         normalize nodelta cases c normalize nodelta
    2032                         [ #H1 #Heq #H2 #H3 #_ @⊥ @(absurd ?? H3) @pe_refl
    2033                         | #d #H1 #Heq #H2 #H3 @⊥ @(absurd ?? H3) @pe_refl
     1685                      | lapply (refl ? (jump_expansion_step program (create_label_map (pi1 ?? program)) «xpol,?»))
     1686                        [ @conj [ @(proj1 ?? (proj1 ?? H)) | @(proj2 ?? H) ]
     1687                        | cases (jump_expansion_step ???) in ⊢ (???% → %); #z cases z -z #a #c
     1688                          normalize nodelta cases c normalize nodelta
     1689                          [ #H1 #Heq #H2 #H3 #_ @⊥ @(absurd ?? H3) @pe_refl
     1690                          | #d #H1 #Heq #H2 #H3 @⊥ @(absurd ?? H3) @pe_refl
     1691                          ]
    20341692                        ]
    20351693                      ]
     
    20421700            ]
    20431701          ]
    2044         | #Hfull cases (jump_expansion_step program (create_label_map program Fp) «Fp,?») in ⊢ (???% → %);
     1702        | #Hfull cases (jump_expansion_step program (create_label_map program) «Fp,?») in ⊢ (???% → %);
    20451703          #x cases x -x #Gch #Gpol cases Gpol normalize nodelta
    2046           [ #H #EQ2 @⊥ @(absurd ?? H) @Hfull
     1704          [ cases daemon (* XXX will need some form of nec_plus_ultra here
     1705            #H #EQ2 @⊥ @(absurd ?? H) @Hfull *)
    20471706          | #Gp #HGp #EQ2 cases Fch
    20481707            [ normalize nodelta #i #Hi
    2049               lapply (refl ? (lookup ?? (bitvector_of_nat 16 i) (\snd Fp) 〈0,0,short_jump〉))
    2050               cases (lookup ?? (bitvector_of_nat 16 i) (\snd Fp) 〈0,0,short_jump〉) in ⊢ (???% → %);
    2051               #x cases x -x #p #a #j normalize nodelta #H
    2052               lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))) i Hi) lapply (Hfull i Hi) >H
    2053               #H2 >H2 normalize nodelta cases (lookup ?? (bitvector_of_nat 16 i) (\snd Gp) 〈0,0,short_jump〉)
    2054               #x cases x -x #p #a #j' cases j' normalize nodelta #H elim H -H #H
    2055               [1,3: @⊥ @H
    2056               |2,4: destruct (H)
    2057               |5,6: @refl
     1708              cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉))) #Hj
     1709              [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))) i Hi)
     1710                lapply (Hfull i Hi Hj) cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Fp) 〈0,short_jump〉)
     1711                #fp #fj #Hfj >Hfj normalize nodelta
     1712                cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Gp) 〈0,short_jump〉) #gp #gj
     1713                cases gj normalize nodelta
     1714                [1,2: #H cases H #H2 cases H2 destruct (H2)
     1715                |3: #_ @refl
     1716                ]
     1717              | >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))) i Hi Hj)
     1718                >(proj2 ?? (proj1 ?? (proj1 ?? HFp)) i Hi Hj) @refl
    20581719              ]
    20591720            | normalize nodelta /2 by pe_int_refl/
     
    20731734    #H destruct (H)
    20741735  |4: #np #Hnp #Sp #HSp whd in match (policy_equal ???); @dec_bounded_forall #m
    2075       cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,0,short_jump〉)
    2076       #x cases x -x #x1 #x2 #x3
    2077       cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,0,short_jump〉)
    2078       #y cases y -y #y1 #y2 #y3 normalize nodelta
     1736      cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,short_jump〉)
     1737      #x1 #x2
     1738      cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,short_jump〉)
     1739      #y1 #y2 normalize nodelta
    20791740      @dec_eq_jump_length 
    20801741  ]
    2081 ] *)
    2082 qed.
    2083 
    2084 nclude alias "arithmetics/nat.ma".
     1742]
     1743qed.
     1744
     1745include alias "arithmetics/nat.ma".
    20851746include alias "basics/logic.ma".
    2086 
    2087 check create_label_cost_map
    20881747
    20891748(* The glue between Policy and Assembly. *)
     
    20961755   let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def ?? labels x 0) in
    20971756   let instruction ≝ \fst (fetch_pseudo_instruction (\snd program) ppc) in
    2098    let next_pc ≝ \fst (sigma (add ppc (bitvector_of_nat ? 1))) in
    2099      (nat_of_bitvector … ppc ≤ |\snd program| →
    2100        next_pc = add … pc (bitvector_of_nat … (instruction_size lookup_labels sigma ppc instruction)))
    2101      
    2102       ((nat_of_bitvector … ppc < |\snd program| →
     1757   let next_pc ≝ \fst (sigma (add ? ppc (bitvector_of_nat ? 1))) in
     1758     And (nat_of_bitvector … ppc ≤ |\snd program| →
     1759       next_pc = add ? pc (bitvector_of_nat …
     1760         (instruction_size lookup_labels (λx.\fst (sigma x)) (λx.\snd (sigma x)) ppc instruction)))
     1761      (Or (nat_of_bitvector … ppc < |\snd program| →
    21031762        nat_of_bitvector … pc < nat_of_bitvector … next_pc)
    2104       ∨
    2105        (nat_of_bitvector … ppc = |\snd program| → next_pc = (zero …)))).
    2106 ≝ λprogram.
     1763       (nat_of_bitvector … ppc = |\snd program| → next_pc = (zero …)))) ≝
     1764 λprogram.
    21071765  let policy ≝ pi1 … (je_fixpoint (\snd program)) in
    21081766  match policy with
     
    21121770        〈bitvector_of_nat 16 pc,jmpeqb jl long_jump〉,?»
    21131771  ].
    2114  cases daemon
    2115 qed.
     1772 #ppc normalize nodelta cases daemon
     1773qed.
Note: See TracChangeset for help on using the changeset viewer.