From 7d8ab196752e951154451f529e37e75e25679421 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Sun, 17 May 2026 18:09:39 +0000 Subject: [PATCH 1/2] struct: model: build rule --- model_with_structures/model.typ | 102 +++++++++++++++++++++++++++----- 1 file changed, 87 insertions(+), 15 deletions(-) diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ index 1912a7b..c2fec46 100644 --- a/model_with_structures/model.typ +++ b/model_with_structures/model.typ @@ -540,9 +540,69 @@ $action$ - действия, совершаемые с примитивным з === Value Construction +#let build = `build` + +#align(center, prooftree( + vertical-spacing: 4pt, + rule( + name: [ build trivial read value], + + $mu xarrowSquiggly(cl Read \, w cr)_build + cl cdl 0_m, 0_r, 0_w cdr, mu cr$, + ) +)) + +#h(10pt) + +#align(center, prooftree( + vertical-spacing: 4pt, + rule( + name: [ build trivial $not$ read value], + + $mu xarrowSquiggly(cl not Read \, w cr)_build + cl cdl bot, 0_r, 0_w cdr, mu cr$, + ) +)) + +#h(10pt) + +// TODO: function pointer type ?? + +#align(center, prooftree( + vertical-spacing: 4pt, + rule( + name: [ build reference value], + + $mu xarrowSquiggly(t)_build cl v, mu_v cr$, + + $mu_v xarrowSquiggly(v)_#[add] cl l, mu_a cr$, + + $mu xarrowSquiggly(rf c t)_build cl rf l, mu_a cr$, + ) +)) + +#h(10pt) + +#align(center, prooftree( + vertical-spacing: 4pt, + rule( + name: [ build tuple value], + + $mu_0 xarrowSquiggly(t_1)_build cl v_1, mu_1 cr$, + $...$, + $mu_(n - 1) xarrowSquiggly(t_n)_build cl v_n, mu_n cr$, + + $mu_0 xarrowSquiggly([t_1, ... t_n])_build cl [v_1, ... v_n], mu_n cr$, + ) +)) + +#h(10pt) + +// --- + // TODO: FIXME:add ref / copy modes correctness check ?? -#let new = `new` +// #let copy = `copy` #align(center, prooftree( vertical-spacing: 4pt, @@ -551,22 +611,26 @@ $action$ - действия, совершаемые с примитивным з $v_m in {0, ?, bot}$, $cl cdl v_m, v_r, v_w cdr, mu cr - xarrowSquiggly(cl Read \, w cr)_new - cl cdl v_m, 0, 0 cdr, mu cr$, + xarrowSquiggly(cl Read \, w cr)_copy + cl cdl v_m, 0_r, 0_w cdr, mu cr$, ) )) +#h(10pt) + // #align(center, prooftree( // vertical-spacing: 4pt, // rule( // name: [ new trivial read $top$ value], // $cl cdl top, v_r, v_w cdr, mu cr -// xarrowSquiggly(cl Read \, w cr)_new +// xarrowSquiggly(cl Read \, w cr)_copy // cl cdl 0, 0, 0 cdr, mu cr$, // ) // )) +#h(10pt) + #align(center, prooftree( vertical-spacing: 4pt, rule( @@ -574,53 +638,61 @@ $action$ - действия, совершаемые с примитивным з $v_m in {0, ?, bot/*, top */}$, $cl cdl v_m, v_r, v_w cdr, mu cr - xarrowSquiggly(cl not Read \, w cr)_new - cl cdl bot, 0, 0 cdr, mu cr$, + xarrowSquiggly(cl not Read \, w cr)_copy + cl cdl bot, 0_r, 0_w cdr, mu cr$, ) )) +#h(10pt) + #align(center, prooftree( vertical-spacing: 4pt, rule( name: [ new funciton pointer value], - $cl lambda overline(s), mu cr xarrowSquiggly(lambda space c space overline(t))_new cl lambda overline(s), mu cr$, + $cl lambda overline(s), mu cr xarrowSquiggly(lambda space c space overline(t))_copy cl lambda overline(s), mu cr$, ) )) +#h(10pt) + // #align(center, prooftree( // vertical-spacing: 4pt, // rule( // name: [ new reference ref value], -// $cl rf l, mu cr xarrowSquiggly(rf Ref t)_new cl rf l, mu cr$, +// $cl rf l, mu cr xarrowSquiggly(rf Ref t)_copy cl rf l, mu cr$, // ) // )) +// #h(10pt) + // NOTE: due to new memory cells types (with rw subcells) valnue should always be copied #align(center, prooftree( vertical-spacing: 4pt, rule( name: [ new reference /* copy */ value], - $cl mu[l], mu cr xarrowSquiggly(t)_new cl v, mu_v cr$, + $cl mu[l], mu cr xarrowSquiggly(t)_copy cl v, mu_v cr$, $mu_v xarrowSquiggly(v)_#[add] cl l', mu_a cr$, - $cl rf l, mu cr xarrowSquiggly(rf c /*Copy*/ t)_new cl rf l', mu_a cr$, + $cl rf l, mu cr xarrowSquiggly(rf c /*Copy*/ t)_copy cl rf l', mu_a cr$, ) )) +#h(10pt) + #align(center, prooftree( vertical-spacing: 4pt, rule( name: [ new tuple value], - $cl v_1, mu_0 cr xarrowSquiggly(t_1)_new cl lambda v'_1, mu_1 cr$, + $cl v_1, mu_0 cr xarrowSquiggly(t_1)_copy cl v'_1, mu_1 cr$, $...$, - $cl v_n, mu_(n - 1) cr xarrowSquiggly(t_n)_new cl lambda v'_n, mu_n cr$, + $cl v_n, mu_(n - 1) cr xarrowSquiggly(t_n)_copy cl v'_n, mu_n cr$, - $cl [v_1, ... v_n], mu_0 cr xarrowSquiggly([t_1, ... t_n])_new cl [v'_1, ... v'_n], mu_n cr$, + $cl [v_1, ... v_n], mu_0 cr xarrowSquiggly([t_1, ... t_n])_copy cl [v'_1, ... v'_n], mu_n cr$, ) )) @@ -1067,7 +1139,7 @@ $action$ - действия, совершаемые с примитивным з // expect well typed program $vals, mu texpre e eqmu v$, - $cl v, mu cr xarrowSquiggly(t)_new cl v', mu' cr$, // TODO: FIXME check (required?) + $cl v, mu cr xarrowSquiggly(t)_copy cl v', mu' cr$, // TODO: FIXME check (required?) $mu' xarrowSquiggly(v')_#[add] cl l, mu'' cr$, $cl types, vals, mu cr xarrowSquiggly("var" x : t = e)_init cl types[x <- t], vals[x <- l], mu'' cr$ @@ -1354,7 +1426,7 @@ $action$ - действия, совершаемые с примитивным з // TODO: check type compatibility for t and type for path p (?) // [*TODO: check t ~ t' in sme way (?)*], // <- programs considired to be well-typed - $cl v, mu cr xarrowSquiggly(t)_new cl v', mu' cr$, + $cl v, mu cr xarrowSquiggly(t)_copy cl v', mu' cr$, $mu' xarrowSquiggly(v')_#[add] cl l, mu'' cr$, // TODO save type mode somewhere ?? // <- not needed because is described by other params <- ?? From fac507bebf28e5dd9e48fda6a59756b9ba8b6282 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Sun, 17 May 2026 18:19:31 +0000 Subject: [PATCH 2/2] struct: analyzer & synthesizer val build, small fixes --- model_with_structures/analyzer.ml | 19 +++++++++++--- model_with_structures/synthesizer.ml | 39 +++++++++++++++++++++++++++- model_with_structures/tests_f.ml | 6 ++--- 3 files changed, 57 insertions(+), 7 deletions(-) diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml index 0c74973..602f81a 100644 --- a/model_with_structures/analyzer.ml +++ b/model_with_structures/analyzer.ml @@ -195,6 +195,19 @@ struct (* - value construction *) + let rec valbuild (mem : mem) (t : atype) : mem * value = + match t with + | UnitT (Rd, _) -> (mem, UnitV (ZeroMV, ZeroRV, ZeroWV)) + | UnitT (NRd, _) -> (mem, UnitV (BotMV, ZeroRV, ZeroWV)) + | FunT _ -> raise @@ Typing_error "valbuild: funciton value is not supported" + | RefT (_, t) -> let (mem', v') = valbuild mem t in + let (mem'', id'') = mem_add mem' v' in + (mem'', RefV id'') + | TupleT ts -> let folder = fun t (mem, vs') -> let (mem', v') = valbuild mem t in + (mem', v' :: vs') in + let mem', vs' = List.fold_right folder ts (mem, []) in + (mem', TupleV vs') + let rec valcopy (mem : mem) (v : value) (t : atype) : mem * value = match t, v with | UnitT (Rd, _), UnitV (v_m, _, _) -> (mem, UnitV (v_m, ZeroRV, ZeroWV)) @@ -204,10 +217,10 @@ struct | RefT (_, t), RefV id -> let (mem', v') = valcopy mem (mem_get mem id) t in let (mem'', id'') = mem_add mem' v' in (mem'', RefV id'') - | TupleT ts, TupleV vs -> let folder = fun (mem, vs') v t -> let (mem', v') = valcopy mem v t in + | TupleT ts, TupleV vs -> let folder = fun v t (mem, vs') -> let (mem', v') = valcopy mem v t in (mem', v' :: vs') in - let mem', vs' = List.fold_left2 folder (mem, []) vs ts in - (mem', TupleV (List.rev vs')) (* TODO: FIXME: should reverse or not ?? *) + let mem', vs' = List.fold_right2 folder vs ts (mem, []) in + (mem', TupleV vs') | _, _ -> raise @@ Typing_error "valcopy: not trivial value, wrong type" (* - action rules *) diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml index a60eafd..2d699bc 100644 --- a/model_with_structures/synthesizer.ml +++ b/model_with_structures/synthesizer.ml @@ -588,6 +588,44 @@ struct (* - value construction *) + let rec valbuild_foldero mem_with_vs tp mem_with_vs' = + ocanren { + fresh mem, vs, mem', v', vs' in + Std.pair mem vs == mem_with_vs & + valbuildo mem tp (Std.pair mem' v') & + vs' == v' :: vs & + mem_with_vs' == Std.pair mem' vs' + } + and valbuildo mem tp mem_with_id' = + let open Type in + 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 + tp == UnitT (r, w) & + { { r == Rd & + mem_with_id' == Std.pair mem (UnitV (ZeroMV, ZeroRV, ZeroWV)) } | + { r == NRd & + mem_with_id' == Std.pair mem (UnitV (BotMV, ZeroRV, ZeroWV)) } } } | + (* { fresh ts in *) + (* tp == FunT ts & *) + (* ??? } | *) + { fresh c, tp' in + tp == RefT (c, tp') & + { fresh mem_cp, v_cp, mem_add, id_add in + valbuildo mem tp' (Std.pair mem_cp v_cp) & + mem_addo mem_cp v_cp (Std.pair mem_add id_add) & + mem_with_id' == (mem_add, RefV id_add) } } | + { fresh tps, mem', vs' in + tp == TupleT tps & + list_foldro valbuild_foldero (Std.pair mem []) tps (Std.pair mem' vs') & + mem_with_id' == Std.pair mem' (TupleV vs') } + } + let rec valcopy_foldero mem_with_vs v tp mem_with_vs' = ocanren { fresh mem, vs, mem', v', vs' in @@ -606,7 +644,6 @@ struct 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 & diff --git a/model_with_structures/tests_f.ml b/model_with_structures/tests_f.ml index dccaa23..6f65938 100644 --- a/model_with_structures/tests_f.ml +++ b/model_with_structures/tests_f.ml @@ -1018,8 +1018,8 @@ let prog_eval_compl_test_send _ = show(answer) (Stream.take (run q ReadS sb_access3] sendFBranch & seqo [ChoiceS (sendFBranch, SkipS); - WriteS (VarP 0)); - ReadS (VarP 0))] + WriteS (VarP 0); + ReadS (VarP 0)] sendF & fresh sa_access0, sa_access1, sa_access2, sa_access3 in @@ -1027,7 +1027,7 @@ let prog_eval_compl_test_send _ = show(answer) (Stream.take (run q access_deref_accesso 1 1 0 sa_access1 & access_deref_access_deref_accesso 0 0 0 0 sa_access2 & access_deref_accesso 0 1 0 sa_access3 & - seqo [WriteS (VarP 0)); + seqo [WriteS (VarP 0); CallS (VarP sendID, [PathE (VarP 0)]); CallS (VarP get_version_idID, [PathE (VarP 0)]); CallS (VarP updated_versionID, [PathE (VarP 0)]);