Changeset 2243 for src


Ignore:
Timestamp:
Jul 24, 2012, 2:31:25 PM (8 years ago)
Author:
sacerdot
Message:

One more lemma streamlined, one to go + one to be completed.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/PolicyStep.ma

    r2242 r2243  
    44include alias "basics/logic.ma".
    55
    6 lemma not_is_jump_to_destination_of_Nome:
     6lemma not_is_jump_to_destination_of_None:
    77 ∀pi. ¬is_jump (Instruction pi) → destination_of pi = None ….
    88 * try (#x #y #H) try (#y #H) try #H cases H %
     9qed.
     10
     11lemma destination_of_None_to_is_jump_false:
     12 ∀instr. destination_of instr = None … → is_jump' instr = false.
     13 * normalize // try (#H1 #H2 #abs) try (#H1 #abs) destruct(abs)
     14qed.
     15
     16lemma destination_of_Some_to_is_jump_true:
     17 ∀instr,dst. destination_of instr = Some … dst → is_jump' instr = true.
     18 #instr #dst cases instr normalize // try (#H1 #H2 #abs) try (#H1 #abs) try #abs
     19 destruct(abs)
    920qed.
    1021
    … …  
    6576     |1: #pi normalize nodelta >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????);
    6677         #H #non_jump whd in match (jump_expansion_step_instruction ??????) in H;
    67          >not_is_jump_to_destination_of_Nome in H; normalize nodelta // ]         
     78         >not_is_jump_to_destination_of_None in H; normalize nodelta // ]         
    6879   | @bitvector_of_nat_abs [3: // | @le_S_to_le ] assumption ]]
    6980qed.
    … …  
    101112     | @bitvector_of_nat_abs try assumption @lt_O_S ]]
    102113 | @bitvector_of_nat_abs [ @lt_O_S | @prefix_ok1 | 3: @lt_to_not_eq @lt_O_S ] ]
    103 qed.
    104 
    105 lemma destination_of_None_to_is_jump_false:
    106  ∀instr. destination_of instr = None … → is_jump' instr = false.
    107  * normalize // try (#H1 #H2 #abs) try (#H1 #abs) destruct(abs)
    108 qed.
    109 
    110 lemma destination_of_Some_to_is_jump_true:
    111  ∀instr,dst. destination_of instr = Some … dst → is_jump' instr = true.
    112  #instr #dst cases instr normalize // try (#H1 #H2 #abs) try (#H1 #abs) try #abs
    113  destruct(abs)
    114114qed.
    115115
    … …  
    968968
    969969lemma jump_expansion_step8:
    970 (*
    971  program :
    972   (Σl:list labelled_instruction.S (|l|)< 2 \sup 16 ∧is_well_labelled_p l)
    973  labels :
    974   (Σlm:label_map
    975    .(∀l:identifier ASMTag
    976      .occurs_exactly_once ASMTag pseudo_instruction l program
    977       →bitvector_of_nat 16 (lookup_def ASMTag ℕ lm l O)
    978        =address_of_word_labels_code_mem program l))*)
    979  ∀old_sigma : ppc_pc_map.(*
    980   (Σpolicy:ppc_pc_map
    981    .not_jump_default program policy
    982     ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
    983                  〈O,short_jump〉)
    984      =O
    985     ∧\fst  policy
    986      =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|program|))
    987                   (\snd  policy) 〈O,short_jump〉)
    988     ∧sigma_compact_unsafe program labels policy
    989     ∧\fst  policy≤ 2 \sup 16 )*)
    990  ∀prefix : list (option Identifier×pseudo_instruction).(*
    991  x : (option Identifier×pseudo_instruction)
    992  tl : (list (option Identifier×pseudo_instruction))
    993  prf : (program=prefix@[x]@tl)
    994  acc :
    995   (Σx0:ℕ×ppc_pc_map
    996    .(let 〈added,policy〉 ≝x0 in 
    997      not_jump_default prefix policy
    998      ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
    999                   〈O,short_jump〉)
    1000       =O
    1001      ∧\fst  policy
    1002       =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
    1003                    (\snd  policy) 〈O,short_jump〉)
    1004      ∧jump_increase prefix old_sigma policy
    1005      ∧sigma_compact_unsafe prefix labels policy
    1006      ∧(sigma_jump_equal prefix old_sigma policy→added=O)
    1007      ∧(added=O→sigma_pc_equal prefix old_sigma policy)
    1008      ∧out_of_program_none prefix policy
    1009      ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
    1010                   (\snd  policy) 〈O,short_jump〉)
    1011       =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
    1012                    (\snd  old_sigma) 〈O,short_jump〉)
    1013        +added
    1014      ∧sigma_safe prefix labels added old_sigma policy))
    1015  inc_added : ℕ
    1016  inc_pc_sigma : ppc_pc_map
    1017  p : (acc≃〈inc_added,inc_pc_sigma〉)*)
     970 ∀program : list labelled_instruction.
     971 ∀labels : label_map.
     972 ∀old_sigma :
     973  Σpolicy:ppc_pc_map.sigma_compact_unsafe program labels policy ∧\fst  policy≤ 2 \sup 16.
     974 ∀prefix : list (option Identifier×pseudo_instruction).
     975 ∀x : option Identifier×pseudo_instruction.
     976 ∀tl : list (option Identifier×pseudo_instruction).
     977 ∀prf : program=prefix@[x]@tl.
     978 ∀inc_added : ℕ.
     979 ∀inc_pc_sigma : ppc_pc_map.
    1018980 ∀label : option Identifier.
    1019  ∀instr : pseudo_instruction.(*
    1020  p1 : (x≃〈label,instr〉)
    1021  add_instr ≝
    1022   match instr
    1023    in pseudo_instruction
    1024    return λ_:pseudo_instruction.(option jump_length)
    1025    with 
    1026   [Instruction (i:(preinstruction Identifier))⇒
    1027    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
    1028    (|prefix|) i
    1029   |Comment (_:String)⇒None jump_length
    1030   |Cost (_:costlabel)⇒None jump_length
    1031   |Jmp (j:Identifier)⇒
    1032    Some jump_length
    1033    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
    1034   |Call (c:Identifier)⇒
    1035    Some jump_length
    1036    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
    1037   |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
    1038  inc_pc : ℕ
    1039  inc_sigma : (BitVectorTrie (ℕ×jump_length) 16)
    1040  Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉)
    1041  old_pc : ℕ
    1042  old_length : jump_length
    1043  Holdeq :
    1044   (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd  old_sigma)
     981 ∀instr : pseudo_instruction.
     982 ∀p1 : x≃〈label,instr〉.
     983 ∀inc_pc : ℕ.
     984 ∀inc_sigma : BitVectorTrie (ℕ×jump_length) 16.
     985 ∀old_pc : ℕ.
     986 ∀old_length : jump_length.
     987 ∀Holdeq :
     988  lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd  old_sigma)
    1045989   〈O,short_jump〉
    1046    =〈old_pc,old_length〉)
    1047  Hpolicy :
    1048   (not_jump_default prefix 〈inc_pc,inc_sigma〉
    1049    ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) inc_sigma
    1050                 〈O,short_jump〉)
    1051     =O
    1052    ∧inc_pc
    1053     =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
    1054                  〈O,short_jump〉)
    1055    ∧jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉
    1056    ∧sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉
    1057    ∧(sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O)
    1058    ∧(inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉)
    1059    ∧out_of_program_none prefix 〈inc_pc,inc_sigma〉
    1060    ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
    1061                 〈O,short_jump〉)
    1062     =old_pc+inc_added
    1063    ∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉)*)
     990   =〈old_pc,old_length〉.
     991 ∀Hpolicy1 : inc_pc
     992    =\fst  (lookup … (bitvector_of_nat … (|prefix|)) inc_sigma 〈O,short_jump〉).
     993 ∀Hpolicy2: \fst  (lookup … (bitvector_of_nat … (|prefix|)) inc_sigma 〈O,short_jump〉)
     994    =old_pc+inc_added.
    1064995 ∀added : ℕ.
    1065  ∀policy : ppc_pc_map.(*
    1066  new_length : jump_length
    1067  isize : ℕ
    1068  Heq1 :
    1069   (match 
    1070    match instr
    1071     in pseudo_instruction
    1072     return λ_:pseudo_instruction.(option jump_length)
    1073     with 
    1074    [Instruction (i:(preinstruction Identifier))⇒
    1075     jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
    1076     (|prefix|) i
    1077    |Comment (_:String)⇒None jump_length
    1078    |Cost (_:costlabel)⇒None jump_length
    1079    |Jmp (j:Identifier)⇒
    1080     Some jump_length
    1081     (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
    1082    |Call (c:Identifier)⇒
    1083     Some jump_length
    1084     (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
    1085    |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
    1086     in option
    1087     return λ_0:(option jump_length).(jump_length×ℕ)
    1088     with 
     996 ∀policy : ppc_pc_map.
     997 ∀new_length : jump_length.
     998 ∀isize : ℕ.
     999 let add_instr ≝ match instr with
     1000  [ Jmp  j        ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
     1001  | Call c        ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
     1002  | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (|prefix|) i
     1003  | _             ⇒ None ?
     1004  ] in
     1005 ∀Heq1 :
     1006  match add_instr with 
    10891007   [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
    10901008   |Some (pl:jump_length)⇒
    10911009    〈max_length old_length pl,
    10921010    instruction_size_jmplen (max_length old_length pl) instr〉]
    1093    =〈new_length,isize〉)
    1094  prefix_ok1 : (S (|prefix|)< 2 \sup 16 )
    1095  prefix_ok : (|prefix|< 2 \sup 16 )
    1096  Heq2a :
    1097   (match 
    1098    match instr
    1099     in pseudo_instruction
    1100     return λ_0:pseudo_instruction.(option jump_length)
    1101     with 
    1102    [Instruction (i:(preinstruction Identifier))⇒
    1103     jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
    1104     (|prefix|) i
    1105    |Comment (_0:String)⇒None jump_length
    1106    |Cost (_0:costlabel)⇒None jump_length
    1107    |Jmp (j:Identifier)⇒
    1108     Some jump_length
    1109     (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
    1110    |Call (c:Identifier)⇒
    1111     Some jump_length
    1112     (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
    1113    |Mov (_0:[[dptr]])   (_00:Identifier)⇒None jump_length]
    1114     in option
    1115     return λ_0:(option jump_length).ℕ
    1116     with 
     1011   =〈new_length,isize〉.
     1012 ∀Heq2a :
     1013  match add_instr with
    11171014   [None⇒inc_added
    11181015   |Some (x0:jump_length)⇒
    11191016    inc_added+(isize-instruction_size_jmplen old_length instr)]
    1120    =added)
    1121  Heq2b :
    1122   (〈inc_pc+isize,
     1017   =added.
     1018 ∀Heq2b :
     1019  〈inc_pc+isize,
    11231020   insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
    11241021   〈inc_pc+isize,
    … …  
    11271024   (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
    11281025    〈inc_pc,new_length〉 inc_sigma)〉
    1129    =policy)
    1130 *)
     1026   =policy.
    11311027   \fst  (lookup (ℕ×jump_length) 16
    11321028              (bitvector_of_nat 16 (|(prefix@[〈label,instr〉])|)) (\snd  policy)
    … …  
    11361032               〈O,short_jump〉)
    11371033   +added.
    1138 cases daemon(*
    1139     <(proj2 ?? (pair_destruct ?????? Heq2)) >append_length <plus_n_Sm <plus_n_O
     1034 #program #labels #old_sigma #prefix #x #tl #prf #inc_added #inc_pc_sigma #label #instr
     1035 #p1 #inc_pc #inc_sigma #old_pc #old_length #Holdeq #Hpolicy1 #Hpolicy2 #added
     1036 #policy #new_length #isize #Heq1 #Heq2a #Heq2b
     1037    <Heq2b >append_length <plus_n_Sm <plus_n_O
    11401038    >lookup_insert_hit
    1141     <(proj1 ?? (pair_destruct ?????? Heq2)) cases instr in p1 Heq1;
    1142     [2,3,6: #x [3: #y] normalize nodelta #p1 #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
    1143       (* USE: sigma_compact_unsafe (from old_sigma) *)
    1144       lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
    1145       [1,3,5: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    1146       |2,4,6: lapply Holdeq -Holdeq
    1147         lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
    1148         cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
    1149         [1,3,5: normalize nodelta #_ #_ #abs cases abs
    1150         |2,4,6: lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
    1151           cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
    1152           [1,3,5: normalize nodelta #_ #x cases x -x #Spc #Sj normalize nodelta #_ #_ #abs cases abs
    1153           |2,4,6: #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #Holdeq #EQ normalize nodelta
    1154             #H (* USE: fst p = lookup |prefix| *)
    1155             >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
    1156             (* USE[pass]: lookup p = lookup old_sigma + added *)
    1157             >(proj2 ?? (proj1 ?? Hpolicy)) >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ;
    1158             -Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ))
    1159             >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H >prf >nth_append_second
    1160             [1,3,5: <minus_n_n >p1 whd in match (nth ????); >associative_plus
    1161               >(associative_plus pc) @plus_left_monotone >commutative_plus
    1162               @plus_right_monotone @instruction_size_irrelevant @nmk #H @H
    1163             |2,4,6: @le_n
    1164             ]
    1165           ]
    1166         ]
    1167       ]
    1168     |4,5: #x normalize nodelta #p1 #Heq1
    1169       (* USE: sigma_compact_unsafe (from old_sigma) *)
    1170       lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
    1171       [1,3: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    1172       |2,4: lapply Holdeq -Holdeq
    1173         lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
    1174         cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
    1175         [1,3: normalize nodelta #_ #_ #abs cases abs
    1176         |2,4: lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
    1177           cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
    1178           [1,3: normalize nodelta #_ #x cases x -x #Spc #Sj normalize nodelta #_ #_ #abs cases abs
    1179           |2,4: #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #Holdeq #EQ normalize nodelta
    1180             #H (* USE: fst p = lookup |prefix| *)
    1181             >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
    1182             (* USE[pass]: lookup p = lookup old_sigma + added *)
    1183             >(proj2 ?? (proj1 ?? Hpolicy)) >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ;
    1184             -Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ))
    1185             >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H >associative_plus
    1186             >(associative_plus pc) @plus_left_monotone >assoc_plus1
    1187             >(associative_plus inc_added) @plus_left_monotone >plus_minus_commutative
    1188             [1,3: >(proj2 ?? (pair_destruct ?????? EQ)) >prf >nth_append_second
    1189               [1,3: <minus_n_n whd in match (nth ????); >p1 >commutative_plus
    1190                 @minus_plus_m_m
    1191               |2,4: @le_n
    1192               ]
    1193             |2,4: <(proj2 ?? (pair_destruct ?????? Heq1)) @jump_length_le_max @I
    1194             ]
    1195           ]
    1196         ]
    1197       ]
    1198     |1: #pi cases pi
    1199       [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:
    1200         [1,2,3,6,7,24,25: #x #y
    1201         |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    1202         normalize nodelta #p1 #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
    1203         (* USE: sigma_compact_unsafe (from old_sigma) *)
    1204         lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
    1205         [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:
    1206           >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    1207         |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:
    1208           lapply Holdeq -Holdeq lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
    1209           cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
    1210           [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:
    1211             normalize nodelta #_ #_ #abs cases abs
    1212           |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:
    1213             lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
    1214             cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
    1215             [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:
    1216               normalize nodelta #_ #x cases x -x #Spc #Sj normalize nodelta #_ #_ #abs cases abs
    1217             |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:
    1218               #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #Holdeq #EQ normalize nodelta
    1219               #H (* USE: fst p = lookup |prefix| *)
    1220               >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
    1221               (* USE[pass]: lookup p = lookup old_sigma + added *)
    1222               >(proj2 ?? (proj1 ?? Hpolicy)) >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ;
    1223               -Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ))
    1224               >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H >prf >nth_append_second
    1225               [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:
    1226                 <minus_n_n >p1 whd in match (nth ????); >associative_plus
    1227                 >(associative_plus pc) @plus_left_monotone >commutative_plus
    1228                 @plus_right_monotone @instruction_size_irrelevant @nmk #H @H
    1229               |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:
    1230                 @le_n
    1231               ]
    1232             ]
    1233           ]
    1234         ]
    1235       |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] normalize nodelta #p1 #Heq1
    1236       (* USE: sigma_compact_unsafe (from old_sigma) *)
    1237         lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
    1238         [1,3,5,7,9,11,13,15,17: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    1239         |2,4,6,8,10,12,14,16,18: lapply Holdeq -Holdeq
    1240           lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
    1241           cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
    1242           [1,3,5,7,9,11,13,15,17: normalize nodelta #_ #_ #abs cases abs
    1243           |2,4,6,8,10,12,14,16,18: lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
    1244             cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
    1245             [1,3,5,7,9,11,13,15,17: normalize nodelta #_ #x cases x -x #Spc #Sj
    1246               normalize nodelta #_ #_ #abs cases abs
    1247             |2,4,6,8,10,12,14,16,18: #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j
    1248               #Holdeq #EQ normalize nodelta #H (* USE: fst p = lookup |prefix| *)
    1249               >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
    1250               (* USE[pass]: lookup p = lookup old_sigma + added *)
    1251               >(proj2 ?? (proj1 ?? Hpolicy)) >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ;
    1252               -Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ))
    1253               >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H >associative_plus
    1254               >(associative_plus pc) @plus_left_monotone >assoc_plus1
    1255               >(associative_plus inc_added) @plus_left_monotone >plus_minus_commutative
    1256               [1,3,5,7,9,11,13,15,17: >(proj2 ?? (pair_destruct ?????? EQ)) >prf
    1257                 >nth_append_second
    1258                 [1,3,5,7,9,11,13,15,17: <minus_n_n whd in match (nth ????); >p1
    1259                   >commutative_plus @minus_plus_m_m
    1260                 |2,4,6,8,10,12,14,16,18: @le_n
    1261                 ]
    1262               |2,4,6,8,10,12,14,16,18: <(proj2 ?? (pair_destruct ?????? Heq1))
    1263                 @jump_length_le_max @I
    1264               ]
    1265             ]
    1266           ]
    1267         ]
    1268       ]
    1269     ] *)
     1039    <Heq2a cases instr in p1 Heq1;
     1040    [1: #pi normalize nodelta whd in match jump_expansion_step_instruction;
     1041        normalize nodelta lapply (destination_of_None_to_is_jump_false pi)
     1042        lapply (destination_of_Some_to_is_jump_true pi)
     1043        cases (destination_of ?) normalize nodelta ]
     1044    try (#x #y #z #p1 #Heq1) try (#x #y #p1 #Heq1) try (#x #p1 #Heq1) try (#p1 #Heq1)
     1045    <(proj2 ?? (pair_destruct ?????? Heq1))
     1046    (* USE: sigma_compact_unsafe (from old_sigma) *)
     1047    lapply (proj1 ?? (pi2 ?? old_sigma) (|prefix|) ?)
     1048    [1,3,5,7,9,11,13,15: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r]
     1049    lapply Holdeq -Holdeq
     1050    inversion (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma))
     1051    [1,3,5,7,9,11,13,15: normalize nodelta #_ #_ #abs cases abs]
     1052    inversion (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma))
     1053    [1,3,5,7,9,11,13,15: normalize nodelta #_ * #Spc #Sj normalize nodelta #_ #_ #abs cases abs]
     1054    * #Spc #Sj #EQS * #pc #j #Holdeq #EQ normalize nodelta
     1055    #H (* USE: fst p = lookup |prefix| *) (*CSC: This part of the proof is repeated somewhere else*)
     1056    >Hpolicy1
     1057    (* USE[pass]: lookup p = lookup old_sigma + added *)
     1058    >Hpolicy2
     1059    [1,3,4,7:
     1060      >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ;
     1061      -Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ))
     1062      >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H >prf >nth_append_second try %
     1063      <minus_n_n >p1 whd in match (nth ????); >associative_plus
     1064      >(associative_plus pc) @plus_left_monotone >commutative_plus
     1065      @plus_right_monotone @instruction_size_irrelevant try %
     1066      whd in match is_jump; normalize nodelta >y %
     1067    |2,5,6:
     1068      >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H
     1069      >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ; #EQ
     1070      -Holdeq <(proj1 ?? (pair_destruct ?????? EQ))
     1071      >associative_plus
     1072      >(associative_plus pc) @plus_left_monotone >assoc_plus1
     1073      >(associative_plus inc_added) @plus_left_monotone >plus_minus_commutative
     1074      [1,3,5: >(proj2 ?? (pair_destruct ?????? EQ)) >prf in old_sigma; #old_sigma
     1075        >nth_append_second try %
     1076        <minus_n_n whd in match (nth ????); >p1 in old_sigma; #old_sigma
     1077        >commutative_plus @minus_plus_m_m
     1078      |*: <(proj2 ?? (pair_destruct ?????? Heq1)) @jump_length_le_max try %
     1079        whd in match is_jump; normalize nodelta >y %]]
    12701080qed.
    12711081
Note: See TracChangeset for help on using the changeset viewer.