Changeset 2445 for src/joint

Timestamp:

Nov 9, 2012, 11:47:57 AM (8 years ago)

Author:

piccolo

Message:

1. sigma function axiomatically defined (together with its spec). It should come from Paolo's linearise function, but there it is existentially (not sigma) quantified and Paolo's records for simulation relations are in Type and not in Prop. One of the two things need to be changed (hopefully the records...)
2. sigma extended to statuses (PC only atm)
3. some preliminary lemmas about commutation of sigma with fetching

File:

• src/joint/lineariseProof.ma (modified) (4 diffs)

src/joint/lineariseProof.ma

@@ -18 +18 @@
 include "joint/SemanticUtils.ma".
 
+definition graph_prog_params:
+  ∀p:unserialized_params. 
+  (∀F.sem_unserialized_params p F) →
+    joint_program (mk_graph_params p) →
+   prog_params
+ ≝
+ λp,p',prog.
+  (mk_prog_params
+   (make_sem_graph_params (mk_graph_params p) p')
+   prog).
+
+definition lin_prog_params:
+  ∀p:unserialized_params. 
+  (∀F.sem_unserialized_params p F) →
+    joint_program (mk_lin_params p) →
+   prog_params
+ ≝
+ λp,p',prog.
+  (mk_prog_params
+   (make_sem_lin_params (mk_lin_params p) p')
+   prog).
+    
 definition graph_abstract_status:
  ∀p:unserialized_params. 
@@ -25 +47 @@
  ≝
  λp,p',prog.
-  joint_abstract_status
-   (mk_prog_params
-    (make_sem_graph_params p p')
-    prog).
+  joint_abstract_status (graph_prog_params p p' prog).
 
 definition lin_abstract_status:
@@ -37 +56 @@
  ≝
  λp,p',prog.
-  joint_abstract_status
-   (mk_prog_params
-    (make_sem_lin_params p p')
-    prog).
+  joint_abstract_status (lin_prog_params p p' prog).
+
+(*CSC: BUG, the natural must be ≤ 2^16! *)
+(*CSC: already defined? *)
+definition pointer_of_block_and_lin_offset :
+ ∀b:block. block_region b = Code → nat → cpointer ≝
+  λb,p,n. «mk_pointer b (mk_offset (bitvector_of_nat … n)), p».
+
+definition well_formed_status:
+ ∀p,p',graph_prog.
+  ∀sigma: identifier LabelTag → option ℕ. 
+  graph_abstract_status p p' graph_prog → Prop
+ ≝
+ λp,p',graph_prog,sigma,s.
+  sigma (point_of_pointer ? (make_sem_graph_params … (mk_graph_params … p) p') (pc ? s))
+   ≠ None ….
+
+definition sigma_pc_of_status:
+ ∀p,p',graph_prog.
+  ∀sigma: identifier LabelTag → option ℕ.
+   ∀s:graph_abstract_status p p' graph_prog.
+    well_formed_status … sigma s → ℕ
+ ≝
+  λp,p',prog,sigma,s.
+   match sigma (point_of_pointer ? (make_sem_graph_params … (mk_graph_params … p) p') (pc ? s))
+   return λx. x ≠ None ? → ℕ
+   with
+   [ None ⇒ λprf.⊥
+   | Some n ⇒ λ_.n ].
+ @(absurd ?? prf) //
+qed.
+    
+definition linearise_status_fun:
+ ∀p,p',graph_prog.
+  ∀sigma: identifier LabelTag → option ℕ.
+   let lin_prog ≝ linearise ? graph_prog in
+    ∀s:graph_abstract_status p p' graph_prog.
+     well_formed_status … sigma s →
+      lin_abstract_status p p' lin_prog
+≝
+ λp,p',graph_prog,sigma,s,prf.
+  mk_state_pc ??
+   (pointer_of_block_and_lin_offset (pblock (pc ? s)) …
+    (sigma_pc_of_status … sigma … prf)).
+[2: cases (pc ??) * normalize //
+| cases daemon (* TODO *) ]
+qed.
 
 definition linearise_status_rel:
  ∀p,p',graph_prog.
+  ∀sigma: identifier LabelTag → option ℕ.
   let lin_prog ≝ linearise ? graph_prog in
    status_rel
     (graph_abstract_status p p' graph_prog)
-    (lin_abstract_status p p' lin_prog).
- cases daemon
+    (lin_abstract_status p p' lin_prog)
+ ≝ λp,p',graph_prog,sigma.mk_status_rel …
+    (λs1,s2.
+     ∃prf: well_formed_status … sigma s1.
+      s2 = linearise_status_fun p p' graph_prog sigma s1 prf) ….
+ cases daemon (* TODO *)
+qed.
+
+(*CSC: Paolo, come to the rescue*)
+axiom choose_sigma:
+  ∀p:unserialized_params. 
+  (∀F.sem_unserialized_params p F) →
+    joint_program (mk_graph_params p) →
+   identifier LabelTag → option ℕ.
+
+(*CSC: Paolo, come to the rescue*)
+axiom linearise_code_spec:
+ ∀p : unserialized_params.
+ ∀p':(∀F.sem_unserialized_params p F).
+ ∀graph_prog:joint_program (mk_graph_params p).
+ ∀graph_fun:joint_closed_internal_function (mk_graph_params p)
+                           (globals (graph_prog_params p p' graph_prog)).
+ let sigma ≝ choose_sigma p p' graph_prog in
+ let lin_fun ≝ linearise_int_fun … graph_fun in
+ let g ≝ joint_if_code ?? (pi1 … graph_fun) in
+ let c ≝ joint_if_code ?? (pi1 … lin_fun) in
+ ∀entry : (Σl.bool_to_Prop (code_has_label … g l)).
+      code_closed … c ∧
+      sigma entry = Some ? 0 ∧
+      ∀l,n.sigma l = Some ? n →
+        ∃s. lookup … g l = Some ? s ∧
+          opt_Exists ?
+            (λls.let 〈lopt, ts〉 ≝ ls in
+              opt_All ? (eq ? l) lopt ∧
+              ts = graph_to_lin_statement … s ∧
+              opt_All ?
+                (λnext.Or (sigma next = Some ? (S n))
+                (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
+                (stmt_implicit_label … s)) (nth_opt … n c). 
+
+axiom fetch_function_sigma_commute:
+ ∀p,p',graph_prog,sigma,st1.
+ ∀prf:well_formed_status ??? sigma st1.
+ let lin_prog ≝ linearise ? graph_prog in
+  fetch_function
+   (lin_prog_params p p' lin_prog)
+   (globals (lin_prog_params p p' lin_prog))
+   (ev_genv (lin_prog_params p p' lin_prog))
+   (pc (lin_prog_params p p' lin_prog)
+    (linearise_status_fun p p' graph_prog sigma st1 prf))
+ =
+  m_map …
+   (linearise_int_fun ??)
+   (fetch_function
+    (graph_prog_params p p' graph_prog)
+    (globals (graph_prog_params p p' graph_prog))
+    (ev_genv (graph_prog_params p p' graph_prog))
+    (pc (graph_prog_params p p' graph_prog) st1)).
+
+lemma stm_at_sigma_commute:
+ ∀p,p',graph_prog,graph_fun,s1.
+ let lin_prog ≝ linearise ? graph_prog in
+ let sigma ≝ choose_sigma p p' graph_prog in
+ ∀prf:well_formed_status ??? sigma s1.
+  stmt_at (lin_prog_params p p' (linearise p graph_prog))
+   (globals (lin_prog_params p p' (linearise p graph_prog)))
+   (joint_if_code (lin_prog_params p p' (linearise p graph_prog))
+    (globals (lin_prog_params p p' (linearise p graph_prog)))
+    (linearise_int_fun p (globals (graph_prog_params p p' graph_prog)) graph_fun))
+   (point_of_pointer (lin_prog_params p p' (linearise p graph_prog))
+    (lin_prog_params p p' (linearise p graph_prog))
+    (pc (lin_prog_params p p' (linearise p graph_prog))
+     (linearise_status_fun p p' graph_prog sigma s1 prf)))
+ =
+  option_map …
+   (graph_to_lin_statement …)
+   (stmt_at (graph_prog_params p p' graph_prog)
+    (globals (graph_prog_params p p' graph_prog))
+    (joint_if_code (graph_prog_params p p' graph_prog)
+     (globals (graph_prog_params p p' graph_prog)) graph_fun)
+    (point_of_pointer (graph_prog_params p p' graph_prog)
+     (graph_prog_params p p' graph_prog)
+     (pc (graph_prog_params p p' graph_prog) s1))).
+ #p #p' #graph_prog #graph_fun #s1 #prf
+ whd in match (stmt_at ????);
+ whd in match (stmt_at ????);
+
+================================
+  normalize nodelta
+
+lemma fetch_statement_sigma_commute:
+ ∀p,p',graph_prog,sigma,st1.
+ let lin_prog ≝ linearise ? graph_prog in
+  fetch_statement
+   (lin_prog_params p p' lin_prog)
+   (lin_prog_params p p' lin_prog)
+   (globals (lin_prog_params p p' lin_prog))
+   (ev_genv (lin_prog_params p p' lin_prog))
+   (pc (lin_prog_params p p' lin_prog)
+    (linearise_status_fun p p' graph_prog sigma st1))
+ =
+  m_map …
+   (λfun_stm.
+     let 〈fun,stm〉 ≝ fun_stm in
+      〈linearise_int_fun ?? fun, graph_to_lin_statement ?? stm〉)
+   (fetch_statement
+    (graph_prog_params p p' graph_prog)
+    (graph_prog_params p p' graph_prog)
+    (globals (graph_prog_params p p' graph_prog))
+    (ev_genv (graph_prog_params p p' graph_prog))
+    (pc (graph_prog_params p p' graph_prog) st1)).
+ #p #p' #graph_prog #sigma #s1
+ whd in match fetch_statement; normalize nodelta
+ >fetch_function_sigma_commute
+ cases (fetch_function ????) [2://]
+ #graph_fun whd in ⊢ (??%%);
+ whd in ⊢ (???(match % with [ _ ⇒ ? | _ ⇒ ?]));
+ >stm_at_sigma_commute
+ cases (stmt_at ????) //
 qed.
 
@@ -57 +237 @@
     (graph_abstract_status p p' graph_prog)
     (lin_abstract_status p p' lin_prog) ≝
- λp,p',graph_prog. mk_status_simulation … (linearise_status_rel p p' graph_prog) ….
- cases daemon
-qed.
+ λp,p',graph_prog.
+  let sigma ≝ choose_sigma p p' graph_prog in
+   mk_status_simulation … (linearise_status_rel p p' graph_prog sigma) ….
+#st1 #cl #st1' #st2 #move_st1_st1' #rel_st1_st2 #classified_st1_cl
+cases cl in classified_st1_cl; -cl #classified_st1_cl whd
+[4:
+ whd in rel_st1_st2; >rel_st1_st2 -st2
+ whd in move_st1_st1';
+ letin lin_prog ≝ (linearise ? graph_prog)
+ letin st2' ≝ (eval_state (globals (lin_prog_params p p' lin_prog)) …
+               (ev_genv (lin_prog_params p p' lin_prog))
+               (linearise_status_fun … sigma st1))
+ whd in st2';
+ whd in match (fetch_statement ?????) in st2';
+ >fetch_function_sigma_commute in st2';
+ whd in match (fetch_function ????) in st2';
+ XXX
+ check fetch_statement
+ CSC
+ %{}
+
+whd in classified_st1_cl;
+whd in classified_st1_cl:(??%?);
+inversion (fetch_statement ?????) in classified_st1_cl;
+
+<classified_st1_cl -cl 
+whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ] ?);
+inversion (fetch_statement ?????)
+
+inversion (fetch_statement ?????)
+qed.