From 18d19051c4d98732d8dfd19849eb131aaa117eb3 Mon Sep 17 00:00:00 2001
From: ProgramSnail <purpurebacterium@yandex.ru>
Date: Sat, 25 Apr 2026 14:51:38 +0000
Subject: [PATCH 1/8] structures: combine in shared memory

---
 model_with_structures/model.typ | 146 ++++++++++++++++++++++++++------
 1 file changed, 121 insertions(+), 25 deletions(-)

diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ
index 0968b8b..db684fe 100644
--- a/model_with_structures/model.typ
+++ b/model_with_structures/model.typ
@@ -529,7 +529,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
 
 === Value Construction
 
-// TODO: FIXME:add ref / copy modes correctness check
+// TODO: FIXME:add ref / copy modes correctness check ??
 
 #let new = `new`
 
@@ -538,7 +538,6 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ new $0$ value],
 
-    // TODO: check that access is what required ??
     $cl 0, mu cr xarrowSquiggly(cl r\, w cr)_new cl 0, mu cr$,
   )
 ))
@@ -548,7 +547,6 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ new $\#$ value],
 
-    // TODO: check that access is what required ??
     $cl \#, mu cr xarrowSquiggly(cl r\, w cr)_new cl \#, mu cr$,
   )
 ))
@@ -611,9 +609,125 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
 
 === Value Update
 
-#let write = `write`
+#let modify = `modify`
 
-*TODO: write to value*
+#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$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ new reference copy value],
+
+    $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$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ modify tuple value],
+
+    $v in {0, \#, bot}$,
+    $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 p.i \, b cr)_modify cl [v_1, ... v'_i, ... v_n], mu' cr$,
+  )
+))
+
+#h(10pt)
+
+=== Value Combination
+
+#let combine = `combine`
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ combine trivial $0$ values],
+
+    $mu xarrowSquiggly(cl 0 \, 0 cr)_combine cl 0, mu cr$
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ combine trivial $bot$ values],
+
+    $mu xarrowSquiggly(cl bot \, bot cr)_combine cl bot, mu cr$
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ combine other trivial values],
+
+    $v_1 in {0, \#, bot}$,
+    $v_2 in {0, \#, bot}$,
+    $v_1 != v_2$,
+    $mu xarrowSquiggly(cl v_1 \, v_2 cr)_combine cl \#, mu cr$
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ combine lambda values],
+
+    $mu xarrowSquiggly(cl lambda \, lambda cr)_combine cl lambda, mu cr$
+  )
+))
+
+#h(10pt)
+
+// NOTE: combine inplace, destroy values (actually only the first value)
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ combine reference values (inplace)],
+
+    $mu xarrowSquiggly(cl mu[l_1] \, mu[l_2] cr)_combine cl v', mu' cr$,
+    // NOTE: not inplace variant // TODO FIXME: choose variant
+    // $mu' xarrowSquiggly(v')_#[add] cl rf l', mu'' cr$,
+    // $mu xarrowSquiggly(cl rf l_1 \, rf l_2 cr)_combine cl rf l', mu'' cr$
+    $mu xarrowSquiggly(cl rf l_1 \, rf l_2 cr)_combine cl rf l_1, mu'[l_1 <- v'] cr$
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ combine tuple values],
+
+    $mu_0 xarrowSquiggly(cl v^1_1 \, v^2_1 cr)_combine cl v'_1, mu_1 cr$,
+    $...$,
+    $mu_(n - 1) xarrowSquiggly(cl v^1_n \, v^2_n cr)_combine cl v'_n, mu_n cr$,
+    $mu_0 xarrowSquiggly(cl [v^1_1, ... v^1_n] \, [v^2_1 ... v^2_n] cr)_combine cl [v'_1, ... v'_n], mu_n cr$
+  )
+))
+
+#h(10pt)
 
 === Call Finalization
 
@@ -788,11 +902,11 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
     $types ttype p : cl r, w cr$,
     $w = MaybeWrite or w = AlwaysWrite$,
     $p arrpath x$,
-    $mu[x] xarrowSquiggly(p)_write v$,
+    $mu[x] xarrowSquiggly(p)_modify v'$,
 
     $cl types, vals, mu cr
      xarrow("WRITE" p)
-     cl types, vals, mu[x <- v] cr$,
+     cl types, vals, mu[x <- v'] cr$,
   )
 ))
 
@@ -819,8 +933,6 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
 
 #h(10pt)
 
-#let combine = `combine`
-
 *TODO: combine replacement* // FIXME
 #align(center, prooftree(
   vertical-spacing: 4pt,
@@ -846,20 +958,4 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   )
 ))
 
-#h(10pt)
-
-=== Combination
-
-*TODO: rewrite as rules, fix* // FIXME
-
-$ combine(mu_1, mu_2)[i] = combine_e (mu_1[i], mu_2[i]) $
-$ combine_e (bot, bot) = bot $
-$ combine_e (0, 0) = 0 $
-$ combine_e (\_, \_) = \# $
-// FIXME: ref to combined memory
-$ combine_e (rf c l_1, rf c' l_2) | c == c' = rf c combine_e(mu_1[l_1], mu_2[l_2])$
-$ combine_e (v^1_1, ... v^1_n, v^2_1 ... v^2_n) = [combine_e(v^1_1, v^2_1), ..., combine_e(v^1_n, v^2_n)]$
-$ combine_e (lambda space overline(t_1) space s_1, lambda space overline(t_2) space s_2) | overline(t_1) == overline(t_2)  = lambda space overline(t_1) space s_1 $
-// TODO: FIXME: statemient in lambda is not important ??
-
 ]

From fd29f7d3da42248057872dd70f88313208395c16 Mon Sep 17 00:00:00 2001
From: ProgramSnail <purpurebacterium@yandex.ru>
Date: Sat, 25 Apr 2026 15:07:16 +0000
Subject: [PATCH 2/8] structures: combine + combine all

---
 model_with_structures/model.typ | 47 +++++++++++++++++++++++----------
 1 file changed, 33 insertions(+), 14 deletions(-)

diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ
index db684fe..e3f1cd1 100644
--- a/model_with_structures/model.typ
+++ b/model_with_structures/model.typ
@@ -657,7 +657,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ combine trivial $0$ values],
 
-    $mu xarrowSquiggly(cl 0 \, 0 cr)_combine cl 0, mu cr$
+    $cl mu_1, mu_2, mu cr xarrowSquiggly(cl 0 \, 0 cr)_combine cl 0, mu cr$
   )
 ))
 
@@ -668,7 +668,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ combine trivial $bot$ values],
 
-    $mu xarrowSquiggly(cl bot \, bot cr)_combine cl bot, mu cr$
+    $cl mu_1, mu_2, mu cr xarrowSquiggly(cl bot \, bot cr)_combine cl bot, mu cr$
   )
 ))
 
@@ -682,7 +682,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
     $v_1 in {0, \#, bot}$,
     $v_2 in {0, \#, bot}$,
     $v_1 != v_2$,
-    $mu xarrowSquiggly(cl v_1 \, v_2 cr)_combine cl \#, mu cr$
+    $cl mu_1, mu_2, mu cr xarrowSquiggly(cl v_1 \, v_2 cr)_combine cl \#, mu cr$
   )
 ))
 
@@ -693,23 +693,25 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ combine lambda values],
 
-    $mu xarrowSquiggly(cl lambda \, lambda cr)_combine cl lambda, mu cr$
+    $cl mu_1, mu_2, mu cr xarrowSquiggly(cl lambda \, lambda cr)_combine cl lambda, mu cr$
   )
 ))
 
 #h(10pt)
 
-// NOTE: combine inplace, destroy values (actually only the first value)
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
     name: [ combine reference values (inplace)],
 
-    $mu xarrowSquiggly(cl mu[l_1] \, mu[l_2] cr)_combine cl v', mu' cr$,
-    // NOTE: not inplace variant // TODO FIXME: choose variant
+    // NOTE: standalome version
+    // $cl mu_1, mu_2, mu cr xarrowSquiggly(cl mu_1[l_1] \, mu_2[l_2] cr)_combine cl v', mu' cr$,
     // $mu' xarrowSquiggly(v')_#[add] cl rf l', mu'' cr$,
-    // $mu xarrowSquiggly(cl rf l_1 \, rf l_2 cr)_combine cl rf l', mu'' cr$
-    $mu xarrowSquiggly(cl rf l_1 \, rf l_2 cr)_combine cl rf l_1, mu'[l_1 <- v'] cr$
+    // $cl mu_1, mu_2, mu cr xarrowSquiggly(cl rf l_1 \, rf l_2 cr)_combine cl rf l', mu'' cr$
+
+    // NOTE: version to use with "combine all"
+    $l_1 = l_2$,
+    $cl mu_1, mu_2, mu cr xarrowSquiggly(cl rf l_1 \, rf l_2 cr)_combine cl rf l_1, mu cr$
   )
 ))
 
@@ -720,10 +722,28 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ combine tuple values],
 
-    $mu_0 xarrowSquiggly(cl v^1_1 \, v^2_1 cr)_combine cl v'_1, mu_1 cr$,
+    $cl mu_1, mu_2, mu'_0 cr xarrowSquiggly(cl v^1_1 \, v^2_1 cr)_combine cl v'_1, mu'_1 cr$,
     $...$,
-    $mu_(n - 1) xarrowSquiggly(cl v^1_n \, v^2_n cr)_combine cl v'_n, mu_n cr$,
-    $mu_0 xarrowSquiggly(cl [v^1_1, ... v^1_n] \, [v^2_1 ... v^2_n] cr)_combine cl [v'_1, ... v'_n], mu_n cr$
+    $cl mu_1, mu_2, mu'_(n - 1) cr xarrowSquiggly(cl v^1_n \, v^2_n cr)_combine cl v'_n, mu'_n cr$,
+    $cl mu_1, mu_2, mu'_0 cr xarrowSquiggly(cl [v^1_1, ... v^1_n] \, [v^2_1 ... v^2_n] cr)_combine cl [v'_1, ... v'_n], mu'_n cr$
+  )
+))
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ combine tuple values],
+
+    $mu'_0 = nothing$,
+    // NOTE: same labels required
+    $mu_1 = {l_1 -> v^1_1, ... l_n -> v^1_n}$,
+    $mu_2 = {l_1 -> v^2_1, ... l_n -> v^2_n}$,
+
+    $cl mu_1, mu_2, mu'_0 cr xarrowSquiggly(cl v^1_1 \, v^2_1 cr)_combine cl v'_1, mu'_1 cr$,
+    $...$,
+    $cl mu_1, mu_2, mu'_(n - 1) cr xarrowSquiggly(cl v^1_n \, v^2_n cr)_combine cl v'_n, mu'_n cr$,
+
+    $cl mu_1, mu_2 cr xarrowSquiggly(space)_#[combine all] mu'_n cr$
   )
 ))
 
@@ -933,7 +953,6 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
 
 #h(10pt)
 
-*TODO: combine replacement* // FIXME
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
@@ -949,7 +968,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
 
     $types_s = types_t$,
     $vals_s = vals_t$,
-    $mu' = combine(mu_s, mu_t)$,
+    $cl mu_s, mu_t cr xarrowSquiggly(space)_#[combine all] mu'$,
 
     // TODO changes ?? two ways ??
     $cl types, vals, mu cr

From 9d8dc1000ccbc4e9bda65f60433171fdabf5805d Mon Sep 17 00:00:00 2001
From: ProgramSnail <purpurebacterium@yandex.ru>
Date: Sat, 25 Apr 2026 15:47:46 +0000
Subject: [PATCH 3/8] structures: partial statement eval

---
 model_with_structures/model.typ | 142 ++++++++++++++++++--------------
 1 file changed, 79 insertions(+), 63 deletions(-)

diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ
index e3f1cd1..54b1187 100644
--- a/model_with_structures/model.typ
+++ b/model_with_structures/model.typ
@@ -118,7 +118,7 @@
   Prod(
     `stmt`,
     {
-      Or[`CALL` $path space expr+$][call function]
+      Or[`CALL` $path expr+$][call function]
       Or[`WRITE` $path$][write to variable]
       Or[`READ` $path$][read from variable]
       Or[$stmt ; stmt$][control flow operator, xecution ]
@@ -153,7 +153,7 @@
       Or[$0$][valid value of simple type] // `Unit`
       Or[$\#$][valid or spoiled value of simple type] // `Unit`
       Or[$bot$][spoiled value of simple type] // `Unit`
-      Or[$lambda$][function pointer value] // `Fun`
+      Or[$lambda overline(x) space stmt$][function pointer value] // `Fun`
       Or[$rf deepValue$][reference value, contains label of the value in the memory] // `Ref`
       Or[$[deepValue+]$][tuple value] // `Prod`
     }
@@ -164,7 +164,7 @@
       Or[$0$][valid value of simple type] // `Unit`
       Or[$\#$][valid or spoiled value of simple type] // `Unit`
       Or[$bot$][spoiled value of simple type] // `Unit`
-      Or[$lambda$][function pointer value] // `Fun`
+      Or[$lambda overline(x) space stmt$][function pointer value] // `Fun`
       Or[$rf LL$][reference value, contains label of the value in the memory] // `Ref`
       Or[$[value+]$][tuple value] // `Prod`
     }
@@ -204,17 +204,12 @@ $v in value$ - произвольное значение
 
 == Semantics
 
+// TODO: FIXME: add vars & funcs from global context in the beginnning
+
 // $V := memelem$ - значения памяти
 
 $X$ - можество переменных
 
-// FIXME: TMP
-#let valuemem = `valuemem`
-#let memelem = `memelem`
-#let pathenvmode = `pathenvmode`
-#let pathenvval = `pathenvval`
-#let pathenvmem = `pathenvmem`
-#let pathenvtype = `pathenvtype`
 
 #let vals = $Sigma$
 #let types = $Gamma$
@@ -734,7 +729,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ combine tuple values],
 
-    $mu'_0 = nothing$,
+    $mu'_0 = []$,
     // NOTE: same labels required
     $mu_1 = {l_1 -> v^1_1, ... l_n -> v^1_n}$,
     $mu_2 = {l_1 -> v^2_1, ... l_n -> v^2_n}$,
@@ -754,16 +749,6 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
 // FIXME: make connected to syntax
 *TODO*
 
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ spoil init],
-    $mu stretch(=>)^nothing_(cl sigma, mu cr) mu$,
-  )
-))
-
-#h(10pt)
-
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
@@ -778,7 +763,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
     $isCorrect_(cl sigma, mu cr) (mode, x)$,
 
     // gamma - memory (as mu)
-    $gamma stretch(=>)^((mode, x) : args)_sigma pathenvval(gamma, sigma, x) <- bot]$
+    $gamma stretch(=>)^((mode, x) : args)_sigma "pathenvval"(gamma, sigma, x) <- bot]$
   )
 ))
 
@@ -794,10 +779,12 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
     $isAlwaysWrite mode$, // NOTE: strong requirement: should write
     $mode = (\_, not Out)$,
 
+    // NOTE: correctness looks like this
+    // $types, vals, mu, m, c tcorrect v : cl r', w' cr -> cl r, w cr$,
     $isCorrect_(cl sigma, mu cr) (mode, x)$,
 
     // gamma - memory (as mu)
-    $gamma stretch(=>)^((mode, x) : args)_sigma pathenvval(gamma, sigma, x) <- 0]$
+    $gamma stretch(=>)^((mode, x) : args)_sigma "pathenvval"(gamma, sigma, x) <- 0]$
   )
 ))
 
@@ -823,52 +810,55 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
 
 #h(10pt)
 
+=== Expression Evaluation
+
+*TODO*
+
+=== Expresion Typing
+
+*TODO*
+
 === Function Evaluation
 
 // FIXME: make connected to syntax
 *TODO*
 
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ $(lambda a : t. d) m$],
+// #align(center, prooftree(
+//   vertical-spacing: 4pt,
+//   rule(
+//     name: [ $(lambda a : t. d) m$],
 
-    // TODO: verify that type of m is t ??
+//     // TODO: verify that type of m is t ??
 
-    $cl sigma [a <- (m, t)], mu, l cr
-     xarrowSquiggly(t)
-     cl sigma', mu', l' cr$,
+//     $cl sigma [a <- (m, t)], mu, l cr
+//      xarrowSquiggly(t)
+//      cl sigma', mu', l' cr$,
 
-    $cl sigma', mu', l' cr
-     xarrowDashed(d space @ space overline(y))
-     cl sigma'', mu'', l'' cr$,
+//     $cl sigma', mu', l' cr
+//      xarrowDashed(d space @ space overline(y))
+//      cl sigma'', mu'', l'' cr$,
 
-    $isRead mode$,
-    $not isCopy mode$,
+//     $isRead mode$,
+//     $not isCopy mode$,
 
-    // NOTE: correctness checked in CALL f
+//     // NOTE: correctness checked in CALL f
 
-    $cl sigma, mu, l cr
-     xarrowDashed((lambda a. d) space @ space x space overline(y))
-     cl sigma'', mu'', l'' cr$,
-  )
-))
+//     $cl sigma, mu, l cr
+//      xarrowDashed()
+//      cl sigma'', mu'', l'' cr$,
+//   )
+// ))
 
-#h(10pt)
+// TODO: FIXME: arrow to eval expr to value ??
+// TODO: fixme 
 
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [decl body],
+    name: [ add argument],
 
     $cl sigma, mu, l cr
-     attach(stretch(->)^overline(s), tr: *)
-     cl sigma', mu', l' cr$,
-
-    $d = overline(s)$,
-
-    $cl sigma, mu, l cr
-     xarrowDashed(d space @)
+     xarrowDashed(x space m space t space p)
      cl sigma', mu', l' cr$,
   )
 ))
@@ -877,23 +867,48 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
 
 === Statement Evaluation
 
-// FIXME: make connected to syntax
-*TODO: check type of lambda?, args from type?*
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
     name: [ CALL $f space overline(p)$],
 
-    $cl [], mu, l cr
-     xarrowDashed(f space @ space overline(p))
-     cl sigma', mu', l' cr$,
+    // TODO: FIXME: take corresponding statement & var names
+    // use eval ??
+    [*TODO: statement (from value?) + x'es \<\- expr eval ? *],
 
-    // TODO: FIXME define args in some way
-    $mu attach(stretch(=>)^args_sigma, tr: *) gamma$,
+    $types ttype f : lambda args $,
+    $args = [m_1 t_1, ... m_n t_n]$,
+    $overline(p) = [p_1, ... p_n]$,
+    $overline(x) = [x_1, ... x_n]$,
 
-    $cl sigma, mu, l cr
+    // TODO: add args before statement eval
+
+    $types_0 = []$,
+    $vals_0 = []$,
+    $mu_0 = mu$,
+
+    // NOTE: dashed arrow to fill context
+    $cl types_0, vals_0,  mu_0, l cr
+     xarrowDashed(x_1 space m_1 space t_1 space p_1)
+     cl types', vals_1, mu_1, l' cr$,
+    $...$,
+    $cl types_(n - 1), vals_(n - 1),  mu_(n - 1), l cr
+     xarrowDashed(x_n space m_n space t_n space p_n)
+     cl types', vals_n, mu_n, l' cr$,
+
+    $cl types_n, vals_n,  mu_n, l cr
+     xarrow(s)
+     cl types', vals', mu', l' cr$,
+
+    // NOTE: thick arrow to "spoil" context
+    $gamma_0 = mu$,
+    $gamma_0 stretch(=>)^(x_1 space m_1 space t_1)_(cl vals, types cr) gamma_1$,
+    $...$,
+    $gamma_(n - 1) stretch(=>)^(x_n space m_n space t_n)_(cl vals, types cr) gamma_n$,
+
+    $cl vals, types, mu, l cr
      xarrow("CALL" f space overline(p))
-     cl sigma, gamma, l cr$,
+     cl vals, types, gamma_n, l cr$,
   )
 ))
 
@@ -917,16 +932,17 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ WRITE $x$],
+    name: [ WRITE $p$],
 
     $types ttype p : cl r, w cr$,
     $w = MaybeWrite or w = AlwaysWrite$,
     $p arrpath x$,
-    $mu[x] xarrowSquiggly(p)_modify v'$,
+    $l = vals(x)$,
+    $mu[l] xarrowSquiggly(cl p \, 0 cr)_modify v'$,
 
     $cl types, vals, mu cr
      xarrow("WRITE" p)
-     cl types, vals, mu[x <- v'] cr$,
+     cl types, vals, mu[l <- v'] cr$,
   )
 ))
 

From 9d21c9955626ffaa87a0ccbfd84ce19a37574742 Mon Sep 17 00:00:00 2001
From: ProgramSnail <purpurebacterium@yandex.ru>
Date: Sat, 25 Apr 2026 16:11:29 +0000
Subject: [PATCH 4/8] structures: expr eval & typing

---
 model_with_structures/model.typ | 176 ++++++++++++++++++--------------
 1 file changed, 101 insertions(+), 75 deletions(-)

diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ
index 54b1187..7feaa10 100644
--- a/model_with_structures/model.typ
+++ b/model_with_structures/model.typ
@@ -36,6 +36,7 @@
 #let Ref = `Ref`
 #let MaybeWrite = [$diamond$ `Write`]
 #let AlwaysWrite = [$square$ `Write`]
+#let NotWrite = [$not$ `Write`]
 #let Read = `Read`
 #let In = `In`
 #let Out = `Out`
@@ -111,7 +112,8 @@
     {
       Or[$()$][value of simple type] // `Unit`
       Or[$path$][value from variable] // `Path`
-      Or[$rf expr$][reference expr] // `Ref`
+      // TODO: FIXME: decide what is the result of ref expr eval
+      // Or[$rf expr$][reference expr] // `Ref`
       Or[$[expr+]$][tuple expr] // `Prod`
     }
   ),
@@ -241,18 +243,7 @@ $s in stmt, f in X, x in X, a in X$
 #let tmode = $attach(tack.r, br: mode)$
 
 #let val = `val`
-#let label = `label`
 #let tval = $attach(tack.r, br: val)$
-#let tlabel = $attach(tack.r, br: label)$
-
-// TODO: TMP, deprecated
-// #let tetype = $attach(tack.r.double, br: type)$
-// #let temode = $attach(tack.r.double, br: mode)$
-// #let telabel = $attach(tack.r.double, br: label)$
-
-#let teval = $attach(tack.r.double, br: val)$
-
-// TODO: env mem label ??, env mem value ??
 
 - #[ Конструирование путей по переменой
 #align(center, prooftree(
@@ -358,66 +349,6 @@ $s in stmt, f in X, x in X, a in X$
 ))
 ]
 
-// TODO: FIXME: not required (trivial) ??
-// - #[ Получение метки поля
-// #align(center, prooftree(
-//   vertical-spacing: 4pt,
-//   rule(
-//     name: [ access],
-
-//     $vals, mu tval p eqmu rf l$,
-//     $vals, mu tmode p arrmu l$,
-//   )
-// ))
-// ]
-
-// TODO: not required (trivial) ??
-// - #[ Получение read-write тега поля по окружению
-// #align(center, prooftree(
-//   vertical-spacing: 4pt,
-//   rule(
-//     name: [ access],
-
-//     $x : types[x] tmode p -> cr r space w cl$,
-//     $sigma temode p -> cr r space w cl$,
-//   )
-// ))
-// ]
-
-- #[ Получение значения поля по окружению
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ access],
-
-    $x eqmu vals[x] tval p eqmu v$,
-    $types, vals, mu teval p eqmu x$,
-  )
-))
-]
-
-// FIXME: move to new mode model
-// === Mode Correctness
-
-// Функции проверки тегов, имеют тип $mode -> #[bool]$:
-
-// #let modevar = $(r space w space c space i space o)$
-
-// $ isRead modevar = r == "Read" $
-// $ isAlwaysWrite modevar = w == square "Write" $
-// $ isPossibleWrite modevar = w == diamond "Write" || w == square "Write" $
-// $ isRef modevar = c == "Ref" $
-// $ isCopy modevar = c == "Copy" $
-// $ isIn modevar = i == "In" $
-// $ isOut modevar = o == "Out" $
-
-// Требования к тегам:
-
-// $ isOut mode -> isAlwaysWrite mode $
-// $ isRead mode -> isIn mode $
-
-// TODO: rest conditions ??
-
 === Eval Rules
 
 #let args = `args`
@@ -812,11 +743,106 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
 
 === Expression Evaluation
 
-*TODO*
+// TODO: check
+
+#let eval = `eval`
+#let texpre = $attach(tack.r.double, br: eval)$
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ path type],
+
+    $vals, mu tval p eqmu v$,
+    $vals, mu texpre p eqmu v$,
+  )
+))
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ unit value type],
+
+    $vals, mu texpre () eqmu 0$,
+  )
+))
+
+// NOTE: tmp removed
+// #align(center, prooftree(
+//   vertical-spacing: 4pt,
+//   rule(
+//     name: [ unit value type],
+
+//     $vals, mu texpre e : t$,
+
+//     [*TODO*],
+
+//     // TODO: reference to what ??
+//     $vals, mu texpre rf e eqmu rf ??$,
+//   )
+// ))
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ unit value type],
+
+    $vals, mu texpre e_1 eqmu v_1$,
+    $...$,
+    $vals, mu texpre e_n eqmu v_n$,
+    $vals, mu texpre [e_1, ... e_n] eqmu [v_1, ... v_n]$,
+  )
+))
+
 
 === Expresion Typing
 
-*TODO*
+// TODO: check
+
+#let texprt = $attach(tack.r.double, br: type)$
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ path type],
+
+    $types ttype p : t$,
+    $types texprt p : t$,
+  )
+))
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ unit value type],
+
+    $types texprt () : cl Read, NotWrite cr$,
+  )
+))
+
+// NOTE: tmp removed
+// #align(center, prooftree(
+//   vertical-spacing: 4pt,
+//   rule(
+//     name: [ unit value type],
+
+//     $types texprt e : t$,
+//     // TODO: why Ref mode ?? <- due to immutability ??
+//     $types texprt rf e : rf Ref t$,
+//   )
+// ))
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ unit value type],
+
+    $types texprt e_1 : t_1$,
+    $...$,
+    $types texprt e_n : t_n$,
+    $types texprt [e_1, ... e_n] : [t_1, ... t_n]$,
+  )
+))
 
 === Function Evaluation
 
@@ -919,7 +945,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ READ $p$],
 
-    $mu, types, vals teval p eqmu 0$,
+    $mu, types, vals tval p eqmu 0$,
 
     $cl types, vals, mu cr
      xarrow("READ" p)

From eb90ba5449c1b3ec3950fa02a7baca0828c4f7ca Mon Sep 17 00:00:00 2001
From: ProgramSnail <purpurebacterium@yandex.ru>
Date: Sat, 25 Apr 2026 16:15:23 +0000
Subject: [PATCH 5/8] structures: statement eval fix (?)

---
 model_with_structures/model.typ | 28 ++++++++++------------------
 1 file changed, 10 insertions(+), 18 deletions(-)

diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ
index 7feaa10..aba93a4 100644
--- a/model_with_structures/model.typ
+++ b/model_with_structures/model.typ
@@ -351,8 +351,6 @@ $s in stmt, f in X, x in X, a in X$
 
 === Eval Rules
 
-#let args = `args`
-
 #[
 
 #let ref = `ref`
@@ -685,7 +683,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ spoil step],
 
-    $mu stretch(=>)^args_sigma gamma$,
+    $mu stretch(=>)^"args"_sigma gamma$,
 
     $isPossibleWrite mode$, // NOTE: weak requirement: may write
     $not isCopy mode$,
@@ -694,7 +692,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
     $isCorrect_(cl sigma, mu cr) (mode, x)$,
 
     // gamma - memory (as mu)
-    $gamma stretch(=>)^((mode, x) : args)_sigma "pathenvval"(gamma, sigma, x) <- bot]$
+    $gamma stretch(=>)^((mode, x) : "args")_sigma "pathenvval"(gamma, sigma, x) <- bot]$
   )
 ))
 
@@ -705,7 +703,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ fix step],
 
-    $mu stretch(=>)^args_sigma gamma$,
+    $mu stretch(=>)^"args"_sigma gamma$,
 
     $isAlwaysWrite mode$, // NOTE: strong requirement: should write
     $mode = (\_, not Out)$,
@@ -715,7 +713,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
     $isCorrect_(cl sigma, mu cr) (mode, x)$,
 
     // gamma - memory (as mu)
-    $gamma stretch(=>)^((mode, x) : args)_sigma "pathenvval"(gamma, sigma, x) <- 0]$
+    $gamma stretch(=>)^((mode, x) : "args")_sigma "pathenvval"(gamma, sigma, x) <- 0]$
   )
 ))
 
@@ -726,7 +724,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ skip step],
 
-    $mu stretch(=>)^args_sigma gamma$,
+    $mu stretch(=>)^"args"_sigma gamma$,
 
     $not "spoil step"$,
     $not "fix step"$,
@@ -734,7 +732,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
     $isCorrect_(cl sigma, mu cr) (mode, x)$,
 
     // mu
-    $gamma stretch(=>)^((mode, x) : args)_sigma gamma$
+    $gamma stretch(=>)^((mode, x) : "args")_sigma gamma$
   )
 ))
 
@@ -896,16 +894,10 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ CALL $f space overline(p)$],
+    name: [ CALL $f space [p_1, ... p_n]$],
 
-    // TODO: FIXME: take corresponding statement & var names
-    // use eval ??
-    [*TODO: statement (from value?) + x'es \<\- expr eval ? *],
-
-    $types ttype f : lambda args $,
-    $args = [m_1 t_1, ... m_n t_n]$,
-    $overline(p) = [p_1, ... p_n]$,
-    $overline(x) = [x_1, ... x_n]$,
+    $vals, mu texpre f eqmu lambda [x_1, ... x_n] space s$,
+    $types ttype f : lambda [m_1 t_1, ... m_n t_n] $,
 
     // TODO: add args before statement eval
 
@@ -933,7 +925,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
     $gamma_(n - 1) stretch(=>)^(x_n space m_n space t_n)_(cl vals, types cr) gamma_n$,
 
     $cl vals, types, mu, l cr
-     xarrow("CALL" f space overline(p))
+     xarrow("CALL" f space [p_1, ... p_n])
      cl vals, types, gamma_n, l cr$,
   )
 ))

From 5a33161117aff166ce68a90d488df171186fac2a Mon Sep 17 00:00:00 2001
From: ProgramSnail <purpurebacterium@yandex.ru>
Date: Sat, 25 Apr 2026 16:44:08 +0000
Subject: [PATCH 6/8] structures: call finalization fix (wothout correctness
 requirements)

---
 model_with_structures/model.typ | 91 ++++++++++++++++++++-------------
 1 file changed, 56 insertions(+), 35 deletions(-)

diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ
index aba93a4..6aee8c0 100644
--- a/model_with_structures/model.typ
+++ b/model_with_structures/model.typ
@@ -9,7 +9,7 @@
 
 #h(10pt)
 
-// TODO: check correctnes for path, mem & type ??
+// TODO: check correctness for path, mem & type ??
 
 == Syntax
 
@@ -462,7 +462,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ new $0$ value],
 
-    $cl 0, mu cr xarrowSquiggly(cl r\, w cr)_new cl 0, mu cr$,
+    $cl 0, mu cr xarrowSquiggly(cl r \, w cr)_new cl 0, mu cr$,
   )
 ))
 
@@ -471,7 +471,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ new $\#$ value],
 
-    $cl \#, mu cr xarrowSquiggly(cl r\, w cr)_new cl \#, mu cr$,
+    $cl \#, mu cr xarrowSquiggly(cl r \, w cr)_new cl \#, mu cr$,
   )
 ))
 
@@ -480,7 +480,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ new $bot$ value],
 
-    $cl bot, mu cr xarrowSquiggly(cl r\, w cr)_new cl bot, mu cr$,
+    $cl bot, mu cr xarrowSquiggly(cl r \, w cr)_new cl bot, mu cr$,
   )
 ))
 
@@ -564,7 +564,6 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ modify tuple value],
 
-    $v in {0, \#, bot}$,
     $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 p.i \, b cr)_modify cl [v_1, ... v'_i, ... v_n], mu' cr$,
   )
@@ -675,24 +674,20 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
 
 === Call Finalization
 
-// FIXME: make connected to syntax
-*TODO*
+#let spoil = `spoil`
+
+// FIXME
+*TODO: embed correctness*
 
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
     name: [ spoil step],
 
-    $mu stretch(=>)^"args"_sigma gamma$,
-
-    $isPossibleWrite mode$, // NOTE: weak requirement: may write
-    $not isCopy mode$,
-    $mode = (\_, not Out)$,
-
-    $isCorrect_(cl sigma, mu cr) (mode, x)$,
-
-    // gamma - memory (as mu)
-    $gamma stretch(=>)^((mode, x) : "args")_sigma "pathenvval"(gamma, sigma, x) <- bot]$
+    $w = AlwaysWrite or w = MaybeWrite$,
+    // TODO: $isCorrect_(cl sigma, mu cr) (mode, x)$,
+    $v in {0, \#, bot}$,
+    $cl v, mu cr xarrowSquiggly(cl r \, w cr \, (\_, not Out) \, not Copy)_spoil cl bot, mu cr$,
   )
 ))
 
@@ -703,17 +698,10 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ fix step],
 
-    $mu stretch(=>)^"args"_sigma gamma$,
-
-    $isAlwaysWrite mode$, // NOTE: strong requirement: should write
-    $mode = (\_, not Out)$,
-
-    // NOTE: correctness looks like this
-    // $types, vals, mu, m, c tcorrect v : cl r', w' cr -> cl r, w cr$,
-    $isCorrect_(cl sigma, mu cr) (mode, x)$,
-
-    // gamma - memory (as mu)
-    $gamma stretch(=>)^((mode, x) : "args")_sigma "pathenvval"(gamma, sigma, x) <- 0]$
+    $w = AlwaysWrite$,
+    // TODO: $isCorrect_(cl sigma, mu cr) (mode, x)$,
+    $v in {0, \#, bot}$,
+    $cl v, mu cr xarrowSquiggly(cl r \, w cr \, (\_, Out) \, c)_spoil cl 0, mu cr$,
   )
 ))
 
@@ -724,18 +712,51 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ skip step],
 
-    $mu stretch(=>)^"args"_sigma gamma$,
-
     $not "spoil step"$,
     $not "fix step"$,
-
-    $isCorrect_(cl sigma, mu cr) (mode, x)$,
-
-    // mu
-    $gamma stretch(=>)^((mode, x) : "args")_sigma gamma$
+    // TODO: $isCorrect_(cl sigma, mu cr) (mode, x)$,
+    $v in {0, \#, bot}$,
+    $cl v, mu cr xarrowSquiggly(cl r \, w cr \, (\_, not Out) \, c)_spoil cl v, mu cr$,
   )
 ))
 
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ lambda step],
+
+    $cl lambda, mu cr xarrowSquiggly(lambda overline(t) \, m \, c)_spoil cl lambda, mu cr$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ reference step],
+
+    $cl mu[l], mu cr xarrowSquiggly(t \, m \, c')_spoil cl v', mu' cr$,
+    $cl rf l, mu cr xarrowSquiggly(rf c' space  t \, m \, c)_spoil cl rf l, mu'[l <- v'] cr$,
+  )
+))
+
+#h(10pt)
+
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ tuple step],
+
+    $cl v_1, mu cr xarrowSquiggly(t_1 \, m \, c)_spoil cl v'_1, mu cr$,
+    $...$,
+    $cl v_n, mu cr xarrowSquiggly(t_n \, m \, c)_spoil cl v'_n, mu cr$,
+    $cl [v_1, ... v_n], mu cr xarrowSquiggly([t_1, ... t_n] \, m \, c)_spoil cl [v'_1, ... v'_n], mu' cr$,
+  )
+))
 
 #h(10pt)
 

From 22111a37edd93e600c5c7738a58efab29bbc522a Mon Sep 17 00:00:00 2001
From: ProgramSnail <purpurebacterium@yandex.ru>
Date: Sat, 25 Apr 2026 16:58:59 +0000
Subject: [PATCH 7/8] structures: call add arguments (without typecheck), new
 value funciton fix

---
 model_with_structures/model.typ | 74 ++++++++++-----------------------
 1 file changed, 22 insertions(+), 52 deletions(-)

diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ
index 6aee8c0..89440fd 100644
--- a/model_with_structures/model.typ
+++ b/model_with_structures/model.typ
@@ -460,27 +460,20 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ new $0$ value],
+    name: [ new trivial read value],
 
-    $cl 0, mu cr xarrowSquiggly(cl r \, w cr)_new cl 0, mu cr$,
+    $v in {0, \#, bot}$,
+    $cl v, mu cr xarrowSquiggly(cl Read \, w cr)_new cl v, mu cr$,
   )
 ))
 
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ new $\#$ value],
+    name: [ new trivial $not$ read value],
 
-    $cl \#, mu cr xarrowSquiggly(cl r \, w cr)_new cl \#, mu cr$,
-  )
-))
-
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ new $bot$ value],
-
-    $cl bot, mu cr xarrowSquiggly(cl r \, w cr)_new cl bot, mu cr$,
+    $v in {0, \#, bot}$,
+    $cl v, mu cr xarrowSquiggly(cl Read \, w cr)_new cl bot, mu cr$,
   )
 ))
 
@@ -672,7 +665,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
 
 #h(10pt)
 
-=== Call Finalization
+=== Call Values Spoil
 
 #let spoil = `spoil`
 
@@ -863,48 +856,25 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   )
 ))
 
-=== Function Evaluation
-
-// FIXME: make connected to syntax
-*TODO*
-
-// #align(center, prooftree(
-//   vertical-spacing: 4pt,
-//   rule(
-//     name: [ $(lambda a : t. d) m$],
-
-//     // TODO: verify that type of m is t ??
-
-//     $cl sigma [a <- (m, t)], mu, l cr
-//      xarrowSquiggly(t)
-//      cl sigma', mu', l' cr$,
-
-//     $cl sigma', mu', l' cr
-//      xarrowDashed(d space @ space overline(y))
-//      cl sigma'', mu'', l'' cr$,
-
-//     $isRead mode$,
-//     $not isCopy mode$,
-
-//     // NOTE: correctness checked in CALL f
-
-//     $cl sigma, mu, l cr
-//      xarrowDashed()
-//      cl sigma'', mu'', l'' cr$,
-//   )
-// ))
-
-// TODO: FIXME: arrow to eval expr to value ??
-// TODO: fixme 
+=== Function Argument Addition
 
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
     name: [ add argument],
 
-    $cl sigma, mu, l cr
-     xarrowDashed(x space m space t space p)
-     cl sigma', mu', l' cr$,
+
+    $vals, mu tval p eqmu v$,
+    $types ttype p : t'$,
+    // TODO: FIXME: check type compatibility for t and type for path p (?)
+    [*TODO: check t ~ t' in sme way (?)*],
+    $cl v', mu cr xarrowSquiggly(t)_new cl v, mu' cr$,
+
+
+    // TODO save type mode somewhere ?? // <- not needed because is described by other params <- ??
+    $cl types, vals, mu cr
+     xarrowDashed(x space t space p)
+     cl types[x <- t], vals[x <- v], mu' cr$,
   )
 ))
 
@@ -928,11 +898,11 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
 
     // NOTE: dashed arrow to fill context
     $cl types_0, vals_0,  mu_0, l cr
-     xarrowDashed(x_1 space m_1 space t_1 space p_1)
+     xarrowDashed(x_1 space t_1 space p_1)
      cl types', vals_1, mu_1, l' cr$,
     $...$,
     $cl types_(n - 1), vals_(n - 1),  mu_(n - 1), l cr
-     xarrowDashed(x_n space m_n space t_n space p_n)
+     xarrowDashed(x_n space t_n space p_n)
      cl types', vals_n, mu_n, l' cr$,
 
     $cl types_n, vals_n,  mu_n, l cr

From 4eb3dea9668aae711387b5288b580cbda4b5d233 Mon Sep 17 00:00:00 2001
From: ProgramSnail <purpurebacterium@yandex.ru>
Date: Sat, 25 Apr 2026 17:25:21 +0000
Subject: [PATCH 8/8] structures: spoil fix, corectness added

---
 model_with_structures/model.typ | 90 ++++++++++++++++++++++++++-------
 1 file changed, 72 insertions(+), 18 deletions(-)

diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ
index 89440fd..1221071 100644
--- a/model_with_structures/model.typ
+++ b/model_with_structures/model.typ
@@ -375,6 +375,8 @@ $s in stmt, f in X, x in X, a in X$
 
 === Moded Type Correctness
 
+*NOTE: скорее всего не нужна в таком виде, перенесено в spoil*
+
 #let tcorrect = $attach(tack.r, br: #[correct])$
 
 // TODO: FIXME: well formatness for mode, extract
@@ -528,12 +530,23 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
 
 #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,
   rule(
-    name: [ modify trivial value],
+    name: [ modify end value],
 
-    $v in {0, \#, bot}$,
+    // $v in {0, \#, bot}$,
     $cl v, mu cr xarrowSquiggly(cl \@ x \, b cr)_modify cl b, mu cr$,
   )
 ))
@@ -669,18 +682,36 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
 
 #let spoil = `spoil`
 
-// FIXME
-*TODO: embed correctness*
+// TODO: FIXME: complete rule check
+#let tcorrectnew = $attach(tack.r.double, br: #[correct])$
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ correctness],
+
+    $r = Read => v = 0$,
+    $r = Read => m = (In, \_)$, 
+    $m = (\_, Out) => w = AlwaysWrite$,
+    $(w = AlwaysWrite or w = MaybeWrite) and (m = (\_, Out) or c = Ref) => w' = AlwaysWrite$,
+
+    $v in {0, \#, bot}$,
+
+    $ tcorrectnew cl v, r, w, r', w', m, c cr $,
+  )
+))
+
+// TODO: extract correctness
 
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
     name: [ spoil step],
 
+    $ tcorrectnew cl v, r, w, r', w', m, c cr $,
+
     $w = AlwaysWrite or w = MaybeWrite$,
-    // TODO: $isCorrect_(cl sigma, mu cr) (mode, x)$,
     $v in {0, \#, bot}$,
-    $cl v, mu cr xarrowSquiggly(cl r \, w cr \, (\_, not Out) \, not Copy)_spoil cl bot, mu cr$,
+    $cl v, mu cr xarrowSquiggly(cl r \, w cr \, cl r' \, w' cr \, (\_, not Out) \, not Copy)_spoil cl bot, mu cr$,
   )
 ))
 
@@ -691,10 +722,11 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ fix step],
 
+    $ tcorrectnew cl v, r, w, r', w', m, c cr $,
+
     $w = AlwaysWrite$,
-    // TODO: $isCorrect_(cl sigma, mu cr) (mode, x)$,
     $v in {0, \#, bot}$,
-    $cl v, mu cr xarrowSquiggly(cl r \, w cr \, (\_, Out) \, c)_spoil cl 0, mu cr$,
+    $cl v, mu cr xarrowSquiggly(cl r \, w cr \, cl r' \, w' cr \,  (\_, Out) \, c)_spoil cl 0, mu cr$,
   )
 ))
 
@@ -705,11 +737,12 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ skip step],
 
+    $ tcorrectnew cl v, r, w, r', w', m, c cr $,
+
     $not "spoil step"$,
     $not "fix step"$,
-    // TODO: $isCorrect_(cl sigma, mu cr) (mode, x)$,
     $v in {0, \#, bot}$,
-    $cl v, mu cr xarrowSquiggly(cl r \, w cr \, (\_, not Out) \, c)_spoil cl v, mu cr$,
+    $cl v, mu cr xarrowSquiggly(cl r \, w cr \, cl r' \, w' cr \, (\_, not Out) \, c)_spoil cl v, mu cr$,
   )
 ))
 
@@ -720,7 +753,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ lambda step],
 
-    $cl lambda, mu cr xarrowSquiggly(lambda overline(t) \, m \, c)_spoil cl lambda, mu cr$,
+    $cl lambda, mu cr xarrowSquiggly(lambda overline(t) \, lambda overline(t) \, m \, c)_spoil cl lambda, mu cr$,
   )
 ))
 
@@ -731,8 +764,9 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ reference step],
 
-    $cl mu[l], mu cr xarrowSquiggly(t \, m \, c')_spoil cl v', mu' cr$,
-    $cl rf l, mu cr xarrowSquiggly(rf c' space  t \, m \, c)_spoil cl rf l, mu'[l <- v'] cr$,
+    $cl mu[l], mu cr xarrowSquiggly(t \, t' m \, c')_spoil cl v', mu' cr$,
+    // NOTE: copy mode of assigned type is not important (c'')
+    $cl rf l, mu cr xarrowSquiggly(rf c' space  t \, rf c'' space  t' \, m \, c)_spoil cl rf l, mu'[l <- v'] cr$,
   )
 ))
 
@@ -744,10 +778,30 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ tuple step],
 
-    $cl v_1, mu cr xarrowSquiggly(t_1 \, m \, c)_spoil cl v'_1, mu cr$,
+    $cl v_1, mu cr xarrowSquiggly(t_1 \, t'_1 \, m \, c)_spoil cl v'_1, mu cr$,
     $...$,
-    $cl v_n, mu cr xarrowSquiggly(t_n \, m \, c)_spoil cl v'_n, mu cr$,
-    $cl [v_1, ... v_n], mu cr xarrowSquiggly([t_1, ... t_n] \, m \, c)_spoil cl [v'_1, ... v'_n], mu' cr$,
+    $cl v_n, mu cr xarrowSquiggly(t_n \, t'_n \, m \, c)_spoil cl v'_n, mu cr$,
+    $cl [v_1, ... v_n], mu cr xarrowSquiggly([t_1, ... t_n] \, [t'_1, ... t'_n] \, m \, c)_spoil cl [v'_1, ... v'_n], mu' cr$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ full spoil],
+
+    $p arrpath x$,
+    $l = vals[x]$,
+    $vals, mu tval p eqmu b$,
+    $types ttype p : t'$,
+    // TODO: FIXME: Ref or Copy ?? in root <- Ref ??, because otherwise there could not b any Refs
+    // FIXME depends on parent ??
+    $cl b, mu cr xarrowSquiggly(t \, t' \, m \, Ref)_spoil cl b', 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']$,
   )
 ))
 
@@ -911,9 +965,9 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
 
     // NOTE: thick arrow to "spoil" context
     $gamma_0 = mu$,
-    $gamma_0 stretch(=>)^(x_1 space m_1 space t_1)_(cl vals, types cr) gamma_1$,
+    $gamma_0 stretch(=>)^(x_1 space m_1 space t_1 space p_1)_(cl vals, types cr) gamma_1$,
     $...$,
-    $gamma_(n - 1) stretch(=>)^(x_n space m_n space t_n)_(cl vals, types cr) gamma_n$,
+    $gamma_(n - 1) stretch(=>)^(m_n space t_n space p_n)_(cl vals, types cr) gamma_n$,
 
     $cl vals, types, mu, l cr
      xarrow("CALL" f space [p_1, ... p_n])