Changeset 1482 for src/ASM/Assembly.ma

Timestamp:

Nov 2, 2011, 2:26:26 PM (9 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:

• src/ASM/Assembly.ma (modified) (4 diffs)

src/ASM/Assembly.ma

@@ -1121 +1121 @@
 qed.
 
+axiom fetch_pseudo_instruction_split:
+ ∀instr_list,ppc.
+  ∃pre,suff,lbl.
+   (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc)〉]) @ suff = instr_list.
+
+lemma sigma00_append:
+ ∀instr_list,jump_expansion,l1,l2,acc.
+  sigma00 instr_list jump_expansion (l1@l2) acc =
+   sigma00 instr_list jump_expansion
+    l2 (sigma00 instr_list jump_expansion l1 acc).
+ whd in match sigma00; normalize nodelta;
+ #instr_list #jump_expansion #l1 #l2 #acc @foldl_append
+qed.
+
+lemma sigma00_strict:
+ ∀instr_list,jump_expansion,l,acc. acc = None ? →
+  sigma00 instr_list jump_expansion l acc = None ….
+ #instr_list #jump_expansion #l elim l
+  [ #acc #H >H %
+  | #hd #tl #IH #acc #H >H change with (sigma00 ?? tl ? = ?) @IH % ]
+qed.
+
+lemma policy_ok_prefix_ok:
+ ∀program.∀pol:policy program.∀suffix,prefix.
+  prefix@suffix = \snd program →
+   sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) ≠ None ….
+ * #preamble #instr_list #pol #suffix #prefix #prf whd in prf:(???%);
+ generalize in match (sig2 ?? pol) whd in prf:(???%) <prf in pol; #pol
+ whd in match policy_ok; whd in match sigma_safe; whd in match sigma0
+ normalize nodelta >sigma00_append
+ cases (sigma00 ?? prefix ?)
+  [2: #x #_ % #abs destruct(abs)
+  | * #abs @⊥ @abs >sigma00_strict % ]
+qed.
+
+lemma policy_ok_prefix_hd_ok:
+ ∀program.∀pol:policy program.∀suffix,hd,prefix,ppc_pc_map.
+  (prefix@[hd])@suffix = \snd program →
+   Some ? ppc_pc_map = sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) →
+    let 〈ppc,pc_map〉 ≝ ppc_pc_map in
+    let 〈program_counter, sigma_map〉 ≝ pc_map in
+    let 〈label, i〉 ≝ hd in
+     construct_costs_safe program pol ppc program_counter (Stub …) i ≠ None ….
+ * #preamble #instr_list #pol #suffix #hd #prefix #ppc_pc_map #EQ1 #EQ2
+ generalize in match (policy_ok_prefix_ok 〈preamble,instr_list〉 pol suffix
+  (prefix@[hd]) EQ1) in ⊢ ? >sigma00_append <EQ2 whd in ⊢ (?(??%?) → ?)
+ @pair_elim' #ppc #pc_map #EQ3 normalize nodelta
+ @pair_elim' #pc #map #EQ4 normalize nodelta
+ @pair_elim' #l' #i' #EQ5 normalize nodelta
+ cases (construct_costs_safe ??????) normalize
+  [* #abs @⊥ @abs % | #X #_ % #abs destruct(abs)]
+qed.
+
 definition expand_pseudo_instruction:
  ∀program:pseudo_assembly_program.∀pol: policy program.
@@ -1133 +1186 @@
     [ None ⇒ let dummy ≝ [ ] in dummy
     | Some res ⇒ res ].
- [ cases daemon
+ [ @⊥ whd in p:(??%??);
+   generalize in match (sig2 ?? pol) whd in ⊢ (% → ?)
+   whd in ⊢ (?(??%?) → ?) change in ⊢ (?(??(match % with [_ ⇒ ? | _ ⇒ ?])?) → ?) with (sigma00 ????)
+   generalize in match (refl … (sigma00 program pol (\snd program) (Some ? 〈O,〈O,Stub (BitVector 16) 16〉〉)))
+   cases (sigma00 ????) in ⊢ (??%? → %) normalize nodelta [#_ * #abs @abs %]
+   #res #K
+   cases (fetch_pseudo_instruction_split (\snd program) ppc) #pre * #suff * #lbl #EQ1
+   generalize in match (policy_ok_prefix_hd_ok program pol … EQ1 ?) in ⊢ ?
+   cases daemon (* CSC: XXXXXXXX Ero qui
+   
+    [3: @policy_ok_prefix_ok ]
+    | sigma00 program pol pre
+
+
+
+   QUA USARE LEMMA policy_ok_prefix_hd_ok combinato a lemma da fare che
+   fetch ppc = hd sse program = pre @ [hd] @ tl e |pre| = ppc
+   per concludere construct_costs_safe ≠ None *)
  | >p %]
 qed.
@@ -1211 +1281 @@
  λprogram,pol,ppc,pc,costs,i. eject … (construct_costs' program pol ppc pc costs i).
 
+(*
+axiom suffix_of: ∀A:Type[0]. ∀l,prefix:list A. list A.
+axiom suffix_of_ok: ∀A,l,prefix. prefix @ suffix_of A l prefix = l.
+
+axiom foldl_strong_step:
+ ∀A:Type[0].
+  ∀P: list A → Type[0].
+   ∀l: list A.
+    ∀H: ∀prefix,hd,tl. l =  prefix @ [hd] @ tl → P prefix → P (prefix @ [hd]).
+     ∀acc: P [ ].
+      ∀Q: ∀prefix. P prefix → Prop.
+       ∀HQ: ∀prefix,hd,tl.∀prf: l = prefix @ [hd] @ tl.
+        ∀acc: P prefix. Q prefix acc → Q (prefix @ [hd]) (H prefix hd tl prf acc).
+       Q [ ] acc →
+        Q l (foldl_strong A P l H acc).
+(*
+ #A #P #l #H #acc #Q #HQ #Hacc normalize;
+ generalize in match
+  (foldl_strong ?
+   (λpre. Q pre (foldl_strong_internal A P l (suffix_of A l pre) ? [ ] pre acc ?))
+   l ? Hacc)
+ [3: >suffix_of_ok % | 2: #prefix #hd #tl #EQ @(H prefix hd (tl@suffix_of A l pre) EQ) ]
+ [2: #prefix #hd #tl #prf #X whd in ⊢ (??%) 
+ #K 
+
+ generalize in match
+  (foldl_strong ?
+   (λpre. Q pre (foldl_strong_internal A P l H pre (suffix_of A l pre) acc (suffix_of_ok A l pre))))
+ [2: @H
+*)
+
+axiom foldl_elim:
+ ∀A:Type[0].
+  ∀B: Type[0].
+   ∀H: A → B → A.
+    ∀acc: A.
+     ∀l: list B.
+      ∀Q: A → Prop.
+       (∀acc:A.∀b:B. Q acc → Q (H acc b)) →
+         Q acc →
+          Q (foldl A B H acc l).
+*)
+
 lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b.
  #A #a #b #EQ destruct //
-qed.
-
-lemma sigma00_strict:
- ∀instr_list,jump_expansion,l,acc. acc = None ? →
-  sigma00 instr_list jump_expansion l acc = None ….
- #instr_list #jump_expansion #l elim l
-  [ #acc #H >H %
-  | #hd #tl #IH #acc #H >H change with (sigma00 ?? tl ? = ?) @IH % ]
-qed.
-
-lemma sigma00_append:
- ∀instr_list,jump_expansion,l1,l2,acc.
-  sigma00 instr_list jump_expansion (l1@l2) acc =
-   sigma00 instr_list jump_expansion
-    l2 (sigma00 instr_list jump_expansion l1 acc).
- whd in match sigma00; normalize nodelta;
- #instr_list #jump_expansion #l1 #l2 #acc @foldl_append
-qed.
-
-lemma policy_ok_prefix_ok:
- ∀program.∀pol:policy program.∀suffix,prefix.
-  prefix@suffix = \snd program →
-   sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) ≠ None ….
- * #preamble #instr_list #pol #suffix #prefix #prf whd in prf:(???%);
- generalize in match (sig2 ?? pol) whd in prf:(???%) <prf in pol; #pol
- whd in match policy_ok; whd in match sigma_safe; whd in match sigma0
- normalize nodelta >sigma00_append
- cases (sigma00 ?? prefix ?)
-  [2: #x #_ % #abs destruct(abs)
-  | * #abs @⊥ @abs >sigma00_strict % ]
-qed.
-
-lemma policy_ok_prefix_hd_ok:
- ∀program.∀pol:policy program.∀suffix,hd,prefix,ppc_pc_map.
-  (prefix@[hd])@suffix = \snd program →
-   Some ? ppc_pc_map = sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) →
-    let 〈ppc,pc_map〉 ≝ ppc_pc_map in
-    let 〈program_counter, sigma_map〉 ≝ pc_map in
-    let 〈label, i〉 ≝ hd in
-     construct_costs_safe program pol ppc program_counter (Stub …) i ≠ None ….
- * #preamble #instr_list #pol #suffix #hd #prefix #ppc_pc_map #EQ1 #EQ2
- generalize in match (policy_ok_prefix_ok 〈preamble,instr_list〉 pol suffix
-  (prefix@[hd]) EQ1) in ⊢ ? >sigma00_append <EQ2 whd in ⊢ (?(??%?) → ?)
- @pair_elim' #ppc #pc_map #EQ3 normalize nodelta
- @pair_elim' #pc #map #EQ4 normalize nodelta
- @pair_elim' #l' #i' #EQ5 normalize nodelta
- cases (construct_costs_safe ??????) normalize
-  [* #abs @⊥ @abs % | #X #_ % #abs destruct(abs)]
 qed.
 
@@ -1352 +1417 @@
         [ #EQ #_ <(eq_bv_eq … EQ) >lookup_insert_hit >address_of_word_labels_code_mem_Some_hit
           <IH0 [@IHn1 | <(eq_bv_eq … EQ) in H #H @H]
-        | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: -IHn1; /2/]
+        | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: -IHn1; (*Andrea:XXXX used to work /2/*)>eq_bv_sym >EQ // ]
           <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 -IHn1; //]]]
  |3: whd % [% [%]] // [>sigma_0//] #id normalize in ⊢ (% → ?) #abs @⊥ //