diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml
index a900c41..a70b099 100644
--- a/model_with_structures/analyzer.ml
+++ b/model_with_structures/analyzer.ml
@@ -73,8 +73,6 @@ struct
              | RefV of memid
              | TupleV of value list
 
-  type revpath = VarRP | DerefRP of revpath | AccessRP of revpath * data
-
   (* TODO: any additional difference between rvalue and lvalue now ?? *)
 
   (* --- *)
@@ -156,19 +154,13 @@ struct
     | DerefP p -> pathvar p
     | AccessP (p, _) -> pathvar p
 
-  let rec pathrev (p : path) (acc : revpath) : revpath = match p with
-    | VarP x -> acc
-    | DerefP p -> pathrev p @@ DerefRP acc
-    | AccessP (p, i) -> pathrev p @@ AccessRP (acc, i)
-
   let rec pathtype (types : types) (p : path) : atype = match p with
     | VarP x -> types_assoc x types
     | DerefP p -> (match pathtype types p with
                     | RefT (_, t) -> t
                     | _ -> raise @@ Typing_error "pathtype: deref")
     | AccessP (p, id) -> match pathtype types p with
-                           | TupleT ts -> (* FIXME TMP Printf.printf "pathtype access sz=%i id=%i\n" (List.length ts) id; *)
-                                          (List.nth ts id)
+                           | TupleT ts -> (List.nth ts id)
                            | _ -> raise @@ Typing_error "pathtype: access"
 
   let rec pathval (mem :  mem) (vals : vals) (p : path) : value = match p with
@@ -182,8 +174,7 @@ struct
                     | RefV id -> mem_get mem id
                     | _ -> raise @@ Typing_error "pathval: deref")
     | AccessP (p, id) -> match pathval mem vals p with
-                           | TupleV vs -> (* FIXME TMP Printf.printf "pathval access sz=%i id=%i\n" (List.length vs) id; *)
-                                          (List.nth vs id)
+                           | TupleV vs -> (List.nth vs id)
                            | _ -> raise @@ Typing_error "pathval: access"
 
   (* --- eval rules --- *)
@@ -217,14 +208,12 @@ struct
 
   (* - value update *)
 
-  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') = valupd mem (mem_get mem id) p b in
-                            (mem_set mem' id v', RefV id)
-    | AccessRP (p, id), TupleV vs -> let (mem', v') = (* FIXME TMP Printf.printf "vs size=%i id=%i\n" (List.length vs) id; *)
-                                                      valupd mem (List.nth vs id) p b in
-                                     (* FIXME TMP Printf.printf "before return\n"; *)
-                                     (mem', TupleV (list_replace vs id v'))
+  let rec valupd (mem : mem) (v : value) (p : path) (b : value) : mem * value = match p, v with
+    | VarP x, _ -> (mem, b)
+    | DerefP p, RefV id -> let (mem', v') = valupd mem (mem_get mem id) p b in
+                           (mem_set mem' id v', RefV id)
+    | AccessP (p, id), TupleV vs -> let (mem', v') = valupd mem (List.nth vs id) p b in
+                                    (mem', TupleV (list_replace vs id v'))
     | _, _ -> raise @@ Typing_error "valupd"
 
   (* - value combination *)
@@ -327,7 +316,7 @@ struct
         let folder = fun (mem, vs') t u v ->
           let (mem', v') = valspoil mem v t u m c in (mem', v' :: vs') in
         let (mem', vs') = list_foldl3 folder (mem, []) ts us vs in
-        (mem', TupleV (List.rev vs'))
+        (mem', TupleV vs')
     | _, _, _ ->  raise @@ Typing_error "valspoil"
 
   (* full spoil *)
@@ -339,9 +328,8 @@ struct
     let b = pathval mem vals p in (* subvalue in var *)
     let t' = pathtype types p in (* type of 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'') = valupd mem' (mem_get mem' id) pi b' in (* set subvalue into var *)
+    (* TODO: FIXME: why copy (Cp)? *)
+    let (mem'', v'') = valupd mem' (mem_get mem' id) p b' in (* set subvalue into var *)
     mem_set mem'' id v''
 
   let rec argsspoile (state : state) (m : mode) (t : atype) (e : expr) : mem =
@@ -411,11 +399,8 @@ struct
                        then raise @@ Eval_error "write: write tag"
                        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 ZeroV in
+                            let (mem', v') = valupd mem (mem_get mem id) p 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 -> if pathval mem vals p == SmthV || pathval mem vals p == BotV 
                  then raise @@ Eval_error "read: spoiled value"
@@ -882,8 +867,6 @@ struct
 
   (* - complex tests *)
 
-  (* NOTE: path access isreversed to intuitive function application
-           by definition *)
   let%expect_test "complex test: send, dsl" =
     prog_eval_noret (
       (* TODO: set optimal ref mods later *)
@@ -912,33 +895,38 @@ struct
       let sendID = vg9 in
       let send_allID = vg10 in
       let get_version_idF = FunD ([moded requestT],
-        (rdS @@ access 0 @@ drf @@ access 1 v0) |. skp) in
+        (* (rdS @@ access 1 @@ drf @@ access 0 v0) |. skp) in *)
+         skp) in
+      (* TODO: real op paths *)
       let updated_versionF = FunD ([moded requestT],
-        (rdS @@ access 0 @@ drf @@ access 2 v0) #.
+        (* (rdS @@ access 2 @@ drf @@ access 0 v0) #. *)
         (* TODO: read all the substructure ?? *)
-        (rdS @@ access 0 @@ drf @@ access 1 v0) #.
-        (rdS @@ access 1 @@ drf @@ access 1 v0)) in
+        (* (rdS @@ access 1 @@ drf @@ access 0 v0) #. *)
+        (* (rdS @@ access 1 @@ drf @@ access 1 v0)) in *)
+         skp) in
       let sendF = FunD ([moded requestT],
-        ((
-           (wrS @@ access 0 @@ drf @@ access 2 v0) #.
-           (rdS @@ drf @@ access 3 v0) #.
-           (wrS @@ drf @@ access 3 v0) #.
-           (rdS @@ access 0 @@ drf @@ access 1 @@ drf @@ access 0 v0)
-         ) |. skp) #.
-         (wrS @@ access 4 v0) #.
+        (* (( *)
+           (* (wrS @@ access 2 @@ drf @@ access 0 v0) #. *)
+           (* (rdS @@ access 3 @@ drf v0) #. *)
+           (* (wrS @@ access 3 @@ drf v0) #. *)
+           (* (rdS @@ access 0 @@ drf @@ access 1 @@ drf @@ access 0 v0) *)
+         (* ) |. skp) #. *)
+         (* (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 *) *)
+         skp) in
       let send_allF = FunD ([moded requestT],
         (wrS @@ access 4 v0) (*wrS v0*) #. (* FIXME: TMP, parial write, should be full *)
-        (callS sendID [pE v0]) #.
-        (callS get_version_idID [pE v0]) #.
-        (callS updated_versionID [pE v0]) #.
+        (* (callS sendID [pE v0]) #. *)
+        (* (callS get_version_idID [pE v0]) #. *)
+        (* (callS updated_versionID [pE v0]) #. *)
         (* TODO: read all the substructure ?? *)
-        (wrS @@ access 0 @@ drf @@ access 1 v0) #.
-        (wrS @@ access 1 @@ drf @@ access 1 v0) #.
+        (wrS @@ access 1 @@ drf @@ access 0 v0) #.
+        (* (wrS @@ access 1 @@ drf @@ access 1 v0) #. *)
         (* --- *)
-        ((rdS @@ access 0 @@ drf @@ access 0 @@ drf @@ access 0 v0) |.
-         (rdS @@ access 0 @@ drf @@ access 1 v0))) in
+        (* ((rdS @@ access 0 @@ drf @@ access 0 @@ drf @@ access 0 v0) |. *)
+         (* (rdS @@ access 2 @@ drf @@ access 0 v0))) in *)
+         skp) in
       let varID = vg6 in
       [
         defg user_utilsT user_utilsE;
@@ -952,11 +940,315 @@ struct
         updated_versionF;
         sendF;
         send_allF
+        (* TODO: var def *)
       ],
       callS send_allID [pE varID]
     );
     Printf.printf "done!";
     [%expect {| done! |}]
 
-  (* TODO: version with more optimal modifiers *)
+  (* --- FIXME --- CURRENT REWRITE POINT --- FIXME --- *)
+
+  (* --- tests --- *)
+
+  (* let rwi_value : tag = (Rd, AlwaysWr, Cp, In, NOut) *)
+  (* let rmwi_value : tag = (Rd, MayWr, Cp, In, NOut) *)
+  (* let ri_value : tag = (Rd, NeverWr, Cp, In, NOut) *)
+  (* let wi_value : tag = (NRd, AlwaysWr, Cp, In, NOut) *)
+  (* let mwi_value : tag = (NRd, MayWr, Cp, In, NOut) *)
+  (* let i_value : tag = (NRd, NeverWr, Cp, In, NOut) *)
+  (* let rwi_ref : tag = (Rd, AlwaysWr, Rf, In, NOut) *)
+  (* let rmwi_ref : tag = (Rd, MayWr, Rf, In, NOut) *)
+  (* let ri_ref : tag = (Rd, NeverWr, Rf, In, NOut) *)
+  (* let wi_ref : tag = (NRd, AlwaysWr, Rf, In, NOut) *)
+  (* let mwi_ref : tag = (NRd, MayWr, Rf, In, NOut) *)
+  (* let i_ref : tag = (NRd, NeverWr, Rf, In, NOut) *)
+
+  (* >> tests without functions *)
+
+  (* let%expect_test "empty" = *)
+    (* eval_prog ([], ([], [])); *)
+    (* Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  (* let%expect_test "ref param in main failure" = *)
+    (* try (eval_prog ([], ([i_ref], [])); *)
+         (* [%expect.unreachable]) *)
+    (* with Ref_rvalue_argument id -> Printf.printf "%i" id; *)
+    (* [%expect {| 0 |}] *)
+
+  (* let%expect_test "read empty args" = *)
+    (* try (eval_prog ([], ([], [Read 0])); *)
+         (* [%expect.unreachable]) *)
+    (* with Not_found -> Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  (* let%expect_test "write empty args" = *)
+    (* try (eval_prog ([], ([], [Write 0])); *)
+         (* [%expect.unreachable]) *)
+    (* with Not_found -> Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  (* let%expect_test "simple write" = *)
+    (* eval_prog ([], ([wi_value], [Write 0])); *)
+    (* Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  (* let%expect_test "simple read" = (* NOTE: should not work with read-before-write check*) *)
+    (* eval_prog ([], ([ri_value], [Read 0])); *)
+    (* Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  (* let%expect_test "multiple read & write" = *)
+    (* eval_prog ([], ([rwi_value], [Write 0; Read 0; Write 0; Write 0; Read 0; Read 0])); *)
+    (* Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  (* let%expect_test "multiple read & write, multiple args" = *)
+    (* eval_prog ([], ([wi_value; wi_value; wi_value], [Write 0; Read 0; Write 1; Write 0; Write 2; Read 1; Write 2; Read 0; Read 2])); *)
+    (* Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  (* let%expect_test "main, access out of range" = *)
+    (* try(eval_prog ([], ([wi_value], [Write 0; Read 5 ])); *)
+         (* [%expect.unreachable]) *)
+    (* with Not_found -> Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  (* let%expect_test "main, access out of range" = *)
+    (* try(eval_prog ([], ([wi_value], [Write 0; Write 5 ])); *)
+         (* [%expect.unreachable]) *)
+    (* with Not_found -> Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  (* >> tests with one function *)
+
+  (* let%expect_test "simple function call with value arg" = *)
+    (* eval_prog ([([wi_value], [Write 0; Read 0; Write 0])], ([wi_value], [Write 0; Call (0, [0]) ])); *)
+    (* Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  (* let%expect_test "simple function call with ref arg" = *)
+    (* eval_prog ([([wi_ref], [Write 0; Read 0; Write 0])], ([wi_value], [Write 0; Call (0, [0]) ])); *)
+    (* Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  (* let%expect_test "function with value arg & read" = *)
+    (* eval_prog ([([wi_value], [Write 0; Read 0; Write 0])], ([wi_value], [Write 0; Call (0, [0]); Read 0 ])); *)
+    (* Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  (* --- *)
+
+  (* let%expect_test "function with ref arg & read" = *)
+    (* try (eval_prog ([([rwi_ref], [Read 0; Write 0])], ([wi_value], [Write 0; Call (0, [0]); Read 0 ])); *)
+         (* [%expect.unreachable]) *)
+    (* with Incorrect_memory_access id -> Printf.printf "%i" id; *)
+    (* [%expect {| 0 |}] *)
+
+  (* let%expect_test "function with ref arg & call twice" = *)
+    (* try (eval_prog ([([rwi_ref], [Read 0; Write 0])], ([wi_value], [Write 0; Call (0, [0]); Call (0, [0]) ])); *)
+         (* [%expect.unreachable]) *)
+    (* with Incorrect_memory_access id -> Printf.printf "%i" id; *)
+    (* [%expect {| 0 |}] *)
+
+  (* NOTE: behaviour is fixed with new capabilities *)
+  (* let%expect_test "function with ref arg, write first & call twice" = *)
+    (* eval_prog ([([wi_ref], [Write 0; Read 0; Write 0])], ([wi_value], [Write 0; Call (0, [0]); Call (0, [0]) ])); *)
+    (* Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+
+  (* let%expect_test "function with ref arg & read, write" = *)
+    (* try (eval_prog ([([rwi_ref], [Read 0; Write 0])], ([wi_value], [Write 0; Call (0, [0]); Read 0; Write 0 ])); *)
+         (* [%expect.unreachable]) *)
+    (* with Incorrect_memory_access id -> Printf.printf "%i" id; *)
+    (* [%expect {| 0 |}] *)
+
+  (* let%expect_test "function with ref arg & write, read" = *)
+    (* eval_prog ([([rwi_ref], [Read 0; Write 0])], ([wi_value], [Write 0; Call (0, [0]); Write 0; Read 0 ])); *)
+    (* Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  (* let%expect_test "function with ref arg, no write inside & read" = *)
+    (* eval_prog ([([ri_ref], [Read 0; Read 0])], ([wi_value], [Write 0; Call (0, [0]); Read 0 ])); *)
+    (* Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  (* --- *)
+
+  (* let%expect_test "function with value arg, read out of range" = *)
+    (* try(eval_prog ([([ri_ref], [Read 0; Read 1])], ([wi_value; i_value], [Write 0; Call (0, [0]); Read 0 ])); *)
+         (* [%expect.unreachable]) *)
+    (* with Not_found -> Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  (* let%expect_test "function with ref arg, read out of range" = *)
+    (* try(eval_prog ([([ri_ref], [Read 0; Read 1])], ([wi_value; i_value], [Write 0; Call (0, [0]); Read 0 ])); *)
+         (* [%expect.unreachable]) *)
+    (* with Not_found -> Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  (* let%expect_test "function with value arg, write out of range" = *)
+    (* try(eval_prog ([([rwi_value], [Read 0; Write 1])], ([wi_value; i_value], [Write 0; Call (0, [0]); Read 0 ])); *)
+         (* [%expect.unreachable]) *)
+    (* with Not_found -> Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  (* let%expect_test "function with value arg, call out of range" = *)
+    (* try(eval_prog ([([ri_value], [Read 0])], ([wi_value; i_value], [Write 0; Call (0, [2]); Read 0 ])); *)
+         (* [%expect.unreachable]) *)
+    (* with Not_found -> Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  (* --- *)
+
+  (* let%expect_test "function with ref & value args, no write inside & read" = *)
+    (* eval_prog ( *)
+      (* [([ri_ref; ri_value], [Read 0; Read 1])], *)
+      (* ([wi_value; wi_value], [Write 0; Write 1; Call (0, [0; 1]); Read 0; Read 1 ])); *)
+    (* Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  (* let%expect_test "function with ref & value args, write value inside & read" = *)
+    (* eval_prog ( *)
+      (* [([ri_ref; rwi_value], [Read 0; Read 1; Write 1; Read 1])], *)
+      (* ([wi_value; wi_value], [Write 0; Write 1; Call (0, [0; 1]); Read 0; Read 1 ])); *)
+    (* Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  (* let%expect_test "function with ref & value args, write both inside & read" = *)
+    (* try (eval_prog ( *)
+      (* [([rwi_ref; rwi_value],[Read 0; Read 1; Write 0; Write 1; Read 1])], *)
+      (* ([wi_value; wi_value], [Write 0; Write 1; Call (0, [0; 1]); Read 0; Read 1 ])); *)
+         (* [%expect.unreachable]) *)
+    (* with Incorrect_memory_access id -> Printf.printf "%i" id; *)
+    (* [%expect {| 0 |}] *)
+
+  (* --- *)
+
+  (* let%expect_test "function with ref two same ref args, read both & read" = *)
+    (* eval_prog ( *)
+      (* [([ri_ref; ri_ref],[Read 0; Read 1; Read 1])], *)
+      (* ([wi_value], [Write 0; Call (0, [0; 0]); Read 0 ])); *)
+    (* Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  (* let%expect_test "function with ref two same ref args, read both & nothing" = *)
+    (* eval_prog ( *)
+      (* [([ri_ref; ri_ref],[Read 0; Read 1; Read 1])], *)
+      (* ([wi_value], [Write 0; Call (0, [0; 0]); ])); *)
+    (* Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  (* let%expect_test "function with ref & copy of the same arg, read & write both & nothing" = *)
+    (* eval_prog ( *)
+      (* [([rwi_ref; rwi_value],[Read 0; Read 1; Write 0; Write 1; Read 1])], *)
+      (* ([wi_value], [Write 0; Call (0, [0; 0]); ])); *)
+    (* Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  (* let%expect_test "function with copy & ref of the same arg, read & write both & nothing" = *)
+    (* eval_prog ( *)
+      (* [([rwi_value; rwi_ref],[Read 0; Read 1; Write 0; Write 1; Read 1])], *)
+      (* ([wi_value], [Write 0; Call (0, [0; 0]); ])); *)
+    (* Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  (* TODO: FIXME: now correct (use state before for mem check), is this good ?, proper way to fix ? *)
+  (* let%expect_test "function with ref two same ref args, read & write both, error" = *)
+    (* try ( *)
+      (* eval_prog ( *)
+      (* [([rwi_ref; rwi_ref],[Read 0; Read 1; Write 0; Write 1; Read 1])], *)
+      (* ([wi_value], [Write 0; Call (0, [0; 0]); ])); *)
+    (* Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  (* >> tests with several functions *)
+
+  (* let%expect_test "two functions with ref arg, read func -> write func" = *)
+    (* eval_prog ( *)
+      (* [([ri_ref], [Read 0]); ([wi_ref], [Write 0])], *)
+      (* ([wi_value], [Write 0; Call (0, [0]); Read 0; Call (1, [0]) ])); *)
+    (* Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  (* let%expect_test "two functions with ref arg, write func -> read func" = *)
+    (* try (eval_prog ( *)
+      (* [([ri_ref], [Read 0]); ([wi_ref], [Write 0])], *)
+      (* ([wi_value], [Write 0; Call (1, [0]); Call (0, [0]) ])); *)
+         (* [%expect.unreachable]) *)
+    (* with Incorrect_memory_access id -> Printf.printf "%i" id; *)
+    (* [%expect {| 0 |}] *)
+
+  (* let%expect_test "two functions: ref arg after value arg" = *)
+    (* eval_prog ( *)
+      (* [([rwi_ref], [Read 0; Write 0]); ([rwi_value], [Read 0; Write 0])], *)
+      (* ([wi_value], [Write 0; Call (1, [0]); Read 0; Call (0, [0]) ])); *)
+    (* Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  (* let%expect_test "two functions: value arg after spoiled ref arg" = *)
+    (* try (eval_prog ( *)
+      (* [([rwi_ref], [Read 0; Write 0]); ([rwi_value], [Read 0; Write 0])], *)
+      (* ([wi_value], [Write 0; Call (0, [0]); Call (1, [0]) ])); *)
+         (* [%expect.unreachable]) *)
+    (* with Incorrect_memory_access id -> Printf.printf "%i" id; *)
+    (* [%expect {| 0 |}] *)
+
+  (* --- *)
+
+  (* let%expect_test "simple function call with value arg, const cast error" = *)
+    (* try (eval_prog ([([ri_value], [Write 0; Read 0; Write 0])], ([wi_value], [Write 0; Call (0, [0]) ])); *)
+         (* [%expect.unreachable]) *)
+    (* with Incorrect_const_cast id -> Printf.printf "%i" id; *)
+    (* [%expect {| 0 |}] *)
+
+  (* let%expect_test "simple function call with ref arg, const cast error" = *)
+    (* try (eval_prog ([([ri_ref], [Write 0; Read 0; Write 0])], ([wi_value], [Write 0; Call (0, [0]) ])); *)
+         (* [%expect.unreachable]) *)
+    (* with Incorrect_const_cast id -> Printf.printf "%i" id; *)
+    (* [%expect {| 0 |}] *)
+
+  (* let%expect_test "simple function call with value arg, const cast ok" = *)
+    (* eval_prog ([([ri_value], [Read 0])], ([wi_value], [Write 0; Call (0, [0]) ])); *)
+    (* Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  (* let%expect_test "simple function call with ref arg, const cast ok" = *)
+    (* eval_prog ([([ri_ref], [Read 0])], ([wi_value], [Write 0; Call (0, [0]) ])); *)
+    (* Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  (* --- *)
+
+  (* let%expect_test "simple function call with arg, recursive calls" = *)
+    (* eval_prog ([([rwi_value], [Write 0; Read 0; Write 0; Call (0, [0])])], ([wi_value], [Write 0; Call (0, [0]) ])); *)
+    (* Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  (* --- *)
+
+  (* TODO: out arguments test, etc. *)
+
+  (* --- *)
+
+  (* TODO: more Combine statement tests *)
+
+  (* let%expect_test "simple function call with value arg and choice, rw" = *)
+    (* eval_prog ([([wi_value], [Choice ([Write 0; Read 0], [Write 0]); Read 0])], ([wi_value], [Write 0; Call (0, [0]) ])); *)
+    (* Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  (* let%expect_test "simple function call with ref arg and choice, rw" = *)
+    (* try (eval_prog ([([ri_ref], [Choice ([Read 0], [Write 0])])], ([wi_value], [Write 0; Call (0, [0]) ])); *)
+         (* [%expect.unreachable]) *)
+    (* with Incorrect_const_cast id -> Printf.printf "%i" id; *)
+    (* [%expect {| 0 |}] *)
+
+  (* let%expect_test "simple function call with ref arg and choice, rr" = *)
+    (* eval_prog ([([ri_ref], [Choice ([Read 0], [Read 0; Read 0])])], ([wi_value], [Write 0; Call (0, [0]) ])); *)
+    (* Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
 end
diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ
index ae6fc97..b3bc24b 100644
--- a/model_with_structures/model.typ
+++ b/model_with_structures/model.typ
@@ -153,7 +153,6 @@
 
 #let deepValue = `deepvalue`
 #let value = `value`
-#let revpath = $#[`path`]_#[`rev`]$
 
 #bnf(
   Prod(
@@ -178,22 +177,12 @@
       Or[$[value+]$][tuple value] // `Prod`
     }
   ),
-  Prod(
-    revpath,
-    {
-      Or[$\# .$][value by itself]
-      Or[$rf revpath$][reference to value]
-      Or[$n . revpath$][tuple with value as $n$-th element]
-    }
-  ),
 )
 
 #deepValue - полное значение, #value - слой значения, привязан к конкретной памяти $mu$
 
 Значения, могут лежать в переменных и передаваться как аргументы функций (то, во что вычисляется $expr$)
 
-$revpath$ - путь в обратную сторону, используется для обновления значений
-
 $v in value$ - произвольное значение
 
 Получение #deepValue по #value:
@@ -240,7 +229,7 @@ $sigma : envt := X -> type, space types : envt$ - #[ типы значений 
 // $DD : X -> decl$ - глобальные определения, частично определённая функция
 
 // $d in decl, $
-$s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
+$s in stmt, f in X, x in X, a in X$
 
 === Path Accessors
 
@@ -252,7 +241,6 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
 #let arrmu = $attach(->, br: mu)$
 
 #let arrpath = $xarrowSquiggly(space)_path$
-#let arrrevpath = $xarrowSquiggly(space)_#[rev path]$
 
 #let ttype = $attach(tack.r, br: type)$
 #let tmode = $attach(tack.r, br: mode)$
@@ -260,7 +248,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
 #let val = `val`
 #let tval = $attach(tack.r, br: val)$
 
-- #[ Соответствующая пути переменная
+- #[ Конструирование путей по переменой
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
@@ -275,7 +263,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
     name: [ reference path],
 
     $p arrpath x$,
-    $* p arrpath x$,
+    $rf p arrpath x$,
   )
 ))
 #align(center, prooftree(
@@ -290,36 +278,6 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
 ))
 ]
 
-- #[ Обращение пути
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ variable path],
-
-    $@x arrrevpath^pi pi$,
-  )
-))
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ reference path],
-
-    $p arrrevpath^(rf pi) pi'$,
-    $*p arrrevpath^pi pi'$,
-  )
-))
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ tuple access path],
-
-    $p arrrevpath^(i.pi) pi'$,
-
-    $p.i arrrevpath^pi pi'$,
-  )
-))
-]
-
 - #[ Получение типа поля
 #align(center, prooftree(
   vertical-spacing: 4pt,
@@ -551,6 +509,16 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
 
 #let modify = `modify`
 
+// #align(center, prooftree(
+//   vertical-spacing: 4pt,
+//   rule(
+//     name: [ modify trivial value],
+
+//     $v in {0, \#, bot}$,
+//     $cl v, mu cr xarrowSquiggly(cl \@ x \, b cr)_modify cl b, mu cr$,
+//   )
+// ))
+
 // TODO: add type check ??
 #align(center, prooftree(
   vertical-spacing: 4pt,
@@ -558,7 +526,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
     name: [ modify end value],
 
     // $v in {0, \#, bot}$,
-    $cl v, mu cr xarrowSquiggly(cl \# . \, b cr)_modify cl b, mu cr$,
+    $cl v, mu cr xarrowSquiggly(cl \@ x \, b cr)_modify cl b, mu cr$,
   )
 ))
 
@@ -569,8 +537,8 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
   rule(
     name: [ new reference copy value],
 
-    $cl mu[l], mu cr xarrowSquiggly(cl pi \, b cr)_modify cl v', mu' cr$,
-    $cl rf l, mu cr xarrowSquiggly(cl rf pi \, b cr)_modify cl rf l, mu'[l <- v'] cr$,
+    $cl mu[l], mu cr xarrowSquiggly(cl p \, b cr)_modify cl v', mu' cr$,
+    $cl rf l, mu cr xarrowSquiggly(cl *p \, b cr)_modify cl rf l, mu'[l <- v'] cr$,
   )
 ))
 
@@ -582,7 +550,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
     name: [ modify tuple value],
 
     $cl v_i, mu cr xarrowSquiggly(cl p \, b cr)_modify cl v'_i, mu', cr$,
-    $cl [v_1, ... v_i, ... v_n], mu cr xarrowSquiggly(cl i.pi \, b cr)_modify cl [v_1, ... v'_i, ... v_n], mu' cr$,
+    $cl [v_1, ... v_i, ... v_n], mu cr xarrowSquiggly(cl p.i \, b cr)_modify cl [v_1, ... v'_i, ... v_n], mu' cr$,
   )
 ))
 
@@ -944,8 +912,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
     // <- otherwise all subsequent copy capabilities will be ref (in current impl)
     // FIXME depends on parent ??
     $cl b, mu cr xarrowSquiggly(t \, t' \, m \, Copy)_spoil cl b', mu' cr$,
-    $p arrrevpath^(\#.) pi$,
-    $cl mu'[l], mu' cr xarrowSquiggly(cl pi \, b' cr)_modify cl v'', mu'' cr$,
+    $cl mu'[l], mu' cr xarrowSquiggly(cl p \, b' cr)_modify cl v'', mu'' cr$,
 
     $mu stretch(=>)^(m space t space p)_(cl vals, types cr) mu''[l <- v'']$,
   )
@@ -1088,8 +1055,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
     $w = MaybeWrite or w = AlwaysWrite$,
     $p arrpath x$,
     $l = vals[x]$,
-    $p arrrevpath^(\#.) pi$,
-    $mu[l] xarrowSquiggly(cl pi \, 0 cr)_modify v'$,
+    $mu[l] xarrowSquiggly(cl p \, 0 cr)_modify v'$,
 
     $cl types, vals, mu cr
      xarrow("WRITE" p)
diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml
index 99de175..2030de9 100644
--- a/model_with_structures/synthesizer.ml
+++ b/model_with_structures/synthesizer.ml
@@ -105,6 +105,7 @@ struct
     (* end *)
   end
 
+  (* TODO: access: data or int ? *)
   module Path = struct
     [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
     [%%ocanren_inject
@@ -173,15 +174,6 @@ struct
     ]
   end
 
-  module RevPath = struct
-    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
-    [%%ocanren_inject
-      type nonrec ('d, 'p) t = VarRP | DerefRP of 'p | AccessRP of 'p * 'd
-      [@@deriving gt ~options:{ show; gmap }]
-      type ground = (Nat.ground, ground) t
-    ]
-  end
-
   (* --- *)
 
   module MemEnv = struct
@@ -470,21 +462,6 @@ struct
       { fresh p', _id in p == AccessP (p', _id) & pathvaro p' x }
   }
 
-  let rec pathrevo p rp rp' =
-    let open Path in
-    let open RevPath in
-    ocanren {
-      { fresh _x in
-        p == VarP _x &
-        rp == rp' } |
-      { fresh p' in
-        p == DerefP p' &
-        pathrevo p' (DerefRP rp) rp' } |
-      { fresh p', id in
-        p == AccessP (p', id) &
-        pathrevo p' (AccessRP (rp, id)) rp' }
-  }
-
   let rec pathtypeo types p tp =
     let open Path in
     let open Type in
@@ -565,32 +542,33 @@ struct
         v == TupleV vs &
         tp == TupleT tps &
         list_foldl2o valcopy_foldero (Std.pair mem []) vs tps (Std.pair mem' vs') &
-        List.reverso vs' vs'' &
+         == mem_with_vs' &
+        List.reverso vs' vs''
         mem_with_id' == Std.pair mem' (TupleV vs'') }
   }
 
   (* - value update *)
 
-  (* NOTE: reversed path used *)
-  let rec valupdo mem v rp b mem_with_v' =
-    let open RevPath in
+  let rec valupdo mem v p b mem_with_v' =
+    let open Path in
     let open Value in
     ocanren {
-      { rp == VarRP &
+      { fresh x in
+        p == VarP x &
         mem_with_v' == Std.pair mem b } |
-      { fresh rp', id, v', mem_upd, v_upd, mem_with_v_upd, mem_st in
-        rp == DerefRP rp' &
+      { fresh p', id, v', mem_upd, v_upd, mem_with_v_upd, mem_st in
+        p == DerefP p' &
         v == RefV id &
         mem_geto mem id v' &
-        valupdo mem v' rp' b mem_with_v_upd &
+        valupdo mem v' p' 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) } |
-      { fresh rp', id, vs', v', mem_upd, v_upd, mem_with_v_upd, vs_upd in
-        rp == AccessRP (rp', id) &
+      { fresh p', id, vs', v', mem_upd, v_upd, mem_with_v_upd, vs_upd in
+        p == AccessP (p', id) &
         v == TupleV vs' &
         list_ntho vs' id v' &
-        valupdo mem v' rp' b mem_with_v_upd &
+        valupdo mem v' p' 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) }
@@ -813,15 +791,14 @@ struct
         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, vs_sp' in
+      { fresh tps, us, vs, mem_sp,vs_sp in
         tp == TupleT tps &
         u == TupleT us &
         v == TupleV vs &
         list_foldl3o (valspoil_foldero m c)
                      (Std.pair mem []) tps us vs
                      (Std.pair mem_sp vs_sp) &
-        List.reverso vs_sp vs_sp' &
-        mem_with_v' == Std.pair mem_sp (TupleV vs_sp')
+        mem_with_v' == Std.pair mem_sp (TupleV vs_sp)
       }
   }
 
@@ -830,10 +807,9 @@ struct
   let argspoilpo st m tp p mem' =
     let open StEnv in
     let open CopyCap in
-    let open RevPath in
     ocanren {
       fresh mem, types, vals, visited,
-            x, id, b, tp', rp,
+            x, id, b, tp',
             mem_sp, b_sp, v_sp, mem_upd, v_upd in
       st == StEnv (mem, types, vals, visited) &
       pathvaro p x &
@@ -842,8 +818,7 @@ struct
       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 &
-      valupdo mem_sp v_sp rp b_sp (Std.pair mem_upd v_upd) &
+      valupdo mem_sp v_sp p b_sp (Std.pair mem_upd v_upd) &
       mem_seto mem_upd id v_upd mem'
   }
 
@@ -939,7 +914,6 @@ struct
     let open WriteCap in
     let open TypesEnv in
     let open ValsEnv in
-    let open RevPath in
     ocanren {
       fresh mem, types, vals, visited in
       st == StEnv (mem, types, vals, visited) &
@@ -975,7 +949,7 @@ struct
                        mem tps es mem_spoiled &
           st' == StEnv (mem_spoiled, types, vals, visited')
         } |
-        { fresh p, tp, _r, w, x, id, v, rp,
+        { fresh p, tp, _r, w, x, id, v,
                 mem_upd, v_upd, mem_set in
           s == WriteS p &
           pathtypeo types p tp &
@@ -984,8 +958,7 @@ struct
           pathvaro p x &
           vals_assoco x vals id &
           mem_geto mem id v &
-          pathrevo p VarRP rp &
-          valupdo mem v rp ZeroV (Std.pair mem_upd v_upd) &
+          valupdo mem v p 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 in