model_with_structures/analyzer.ml

@@ -59,26 +59,22 @@ struct
 
   (* value model & memory model *)
 
-  (* type deepvalue = ZeroDV *)
+  type deepvalue = ZeroDV
-                 (* | SmthDV *)
+                 | SmthDV
-                 (* | BotDV *)
+                 | BotDV
-                 (* | FunDV of ((* data list * *) stmt) list *)
+                 | FunDV of ((* data list * *) stmt) list
-                 (* | RefDV of deepvalue *)
+                 | RefDV of deepvalue
-                 (* | TupleDV of deepvalue list *)
+                 | TupleDV of deepvalue list
 
-  type memval = ZeroMV | SmthMV | BotMV (* | TopMV ?? *)
+  type value = ZeroV
-  type readval = ZeroRV | OneRV | TopRV
+             | SmthV
-  type writeval = ZeroWV | SmthWV | OneWV
+             | BotV
-
-  type value = UnitV of memval * readval * writeval
              | FunV of ((* data list * *) stmt) list
              | RefV of memid
              | TupleV of value list
 
   type revpath = VarRP | DerefRP of revpath | AccessRP of revpath * data
 
-  type action = ReadA | AlwaysWriteA | MayWriteA
-
   (* TODO: any additional difference between rvalue and lvalue now ?? *)
 
   (* --- *)
@@ -142,17 +138,16 @@ struct
   let mem_set (mem : mem) (id : memid) (v : value) : mem =
     (list_replace (fst mem) (snd mem - id - 1) v, snd mem)
 
-  (* let rec v_to_deepv (mem : mem) (v : value) : deepvalue = match v with *)
+  let rec v_to_deepv (mem : mem) (v : value) : deepvalue = match v with
-    (* | ZeroV -> ZeroDV *)
+    | ZeroV -> ZeroDV
-    (* | SmthV -> SmthDV *)
+    | SmthV -> SmthDV
-    (* | BotV -> BotDV *)
+    | BotV -> BotDV
-    (* | FunV s -> FunDV s *)
+    | FunV s -> FunDV s
-    (* | RefV id -> RefDV (v_to_deepv mem @@ mem_get mem id) *)
+    | RefV id -> RefDV (v_to_deepv mem @@ mem_get mem id)
-    (* | TupleV vs -> TupleDV (List.map (v_to_deepv mem) vs) *)
+    | TupleV vs -> TupleDV (List.map (v_to_deepv mem) vs)
 
-  let is_trivial_v (v : value) : bool =
+  let is_trivial_v (v : value) : bool = 
-    match v with | UnitV (_, _, _) -> true
+    v == ZeroV || v == SmthV || v == BotV
-                 | _ -> false
 
   (* --- path accessors --- *)
 
@@ -196,9 +191,19 @@ struct
   (* - value construction *)
 
   let rec valcopy (mem : mem) (v : value) (t : atype) : mem * value =
-    match t, v with
+    if is_trivial_v v
-    | UnitT (Rd, _), UnitV (v_m, _, _) -> (mem, UnitV (v_m, ZeroRV, ZeroWV))
+    then match t with
-    | UnitT (NRd, _), UnitV _ -> (mem, UnitV (BotMV, ZeroRV, ZeroWV))
+    | UnitT (Rd, _) -> (mem, v)
+    | UnitT (NRd, _) -> (mem, BotV)
+    | _ -> raise @@ Typing_error "valcopy: trivial value, wrong type"
+    else match t, v with
+    (* NOTE: replaced with if | best choice ?? *)
+    (* | UnitT (Rd, w), ZeroV -> (mem, v) *)
+    (* | UnitT (Rd, w), SmthV -> (mem, v) *)
+    (* | UnitT (Rd, w), BotV -> (mem, v) *)
+    (* | UnitT (NRd, w), ZeroV -> (mem, BotV) *)
+    (* | UnitT (NRd, w), SmthV -> (mem, BotV) *)
+    (* | UnitT (NRd, w), BotV -> (mem, BotV) *)
     | FunT _, FunV _ -> (mem, v)
     | RefT (Rf, _), RefV _ -> (mem, v)
     | RefT (Cp, t), RefV id -> let (mem', v') = valcopy mem (mem_get mem id) t in
@@ -210,76 +215,25 @@ struct
                               (mem', TupleV (List.rev vs')) (* TODO: FIXME: should reverse or not ?? *)
     | _, _ -> raise @@ Typing_error "valcopy: not trivial value, wrong type"
 
-  (* - action rules *)
-
-  let memvmod (a : action) (v_m : memval) : memval =
-    match a, v_m with
-      | ReadA, ZeroMV -> ZeroMV
-      | ReadA, _ -> raise @@ Eval_error "memvmod: forbidden read"
-      | AlwaysWriteA, _ -> ZeroMV
-      | MayWriteA, ZeroMV -> ZeroMV
-      | MayWriteA, _ -> SmthMV
-
-  let readvmod (a : action) (v_r : readval) : readval =
-    match a, v_r with
-      | _, TopRV -> TopRV
-      | _, OneRV -> OneRV
-      | ReadA, ZeroRV -> OneRV
-      | AlwaysWriteA, ZeroRV -> TopRV
-      | MayWriteA, ZeroRV -> ZeroRV
-
-  let writevmod (a : action) (v_w : writeval) : writeval =
-    match a, v_w with
-      | ReadA, v -> v
-      | AlwaysWriteA, _ -> OneWV
-      | MayWriteA, OneWV -> OneWV
-      | MayWriteA, v -> v
-
   (* - value update *)
 
-  let rec valchange (mem : mem) (v : value) (p : revpath) (b : value) : mem * value = match p, v with
+  let rec valupd (mem : mem) (v : value) (p : revpath) (b : value) : mem * value = match p, v with
     | VarRP, _ -> (mem, b)
-    | DerefRP p, RefV id -> let (mem', v') = valchange mem (mem_get mem id) p b in
+    | DerefRP p, RefV id -> let (mem', v') = valupd mem (mem_get mem id) p b in
                             (mem_set mem' id v', RefV id)
-    | AccessRP (p, id), TupleV vs -> let (mem', v') = valchange mem (List.nth vs id) p b in
+    | AccessRP (p, id), TupleV vs -> let (mem', v') = (* FIXME TMP Printf.printf "vs size=%i id=%i\n" (List.length vs) id; *)
-                                     (mem', TupleV (list_replace vs id v'))
+                                                      valupd mem (List.nth vs id) p b in
-    | _, _ -> raise @@ Typing_error "valupd"
+                                     (* FIXME TMP Printf.printf "before return\n"; *)
-
-  let rec valupd (mem : mem) (v : value) (p : revpath) (a : action) : mem * value = match p, v with
-    | VarRP, UnitV (v_m, v_r, v_w) -> (mem, UnitV (memvmod a v_m, readvmod a v_r, writevmod a v_w))
-    | DerefRP p, RefV id -> let (mem', v') = valupd mem (mem_get mem id) p a in
-                            (mem_set mem' id v', RefV id)
-    | AccessRP (p, id), TupleV vs -> let (mem', v') = valupd mem (List.nth vs id) p a in
                                      (mem', TupleV (list_replace vs id v'))
     | _, _ -> raise @@ Typing_error "valupd"
 
   (* - value combination *)
 
-  let memvalcomb (u : memval) (v : memval) : memval =
-    match u, v with
-      | ZeroMV, ZeroMV -> ZeroMV
-      | BotMV, BotMV -> BotMV
-      | _, _ -> SmthMV
-
-  let readvalcomb (u : readval) (v : readval) : readval =
-    match u, v with
-      | TopRV, TopRV -> TopRV
-      | ZeroRV, ZeroRV -> ZeroRV
-      | TopRV, ZeroRV -> ZeroRV
-      | ZeroRV, TopRV -> ZeroRV
-      | _, _ -> OneRV
-
-  let writevalcomb (u : writeval) (v : writeval) : writeval =
-    match u, v with
-      | OneWV, OneWV -> OneWV
-      | ZeroWV, ZeroWV -> ZeroWV
-      | _, _ -> SmthWV
-
   let rec valcomb (u : value) (v : value) : value =
-    match u, v with
+    if is_trivial_v u && is_trivial_v v
-      | UnitV (u_m, u_r, u_w), UnitV (v_m, v_r, v_w) ->
+    then (if u == v then u else BotV)
-        UnitV (memvalcomb u_m v_m, readvalcomb u_r v_r, writevalcomb u_w v_w)
+    else match u, v with
-      | FunV ustmts, FunV vstmts -> FunV (ustmts @ vstmts)
+      | FunV ustmts, FunV vstmts  -> FunV (ustmts @ vstmts)
       | RefV a, RefV b -> if a == b then u else raise @@ Typing_error "valcomb: ref"
       | TupleV us, TupleV vs -> TupleV (List.map2 valcomb us vs)
       | _, _ -> raise @@ Typing_error "valcomb"
@@ -292,7 +246,7 @@ struct
   (* - expression evaluation *)
 
   let rec exprval (mem : mem) (vals : vals) (e : expr) : value = match e with
-    | UnitE -> UnitV (ZeroMV, ZeroRV, ZeroWV)
+    | UnitE -> ZeroV
     | PathE p -> pathval mem vals p
     | RefE x -> RefV (vals_assoc x vals)
     | TupleE es -> TupleV (List.map (exprval mem vals) es)
@@ -333,64 +287,48 @@ struct
 
   (* - call values spoil *)
 
-  (* TODO: check assignment type matches types separately later ?? *)
+  (* TODO: check all cases *)
-  let is_correct_tags (r : read_cap) (w : write_cap)
+  let is_correct_tags (v : value) (r : read_cap) (w : write_cap)
-                      (m : mode) (c : copy_cap) : bool =
+                      (r' : read_cap) (w' : write_cap) (m : mode)
-    (snd m != Out || c == Rf) &&
+                      (c : copy_cap) : bool =
+    (* FIXME TMP *)
+    (* Printf.printf "%b %b %b %b %b\n" *)
+      (* (r != Rd || v == ZeroV) *)
+      (* (r != Rd || fst m == In) *)
+      (* (snd m != Out || w == AlwaysWr) *)
+      (* (* TODO: FIXME: why always write ?? *) *)
+      (* (((not ((w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf))) || w' == AlwaysWr)) *)
+      (* (is_trivial_v v); *)
+    (r != Rd || v == ZeroV) &&
+    (r != Rd || fst m == In) &&
     (snd m != Out || w == AlwaysWr) &&
-    (r != Rd || fst m == In)
+    (* TODO: FIXME: check *)
-
+    ((not ((w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf))) || w' == AlwaysWr) &&
-  let tryread (r : read_cap) (v_m : memval)
+    is_trivial_v v
-              (v_r : readval) (v_w : writeval) : value =
-    match r with
-      | Rd -> UnitV (memvmod ReadA v_m,
-                     readvmod ReadA v_r,
-                     writevmod ReadA v_w)
-      | NRd -> UnitV (v_m, v_r, v_w) 
-  
-  let tryspoil (m : mode) (w : write_cap) (v_m : memval) : memval =
-    match m, w with
-      | (_, Out), AlwaysWr -> v_m
-      | (_, Out), MayWr -> v_m
-      | (_, NOut), AlwaysWr -> BotMV
-      | (_, NOut), MayWr -> SmthMV
-      | _ -> raise @@ Typing_error "tryspoil: unexpected pair mode + write cap"
 
   let rec valspoil (mem : mem) (v : value) (t : atype)
-                   (m : mode) (c : copy_cap)
+                   (u : atype) (m : mode) (c : copy_cap)
-                   : mem * value = match t, v with
+                   : mem * value = match t, u, v with
-    | UnitT (r, w), UnitV (v_m, v_r, v_w) ->
+    | UnitT (r, w), UnitT (r', w'), _ ->
-      if not @@ is_correct_tags r w m c
+      if not @@ is_trivial_v v
-        then raise @@ Typing_error "valspoil: trivial type tags combination is not correct"
+        then raise @@ Typing_error "valspoil: unit, not trivial"
-      else
+      else if not @@ is_correct_tags v r w r' w' m c
-        let v' = tryread r v_m v_r v_w in
+        then raise @@ Typing_error "valspoil: unit, not correct"
-        if c == Cp || w == NeverWr
+      else if snd m == NOut && c == Rf && (w == AlwaysWr || w == MayWr)
-          then (mem, v')
+        then (mem, BotV)
-        else (match v' with
+      else if snd m == Out && w == AlwaysWr
-          | UnitV (v_m', v_r', v_w') ->
+        then (mem, ZeroV)
-            let (v_m'', v_r'', v_w'') =
+      else (mem, v)
-              (if w == AlwaysWr
+    | FunT ts, FunT us, FunV _ -> if ts == us then (mem, v) else raise @@ Typing_error "valspoil: fun"
-                then (memvmod AlwaysWriteA v_m',
+    | RefT (ct, t), RefT (cu, u), RefV id ->
-                      readvmod AlwaysWriteA v_r',
+      let (mem', v') = valspoil mem (mem_get mem id) t u m ct in
-                      writevmod AlwaysWriteA v_w')
-                else (* MayWr *)
-                     (memvmod MayWriteA v_m',
-                      readvmod MayWriteA v_r',
-                      writevmod MayWriteA v_w'))
-            in
-            let v_m''' = tryspoil m w v_m'' in
-            (mem, UnitV (v_m''', v_r'', v_w''))
-          | _ -> raise @@ Typing_error "valspoil: value after tryread is not unit")
-    | FunT ts, FunV _ -> (mem, v)
-    | RefT (ct, t), RefV id ->
-      let (mem', v') = valspoil mem (mem_get mem id) t m ct in
       (mem_set mem id v', RefV id)
-    | TupleT ts, TupleV vs ->
+    | TupleT ts, TupleT us, TupleV vs ->
-        let folder = fun (mem, vs') t v ->
+        let folder = fun (mem, vs') t u v ->
-          let (mem', v') = valspoil mem v t m c in (mem', v' :: vs') in
+          let (mem', v') = valspoil mem v t u m c in (mem', v' :: vs') in
-        let (mem', vs') = List.fold_left2 folder (mem, []) ts vs in
+        let (mem', vs') = list_foldl3 folder (mem, []) ts us vs in
         (mem', TupleV (List.rev vs'))
-    | _, _ ->  raise @@ Typing_error "valspoil"
+    | _, _, _ ->  raise @@ Typing_error "valspoil"
 
   (* full spoil *)
 
@@ -399,11 +337,11 @@ struct
     let x = pathvar p in
     let id = vals_assoc x vals in (* base var address *)
     let b = pathval mem vals p in (* subvalue in var *)
-    (* let t' = pathtype types p in (* type of subvalue *) *)
+    let t' = pathtype types p in (* type of subvalue *)
-    let (mem', b') = valspoil mem b t m Cp in (* spoil subvalue *)
+    let (mem', b') = valspoil mem b t t' m Cp in (* spoil subvalue *)
     (* TODO: FIXME: why copy (Cp)? maybe sometimes use top-level capability ? *)
     let pi = pathrev p VarRP in
-    let (mem'', v'') = valchange mem' (mem_get mem' id) pi b' in (* set subvalue into var *)
+    let (mem'', v'') = valupd mem' (mem_get mem' id) pi b' in (* set subvalue into var *)
     mem_set mem'' id v''
 
   let rec argsspoile (state : state) (m : mode) (t : atype) (e : expr) : mem =
@@ -431,34 +369,15 @@ struct
   (* NOTE: not needed due to performed optimization in stmt_eval *)
   (* let func_eval (mem : mem) (vals : vals) (s : stmt) (ts : mtype list) (es : expr list) = *)
 
-  let writeval_to_cap (v_w : writeval) : write_cap =
-    match v_w with
-      | ZeroWV -> NeverWr
-      | SmthWV -> MayWr
-      | OneWV -> AlwaysWr
-
-  let rec tags_check (mem : mem) (v : value) (t : atype) : unit =
-    match v, t with
-      | UnitV (v_m, v_r, v_w), UnitT (r, w) ->
-        if (r == Rd) && (v_r != OneRV)
-          then raise @@ Eval_error "tags_check: wrong read tag"
-        else if (r == NRd) && (v_r == OneRV)
-          then raise @@ Eval_error "tags_check: wrong not read tag"
-        else if writeval_to_cap v_w != w
-          then raise @@ Eval_error "tags_check: wrong write tag"
-        else ()
-      | FunV _, FunT _ -> ()
-      | RefV id, RefT (_, t) -> tags_check mem (mem_get mem id) t
-      | TupleV vs, TupleT ts -> ignore @@ List.map2 (tags_check mem) vs ts
-      | _, _ -> raise @@ Typing_error "tags_check"
-
   (* - statement evaluation *)
 
   let rec stmt_eval (state : state) (s : stmt) : state =
     match state with (mem, types, vals, visited) -> match s with
     | SkipS -> state
-    | CallS (f, es) -> let v = pathval mem vals f in
+    | CallS (f, es) -> let v = (* FIXME TMP Printf.printf "call, before v\n"; *)
-                       let t = pathtype types f in
+                               pathval mem vals f in
+                       let t = (* FIXME TMP Printf.printf "call, before t\n"; *)
+                               pathtype types f in
                        let types' : types = (fst types, fst types) in
                        let vals' : vals = (fst vals, fst vals) in
                        (match v, t with
@@ -475,14 +394,7 @@ struct
                                                     if List.mem stmt visited_old
                                                     then stmt :: visited_old
                                                     else match stmt_eval (mem_swa, types_swa, vals_swa, stmt :: visited_old) stmt with
-                                                      (mem_after_stmt, _, vals_after_stmt, visited_after_stmt) ->
+                                                      (_, _, _, visited_after_stmt) -> visited_after_stmt)
-                                                        ignore @@ List.fold_left
-                                                          (fun x (_, t) ->
-                                                             let id = vals_assoc x vals_after_stmt in
-                                                             let v = mem_get mem_after_stmt id in
-                                                             tags_check mem_after_stmt v t; x + 1)
-                                                          0 ts;
-                                                        visited_after_stmt)
                                                  visited_swa
                                                  fstmts in
                              let mem_spoiled = (* FIXME TMP Printf.printf "call, before spoil\n"; *)
@@ -500,28 +412,16 @@ struct
                        else let x = pathvar p in
                             let id = vals_assoc x vals in
                             let pi = pathrev p VarRP in
-                            let (mem', v') = valupd mem (mem_get mem id) pi AlwaysWriteA in
+                            let (mem', v') = valupd mem (mem_get mem id) pi ZeroV in
                             (mem_set mem' id v', types, vals, visited)
                      | RefT _ -> raise @@ Eval_error "write: ref type"
                      | TupleT _ -> raise @@ Eval_error "write: tuple type"
                      | _ -> raise @@ Eval_error "write: type")
-    | ReadS p -> (match pathtype types p with
+    | ReadS p -> if pathval mem vals p == SmthV || pathval mem vals p == BotV 
-                    | UnitT (_, _) ->
+                 then raise @@ Eval_error "read: spoiled value"
-                      (* NOTE: not required *)
+                 else if pathval mem vals p != ZeroV 
-                      (* if r == NRd *)
+                 then raise @@ Eval_error "read: nontrivial value"
-                      (* then raise @@ Eval_error "read: not read tag" *)
+                 else state
-                      (* else *)
-                      let x = pathvar p in
-                      let id = vals_assoc x vals in
-                      let pi = pathrev p VarRP in
-                      let (mem', v') = valupd mem (mem_get mem id) pi ReadA in
-                      (mem_set mem' id v', types, vals, visited)
-                    | RefT _ -> raise @@ Eval_error "read: ref type"
-                    | TupleT _ -> raise @@ Eval_error "read: tuple type"
-                    | _ -> raise @@ Eval_error "read: type")
-                 (* NOTE: handled inside through undefined in memvmod *)
-                 (* if pathval mem vals p == SmthV || pathval mem vals p == BotV *) 
-                 (* then raise @@ Eval_error "read: spoiled value" *)
     | SeqS (sl, sr) -> let statel = stmt_eval state sl in
                        stmt_eval statel sr
     | ChoiceS (sl, sr) -> let statel = stmt_eval state sl in
@@ -618,30 +518,23 @@ struct
   let rdS p = ReadS p 
   let callS f args = CallS (f, args)
 
-  let uV m = UnitV (m, ZeroRV, ZeroWV)
-
   (* - utils tests *)
 
-  let v_memval_is v m =
-    match v with
-     | UnitV (v_m, _, _) -> v_m == m
-     | _ -> false
-
   let%expect_test "mem add / get / set" =
     let mem = empty_mem in
-    let (mem, id1) = mem_add mem @@ uV ZeroMV in 
+    let (mem, id1) = mem_add mem ZeroV in 
-    let (mem, id2) = mem_add mem @@ uV SmthMV in 
+    let (mem, id2) = mem_add mem SmthV in 
-    let (mem, id3) = mem_add mem @@ uV BotMV in 
+    let (mem, id3) = mem_add mem BotV in 
     Printf.printf "%i %i %i " id1 id2 id3;
-    Printf.printf "%b %b %b " (v_memval_is (mem_get mem id1) ZeroMV)
+    Printf.printf "%b %b %b " (mem_get mem id1 == ZeroV)
-                              (v_memval_is (mem_get mem id2) SmthMV)
+                              (mem_get mem id2 == SmthV)
-                              (v_memval_is (mem_get mem id3) BotMV);
+                              (mem_get mem id3 == BotV);
-    let mem = mem_set mem id1 @@ uV BotMV in 
+    let mem = mem_set mem id1 BotV in 
-    let mem = mem_set mem id2 @@ uV ZeroMV in 
+    let mem = mem_set mem id2 ZeroV in 
-    let mem = mem_set mem id3 @@ uV SmthMV in 
+    let mem = mem_set mem id3 SmthV in 
-    Printf.printf "%b %b %b" (v_memval_is (mem_get mem id1) BotMV)
+    Printf.printf "%b %b %b" (mem_get mem id1 == BotV)
-                             (v_memval_is (mem_get mem id2) ZeroMV)
+                              (mem_get mem id2 == ZeroV)
-                             (v_memval_is (mem_get mem id3) SmthMV);
+                              (mem_get mem id3 == SmthV);
     [%expect {| 0 1 2 true true true true true true |}]
 
   (* - basic var tests *)
@@ -662,7 +555,7 @@ struct
                          ReadS (VarP globals_min_id));
          [%expect.unreachable]);
     with Eval_error msg -> Printf.printf "%s" msg;
-    [%expect {| memvmod: forbidden read |}]
+    [%expect {| read: spoiled value |}]
 
   let%expect_test "simple vars, no read & read" =
     prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE);
@@ -728,10 +621,10 @@ struct
   let%expect_test "simple call with write, dsl" =
     prog_eval_noret (
       [
-        defgu uT_aw;
+        defgu uT_r_mw;
-        defg (rfT uT_aw) rfg0E;
+        defg (rfT uT_r_mw) rfg0E;
         FunD (
-          [moded @@ cpT @@ uT_aw],
+          [moded @@ cpT @@ uT_r_mw],
           wrS @@ drf @@ v0
         )
       ],
@@ -743,10 +636,10 @@ struct
   let%expect_test "simple call with read after write, dsl" =
     prog_eval_noret (
       [
-        defgu uT_aw;
+        defgu uT_r_mw;
-        defg (rfT uT_aw) rfg0E;
+        defg (rfT uT_r_mw) rfg0E;
         FunD (
-          [moded @@ cpT @@ uT_aw],
+          [moded @@ cpT @@ uT_mw],
           (wrS @@ drf @@ v0) #.
           (rdS @@ drf @@ v0)
         )
@@ -803,7 +696,7 @@ struct
     );
     [%expect.unreachable]);
     with Eval_error msg -> Printf.printf "%s" msg;
-    [%expect {| memvmod: forbidden read |}]
+    [%expect {| read: spoiled value |}]
 
   let%expect_test "simple call with write to ref with fix, dsl" =
     prog_eval_noret (
@@ -886,9 +779,9 @@ struct
     prog_eval_noret (
       [
         defgu uT_r_aw;
-        defg (rfT uT_r) rfg0E;
+        defg (rfT uT_r_aw) rfg0E;
         FunD (
-          [moded @@ cpT @@ uT],
+          [moded @@ cpT @@ uT_aw],
           (wrS @@ vg0) #.
           (rdS @@ drf @@ vg1)
         )
@@ -902,10 +795,10 @@ struct
   let%expect_test "simple call with read & write (2 args), dsl" =
     prog_eval_noret (
       [
-        defgu uT_r;
+        defgu uT_r_aw;
-        defg (rfT uT_r) rfg0E;
+        defg (rfT uT_r_aw) rfg0E;
-        defgu uT_aw;
+        defgu uT_r_aw;
-        defg (rfT uT_aw) rfg2E;
+        defg (rfT uT_r_aw) rfg2E;
         FunD (
           [
             moded @@ rfT @@ uT_r;
@@ -933,10 +826,10 @@ struct
         defg (rfT uT_r_aw) rfg6E;
         FunD (
           [
-            ((NIn, NOut), cpT @@ uT);
+            ((NIn, NOut), cpT @@ uT_aw);
             ((In, NOut), cpT @@ uT_r_aw);
-            ((NIn, Out), rfT @@ uT_aw);
+            ((NIn, Out), cpT @@ uT_aw);
-            ((In, Out), rfT @@ uT_r_aw);
+            ((In, Out), cpT @@ uT_r_aw);
           ],
           (rdS @@ drf @@ v1) #.
           (rdS @@ drf @@ v3) #.
@@ -957,10 +850,10 @@ struct
   let%expect_test "simple call with different arguments modifiers, ref, dsl" =
     prog_eval_noret (
       [
-        defgu uT_r;
+        defgu uT_r_aw;
-        defg (rfT uT_r) rfg0E;
+        defg (rfT uT_r_aw) rfg0E;
-        defgu uT_r;
+        defgu uT_r_aw;
-        defg (rfT uT_r) rfg2E;
+        defg (rfT uT_r_aw) rfg2E;
         defgu uT_r_aw;
         defg (rfT uT_r_aw) rfg4E;
         defgu uT_r_aw;
@@ -989,82 +882,81 @@ struct
 
   (* - complex tests *)
 
-  (* TODO: FIXME: rw tags *)
   (* NOTE: path access isreversed to intuitive function application
            by definition *)
-  (* let%expect_test "complex test: send, dsl" = *)
+  let%expect_test "complex test: send, dsl" =
-    (* prog_eval_noret ( *)
+    prog_eval_noret (
       (* TODO: set optimal ref mods later *)
-      (* let user_utilsT = TupleT [uT_r_aw (* 0 id *); uT_r_aw] in *)
+      let user_utilsT = TupleT [uT_r_aw (* 0 id *); uT_r_aw] in
-      (* let user_infoT =  TupleT [uT_r_aw (* 0 name *); uT_r_aw; uT_r_aw] in *)
+      let user_infoT =  TupleT [uT_r_aw (* 0 name *); uT_r_aw; uT_r_aw] in
-      (* let userT = TupleT [cpT user_utilsT (* 0 utils *); cpT user_infoT (* 1 info *)] in *)
+      let userT = TupleT [cpT user_utilsT (* 0 utils *); cpT user_infoT (* 1 info *)] in
-      (* let versionT = TupleT [uT_r_aw (* 0 id *); uT_r_aw; uT_r_aw] in *)
+      let versionT = TupleT [uT_r_aw (* 0 id *); uT_r_aw; uT_r_aw] in
-      (* let utilsT = TupleT [uT_r_aw (* 0 has_version *); uT_r_aw (* 1 id *)] in *)
+      let utilsT = TupleT [uT_r_aw (* 0 has_version *); uT_r_aw (* 1 id *)] in
-      (* let requestT = TupleT [cpT userT (* 0 user *); *)
+      let requestT = TupleT [cpT userT (* 0 user *);
-                             (* cpT versionT (* 1 version *); *)
+                             cpT versionT (* 1 version *);
-                             (* cpT utilsT (* 2 utils *); *)
+                             cpT utilsT (* 2 utils *);
-                             (* cpT uT_r_aw (* 3 data *); *)
+                             cpT uT_r_aw (* 3 data *);
-                             (* uT_r_aw (* 4 operation_date *)] in *)
+                             uT_r_aw (* 4 operation_date *)] in
-      (* let user_utilsE = TupleE [UnitE (* 0 id *); UnitE] in *)
+      let user_utilsE = TupleE [UnitE (* 0 id *); UnitE] in
-      (* let user_infoE =  TupleE [UnitE (* 0 name *); UnitE; UnitE] in *)
+      let user_infoE =  TupleE [UnitE (* 0 name *); UnitE; UnitE] in
-      (* let userE = TupleE [rfg0E (* 0 utils *); rfg1E (* 1 info *)] in *)
+      let userE = TupleE [rfg0E (* 0 utils *); rfg1E (* 1 info *)] in
-      (* let versionE = TupleE [UnitE (* 0 id *); UnitE; UnitE] in *)
+      let versionE = TupleE [UnitE (* 0 id *); UnitE; UnitE] in
-      (* let utilsE = TupleE [UnitE (* 0 has_version *); UnitE (* 1 id *)] in *)
+      let utilsE = TupleE [UnitE (* 0 has_version *); UnitE (* 1 id *)] in
-      (* let requestE = TupleE [rfg2E (* 0 user *); *)
+      let requestE = TupleE [rfg2E (* 0 user *);
-                             (* rfg3E (* 1 version *); *)
+                             rfg3E (* 1 version *);
-                             (* rfg4E (* 2 utils *); *)
+                             rfg4E (* 2 utils *);
-                             (* rfg5E (* 3 data *); *)
+                             rfg5E (* 3 data *);
-                             (* UnitE (* 4 operation_date *)] in *)
+                             UnitE (* 4 operation_date *)] in
-      (* let get_version_idID = vg7 in *)
+      let get_version_idID = vg7 in
-      (* let updated_versionID = vg8 in *)
+      let updated_versionID = vg8 in
-      (* let sendID = vg9 in *)
+      let sendID = vg9 in
-      (* let send_allID = vg10 in *)
+      let send_allID = vg10 in
-      (* let get_version_idF = FunD ([moded requestT], *)
+      let get_version_idF = FunD ([moded requestT],
-        (* (rdS @@ access 0 @@ drf @@ access 1 v0) |. skp) in *)
+        (rdS @@ access 0 @@ drf @@ access 1 v0) |. skp) in
-      (* let updated_versionF = FunD ([moded requestT], *)
+      let updated_versionF = FunD ([moded requestT],
-        (* (rdS @@ access 0 @@ drf @@ access 2 v0) #. *)
+        (rdS @@ access 0 @@ drf @@ access 2 v0) #.
         (* TODO: read all the substructure ?? *)
-        (* (rdS @@ access 0 @@ drf @@ access 1 v0) #. *)
+        (rdS @@ access 0 @@ drf @@ access 1 v0) #.
-        (* (rdS @@ access 1 @@ drf @@ access 1 v0)) in *)
+        (rdS @@ access 1 @@ drf @@ access 1 v0)) in
-      (* let sendF = FunD ([moded requestT], *)
+      let sendF = FunD ([moded requestT],
-        (* (( *)
+        ((
-           (* (wrS @@ access 0 @@ drf @@ access 2 v0) #. *)
+           (wrS @@ access 0 @@ drf @@ access 2 v0) #.
-           (* (rdS @@ drf @@ access 3 v0) #. *)
+           (rdS @@ drf @@ access 3 v0) #.
-           (* (wrS @@ drf @@ access 3 v0) #. *)
+           (wrS @@ drf @@ access 3 v0) #.
-           (* (rdS @@ access 0 @@ drf @@ access 1 @@ drf @@ access 0 v0) *)
+           (rdS @@ access 0 @@ drf @@ access 1 @@ drf @@ access 0 v0)
-         (* ) |. skp) #. *)
+         ) |. skp) #.
-         (* (wrS @@ access 4 v0) #. *)
+         (wrS @@ access 4 v0) #.
          (* TODO: read all the substructure ?? *)
-         (* (rdS @@ access 4 v0) (*rdS v0*)) in (* FIXME: TMP, parial read, should be full *) *)
+         (rdS @@ access 4 v0) (*rdS v0*)) in (* FIXME: TMP, parial read, should be full *)
-      (* let send_allF = FunD ([moded requestT], *)
+      let send_allF = FunD ([moded requestT],
-        (* (wrS @@ access 4 v0) (*wrS v0*) #. (* FIXME: TMP, parial write, should be full *) *)
+        (wrS @@ access 4 v0) (*wrS v0*) #. (* FIXME: TMP, parial write, should be full *)
-        (* (callS sendID [pE v0]) #. *)
+        (callS sendID [pE v0]) #.
-        (* (callS get_version_idID [pE v0]) #. *)
+        (callS get_version_idID [pE v0]) #.
-        (* (callS updated_versionID [pE v0]) #. *)
+        (callS updated_versionID [pE v0]) #.
         (* TODO: read all the substructure ?? *)
-        (* (wrS @@ access 0 @@ drf @@ access 1 v0) #. *)
+        (wrS @@ access 0 @@ drf @@ access 1 v0) #.
-        (* (wrS @@ access 1 @@ drf @@ access 1 v0) #. *)
+        (wrS @@ access 1 @@ drf @@ access 1 v0) #.
         (* --- *)
-        (* ((rdS @@ access 0 @@ drf @@ access 0 @@ drf @@ access 0 v0) |. *)
+        ((rdS @@ access 0 @@ drf @@ access 0 @@ drf @@ access 0 v0) |.
-         (* (rdS @@ access 0 @@ drf @@ access 1 v0))) in *)
+         (rdS @@ access 0 @@ drf @@ access 1 v0))) in
-      (* let varID = vg6 in *)
+      let varID = vg6 in
-      (* [ *)
+      [
-        (* defg user_utilsT user_utilsE; *)
+        defg user_utilsT user_utilsE;
-        (* defg user_infoT user_infoE; *)
+        defg user_infoT user_infoE;
-        (* defg userT userE; *)
+        defg userT userE;
-        (* defg versionT versionE; *)
+        defg versionT versionE;
-        (* defg utilsT utilsE; *)
+        defg utilsT utilsE;
-        (* defgu uT_r_aw; *)
+        defgu uT_r_aw;
-        (* defg requestT requestE; *)
+        defg requestT requestE;
-        (* get_version_idF; *)
+        get_version_idF;
-        (* updated_versionF; *)
+        updated_versionF;
-        (* sendF; *)
+        sendF;
-        (* send_allF *)
+        send_allF
-      (* ], *)
+      ],
-      (* callS send_allID [pE varID] *)
+      callS send_allID [pE varID]
-    (* ); *)
+    );
-    (* Printf.printf "done!"; *)
+    Printf.printf "done!";
-    (* [%expect {| done! |}] *)
+    [%expect {| done! |}]
 
   (* TODO: version with more optimal modifiers *)
 end

model_with_structures/model.typ

@@ -816,9 +816,9 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
     $bot$, $0$, $?$,
     $bot$, $?$, $?$,
     // $bot$, $top$, $?$,
-    // $top$, $0$, $?$,
+    $top$, $0$, $?$,
-    // $top$, $?$, $?$,
+    $top$, $?$, $?$,
-    // $top$, $bot$, $?$,
+    $top$, $bot$, $?$,
     $bot$, $bot$, $bot$,
     // $top$, $top$, $top$,
   ),
@@ -942,7 +942,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
   rule(
     name: [ unit expr value],
 
-    $vals, mu texpre () eqmu cdl 0_m, 0_r, 0_w cdr$,
+    $vals, mu texpre () eqmu 0$,
   )
 ))
 
@@ -1064,7 +1064,6 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
 
 #let spoil = `spoil`
 #let tryread = `try read`
-#let tryspoil = `try spoil`
 
 #let tcorrectnew = $attach(tack.r.double, br: #[correct])$
 #align(center, prooftree(
@@ -1106,44 +1105,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
   )
 ))
 
-#h(10pt)
+// TODO: extract correctness
-
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ value maybe spoiled],
-
-    $v_m,
-     xarrowSquiggly(not Out \, MaybeWrite)_tryspoil
-     ?$,
-  )
-))
-
-#h(10pt)
-
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ value always spoiled],
-
-    $v_m,
-     xarrowSquiggly(not Out \, AlwaysWrite)_tryspoil
-     bot$,
-  )
-))
-
-#h(10pt)
-
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ value not spoiled],
-
-    $v_m,
-     xarrowSquiggly(Out \, w)_tryspoil
-     v_m$,
-  )
-))
 
 #h(10pt)
 
@@ -1157,11 +1119,10 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
      xarrowSquiggly(r)_tryread
      cl v_m', v_r', v_w' cr$,
 
-    $v_m' modW writeA xarrowSquiggly(o \, AlwaysWrite)_tryspoil v_m''$,
+    $w = AlwaysWrite$,
-
     $cl cdl v_m, v_r, v_w cdr, mu cr
-     xarrowSquiggly(cl r \, AlwaysWrite cr \, (\_, o) \, Ref)_spoil
+     xarrowSquiggly(cl r \, w cr \, (\_, not Out) \, Ref)_spoil
-     cl cdl v_m'', v_r' modR writeA, v_w' modW writeA cdr, cdr, mu cr$,
+     cl cdl bot, v_r' modR writeA, v_w' modW writeA cdr, cdr, mu cr$,
   )
 ))
 
@@ -1177,11 +1138,10 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
      xarrowSquiggly(r)_tryread
      cl v_m', v_r', v_w' cr$,
 
-    $v_m' modW mbwriteA xarrowSquiggly(o \, MaybeWrite)_tryspoil v_m''$,
+    $w = MaybeWrite$,
-
     $cl cdl v_m, v_r, v_w cdr, mu cr
-     xarrowSquiggly(cl r \, MaybeWrite cr \, (\_, o) \, Ref)_spoil
+     xarrowSquiggly(cl r \, w cr \, (\_, not Out) \, Ref)_spoil
-     cl cdl v_m'', v_r' modR mbwriteA, v_w' modW mbwriteA cdr, mu cr$,
+     cl cdl ?, v_r' modR mbwriteA, v_w' modW mbwriteA cdr, mu cr$,
   )
 ))
 
@@ -1193,15 +1153,12 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
     name: [ skip step],
 
     $ tcorrectnew cl r, w, m, c cr $,
-    $cl v_m, v_r, v_w cr,
-     xarrowSquiggly(r)_tryread
-     cl v_m', v_r', v_w' cr$,
 
-    $c = Copy or w = NotWrite$,
+    $o == Out or c == Copy or w = NotWrite$,
 
     $cl cdl v_m, v_r, v_w cdr, mu cr
-     xarrowSquiggly(cl r \, w cr cr \, (\_, \_) \, c)_spoil
+     xarrowSquiggly(cl r \, w cr cr \, (\_, o) \, c)_spoil
-     cl cdl v_m', v_r', v_w' cdr mu cr$,
+     cl cdl v_m, v_r, v_w cdr mu cr$,
   )
 ))
 
@@ -1387,7 +1344,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
   rule(
     name: [ lambda check],
 
-    $mu ttags lambda space overline(s) :$,
+    $mu ttags lambda overline(s) :$,
   )
 ))
 #align(center, prooftree(
@@ -1436,9 +1393,9 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
      cl types', vals', mu' cr$,
 
     // NOTE: check that read and write tags are used properly
-    $mu' ttags mu'[vals'[x_1]] : t_1$,
+    $mu' ttags x_1 : t_1$,
     $...$,
-    $mu' ttags mu'[vals'[x_n]] : t_n$,
+    $mu' ttags x_n : t_n$,
 
     $vals, mu_0 tfunceval cl s, [x_1, .. x_n], [t_1, ... t_n], [e_1, ... e_n] cr$,
   )

model_with_structures/synthesizer.ml

@@ -164,44 +164,12 @@ struct
 
   (* NOTE: deepvalue - not used (?) *)
 
-  module MemVal = struct
-    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
-    [%%ocanren_inject
-      type nonrec t = ZeroMV | SmthMV | BotMV
-      [@@deriving gt ~options:{ show; gmap }]
-      type ground = t
-    ]
-  end
-
-  module ReadVal = struct
-    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
-    [%%ocanren_inject
-      type nonrec t = ZeroRV | OneRV | TopRV
-      [@@deriving gt ~options:{ show; gmap }]
-      type ground = t
-    ]
-  end
-
-  module WriteVal = struct
-    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
-    [%%ocanren_inject
-      type nonrec t = ZeroWV | SmthWV | OneWV
-      [@@deriving gt ~options:{ show; gmap }]
-      type ground = t
-    ]
-  end
-
   module Value = struct
     [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
     [%%ocanren_inject
-      type nonrec ('vm, 'vr, 'vw, 'sl, 'd, 'vl) t = UnitV of 'vm * 'vr * 'vw
+      type nonrec ('sl, 'd, 'vl) t = ZeroV | SmthV | BotV | FunV of 'sl | RefV of 'd | TupleV of 'vl
-                                                  | FunV of 'sl
-                                                  | RefV of 'd
-                                                  | TupleV of 'vl
       [@@deriving gt ~options:{ show; gmap }]
-      type ground = (MemVal.ground, ReadVal.ground, WriteVal.ground,
+      type ground = (((* Nat.ground List.ground * *) Stmt.ground) List.ground, Nat.ground, ground List.ground) t
-                     ((* Nat.ground List.ground * *) Stmt.ground) List.ground,
-                     Nat.ground, ground List.ground) t
     ]
   end
 
@@ -214,15 +182,6 @@ struct
     ]
   end
 
-  module Action = struct
-    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
-    [%%ocanren_inject
-      type nonrec t = ReadA | AlwaysWriteA | MayWriteA
-      [@@deriving gt ~options:{ show; gmap }]
-      type ground = t
-    ]
-  end
-
   (* --- *)
 
   module MemEnv = struct
@@ -381,17 +340,6 @@ struct
     { xs == [] & ys == [] & zs == [] }
   }
 
-  (* NOTE: unrequired ? *)
-  (* let list_map2o f xs ys zs = ocanren { *)
-    (* { xs == [] & ys == [] } | *)
-    (* { fresh x', xs', y', ys', z', zs' in *)
-      (* xs == x' :: xs' & *)
-      (* ys == y' :: ys' & *)
-      (* f x' y' z' *)
-      (* mapo f xs' ys' zs' & *)
-      (* zs == z' :: zs' } *)
-  (* } *)
-
   (* - state utils *)
 
   let types_assoco id types tp =
@@ -511,8 +459,7 @@ struct
   let is_trivial_vo v =
     let open Value in
     ocanren {
-    fresh v_m, v_r, v_w in
+    v == ZeroV | v == SmthV | v == BotV
-    v == UnitV (v_m, v_r, v_w)
   }
 
   let rec pathvaro p x =
@@ -593,19 +540,12 @@ struct
     let open Value in
     let open ReadCap in
     let open CopyCap in
-    let open MemVal in
-    let open ReadVal in
-    let open WriteVal in
     ocanren {
       { fresh r, w in
         is_trivial_vo v &
         tp == UnitT (r, w) &
-        { { fresh v_m, _v_r, _v_w in
+        { { r == Rd & mem_with_id' == Std.pair mem v } |
-            r == Rd &
+          { r == NRd & mem_with_id' == Std.pair mem BotV } } } |
-            v == UnitV (v_m, _v_r, _v_w) &
-            mem_with_id' == Std.pair mem (UnitV (v_m, ZeroRV, ZeroWV)) } |
-          { r == NRd &
-            mem_with_id' == Std.pair mem (UnitV (BotMV, ZeroRV, ZeroWV)) } } } |
       { fresh stmts, ts in
         v == FunV stmts &
         tp == FunT ts &
@@ -627,43 +567,10 @@ struct
         mem_with_id' == Std.pair mem' (TupleV vs') }
   }
 
-  (* - action rules *)
-
-  let memvmodo a v_m v_m' =
-    let open MemVal in
-    let open Action in
-    ocanren {
-      { a == ReadA & v_m == ZeroMV & v_m' == ZeroMV } |
-      { a == AlwaysWriteA & v_m' == ZeroMV } |
-      { a == MayWriteA & v_m == ZeroMV & v_m' == ZeroMV } |
-      { a == MayWriteA & v_m =/= ZeroMV & v_m' == SmthMV }
-  }
-
-  let readvmodo a v_r v_r' =
-    let open ReadVal in
-    let open Action in
-    ocanren {
-      { v_r == TopRV & v_r' == TopRV } |
-      { v_r == OneRV & v_r' == OneRV } |
-      { a == ReadA & v_r == ZeroRV & v_r' == OneRV } |
-      { a == AlwaysWriteA & v_r == ZeroRV & v_r' == TopRV } |
-      { a == MayWriteA & v_r == ZeroRV & v_r' == ZeroRV }
-  }
-
-  let writevmodo a v_w v_w' =
-    let open WriteVal in
-    let open Action in
-    ocanren {
-      { a == ReadA & v_w' == v_w } |
-      { a == AlwaysWriteA & v_w' == OneWV } |
-      { a == MayWriteA & v_w == OneWV & v_w' == OneWV } |
-      { a == MayWriteA & v_w =/= OneWV & v_w' == v_w }
-  }
-
   (* - value update *)
 
   (* NOTE: reversed path used *)
-  let rec valchangeo mem v rp b mem_with_v' =
+  let rec valupdo mem v rp b mem_with_v' =
     let open RevPath in
     let open Value in
     ocanren {
@@ -673,7 +580,7 @@ struct
         rp == DerefRP rp' &
         v == RefV id &
         mem_geto mem id v' &
-        valchangeo mem v' rp' b mem_with_v_upd &
+        valupdo mem v' rp' b mem_with_v_upd &
         Std.pair mem_upd v_upd == mem_with_v_upd &
         mem_seto mem_upd id v_upd mem_st &
         mem_with_v' == Std.pair mem_st (RefV id) } |
@@ -681,40 +588,7 @@ struct
         rp == AccessRP (rp', id) &
         v == TupleV vs' &
         list_ntho vs' id v' &
-        valchangeo mem v' rp' b mem_with_v_upd &
+        valupdo mem v' rp' b mem_with_v_upd &
-        Std.pair mem_upd v_upd == mem_with_v_upd &
-        list_replaceo vs' id v_upd vs_upd &
-        mem_with_v' == Std.pair mem_upd (TupleV vs_upd) }
-  }
-
-  (* NOTE: reversed path used *)
-  let rec valupdo mem v rp a mem_with_v' =
-    let open RevPath in
-    let open Value in
-    ocanren {
-      { fresh v_m, v_r, v_w,
-              v_m', v_r', v_w',
-              v' in
-        rp == VarRP &
-        v == UnitV (v_m, v_r, v_w) &
-        memvmodo a v_m v_m' &
-        readvmodo a v_r v_r' &
-        writevmodo a v_w v_w' &
-        v' == UnitV (v_m', v_r', v_w') &
-        mem_with_v' == Std.pair mem v' } |
-      { fresh rp', id, v', mem_upd, v_upd, mem_with_v_upd, mem_st in
-        rp == DerefRP rp' &
-        v == RefV id &
-        mem_geto mem id v' &
-        valupdo mem v' rp' a mem_with_v_upd &
-        Std.pair mem_upd v_upd == mem_with_v_upd &
-        mem_seto mem_upd id v_upd mem_st &
-        mem_with_v' == Std.pair mem_st (RefV id) } |
-      { fresh rp', id, vs', v', mem_upd, v_upd, mem_with_v_upd, vs_upd in
-        rp == AccessRP (rp', id) &
-        v == TupleV vs' &
-        list_ntho vs' id v' &
-        valupdo mem v' rp' a mem_with_v_upd &
         Std.pair mem_upd v_upd == mem_with_v_upd &
         list_replaceo vs' id v_upd vs_upd &
         mem_with_v' == Std.pair mem_upd (TupleV vs_upd) }
@@ -722,50 +596,13 @@ struct
 
   (* - value combination *)
 
-  let memvalcombo u v u' =
-    let open MemVal in
-    ocanren {
-      { u == ZeroMV & v == ZeroMV & u' == ZeroMV } |
-      { u == BotMV & v == BotMV & u' == BotMV } |
-      { u =/= ZeroMV & v =/= ZeroMV &
-        u =/= BotMV & v =/= BotMV & 
-        u' == SmthMV }
-  }
-
-  let readvalcombo u v u' =
-    let open ReadVal in
-    ocanren {
-      { u == TopRV & v == TopRV & u' == TopRV } |
-      { u == ZeroRV & v == ZeroRV & u' == ZeroRV } |
-      { u == TopRV & v == ZeroRV & u' == ZeroRV } |
-      { u == ZeroRV & v == TopRV & u' == ZeroRV } |
-      { u =/= TopRV & v =/= TopRV &
-        u =/= ZeroRV & v =/= ZeroRV & 
-        u' == OneRV }
-  }
-
-  let writevalcombo u v u' =
-    let open WriteVal in
-    ocanren {
-      { u == OneWV & v == OneWV & u' == OneWV } |
-      { u == ZeroWV & v == ZeroWV & u' == ZeroWV } |
-      { u =/= ZeroWV & v =/= ZeroWV &
-        u =/= OneWV & v =/= OneWV & 
-        u' == SmthWV }
-  }
-
   let rec valcombo u v u' =
     let open Value in
     ocanren {
-    { fresh u_m, u_r, u_w,
+    { is_trivial_vo u &
-            v_m, v_r, v_w,
+      is_trivial_vo v &
-            u_m', u_r', u_w' in
+      (* TODO: do not use disequality constraint ? *)
-      u == UnitV (u_m, u_r, u_w) &
+      { { u == v & u' == u } | { u =/= v & u' == BotV } } } |
-      v == UnitV (v_m, v_r, v_w) &
-      memvalcombo u_m v_m u_m' &
-      readvalcombo u_r v_r u_r' &
-      writevalcombo u_w v_w u_w' &
-      u' == UnitV (u_m', u_r', u_w') } |
     { fresh ustmts, vstmts, ustmts' in
       u == FunV ustmts &
       v == FunV vstmts &
@@ -805,11 +642,8 @@ struct
   exprvalo mem vals e v' = 
     let open Expr in
     let open Value in
-    let open MemVal in
-    let open ReadVal in
-    let open WriteVal in
     ocanren {
-      { e == UnitE & v' == UnitV (ZeroMV, ZeroRV, ZeroWV) } |
+      { e == UnitE & v' == ZeroV } |
       { fresh p in
         e == PathE p &
         pathvalo mem vals p v' } |
@@ -926,99 +760,76 @@ struct
   (* - call values spoil *)
 
   (* TODO: check that negation is interpreted correctly *)
-  let is_correct_tagso r w m c =
+  let is_correct_tagso v r w _r' w' m c =
+    let open Value in
     let open ReadCap in
     let open WriteCap in
     let open Mode in
     let open CopyCap in
     ocanren {
+      { r == NRd | r == Rd & v == ZeroV } &
       { r == NRd | r == Rd & is_ino m } &
-      { is_not_outo m | is_outo m & w == AlwaysWr & c == Rf }
+      { is_not_outo m | is_outo m & w == AlwaysWr } &
+      { w == NeverWr |
+        w =/= NeverWr & w' =/= AlwaysWr & is_not_outo m & c == Cp |
+        w =/= NeverWr & w' == AlwaysWr } &
+      is_trivial_vo v
   }
 
-  let tryreado r v_m v_r v_w v' =
+  let rec valspoil_foldero m c mem_with_vs tp u v mem_with_vs' = ocanren {
-    let open Action in
-    let open Value in
-    let open ReadCap in
-    ocanren {
-      { fresh v_m', v_r', v_w' in
-        r == Rd &
-        memvmodo ReadA v_m v_m' &
-        readvmodo ReadA v_r v_r' &
-        writevmodo ReadA v_w v_w' &
-        v' == UnitV (v_m', v_r', v_w') } |
-      { r == NRd &
-        v' == UnitV (v_m, v_r, v_w)}
-  }
-
-  let tryspoilo m w v_m v_m' =
-    let open Mode in
-    let open WriteCap in
-    let open MemVal in
-    ocanren {
-      { is_outo m & { w == AlwaysWr | w == MayWr } & v_m' == v_m } |
-      { is_not_outo m & w == AlwaysWr & v_m' == BotMV } |
-      { is_not_outo m & w == MayWr & v_m' == SmthMV }
-  }
-
-  let rec valspoil_foldero m c mem_with_vs tp v mem_with_vs' = ocanren {
     fresh mem, vs, mem', v' in
     Std.pair mem vs == mem_with_vs &
-    valspoilo mem v tp m c (Std.pair mem' v') &
+    valspoilo mem v tp u m c (Std.pair mem' v') &
     mem_with_vs' == Std.pair mem' (v' :: vs)
   }
-  and valspoilo mem v tp m c mem_with_v' =
+  and valspoilo mem v tp u m c mem_with_v' =
     let open Type in
     let open Value in
     let open Mode in
     let open WriteCap in
     let open CopyCap in
-    let open Action in
     ocanren {
-      { fresh r, w,
+      { fresh r, w, r', w' in
-              v_m, v_r, v_w,
-              v', v'' in
         tp == UnitT (r, w) &
-        v == UnitV (v_m, v_r, v_w) &
+        u == UnitT (r', w') &
-        is_correct_tagso r w m c &
+        is_trivial_vo v &
-        tryreado r v_m v_r v_w v' &
+        is_correct_tagso v r w r' w' m c &
         {
-          { c == Cp & w == NeverWr &
+          { is_not_outo m &
-            mem_with_v' == Std.pair mem v' } |
+            c == Rf &
-          { fresh v_m', v_r', v_w',
+            { w == AlwaysWr | w == MayWr } &
-                  v_m'', v_r'', v_w'',
+            mem_with_v' == Std.pair mem BotV } |
-                  v_m''' in
+          { is_outo m &
-            v' == UnitV (v_m', v_r', v_w') &
+            w == AlwaysWr &
-            {
+            mem_with_v' == Std.pair mem ZeroV } |
-              { w == AlwaysWr &
+          { { is_outo m |
-                memvmodo AlwaysWriteA v_m' v_m'' &
+              is_not_outo m & c == Cp |
-                readvmodo AlwaysWriteA v_r' v_r'' &
+              is_not_outo m & c == Rf & w == NeverWr } &
-                writevmodo AlwaysWriteA v_w' v_w'' } |
+            { is_not_outo m |
-              { w == MayWr &
+              is_outo m & w == MayWr |
-                memvmodo MayWriteA v_m' v_m'' &
+              is_outo m & w == NeverWr } &
-                readvmodo MayWriteA v_r' v_r'' &
+            mem_with_v' == Std.pair mem v }
-                writevmodo MayWriteA v_w' v_w'' }
-            } &
-            tryspoilo m w v_m'' v_m''' &
-            v'' == UnitV (v_m''', v_r'', v_w'') &
-            mem_with_v' == Std.pair mem v'' }
         } } |
-      { fresh ts, _stmts in
+      { fresh ts, us, _stmts in
         tp == FunT ts &
+        u == FunT us &
         v == FunV _stmts &
+        ts == us &
         mem_with_v' == Std.pair mem v } |
-      { fresh ctp', tp', cu', id', v', mem_sp, v_sp, mem_set in
+      { fresh ctp', tp', cu', u', id', v', mem_sp, v_sp, mem_set in
         tp == RefT (ctp', tp') &
+        u == RefT (cu', u') &
         v == RefV id' &
         mem_geto mem id' v' &
-        valspoilo mem v' tp' m ctp' (Std.pair mem_sp v_sp) &
+        valspoilo mem v' tp' u' m ctp' (Std.pair mem_sp v_sp) &
         mem_seto mem_sp id' v_sp mem_set &
         mem_with_v' == Std.pair mem_set (RefV id') } |
       { fresh tps, us, vs, mem_sp, vs_sp in
         tp == TupleT tps &
+        u == TupleT us &
         v == TupleV vs &
-        list_foldr2o (valspoil_foldero m c)
+        list_foldr3o (valspoil_foldero m c)
-                     (Std.pair mem []) tps vs
+                     (Std.pair mem []) tps us vs
                      (Std.pair mem_sp vs_sp) &
         mem_with_v' == Std.pair mem_sp (TupleV vs_sp)
       }
@@ -1032,17 +843,17 @@ struct
     let open RevPath in
     ocanren {
       fresh mem, types, vals, visited,
-            x, id, b(* , tp' *), rp,
+            x, id, b, tp', rp,
             mem_sp, b_sp, v_sp, mem_upd, v_upd in
       st == StEnv (mem, types, vals, visited) &
       pathvaro p x &
       vals_assoco x vals id &
       pathvalo mem vals p b &
-      (* pathtypeo types p tp' & *)
+      pathtypeo types p tp' &
       valspoilo mem b tp tp' m Cp (Std.pair mem_sp b_sp) &
       mem_geto mem_sp id v_sp &
       pathrevo p VarRP rp &
-      valchangeo mem_sp v_sp rp b_sp (Std.pair mem_upd v_upd) &
+      valupdo mem_sp v_sp rp b_sp (Std.pair mem_upd v_upd) &
       mem_seto mem_upd id v_upd mem'
   }
 
@@ -1099,45 +910,8 @@ struct
   (* - function evaluation *)
   (* NOTE: not needed due to performed optimization in stmt_eval ? *)
 
-  let writeval_to_capo v_w w' =
-    let open WriteVal in
-    let open WriteCap in
-    ocanren {
-      { v_w == ZeroWV & w' == NeverWr } |
-      { v_w == SmthWV & w' == MayWr } |
-      { v_w == OneWV & w' == AlwaysWr }
-  }
-
-  let rec tags_checko mem v tp =
-    let open ReadVal in
-    let open ReadCap in
-    let open Type in
-    let open Value in
-    ocanren {
-      { fresh v_m, v_r, v_w,
-              r, w in
-        v == unitV (v_m, v_r, v_w) &
-        tp == UnitT (r, w) &
-        {
-          { r == R & v_r == OneRV } |
-          { r == NRd & v_r == ZeroRV } |
-          { r == NRd & v_r == TopRV }
-        } &
-        writeval_to_vapo v_w w
-         } |
-      { fresh _stmts, _ts in
-        v == FunV _stmts &
-        tp == FunT _ts } |
-      { fresh id, _c, tp', v' in
-        v == RefV id &
-        tp == RefT (_c, tp') &
-        mem_geto mem id v' &
-        tags_checko mem v' tp' } |
-      { fresh vs, ts in
-        List.mapo (tags_checko mem) vs ts }
-  }
-
   (* - statement evaluation *)
+  (* TODO *)
 
   let rec stmt_addarg_foldero vals st_with_id mtp e st_with_id' = ocanren {
     fresh st, x, m, tp, st' in
@@ -1146,26 +920,16 @@ struct
     addargo st vals x tp e st' &
     st_with_id' == Std.pair st' (Nat.s x)
   }
-  and f_tags_check_foldero mem vals x mtp x' = ocanren {
-    fresh m, tp, id', v' in
-    mtp == Std.pair m tp &
-    vals_assoco x vals id' &
-    mem_geto mem id' v' &
-    tags_checko mem v' tp &
-    x' == Nat.s x
-  }
   and stmt_eval_func_foldero mem types vals visited stmt visited' =
     let open StEnv in
     ocanren {
       { fresh visited_add, st,
-              st', mem', types', vals',
+              st', mem', types', vals' in
-              _x' in
         not_visited_checko visited stmt &
         visited_addo visited stmt visited_add &
         st == StEnv (mem, types, vals, visited_add) &
         stmt_evalo st stmt st' &
-        st' == StEnv (mem', types', vals', visited') &
+        st' == StEnv (mem', types', vals', visited') } |
-        list_foldlo (f_tags_check_foldero mem' vals') 0 ts _x' } |
       { visited_checko visited stmt &
         visited == visited' }
   }
@@ -1186,7 +950,6 @@ struct
     let open TypesEnv in
     let open ValsEnv in
     let open RevPath in
-    let open Action in
     ocanren {
       fresh mem, types, vals, visited in
       st == StEnv (mem, types, vals, visited) &
@@ -1232,25 +995,13 @@ struct
           vals_assoco x vals id &
           mem_geto mem id v &
           pathrevo p VarRP rp &
-          valupdo mem v rp AlwaysWriteA (Std.pair mem_upd v_upd) &
+          valupdo mem v rp ZeroV (Std.pair mem_upd v_upd) &
           mem_seto mem_upd id v_upd mem_set &
           st' == StEnv (mem_set, types, vals, visited) } |
-        { fresh p, tp, _r, _w, x, id, v, rp,
+        { fresh p in
-                mem_upd, v_upd, mem_set in
           s == ReadS p &
-          pathtypeo types p tp &
+          pathvalo mem vals p ZeroV &
-          tp == UnitT (_r, _w) &
+          st == st' } |
-          pathvaro p x &
-          vals_assoco x vals id &
-          mem_geto mem id v &
-          pathrevo p VarRP rp &
-          valupdo mem v rp ReadA (Std.pair mem_upd v_upd) &
-          mem_seto mem_upd id v_upd mem_set &
-          st' == StEnv (mem_set, types, vals, visited) } |
-        (* { fresh p in *)
-          (* s == ReadS p & *)
-          (* pathvalo mem vals p ZeroV & *)
-          (* st == st' } | *)
         { fresh sl, sr, stl in
           s == SeqS (sl, sr) &
           stmt_evalo st sl stl &