Making program logic formulas memory-agnostic

src/ecAst.mli

@@ -201,80 +201,214 @@ and f_node =
 
   | Fpr of pr (* hr *)
 
+(* We use the alert system for privacy because we want to 
+   permit access in *some* instances, and the other fields are fine *)
 and eagerF = {
+  eg_ml : memory;
+  eg_mr : memory;
   eg_pr : form;
+  (*[@alert priv_pl "Use the accessor function `eg_pr` instead of the field"]*)
   eg_sl : stmt;  (* No local program variables *)
   eg_fl : EcPath.xpath;
   eg_fr : EcPath.xpath;
   eg_sr : stmt;  (* No local program variables *)
   eg_po : form
+  (*[@alert priv_pl "Use the accessor function `es_po` instead of the field"]*)
 }
 
 and equivF = {
+  ef_ml : memory;
+  ef_mr : memory;
   ef_pr : form;
+  (*[@alert priv_pl "Use the accessor function `ef_pr` instead of the field"]*)
   ef_fl : EcPath.xpath;
   ef_fr : EcPath.xpath;
   ef_po : form;
+  (*[@alert priv_pl "Use the accessor function `ef_po` instead of the field"]*)
 }
 
 and equivS = {
   es_ml  : memenv;
   es_mr  : memenv;
   es_pr  : form;
+  (*[@alert priv_pl "Use the accessor function `es_pr` instead of the field"]*)
   es_sl  : stmt;
   es_sr  : stmt;
-  es_po  : form; }
+  es_po  : form;
+  (*[@alert priv_pl "Use the accessor function `es_po` instead of the field"]*)
+}
 
 and sHoareF = {
+  hf_m : memory;
   hf_pr : form;
+  [@alert priv_pl "Use the accessor function `hf_pr` instead of the field"]
   hf_f  : EcPath.xpath;
   hf_po : form;
+  [@alert priv_pl "Use the accessor function `hf_pr` instead of the field"]
 }
 
 and sHoareS = {
   hs_m  : memenv;
   hs_pr : form;
+  (*[@alert priv_pl "Use the accessor function `hs_pr` instead of the field"]*)
   hs_s  : stmt;
-  hs_po : form; }
+  hs_po : form;
+  (*[@alert priv_pl "Use the accessor function `hs_po` instead of the field"]*)
+}
 
 
 and eHoareF = {
+  ehf_m  : memory;
   ehf_pr  : form;
+  (*[@alert priv_pl "Use the accessor function `ehf_pr` instead of the field"]*)
   ehf_f   : EcPath.xpath;
   ehf_po  : form;
+  (*[@alert priv_pl "Use the accessor function `ehf_po` instead of the field"]*)
 }
 
 and eHoareS = {
   ehs_m   : memenv;
   ehs_pr  : form;
+  (*[@alert priv_pl "Use the accessor function `ehs_pr` instead of the field"]*)
   ehs_s   : stmt;
   ehs_po  : form;
+  (*[@alert priv_pl "Use the accessor function `ehs_po` instead of the field"]*)
 }
 
 and bdHoareF = {
+  bhf_m   : memory;
   bhf_pr  : form;
+  (*[@alert priv_pl "Use the accessor function `bhf_pr` instead of the field"]*)
   bhf_f   : EcPath.xpath;
   bhf_po  : form;
+  (*[@alert priv_pl "Use the accessor function `bhf_po` instead of the field"]*)
   bhf_cmp : hoarecmp;
   bhf_bd  : form;
 }
 
 and bdHoareS = {
   bhs_m   : memenv;
   bhs_pr  : form;
+  (*[@alert priv_pl "Use the accessor function `bhs_pr` instead of the field"]*)
   bhs_s   : stmt;
   bhs_po  : form;
+  (*[@alert priv_pl "Use the accessor function `bhs_po` instead of the field"]*)
   bhs_cmp : hoarecmp;
   bhs_bd  : form;
 }
 
+and ss_inv = {
+  m   : memory;
+  inv : form;
+}
+
 and pr = {
   pr_mem   : memory;
   pr_fun   : EcPath.xpath;
   pr_args  : form;
-  pr_event : form;
+  pr_event : ss_inv;
+}
+
+
+val map_ss_inv : ?m:memory -> (form list -> form) -> ss_inv list -> ss_inv
+val map_ss_inv1 : (form -> form) -> ss_inv -> ss_inv
+val map_ss_inv2 : (form -> form -> form) -> ss_inv -> ss_inv -> ss_inv
+val map_ss_inv3 : (form -> form -> form -> form) -> ss_inv -> ss_inv -> ss_inv -> ss_inv
+
+val map_ss_inv_destr2 : (form -> form * form) -> ss_inv -> ss_inv * ss_inv
+val map_ss_inv_destr3 : (form -> form * form * form) -> ss_inv -> ss_inv * ss_inv * ss_inv
+
+type ts_inv = {
+  ml  : memory;
+  mr  : memory;
+  inv : form;
 }
 
+val map_ts_inv : ?ml:memory -> ?mr:memory -> (form list -> form) -> ts_inv list -> ts_inv
+val map_ts_inv1 : (form -> form) -> ts_inv -> ts_inv
+val map_ts_inv2 : (form -> form -> form) -> ts_inv -> ts_inv -> ts_inv
+val map_ts_inv3 : (form -> form -> form -> form) -> ts_inv -> ts_inv -> ts_inv -> ts_inv
+
+val map_ts_inv_left : (ss_inv list -> ss_inv) -> ts_inv list -> ts_inv
+val map_ts_inv_left1 : (ss_inv -> ss_inv) -> ts_inv -> ts_inv
+val map_ts_inv_left2 : (ss_inv -> ss_inv -> ss_inv) -> ts_inv -> ts_inv -> ts_inv
+val map_ts_inv_left3 : (ss_inv -> ss_inv -> ss_inv -> ss_inv) -> 
+    ts_inv -> ts_inv -> ts_inv -> ts_inv
+
+val map_ts_inv_right : (ss_inv list -> ss_inv) -> ts_inv list -> ts_inv
+val map_ts_inv_right1 : (ss_inv -> ss_inv) -> ts_inv -> ts_inv
+val map_ts_inv_right2 : (ss_inv -> ss_inv -> ss_inv) -> ts_inv -> ts_inv -> ts_inv
+val map_ts_inv_right3 : (ss_inv -> ss_inv -> ss_inv -> ss_inv) -> 
+    ts_inv -> ts_inv -> ts_inv -> ts_inv
+
+val map_ts_inv_destr2 : (form -> form * form) -> ts_inv -> ts_inv * ts_inv
+val map_ts_inv_destr3 : (form -> form * form * form) -> ts_inv -> ts_inv * ts_inv * ts_inv
+
+(* -------------------------------------------------------------------- *)
+(* Lowering tactics                                                    *)
+(* -------------------------------------------------------------------- *)
+
+val ts_inv_lower_left : (ss_inv list -> form) -> ts_inv list -> ss_inv
+val ts_inv_lower_left1 : (ss_inv -> form) -> ts_inv -> ss_inv
+val ts_inv_lower_left2 : (ss_inv -> ss_inv -> form) -> ts_inv -> ts_inv -> ss_inv
+val ts_inv_lower_left3 : (ss_inv -> ss_inv -> ss_inv -> form) -> 
+    ts_inv -> ts_inv -> ts_inv -> ss_inv
+
+val ts_inv_lower_right : (ss_inv list -> form) -> ts_inv list -> ss_inv
+val ts_inv_lower_right1 : (ss_inv -> form) -> ts_inv -> ss_inv
+val ts_inv_lower_right2 : (ss_inv -> ss_inv -> form) -> ts_inv -> ts_inv -> ss_inv
+val ts_inv_lower_right3 : (ss_inv -> ss_inv -> ss_inv -> form) -> 
+    ts_inv -> ts_inv -> ts_inv -> ss_inv
+
+(* -------------------------------------------------------------------- *)
+(* Invariants                                                          *)
+(* -------------------------------------------------------------------- *)
+
+type inv =
+  | Inv_ss of ss_inv
+  | Inv_ts of ts_inv
+
+val inv_of_inv : inv -> form
+
+val lift_ss_inv : (ss_inv -> 'a) -> inv -> 'a
+val lift_ss_inv2 : (ss_inv -> ss_inv -> 'a) -> inv -> inv -> 'a
+val lift_ss_inv3 : (ss_inv -> ss_inv -> ss_inv -> 'a) -> inv -> inv -> inv -> 'a
+val lift_ts_inv : (ts_inv -> 'a) -> inv -> 'a
+val lift_ts_inv2 : (ts_inv -> ts_inv -> 'a) -> inv -> inv -> 'a
+val lift_inv_adapter : (form -> 'a) -> inv -> 'a
+val lift_inv_adapter2 : (form -> form -> 'a) -> inv -> inv -> 'a
+
+val ss_inv_generalize_left : ss_inv -> memory -> ts_inv
+val ss_inv_generalize_right : ss_inv -> memory -> ts_inv
+
+val map_inv : (form list -> form) -> inv list -> inv
+val map_inv1 : (form -> form) -> inv -> inv
+val map_inv2 : (form -> form -> form) -> inv -> inv -> inv
+val map_inv3 : (form -> form -> form -> form) -> inv -> inv -> inv -> inv
+
+val eg_pr : eagerF -> ts_inv
+val eg_po : eagerF -> ts_inv
+val ef_pr : equivF -> ts_inv
+val ef_po : equivF -> ts_inv
+val es_pr : equivS -> ts_inv
+val es_po : equivS -> ts_inv
+val hf_pr : sHoareF -> ss_inv
+val hf_po : sHoareF -> ss_inv
+val hs_pr : sHoareS -> ss_inv
+val hs_po : sHoareS -> ss_inv
+val ehf_pr : eHoareF -> ss_inv
+val ehf_po : eHoareF -> ss_inv
+val ehs_pr : eHoareS -> ss_inv
+val ehs_po : eHoareS -> ss_inv
+val bhf_pr : bdHoareF -> ss_inv
+val bhf_po : bdHoareF -> ss_inv
+val bhf_bd : bdHoareF -> ss_inv
+val bhs_pr : bdHoareS -> ss_inv
+val bhs_po : bdHoareS -> ss_inv
+val bhs_bd : bdHoareS -> ss_inv
+
+(* -------------------------------------------------------------------- *)
+
 type 'a equality = 'a -> 'a -> bool
 type 'a hash = 'a -> int
 type 'a fv   = 'a -> int EcIdent.Mid.t

src/ecCallbyValue.ml

@@ -7,6 +7,7 @@ open EcEnv
 open EcFol
 open EcReduction
 open EcBaseLogic
+open EcMemory
 module BI = EcBigInt
 
 (* -------------------------------------------------------------------- *)
@@ -297,7 +298,7 @@ and try_reduce_fixdef
             subst bds cargs)
         subst bds pargs in
 
-    let body = EcFol.form_of_expr EcFol.mhr body in
+    let body = EcFol.form_of_expr body in
     let body =
       Tvar.f_subst ~freshen:true (List.map fst op.EcDecl.op_tparams) tys body in
 
@@ -457,7 +458,7 @@ and cbv (st : state) (s : subst) (f : form) (args : args) : form =
       if   st.st_ri.modpath
       then EcEnv.NormMp.norm_pvar st.st_env pv
       else pv in
-    app_red st (f_pvar pv f.f_ty m) args
+    app_red st (f_pvar pv f.f_ty m).inv args
 
   | Fop _ -> app_red st (Subst.subst s f) args
 
@@ -479,11 +480,12 @@ and cbv (st : state) (s : subst) (f : form) (args : args) : form =
 
   | FhoareF hf ->
     assert (Args.isempty args);
-    assert (not (Subst.has_mem s mhr));
-    let hf_pr = norm st s hf.hf_pr in
-    let hf_po = norm st s hf.hf_po in
+    assert (not (Subst.has_mem s hf.hf_m));
+    let hf_pr = norm st s hf.hf_pr [@alert "-priv_pl"] in
+    let hf_po = norm st s hf.hf_po [@alert "-priv_pl"] in
     let hf_f  = norm_xfun st s hf.hf_f in
-    f_hoareF_r { hf_pr; hf_f; hf_po }
+    let (m,_) = norm_me s (abstract hf.hf_m) in
+    f_hoareF {m;inv=hf_pr} hf_f {m;inv=hf_po}
 
   | FhoareS hs ->
     assert (Args.isempty args);
@@ -492,33 +494,36 @@ and cbv (st : state) (s : subst) (f : form) (args : args) : form =
     let hs_po = norm st s hs.hs_po in
     let hs_s  = norm_stmt s hs.hs_s in
     let hs_m  = norm_me s hs.hs_m in
-    f_hoareS_r { hs_pr; hs_po; hs_s; hs_m }
+    let m = fst hs_m in
+    f_hoareS (snd hs_m) {m;inv=hs_pr} hs_s {m;inv=hs_po}
 
   | FeHoareF hf ->
     assert (Args.isempty args);
     assert (not (Subst.has_mem s mhr));
     let ehf_pr  = norm st s hf.ehf_pr  in
     let ehf_po  = norm st s hf.ehf_po  in
     let ehf_f   = norm_xfun st s hf.ehf_f in
-    f_eHoareF_r { ehf_pr; ehf_f; ehf_po; }
+    let (m,_) = norm_me s (abstract hf.ehf_m) in
+    f_eHoareF {m;inv=ehf_pr} ehf_f {m;inv=ehf_po}
 
   | FeHoareS hs ->
     assert (Args.isempty args);
     assert (not (Subst.has_mem s (fst hs.ehs_m)));
     let ehs_pr  = norm st s hs.ehs_pr in
     let ehs_po  = norm st s hs.ehs_po in
     let ehs_s   = norm_stmt s hs.ehs_s in
-    let ehs_m   = norm_me s hs.ehs_m in
-    f_eHoareS_r { ehs_pr; ehs_po; ehs_s; ehs_m }
+    let (m,mt)   = norm_me s hs.ehs_m in
+    f_eHoareS mt {m;inv=ehs_pr} ehs_s {m;inv=ehs_po}
 
   | FbdHoareF hf ->
     assert (Args.isempty args);
-    assert (not (Subst.has_mem s mhr));
+    assert (not (Subst.has_mem s hf.bhf_m));
     let bhf_pr = norm st s hf.bhf_pr in
     let bhf_po = norm st s hf.bhf_po in
     let bhf_f  = norm_xfun st s hf.bhf_f in
     let bhf_bd = norm st s hf.bhf_bd in
-    f_bdHoareF_r { hf with bhf_pr; bhf_po; bhf_f; bhf_bd }
+    let (m,_) = norm_me s (abstract hf.bhf_m) in
+    f_bdHoareF {m;inv=bhf_pr} bhf_f {m;inv=bhf_po} hf.bhf_cmp {m;inv=bhf_bd}
 
   | FbdHoareS bhs ->
     assert (Args.isempty args);
@@ -527,18 +532,20 @@ and cbv (st : state) (s : subst) (f : form) (args : args) : form =
     let bhs_po = norm st s bhs.bhs_po in
     let bhs_s  = norm_stmt s bhs.bhs_s in
     let bhs_bd = norm st s bhs.bhs_bd in
-    let bhs_m  = norm_me s bhs.bhs_m in
-    f_bdHoareS_r { bhs with bhs_m; bhs_pr; bhs_po; bhs_s; bhs_bd }
+    let (m,mt)  = norm_me s bhs.bhs_m in
+    f_bdHoareS mt {m;inv=bhs_pr} bhs_s {m;inv=bhs_po} bhs.bhs_cmp {m;inv=bhs_bd}
 
   | FequivF ef ->
     assert (Args.isempty args);
-    assert (not (Subst.has_mem s mleft));
-    assert (not (Subst.has_mem s mright));
+    assert (not (Subst.has_mem s ef.ef_ml));
+    assert (not (Subst.has_mem s ef.ef_mr));
     let ef_pr = norm st s ef.ef_pr in
     let ef_po = norm st s ef.ef_po in
     let ef_fl = norm_xfun st s ef.ef_fl in
     let ef_fr = norm_xfun st s ef.ef_fr in
-    f_equivF_r {ef_pr; ef_fl; ef_fr; ef_po }
+    let (ml,_) = norm_me s (abstract ef.ef_ml) in
+    let (mr,_) = norm_me s (abstract ef.ef_mr) in
+    f_equivF {ml;mr;inv=ef_pr} ef_fl ef_fr {ml;mr;inv=ef_po}
 
   | FequivS es ->
     assert (Args.isempty args);
@@ -548,9 +555,9 @@ and cbv (st : state) (s : subst) (f : form) (args : args) : form =
     let es_po = norm st s es.es_po in
     let es_sl = norm_stmt s es.es_sl in
     let es_sr = norm_stmt s es.es_sr in
-    let es_ml  = norm_me s es.es_ml in
-    let es_mr  = norm_me s es.es_mr in
-    f_equivS_r {es_ml; es_mr; es_pr; es_sl; es_sr; es_po }
+    let (ml,mlt)  = norm_me s es.es_ml in
+    let (mr,mrt)  = norm_me s es.es_mr in
+    f_equivS mlt mrt {ml;mr;inv=es_pr} es_sl es_sr {ml;mr;inv=es_po}
 
   | FeagerF eg ->
     assert (Args.isempty args);
@@ -562,16 +569,19 @@ and cbv (st : state) (s : subst) (f : form) (args : args) : form =
     let eg_fr = norm_xfun st s eg.eg_fr in
     let eg_sl = norm_stmt s eg.eg_sl in
     let eg_sr = norm_stmt s eg.eg_sr in
-    f_eagerF_r {eg_pr; eg_sl; eg_fl; eg_fr; eg_sr; eg_po }
+    let (ml,_) = norm_me s (abstract eg.eg_ml) in
+    let (mr,_) = norm_me s (abstract eg.eg_mr) in
+    f_eagerF {ml;mr;inv=eg_pr} eg_sl eg_fl eg_fr eg_sr {ml;mr;inv=eg_po}
 
   | Fpr pr ->
     assert (Args.isempty args);
     assert (not (Subst.has_mem s mhr));
     let pr_mem   = Subst.subst_m s pr.pr_mem in
     let pr_fun   = norm_xfun st s pr.pr_fun in
     let pr_args  = norm st s pr.pr_args in
-    let pr_event = norm st s pr.pr_event in
-    f_pr_r { pr_mem; pr_fun; pr_args; pr_event; }
+    let pr_event = norm st s pr.pr_event.inv in
+    let (m,_) = norm_me s (abstract pr.pr_event.m) in
+    f_pr pr_mem pr_fun pr_args {m;inv=pr_event}
 
 (* -------------------------------------------------------------------- *)
 (* FIXME : initialize the subst with let in hyps *)