st/pass_strategy_synthesis
1
0
Fork 0
mirror of https://github.com/ProgramSnail/pass_strategy_synthesis.git synced 2026-06-10 19:28:16 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

struct: model change in analyzer (tests are not fixed yet), semantics fixes

Browse source
This commit is contained in:
ProgramSnail 2026-05-13 15:54:40 +00:00
parent 18481550d3
commit 60da9bdb3f
2 changed files with 263 additions and 119 deletions
Download patch file Download diff file Expand all files Collapse all files

305
model_with_structures/analyzer.ml
View file

@ -59,22 +59,26 @@ struct
(* value model & memory model *) (* 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 value = ZeroV type memval = ZeroMV | SmthMV | BotMV (* | TopMV ?? *)
| SmthV type readval = ZeroRV | OneRV | TopRV
| BotV type writeval = ZeroWV | SmthWV | OneWV
type value = UnitV of memval * readval * writeval
| FunV of ((* data list * *) stmt) list | FunV of ((* data list * *) stmt) list
| RefV of memid | RefV of memid
| TupleV of value list | TupleV of value list
type revpath = VarRP | DerefRP of revpath | AccessRP of revpath * data type revpath = VarRP | DerefRP of revpath | AccessRP of revpath * data
type action = ReadA | AlwaysWriteA | MayWriteA
(* TODO: any additional difference between rvalue and lvalue now ?? *) (* TODO: any additional difference between rvalue and lvalue now ?? *)
(* --- *) (* --- *)
@ -138,16 +142,17 @@ struct
let mem_set (mem : mem) (id : memid) (v : value) : mem = let mem_set (mem : mem) (id : memid) (v : value) : mem =
(list_replace (fst mem) (snd mem - id - 1) v, snd 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 =
v == ZeroV || v == SmthV || v == BotV match v with | UnitV (_, _, _) -> true
| _ -> false
(* --- path accessors --- *) (* --- path accessors --- *)
@ -191,19 +196,9 @@ struct
(* - value construction *) (* - value construction *)
let rec valcopy (mem : mem) (v : value) (t : atype) : mem * value = let rec valcopy (mem : mem) (v : value) (t : atype) : mem * value =
if is_trivial_v v match t, v with
then match t with | UnitT (Rd, _), UnitV (v_m, _, _) -> (mem, UnitV (v_m, ZeroRV, ZeroWV))
| UnitT (Rd, _) -> (mem, v) | UnitT (NRd, _), UnitV _ -> (mem, UnitV (BotMV, ZeroRV, ZeroWV))
| 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) | FunT _, FunV _ -> (mem, v)
| RefT (Rf, _), RefV _ -> (mem, v) | RefT (Rf, _), RefV _ -> (mem, v)
| RefT (Cp, t), RefV id -> let (mem', v') = valcopy mem (mem_get mem id) t in | RefT (Cp, t), RefV id -> let (mem', v') = valcopy mem (mem_get mem id) t in
@ -215,25 +210,78 @@ struct
(mem', TupleV (List.rev vs')) (* TODO: FIXME: should reverse or not ?? *) (mem', TupleV (List.rev vs')) (* TODO: FIXME: should reverse or not ?? *)
| _, _ -> raise @@ Typing_error "valcopy: not trivial value, wrong type" | _, _ -> 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 @@ Typing_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 *) (* - value update *)
let rec valupd (mem : mem) (v : value) (p : revpath) (b : value) : mem * value = match p, v with (* TODO: change and modify are different *)
let rec valchange (mem : mem) (v : value) (p : revpath) (b : value) : mem * value = match p, v with
| VarRP, _ -> (mem, b) | VarRP, _ -> (mem, b)
| DerefRP p, RefV id -> let (mem', v') = valupd mem (mem_get mem id) p b in | DerefRP p, RefV id -> let (mem', v') = valchange mem (mem_get mem id) p b in
(mem_set mem' id v', RefV id) (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; *) | AccessRP (p, id), TupleV vs -> let (mem', v') = valchange mem (List.nth vs id) p b in
valupd mem (List.nth vs id) p b in (mem', TupleV (list_replace vs id v'))
(* FIXME TMP Printf.printf "before return\n"; *) | _, _ -> raise @@ Typing_error "valupd"
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')) (mem', TupleV (list_replace vs id v'))
| _, _ -> raise @@ Typing_error "valupd" | _, _ -> raise @@ Typing_error "valupd"
(* - value combination *) (* - 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 = let rec valcomb (u : value) (v : value) : value =
if is_trivial_v u && is_trivial_v v match u, v with
then (if u == v then u else BotV) | UnitV (u_m, u_r, u_w), UnitV (v_m, v_r, v_w) ->
else match u, v with UnitV (memvalcomb u_m v_m, readvalcomb u_r v_r, writevalcomb u_w v_w)
| 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" | 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) | TupleV us, TupleV vs -> TupleV (List.map2 valcomb us vs)
| _, _ -> raise @@ Typing_error "valcomb" | _, _ -> raise @@ Typing_error "valcomb"
@ -246,7 +294,7 @@ struct
(* - expression evaluation *) (* - expression evaluation *)
let rec exprval (mem : mem) (vals : vals) (e : expr) : value = match e with let rec exprval (mem : mem) (vals : vals) (e : expr) : value = match e with
| UnitE -> ZeroV | UnitE -> UnitV (ZeroMV, ZeroRV, ZeroWV)
| PathE p -> pathval mem vals p | PathE p -> pathval mem vals p
| RefE x -> RefV (vals_assoc x vals) | RefE x -> RefV (vals_assoc x vals)
| TupleE es -> TupleV (List.map (exprval mem vals) es) | TupleE es -> TupleV (List.map (exprval mem vals) es)
@ -287,48 +335,65 @@ struct
(* - call values spoil *) (* - call values spoil *)
(* TODO: check assignment type matches types separately later ?? *)
(* TODO: check all cases *) (* TODO: check all cases *)
let is_correct_tags (v : value) (r : read_cap) (w : write_cap) let is_correct_tags (r : read_cap) (w : write_cap)
(r' : read_cap) (w' : write_cap) (m : mode) (m : mode) (c : copy_cap) : bool =
(c : copy_cap) : bool = (snd m != Out || c == Rf) &&
(* 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) && (snd m != Out || w == AlwaysWr) &&
(* TODO: FIXME: check *) (r != Rd || fst m == In)
((not ((w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf))) || w' == AlwaysWr) &&
is_trivial_v v let tryread (r : read_cap) (v_m : memval)
(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) let rec valspoil (mem : mem) (v : value) (t : atype)
(u : atype) (m : mode) (c : copy_cap) (m : mode) (c : copy_cap)
: mem * value = match t, u, v with : mem * value = match t, v with
| UnitT (r, w), UnitT (r', w'), _ -> | UnitT (r, w), UnitV (v_m, v_r, v_w) ->
if not @@ is_trivial_v v if not @@ is_correct_tags r w m c
then raise @@ Typing_error "valspoil: unit, not trivial"
else if not @@ is_correct_tags v r w r' w' m c
then raise @@ Typing_error "valspoil: unit, not correct" then raise @@ Typing_error "valspoil: unit, not correct"
else if snd m == NOut && c == Rf && (w == AlwaysWr || w == MayWr) else
then (mem, BotV) let v' = tryread r v_m v_r v_w in
else if snd m == Out && w == AlwaysWr if c == Cp || w == NeverWr
then (mem, ZeroV) then (mem, v')
else (mem, v) else (match v' with
| FunT ts, FunT us, FunV _ -> if ts == us then (mem, v) else raise @@ Typing_error "valspoil: fun" | UnitV (v_m', v_r', v_w') ->
| RefT (ct, t), RefT (cu, u), RefV id -> let (v_m'', v_r'', v_w'') =
let (mem', v') = valspoil mem (mem_get mem id) t u m ct in (if w == AlwaysWr
then (memvmod AlwaysWriteA v_m',
readvmod AlwaysWriteA v_r',
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) (mem_set mem id v', RefV id)
| TupleT ts, TupleT us, TupleV vs -> | TupleT ts, TupleV vs ->
let folder = fun (mem, vs') t u v -> let folder = fun (mem, vs') t v ->
let (mem', v') = valspoil mem v t u m c in (mem', v' :: vs') in let (mem', v') = valspoil mem v t m c in (mem', v' :: vs') in
let (mem', vs') = list_foldl3 folder (mem, []) ts us vs in let (mem', vs') = List.fold_left2 folder (mem, []) ts vs in
(mem', TupleV (List.rev vs')) (mem', TupleV (List.rev vs'))
| _, _, _ -> raise @@ Typing_error "valspoil" | _, _ -> raise @@ Typing_error "valspoil"
(* full spoil *) (* full spoil *)
@ -337,11 +402,11 @@ struct
let x = pathvar p in let x = pathvar p in
let id = vals_assoc x vals in (* base var address *) let id = vals_assoc x vals in (* base var address *)
let b = pathval mem vals p in (* subvalue in var *) 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 t' m Cp in (* spoil subvalue *) let (mem', b') = valspoil mem b t m Cp in (* spoil subvalue *)
(* TODO: FIXME: why copy (Cp)? maybe sometimes use top-level capability ? *) (* TODO: FIXME: why copy (Cp)? maybe sometimes use top-level capability ? *)
let pi = pathrev p VarRP in let pi = pathrev p VarRP in
let (mem'', v'') = valupd mem' (mem_get mem' id) pi b' in (* set subvalue into var *) let (mem'', v'') = valchange mem' (mem_get mem' id) pi b' in (* set subvalue into var *)
mem_set mem'' id v'' mem_set mem'' id v''
let rec argsspoile (state : state) (m : mode) (t : atype) (e : expr) : mem = let rec argsspoile (state : state) (m : mode) (t : atype) (e : expr) : mem =
@ -369,15 +434,32 @@ struct
(* NOTE: not needed due to performed optimization in stmt_eval *) (* 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 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 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 *) (* - statement evaluation *)
let rec stmt_eval (state : state) (s : stmt) : state = let rec stmt_eval (state : state) (s : stmt) : state =
match state with (mem, types, vals, visited) -> match s with match state with (mem, types, vals, visited) -> match s with
| SkipS -> state | SkipS -> state
| CallS (f, es) -> let v = (* FIXME TMP Printf.printf "call, before v\n"; *) | CallS (f, es) -> let v = pathval mem vals f in
pathval mem vals f in let t = pathtype types 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 types' : types = (fst types, fst types) in
let vals' : vals = (fst vals, fst vals) in let vals' : vals = (fst vals, fst vals) in
(match v, t with (match v, t with
@ -394,7 +476,14 @@ struct
if List.mem stmt visited_old if List.mem stmt visited_old
then stmt :: visited_old then stmt :: visited_old
else match stmt_eval (mem_swa, types_swa, vals_swa, stmt :: visited_old) stmt with else match stmt_eval (mem_swa, types_swa, vals_swa, stmt :: visited_old) stmt with
(_, _, _, visited_after_stmt) -> visited_after_stmt) (mem_after_stmt, _, vals_after_stmt, visited_after_stmt) ->
ignore @@ List.fold_right
(fun (_, t) x ->
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)
ts 0;
visited_after_stmt)
visited_swa visited_swa
fstmts in fstmts in
let mem_spoiled = (* FIXME TMP Printf.printf "call, before spoil\n"; *) let mem_spoiled = (* FIXME TMP Printf.printf "call, before spoil\n"; *)
@ -412,16 +501,26 @@ struct
else let x = pathvar p in else let x = pathvar p in
let id = vals_assoc x vals in let id = vals_assoc x vals in
let pi = pathrev p VarRP 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) pi AlwaysWriteA in
(mem_set mem' id v', types, vals, visited) (mem_set mem' id v', types, vals, visited)
| RefT _ -> raise @@ Eval_error "write: ref type" | RefT _ -> raise @@ Eval_error "write: ref type"
| TupleT _ -> raise @@ Eval_error "write: tuple type" | TupleT _ -> raise @@ Eval_error "write: tuple type"
| _ -> raise @@ Eval_error "write: type") | _ -> raise @@ Eval_error "write: type")
| ReadS p -> if pathval mem vals p == SmthV || pathval mem vals p == BotV | ReadS p -> (match pathtype types p with
then raise @@ Eval_error "read: spoiled value" | UnitT (r, _) ->
else if pathval mem vals p != ZeroV if r == NRd
then raise @@ Eval_error "read: nontrivial value" then raise @@ Eval_error "read: write 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 | SeqS (sl, sr) -> let statel = stmt_eval state sl in
stmt_eval statel sr stmt_eval statel sr
| ChoiceS (sl, sr) -> let statel = stmt_eval state sl in | ChoiceS (sl, sr) -> let statel = stmt_eval state sl in
@ -518,23 +617,25 @@ struct
let rdS p = ReadS p let rdS p = ReadS p
let callS f args = CallS (f, args) let callS f args = CallS (f, args)
let uV m = UnitV (m, ZeroRV, ZeroWV)
(* - utils tests *) (* - utils tests *)
let%expect_test "mem add / get / set" = let%expect_test "mem add / get / set" =
let mem = empty_mem in let mem = empty_mem in
let (mem, id1) = mem_add mem ZeroV in let (mem, id1) = mem_add mem @@ uV ZeroMV in
let (mem, id2) = mem_add mem SmthV in let (mem, id2) = mem_add mem @@ uV SmthMV in
let (mem, id3) = mem_add mem BotV in let (mem, id3) = mem_add mem @@ uV BotMV in
Printf.printf "%i %i %i " id1 id2 id3; Printf.printf "%i %i %i " id1 id2 id3;
Printf.printf "%b %b %b " (mem_get mem id1 == ZeroV) Printf.printf "%b %b %b " (mem_get mem id1 == uV ZeroMV)
(mem_get mem id2 == SmthV) (mem_get mem id2 == uV SmthMV)
(mem_get mem id3 == BotV); (mem_get mem id3 == uV BotMV);
let mem = mem_set mem id1 BotV in let mem = mem_set mem id1 @@ uV BotMV in
let mem = mem_set mem id2 ZeroV in let mem = mem_set mem id2 @@ uV ZeroMV in
let mem = mem_set mem id3 SmthV in let mem = mem_set mem id3 @@ uV SmthMV in
Printf.printf "%b %b %b" (mem_get mem id1 == BotV) Printf.printf "%b %b %b" (mem_get mem id1 == uV BotMV)
(mem_get mem id2 == ZeroV) (mem_get mem id2 == uV ZeroMV)
(mem_get mem id3 == SmthV); (mem_get mem id3 == uV SmthMV);
[%expect {| 0 1 2 true true true true true true |}] [%expect {| 0 1 2 true true true true true true |}]
(* - basic var tests *) (* - basic var tests *)

77
model_with_structures/model.typ
View file

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