Changeset 2548

Timestamp:

Dec 10, 2012, 2:33:40 PM (8 years ago)

Author:

tranquil

Message:

in BackEndOps?, cleaner def of be_op2
new statement of fetch_statement_sigma_commute and first part of further lemmas

Location:

src

Files:

• common/BackEndOps.ma (modified) (3 diffs)
• joint/lineariseProof.ma (modified) (7 diffs)

src/common/BackEndOps.ma

@@ -221 +221 @@
     ]
   | BVnull p1 ⇒
-    match op with
-    [ Xor ⇒
-      match a2 with
-      [ BVptr ptr2 p2 ⇒
+    match a2 with
+    [ BVptr ptr2 p2 ⇒
+      match op with
+      [ Xor ⇒
         if eqb p1 p2 then
           return 〈BVXor (None ?) (Some ? ptr2) p1, carry〉
         else
           Error … [MSG UnsupportedOp]
-      | BVnull p2 ⇒
+      | _ ⇒ Error … [MSG UnsupportedOp]
+      ]
+    | BVnull p2 ⇒
+      match op with
+      [ Xor ⇒
         if eqb p1 p2 then
           return 〈BVXor (None ?) (None ?) p1, carry〉
@@ -239 +243 @@
     ]
   | BVXor ptr1_opt ptr1_opt' p1 ⇒
-    match op with
-    [ Or ⇒
-      match a2 with
-      [ BVByte b2 ⇒
+    match a2 with
+    [ BVByte b2 ⇒
+      match op with
+      [ Or ⇒
         if eq_bv … (bv_zero …) b2 then return 〈a1, carry〉
         else Error … [MSG UnsupportedOp]
-      | BVnonzero ⇒ return 〈BVnonzero, carry〉
-      | BVXor ptr2_opt ptr2_opt' p2 ⇒
+      | _ ⇒ Error … [MSG UnsupportedOp]
+      ]
+    | BVnonzero ⇒
+      match op with
+      [ Or ⇒
+        return 〈BVnonzero, carry〉
+      | _ ⇒ Error … [MSG UnsupportedOp]
+      ]
+    | BVXor ptr2_opt ptr2_opt' p2 ⇒
+      match op with
+      [ Or ⇒
         if ((eqb p1 0 ∧ eqb p2 1) ∨ (eqb p1 1 ∧ eqb p2 0)) then
           let eq_at ≝ λp,ptr1,ptr2.
@@ -262 +275 @@
     ]
   | BVnonzero ⇒
-    match op with
-    [ Or ⇒
-      match a2 with
-      [ BVByte _ ⇒ return 〈BVnonzero, carry〉
-      | BVnonzero ⇒ return 〈BVnonzero, carry〉
-      | BVXor _ _ _ ⇒ return 〈BVnonzero, carry〉
+    match a2 with
+    [ BVByte _ ⇒
+      match op with
+      [ Or ⇒ return 〈BVnonzero, carry〉
+      | _ ⇒ Error … [MSG UnsupportedOp]
+      ]
+    | BVnonzero ⇒
+      match op with
+      [ Or ⇒ return 〈BVnonzero, carry〉
+      | _ ⇒ Error … [MSG UnsupportedOp]
+      ]
+    | BVXor _ _ _ ⇒
+      match op with
+      [ Or ⇒ return 〈BVnonzero, carry〉
       | _ ⇒ Error … [MSG UnsupportedOp]
       ]

src/joint/lineariseProof.ma

@@ -1221 +1221 @@
 normalize //
 qed.
-
+check pc_of_label
 lemma fetch_statement_sigma_commute:
   ∀p,p',graph_prog,pc,f,fn,stmt.
@@ -1229 +1229 @@
   fetch_statement (make_sem_graph_params p p') …
     (globalenv_noinit ? graph_prog) pc = return 〈f, fn,stmt〉 →
-  All ? (λlbl.well_formed_pc p p' graph_prog sigma
-      (pc_of_point (make_sem_graph_params p p') (pc_block pc) lbl))
-    (stmt_labels … stmt) ∧ 
+  All ? (λlbl.∃prf:well_formed_pc p p' graph_prog sigma
+      (pc_of_point (make_sem_graph_params p p') (pc_block pc) lbl).
+      pc_of_label (make_sem_lin_params p p') …
+          (globalenv_noinit … lin_prog)
+          (pc_block pc)
+          lbl = return sigma_pc … prf)
+    (stmt_explicit_labels … stmt) ∧ 
   match stmt with
   [  sequential s nxt ⇒
@@ -1241 +1245 @@
                       sequential (mk_lin_params p) … (step_seq … x ) it〉 ∧
           ∃prf'.
+            let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (make_sem_graph_params p p') pc nxt) prf' in 
             let nxt_pc ≝ succ_pc (make_sem_lin_params p p') (sigma_pc … pc prf) it in
+            (nxt_pc = sigma_nxt ∨
+              (fetch_statement (make_sem_lin_params p p') …
+                (globalenv_noinit … lin_prog) nxt_pc =
+                return 〈f, \fst (linearise_int_fun … fn),
+                         final (mk_lin_params p) … (GOTO … nxt)〉 ∧
+              (pc_of_label (make_sem_lin_params p p') …
+                (globalenv_noinit … lin_prog)
+                (pc_block pc)
+                nxt = return sigma_nxt)))
+        | COND a ltrue ⇒ 
+            ∃prf'.
             let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (make_sem_graph_params p p') pc nxt) prf' in 
-            (nxt_pc = sigma_nxt ∨ fetch_statement (make_sem_lin_params p p') …
-             (globalenv_noinit … lin_prog) nxt_pc =
-             return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉)
-        | COND a ltrue ⇒ 
-            (∃ prf'.
-            let nxt_pc ≝ succ_pc (make_sem_lin_params p p') (sigma_pc … pc prf) it in
-            let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (make_sem_graph_params p p') pc nxt) prf' in 
+            (let nxt_pc ≝ succ_pc (make_sem_lin_params p p') (sigma_pc … pc prf) it in
             (fetch_statement (make_sem_lin_params p p') …
             (globalenv_noinit … lin_prog) (sigma_pc … pc prf) = 
               return 〈f, \fst (linearise_int_fun … fn), 
                       sequential (mk_lin_params p) … (COND … a ltrue) it〉 ∧
-             nxt_pc = sigma_nxt)) ∨ 
-             fetch_statement (make_sem_lin_params p p') … (globalenv_noinit … lin_prog) (sigma_pc … pc prf)  
+             nxt_pc = sigma_nxt)) ∨
+            (fetch_statement (make_sem_lin_params p p') … (globalenv_noinit … lin_prog) (sigma_pc … pc prf)  
              = 
-             return 〈f, \fst (linearise_int_fun … fn), FCOND (mk_lin_params p) … I a ltrue nxt〉
+             return 〈f, \fst (linearise_int_fun … fn), FCOND (mk_lin_params p) … I a ltrue nxt〉 ∧
+            pc_of_label (make_sem_lin_params p p') …
+                (globalenv_noinit … lin_prog)
+                (pc_block pc)
+                nxt = return sigma_nxt)
          ]
     | final z ⇒   fetch_statement (make_sem_lin_params p p') … 
@@ -1277 +1291 @@
 lapply(stmt_at_sigma_commute ???????? (good graph_fun) ?? graph_stmt)
 [@lin_pt_spec|] * #H1 #H2 %
-[ -H2 @(All_mp … H1) #lab #lab_spec
+[ -H2 @(All_mp … (All_append_r H1) #lab #lab_spec
   whd in match well_formed_pc; normalize nodelta
   whd in match sigma_pc_opt; normalize nodelta >fetchfn
@@ -1409 +1423 @@
 @opt_safe_elim -H
 #res #_
-#H
+#H cases daemon (*
 #H  @('bind_inversion H) -H
 * #f #stmt
@@ -1461 +1475 @@
 
 xxxxxxxxxxxxxx
-
+*)
 qed.
 
@@ -1899 +1913 @@
  qed.
 
+lemma eval_seq_no_call_no_goto :
+ ∀p,p',graph_prog.
+ let lin_prog ≝ linearise p graph_prog in
+ ∀stack_sizes.
+ ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma.
+ ∀st,st',f,fn,stmt,nxt.no_call ?? stmt →
+ ∀prf : well_formed_state_pc … gss st.
+   fetch_statement (make_sem_lin_params p p') …
+    (globalenv_noinit ? lin_prog) (pc … (sigma_state_pc … st prf)) =
+      return 〈f, \fst (linearise_int_fun … fn),
+        sequential … (step_seq (mk_lin_params p) … stmt) it〉 →
+   eval_seq_no_pc … (ev_genv … (graph_prog_params … graph_prog stack_sizes))
+      f fn stmt st = return st' →
+ let st_pc' ≝ mk_state_pc ? st'
+  (succ_pc (make_sem_graph_params p p') …
+    (pc … st) nxt) in
+ ∀prf'.
+ succ_pc (make_sem_lin_params p p') (sigma_pc … (pc … st) (proj1 … prf)) it =
+   sigma_pc p p' graph_prog sigma
+    (succ_pc (make_sem_graph_params p p') (pc … st) nxt) prf' →
+ ∃prf''.
+ ∃taf : trace_any_any_free (lin_abstract_status p p' lin_prog stack_sizes)
+  (sigma_state_pc … gss st prf)
+  (sigma_state_pc … gss st_pc' prf'').
+ bool_to_Prop (taaf_non_empty … taf).
+#p #p' #graph_prog #stack_sizes #sigma #gss #st #st' #f #fn #stmt #nxt #stmt_no_call
+#prf #EQfetch' #EQeval #prf' #EQsucc_pc
+cases (eval_seq_no_pc_sigma_commute … gss … EQeval) [2: @(proj2 … prf)]
+#prf'' #EQeval'
+% [ @hide_prf % assumption ]
+%{(taaf_step … (taa_base …) …)} [3: % ]
+[ whd whd in ⊢ (??%?); >EQfetch' normalize nodelta
+  whd in match joint_classify_step; normalize nodelta
+  @no_call_other assumption
+| whd whd in match eval_state; normalize nodelta >EQfetch' >m_return_bind
+  whd in match eval_statement_no_pc; normalize nodelta
+  >EQeval' >m_return_bind
+  whd in match eval_statement_advance; normalize nodelta
+  >no_call_advance [2: assumption ]
+  whd in match (next ???);
+  >EQsucc_pc %
+]
+qed.
+
+lemma eval_seq_no_call_goto :
+ ∀p,p',graph_prog.
+ let lin_prog ≝ linearise p graph_prog in
+ ∀stack_sizes.
+ ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma.
+ ∀st,st',f,fn,stmt,nxt.no_call ?? stmt →
+ ∀prf : well_formed_state_pc … gss st.
+  fetch_statement (make_sem_lin_params p p') …
+    (globalenv_noinit ? lin_prog) (pc … (sigma_state_pc … st prf)) =
+      return 〈f, \fst (linearise_int_fun … fn),
+        sequential … (step_seq (mk_lin_params p) … stmt) it〉 →
+   eval_seq_no_pc … (ev_genv … (graph_prog_params … graph_prog stack_sizes))
+      f fn stmt st = return st' →
+ let st_pc' ≝ mk_state_pc ? st'
+  (succ_pc (make_sem_graph_params p p') …
+    (pc … st) nxt) in
+ (? : Prop) →
+ fetch_statement (make_sem_lin_params p p') …
+   (globalenv_noinit … lin_prog)
+     (succ_pc (make_sem_lin_params p p') (sigma_pc … (pc … st) (proj1 … prf)) it) =
+   return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉 →
+ ∃prf''.
+ ∃taf : trace_any_any_free (lin_abstract_status p p' lin_prog stack_sizes)
+  (sigma_state_pc … gss st prf)
+  (sigma_state_pc … gss st_pc' prf'').
+ bool_to_Prop (taaf_non_empty … taf).
+#p #p' #graph_prog #stack_sizes #sigma #gss #st #st' #f #fn #stmt #nxt #stmt_no_call
+#prf #EQfetch' #EQeval #prf' #EQsucc_pc
+cases (eval_seq_no_pc_sigma_commute … gss … EQeval) [2: @(proj2 … prf)]
+#prf'' #EQeval'
+% [ @hide_prf % assumption ]
+%{(taaf_step … (taa_base …) …)} [3: % ]
+[ whd whd in ⊢ (??%?); >EQfetch' normalize nodelta
+  whd in match joint_classify_step; normalize nodelta
+  @no_call_other assumption
+| whd whd in match eval_state; normalize nodelta >EQfetch' >m_return_bind
+  whd in match eval_statement_no_pc; normalize nodelta
+  >EQeval' >m_return_bind
+  whd in match eval_statement_advance; normalize nodelta
+  >no_call_advance [2: assumption ]
+  whd in match (next ???);
+  >EQsucc_pc %
+]
+qed.
+
+
+  
+
+  [ assumption
+  | assu
+ 
+  fetch_statement (make_sem_lin_params p p') …
+          (globalenv_noinit … lin_prog) (sigma_pc … pc prf) =
+              return 〈f, \fst (linearise_int_fun … fn),
+                      sequential (mk_lin_params p) … (step_seq … x ) it〉 ∧
+          ∃prf'.
+            let nxt_pc ≝  in
+            let sigma_nxt ≝  in 
+            (nxt_pc = sigma_nxt ∨ fetch_statement (make_sem_lin_params p p') …
+             (globalenv_noinit … lin_prog) nxt_pc =
+             return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉)
+
 inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
     ex1_intro: ∀ x:A. P x →  ex_Type1 A P.