Changeset 1482 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Nov 2, 2011, 2:26:26 PM (8 years ago)
Author:
sacerdot
Message:
  1. very long standing conflict committed (but don't ask me what the stuff I added is used for...)
  2. ported to new automation (which seems to be slower on one example)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r1479 r1482  
    11211121qed.
    11221122
     1123axiom fetch_pseudo_instruction_split:
     1124 ∀instr_list,ppc.
     1125  ∃pre,suff,lbl.
     1126   (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc)〉]) @ suff = instr_list.
     1127
     1128lemma sigma00_append:
     1129 ∀instr_list,jump_expansion,l1,l2,acc.
     1130  sigma00 instr_list jump_expansion (l1@l2) acc =
     1131   sigma00 instr_list jump_expansion
     1132    l2 (sigma00 instr_list jump_expansion l1 acc).
     1133 whd in match sigma00; normalize nodelta;
     1134 #instr_list #jump_expansion #l1 #l2 #acc @foldl_append
     1135qed.
     1136
     1137lemma sigma00_strict:
     1138 ∀instr_list,jump_expansion,l,acc. acc = None ? →
     1139  sigma00 instr_list jump_expansion l acc = None ….
     1140 #instr_list #jump_expansion #l elim l
     1141  [ #acc #H >H %
     1142  | #hd #tl #IH #acc #H >H change with (sigma00 ?? tl ? = ?) @IH % ]
     1143qed.
     1144
     1145lemma policy_ok_prefix_ok:
     1146 ∀program.∀pol:policy program.∀suffix,prefix.
     1147  prefix@suffix = \snd program →
     1148   sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) ≠ None ….
     1149 * #preamble #instr_list #pol #suffix #prefix #prf whd in prf:(???%);
     1150 generalize in match (sig2 ?? pol) whd in prf:(???%) <prf in pol; #pol
     1151 whd in match policy_ok; whd in match sigma_safe; whd in match sigma0
     1152 normalize nodelta >sigma00_append
     1153 cases (sigma00 ?? prefix ?)
     1154  [2: #x #_ % #abs destruct(abs)
     1155  | * #abs @⊥ @abs >sigma00_strict % ]
     1156qed.
     1157
     1158lemma policy_ok_prefix_hd_ok:
     1159 ∀program.∀pol:policy program.∀suffix,hd,prefix,ppc_pc_map.
     1160  (prefix@[hd])@suffix = \snd program →
     1161   Some ? ppc_pc_map = sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) →
     1162    let 〈ppc,pc_map〉 ≝ ppc_pc_map in
     1163    let 〈program_counter, sigma_map〉 ≝ pc_map in
     1164    let 〈label, i〉 ≝ hd in
     1165     construct_costs_safe program pol ppc program_counter (Stub …) i ≠ None ….
     1166 * #preamble #instr_list #pol #suffix #hd #prefix #ppc_pc_map #EQ1 #EQ2
     1167 generalize in match (policy_ok_prefix_ok 〈preamble,instr_list〉 pol suffix
     1168  (prefix@[hd]) EQ1) in ⊢ ? >sigma00_append <EQ2 whd in ⊢ (?(??%?) → ?)
     1169 @pair_elim' #ppc #pc_map #EQ3 normalize nodelta
     1170 @pair_elim' #pc #map #EQ4 normalize nodelta
     1171 @pair_elim' #l' #i' #EQ5 normalize nodelta
     1172 cases (construct_costs_safe ??????) normalize
     1173  [* #abs @⊥ @abs % | #X #_ % #abs destruct(abs)]
     1174qed.
     1175
    11231176definition expand_pseudo_instruction:
    11241177 ∀program:pseudo_assembly_program.∀pol: policy program.
     
    11331186    [ None ⇒ let dummy ≝ [ ] in dummy
    11341187    | Some res ⇒ res ].
    1135  [ cases daemon
     1188 [ @⊥ whd in p:(??%??);
     1189   generalize in match (sig2 ?? pol) whd in ⊢ (% → ?)
     1190   whd in ⊢ (?(??%?) → ?) change in ⊢ (?(??(match % with [_ ⇒ ? | _ ⇒ ?])?) → ?) with (sigma00 ????)
     1191   generalize in match (refl … (sigma00 program pol (\snd program) (Some ? 〈O,〈O,Stub (BitVector 16) 16〉〉)))
     1192   cases (sigma00 ????) in ⊢ (??%? → %) normalize nodelta [#_ * #abs @abs %]
     1193   #res #K
     1194   cases (fetch_pseudo_instruction_split (\snd program) ppc) #pre * #suff * #lbl #EQ1
     1195   generalize in match (policy_ok_prefix_hd_ok program pol … EQ1 ?) in ⊢ ?
     1196   cases daemon (* CSC: XXXXXXXX Ero qui
     1197   
     1198    [3: @policy_ok_prefix_ok ]
     1199    | sigma00 program pol pre
     1200
     1201
     1202
     1203   QUA USARE LEMMA policy_ok_prefix_hd_ok combinato a lemma da fare che
     1204   fetch ppc = hd sse program = pre @ [hd] @ tl e |pre| = ppc
     1205   per concludere construct_costs_safe ≠ None *)
    11361206 | >p %]
    11371207qed.
     
    12111281 λprogram,pol,ppc,pc,costs,i. eject … (construct_costs' program pol ppc pc costs i).
    12121282
     1283(*
     1284axiom suffix_of: ∀A:Type[0]. ∀l,prefix:list A. list A.
     1285axiom suffix_of_ok: ∀A,l,prefix. prefix @ suffix_of A l prefix = l.
     1286
     1287axiom foldl_strong_step:
     1288 ∀A:Type[0].
     1289  ∀P: list A → Type[0].
     1290   ∀l: list A.
     1291    ∀H: ∀prefix,hd,tl. l =  prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]).
     1292     ∀acc: P [ ].
     1293      ∀Q: ∀prefix. P prefix → Prop.
     1294       ∀HQ: ∀prefix,hd,tl.∀prf: l = prefix @ [hd] @ tl.
     1295        ∀acc: P prefix. Q prefix acc → Q (prefix @ [hd]) (H prefix hd tl prf acc).
     1296       Q [ ] acc →
     1297        Q l (foldl_strong A P l H acc).
     1298(*
     1299 #A #P #l #H #acc #Q #HQ #Hacc normalize;
     1300 generalize in match
     1301  (foldl_strong ?
     1302   (λpre. Q pre (foldl_strong_internal A P l (suffix_of A l pre) ? [ ] pre acc ?))
     1303   l ? Hacc)
     1304 [3: >suffix_of_ok % | 2: #prefix #hd #tl #EQ @(H prefix hd (tl@suffix_of A l pre) EQ) ]
     1305 [2: #prefix #hd #tl #prf #X whd in ⊢ (??%)
     1306 #K
     1307
     1308 generalize in match
     1309  (foldl_strong ?
     1310   (λpre. Q pre (foldl_strong_internal A P l H pre (suffix_of A l pre) acc (suffix_of_ok A l pre))))
     1311 [2: @H
     1312*)
     1313
     1314axiom foldl_elim:
     1315 ∀A:Type[0].
     1316  ∀B: Type[0].
     1317   ∀H: A → B → A.
     1318    ∀acc: A.
     1319     ∀l: list B.
     1320      ∀Q: A → Prop.
     1321       (∀acc:A.∀b:B. Q acc → Q (H acc b)) →
     1322         Q acc →
     1323          Q (foldl A B H acc l).
     1324*)
     1325
    12131326lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b.
    12141327 #A #a #b #EQ destruct //
    1215 qed.
    1216 
    1217 lemma sigma00_strict:
    1218  ∀instr_list,jump_expansion,l,acc. acc = None ? →
    1219   sigma00 instr_list jump_expansion l acc = None ….
    1220  #instr_list #jump_expansion #l elim l
    1221   [ #acc #H >H %
    1222   | #hd #tl #IH #acc #H >H change with (sigma00 ?? tl ? = ?) @IH % ]
    1223 qed.
    1224 
    1225 lemma sigma00_append:
    1226  ∀instr_list,jump_expansion,l1,l2,acc.
    1227   sigma00 instr_list jump_expansion (l1@l2) acc =
    1228    sigma00 instr_list jump_expansion
    1229     l2 (sigma00 instr_list jump_expansion l1 acc).
    1230  whd in match sigma00; normalize nodelta;
    1231  #instr_list #jump_expansion #l1 #l2 #acc @foldl_append
    1232 qed.
    1233 
    1234 lemma policy_ok_prefix_ok:
    1235  ∀program.∀pol:policy program.∀suffix,prefix.
    1236   prefix@suffix = \snd program →
    1237    sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) ≠ None ….
    1238  * #preamble #instr_list #pol #suffix #prefix #prf whd in prf:(???%);
    1239  generalize in match (sig2 ?? pol) whd in prf:(???%) <prf in pol; #pol
    1240  whd in match policy_ok; whd in match sigma_safe; whd in match sigma0
    1241  normalize nodelta >sigma00_append
    1242  cases (sigma00 ?? prefix ?)
    1243   [2: #x #_ % #abs destruct(abs)
    1244   | * #abs @⊥ @abs >sigma00_strict % ]
    1245 qed.
    1246 
    1247 lemma policy_ok_prefix_hd_ok:
    1248  ∀program.∀pol:policy program.∀suffix,hd,prefix,ppc_pc_map.
    1249   (prefix@[hd])@suffix = \snd program →
    1250    Some ? ppc_pc_map = sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) →
    1251     let 〈ppc,pc_map〉 ≝ ppc_pc_map in
    1252     let 〈program_counter, sigma_map〉 ≝ pc_map in
    1253     let 〈label, i〉 ≝ hd in
    1254      construct_costs_safe program pol ppc program_counter (Stub …) i ≠ None ….
    1255  * #preamble #instr_list #pol #suffix #hd #prefix #ppc_pc_map #EQ1 #EQ2
    1256  generalize in match (policy_ok_prefix_ok 〈preamble,instr_list〉 pol suffix
    1257   (prefix@[hd]) EQ1) in ⊢ ? >sigma00_append <EQ2 whd in ⊢ (?(??%?) → ?)
    1258  @pair_elim' #ppc #pc_map #EQ3 normalize nodelta
    1259  @pair_elim' #pc #map #EQ4 normalize nodelta
    1260  @pair_elim' #l' #i' #EQ5 normalize nodelta
    1261  cases (construct_costs_safe ??????) normalize
    1262   [* #abs @⊥ @abs % | #X #_ % #abs destruct(abs)]
    12631328qed.
    12641329
     
    13521417        [ #EQ #_ <(eq_bv_eq … EQ) >lookup_insert_hit >address_of_word_labels_code_mem_Some_hit
    13531418          <IH0 [@IHn1 | <(eq_bv_eq … EQ) in H #H @H]
    1354         | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: -IHn1; /2/]
     1419        | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: -IHn1; (*Andrea:XXXX used to work /2/*)>eq_bv_sym >EQ // ]
    13551420          <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 -IHn1; //]]]
    13561421 |3: whd % [% [%]] // [>sigma_0//] #id normalize in ⊢ (% → ?) #abs @⊥ //
Note: See TracChangeset for help on using the changeset viewer.