Skip to content

[spectec] Make definition of state access nicer #2036

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
rossberg merged 7 commits into from
Mar 24, 2026
Merged

[spectec] Make definition of state access nicer #2036

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
c7edbd0
[spectec] Make definition of state access nicer
rossberg Dec 2, 2025
56ca24e
Merge branch 'main' into state-shorthands
rossberg Mar 23, 2026
87835a2
HARDCODE: Handle the function '$store'
f52985 Mar 24, 2026
d2d3895
Test expects
rossberg Mar 24, 2026
db2d5c7
Merge branch 'main' into state-shorthands
rossberg Mar 24, 2026
e59bb69
Sync latest
rossberg Mar 24, 2026
4aa6930
Test expects
rossberg Mar 24, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 13 additions & 6 deletions specification/sync-wasm-latest.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,19 +30,26 @@ for FILE in $HIGHEST_FILES; do
if [ ! -f "$LATEST/$FILE" ]; then
echo "Added file $HIGHEST/$FILE"
((++HIGHEST_CHANGED))
elif [ "$HIGHEST/$FILE" -nt "$LATEST/$FILE" ] && ! diff -q "$HIGHEST/$FILE" "$LATEST/$FILE" >/dev/null; then
echo "Modified file $HIGHEST/$FILE"
((++HIGHEST_CHANGED))
elif ! diff -q "$HIGHEST/$FILE" "$LATEST/$FILE" >/dev/null; then
if [ "$HIGHEST/$FILE" -nt "$LATEST/$FILE" ]; then
echo "Modified file $HIGHEST/$FILE"
((++HIGHEST_CHANGED))
elif ! [ "$HIGHEST/$FILE" -ot "$LATEST/$FILE" ]; then
echo "❌ Error: Changes in both $HIGHEST/$FILE and $LATEST/$FILE with same date."
exit 1
fi
fi
done

for FILE in $LATEST_FILES; do
if [ ! -f "$HIGHEST/$FILE" ]; then
echo "Added file $LATEST/$FILE"
((++LATEST_CHANGED))
elif [ "$LATEST/$FILE" -nt "$HIGHEST/$FILE" ] && ! diff -q "$HIGHEST/$FILE" "$LATEST/$FILE" >/dev/null; then
echo "Modified file $LATEST/$FILE"
((++LATEST_CHANGED))
elif ! diff -q "$HIGHEST/$FILE" "$LATEST/$FILE" >/dev/null; then
if [ "$LATEST/$FILE" -nt "$HIGHEST/$FILE" ]; then
echo "Modified file $LATEST/$FILE"
((++LATEST_CHANGED))
fi
fi
done

Expand Down
50 changes: 28 additions & 22 deletions specification/wasm-3.0/4.0-execution.configurations.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -260,15 +260,21 @@ def $data(state, dataidx) : datainst hint(show %.DATAS[%]) hint(macro "
def $elem(state, tableidx) : eleminst hint(show %.ELEMS[%]) hint(macro "Z%")
def $local(state, localidx) : val? hint(show %.LOCALS[%]) hint(macro "Z%")

def $type((s; f), x) = f.MODULE.TYPES[x]
def $tag((s; f), x) = s.TAGS[f.MODULE.TAGS[x]]
def $global((s; f), x) = s.GLOBALS[f.MODULE.GLOBALS[x]]
def $mem((s; f), x) = s.MEMS[f.MODULE.MEMS[x]]
def $table((s; f), x) = s.TABLES[f.MODULE.TABLES[x]]
def $func((s; f), x) = s.FUNCS[f.MODULE.FUNCS[x]]
def $data((s; f), x) = s.DATAS[f.MODULE.DATAS[x]]
def $elem((s; f), x) = s.ELEMS[f.MODULE.ELEMS[x]]
def $local((s; f), x) = f.LOCALS[x]
def $sof(state) : store hint(show s)
def $fof(state) : frame hint(show f)

def $sof(z) = $store(z)
def $fof(z) = $frame(z)

def $type(z, x) = $fof(z).MODULE.TYPES[x]
def $tag(z, x) = $sof(z).TAGS[$fof(z).MODULE.TAGS[x]]
def $global(z, x) = $sof(z).GLOBALS[$fof(z).MODULE.GLOBALS[x]]
def $mem(z, x) = $sof(z).MEMS[$fof(z).MODULE.MEMS[x]]
def $table(z, x) = $sof(z).TABLES[$fof(z).MODULE.TABLES[x]]
def $func(z, x) = $sof(z).FUNCS[$fof(z).MODULE.FUNCS[x]]
def $data(z, x) = $sof(z).DATAS[$fof(z).MODULE.DATAS[x]]
def $elem(z, x) = $sof(z).ELEMS[$fof(z).MODULE.ELEMS[x]]
def $local(z, x) = $fof(z).LOCALS[x]


;; State update
Expand All @@ -284,25 +290,25 @@ def $with_data(state, dataidx, byte*) : state hint(show %[.DATAS[%
def $with_struct(state, structaddr, nat, fieldval) : state hint(show %[.STRUCTS[%].FIELDS[%] = %]) hint(macro "ZS%") hint(prose "Replace" $structinst(%1)[%2].FIELDS[%3] "with" %4)
def $with_array(state, arrayaddr, nat, fieldval) : state hint(show %[.ARRAYS[%].FIELDS[%] = %]) hint(macro "ZA%") hint(prose "Replace" $arrayinst(%1)[%2].FIELDS[%3] "with" %4)

def $with_local((s; f), x, v) = s; f[.LOCALS[x] = v]
def $with_global((s; f), x, v) = s[.GLOBALS[f.MODULE.GLOBALS[x]].VALUE = v]; f
def $with_table((s; f), x, i, r) = s[.TABLES[f.MODULE.TABLES[x]].REFS[i] = r]; f
def $with_tableinst((s; f), x, ti) = s[.TABLES[f.MODULE.TABLES[x]] = ti]; f
def $with_mem((s; f), x, i, j, b*) = s[.MEMS[f.MODULE.MEMS[x]].BYTES[i : j] = b*]; f
def $with_meminst((s; f), x, mi) = s[.MEMS[f.MODULE.MEMS[x]] = mi]; f
def $with_elem((s; f), x, r*) = s[.ELEMS[f.MODULE.ELEMS[x]].REFS = r*]; f
def $with_data((s; f), x, b*) = s[.DATAS[f.MODULE.DATAS[x]].BYTES = b*]; f
def $with_struct((s; f), a, i, fv) = s[.STRUCTS[a].FIELDS[i] = fv]; f
def $with_array((s; f), a, i, fv) = s[.ARRAYS[a].FIELDS[i] = fv]; f
def $with_local(z, x, v) = $sof(z); $fof(z)[.LOCALS[x] = v]
def $with_global(z, x, v) = $sof(z)[.GLOBALS[$fof(z).MODULE.GLOBALS[x]].VALUE = v]; $fof(z)
def $with_table(z, x, i, r) = $sof(z)[.TABLES[$fof(z).MODULE.TABLES[x]].REFS[i] = r]; $fof(z)
def $with_tableinst(z, x, ti) = $sof(z)[.TABLES[$fof(z).MODULE.TABLES[x]] = ti]; $fof(z)
def $with_mem(z, x, i, j, b*) = $sof(z)[.MEMS[$fof(z).MODULE.MEMS[x]].BYTES[i : j] = b*]; $fof(z)
def $with_meminst(z, x, mi) = $sof(z)[.MEMS[$fof(z).MODULE.MEMS[x]] = mi]; $fof(z)
def $with_elem(z, x, r*) = $sof(z)[.ELEMS[$fof(z).MODULE.ELEMS[x]].REFS = r*]; $fof(z)
def $with_data(z, x, b*) = $sof(z)[.DATAS[$fof(z).MODULE.DATAS[x]].BYTES = b*]; $fof(z)
def $with_struct(z, a, i, fv) = $sof(z)[.STRUCTS[a].FIELDS[i] = fv]; $fof(z)
def $with_array(z, a, i, fv) = $sof(z)[.ARRAYS[a].FIELDS[i] = fv]; $fof(z)


def $add_structinst(state, structinst*) : state hint(show %[.STRUCTS =++ %]) hint(macro "Z%") hint(prose "Append" %2 "to" $structinst(%1))
def $add_arrayinst(state, arrayinst*) : state hint(show %[.ARRAYS =++ %]) hint(macro "Z%") hint(prose "Append" %2 "to" $arrayinst(%1))
def $add_exninst(state, exninst*) : state hint(show %[.EXNS =++ %]) hint(macro "Z%") hint(prose "Append" %2 "to" $exninst(%1))

def $add_structinst((s; f), si*) = s[.STRUCTS =++ si*]; f
def $add_arrayinst((s; f), ai*) = s[.ARRAYS =++ ai*]; f
def $add_exninst((s; f), exn*) = s[.EXNS =++ exn*]; f
def $add_structinst(z, si*) = $sof(z)[.STRUCTS =++ si*]; $fof(z)
def $add_arrayinst(z, ai*) = $sof(z)[.ARRAYS =++ ai*]; $fof(z)
def $add_exninst(z, exn*) = $sof(z)[.EXNS =++ exn*]; $fof(z)


;; Growing
Expand Down
50 changes: 28 additions & 22 deletions specification/wasm-latest/4.0-execution.configurations.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -260,15 +260,21 @@ def $data(state, dataidx) : datainst hint(show %.DATAS[%]) hint(macro "
def $elem(state, tableidx) : eleminst hint(show %.ELEMS[%]) hint(macro "Z%")
def $local(state, localidx) : val? hint(show %.LOCALS[%]) hint(macro "Z%")

def $type((s; f), x) = f.MODULE.TYPES[x]
def $tag((s; f), x) = s.TAGS[f.MODULE.TAGS[x]]
def $global((s; f), x) = s.GLOBALS[f.MODULE.GLOBALS[x]]
def $mem((s; f), x) = s.MEMS[f.MODULE.MEMS[x]]
def $table((s; f), x) = s.TABLES[f.MODULE.TABLES[x]]
def $func((s; f), x) = s.FUNCS[f.MODULE.FUNCS[x]]
def $data((s; f), x) = s.DATAS[f.MODULE.DATAS[x]]
def $elem((s; f), x) = s.ELEMS[f.MODULE.ELEMS[x]]
def $local((s; f), x) = f.LOCALS[x]
def $sof(state) : store hint(show s)
def $fof(state) : frame hint(show f)

def $sof(z) = $store(z)
def $fof(z) = $frame(z)

def $type(z, x) = $fof(z).MODULE.TYPES[x]
def $tag(z, x) = $sof(z).TAGS[$fof(z).MODULE.TAGS[x]]
def $global(z, x) = $sof(z).GLOBALS[$fof(z).MODULE.GLOBALS[x]]
def $mem(z, x) = $sof(z).MEMS[$fof(z).MODULE.MEMS[x]]
def $table(z, x) = $sof(z).TABLES[$fof(z).MODULE.TABLES[x]]
def $func(z, x) = $sof(z).FUNCS[$fof(z).MODULE.FUNCS[x]]
def $data(z, x) = $sof(z).DATAS[$fof(z).MODULE.DATAS[x]]
def $elem(z, x) = $sof(z).ELEMS[$fof(z).MODULE.ELEMS[x]]
def $local(z, x) = $fof(z).LOCALS[x]


;; State update
Expand All @@ -284,25 +290,25 @@ def $with_data(state, dataidx, byte*) : state hint(show %[.DATAS[%
def $with_struct(state, structaddr, nat, fieldval) : state hint(show %[.STRUCTS[%].FIELDS[%] = %]) hint(macro "ZS%") hint(prose "Replace" $structinst(%1)[%2].FIELDS[%3] "with" %4)
def $with_array(state, arrayaddr, nat, fieldval) : state hint(show %[.ARRAYS[%].FIELDS[%] = %]) hint(macro "ZA%") hint(prose "Replace" $arrayinst(%1)[%2].FIELDS[%3] "with" %4)

def $with_local((s; f), x, v) = s; f[.LOCALS[x] = v]
def $with_global((s; f), x, v) = s[.GLOBALS[f.MODULE.GLOBALS[x]].VALUE = v]; f
def $with_table((s; f), x, i, r) = s[.TABLES[f.MODULE.TABLES[x]].REFS[i] = r]; f
def $with_tableinst((s; f), x, ti) = s[.TABLES[f.MODULE.TABLES[x]] = ti]; f
def $with_mem((s; f), x, i, j, b*) = s[.MEMS[f.MODULE.MEMS[x]].BYTES[i : j] = b*]; f
def $with_meminst((s; f), x, mi) = s[.MEMS[f.MODULE.MEMS[x]] = mi]; f
def $with_elem((s; f), x, r*) = s[.ELEMS[f.MODULE.ELEMS[x]].REFS = r*]; f
def $with_data((s; f), x, b*) = s[.DATAS[f.MODULE.DATAS[x]].BYTES = b*]; f
def $with_struct((s; f), a, i, fv) = s[.STRUCTS[a].FIELDS[i] = fv]; f
def $with_array((s; f), a, i, fv) = s[.ARRAYS[a].FIELDS[i] = fv]; f
def $with_local(z, x, v) = $sof(z); $fof(z)[.LOCALS[x] = v]
def $with_global(z, x, v) = $sof(z)[.GLOBALS[$fof(z).MODULE.GLOBALS[x]].VALUE = v]; $fof(z)
def $with_table(z, x, i, r) = $sof(z)[.TABLES[$fof(z).MODULE.TABLES[x]].REFS[i] = r]; $fof(z)
def $with_tableinst(z, x, ti) = $sof(z)[.TABLES[$fof(z).MODULE.TABLES[x]] = ti]; $fof(z)
def $with_mem(z, x, i, j, b*) = $sof(z)[.MEMS[$fof(z).MODULE.MEMS[x]].BYTES[i : j] = b*]; $fof(z)
def $with_meminst(z, x, mi) = $sof(z)[.MEMS[$fof(z).MODULE.MEMS[x]] = mi]; $fof(z)
def $with_elem(z, x, r*) = $sof(z)[.ELEMS[$fof(z).MODULE.ELEMS[x]].REFS = r*]; $fof(z)
def $with_data(z, x, b*) = $sof(z)[.DATAS[$fof(z).MODULE.DATAS[x]].BYTES = b*]; $fof(z)
def $with_struct(z, a, i, fv) = $sof(z)[.STRUCTS[a].FIELDS[i] = fv]; $fof(z)
def $with_array(z, a, i, fv) = $sof(z)[.ARRAYS[a].FIELDS[i] = fv]; $fof(z)


def $add_structinst(state, structinst*) : state hint(show %[.STRUCTS =++ %]) hint(macro "Z%") hint(prose "Append" %2 "to" $structinst(%1))
def $add_arrayinst(state, arrayinst*) : state hint(show %[.ARRAYS =++ %]) hint(macro "Z%") hint(prose "Append" %2 "to" $arrayinst(%1))
def $add_exninst(state, exninst*) : state hint(show %[.EXNS =++ %]) hint(macro "Z%") hint(prose "Append" %2 "to" $exninst(%1))

def $add_structinst((s; f), si*) = s[.STRUCTS =++ si*]; f
def $add_arrayinst((s; f), ai*) = s[.ARRAYS =++ ai*]; f
def $add_exninst((s; f), exn*) = s[.EXNS =++ exn*]; f
def $add_structinst(z, si*) = $sof(z)[.STRUCTS =++ si*]; $fof(z)
def $add_arrayinst(z, ai*) = $sof(z)[.ARRAYS =++ ai*]; $fof(z)
def $add_exninst(z, exn*) = $sof(z)[.EXNS =++ exn*]; $fof(z)


;; Growing
Expand Down
Binary file modified spectec/doc/example/output/NanoWasm.pdf
View file
Open in desktop
Binary file not shown.
4 changes: 4 additions & 0 deletions spectec/src/backend-interpreter/interpreter.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -359,6 +359,7 @@ and eval_expr env expr =
fail_expr expr (sprintf "cannot choose an element from %s because it's empty" (string_of_expr e))
else
Array.get a 0
(* HARDCODE: The variable s is always assumed to be the implicit store *)
| VarE "s" -> Store.get ()
| VarE name -> lookup_env name env
(* Optimized getter for simple IterE(VarE, ...) *)
Expand Down Expand Up @@ -796,6 +797,9 @@ and create_context (name: string) (args: value list) : AlContext.mode =
AlContext.al (name, params, body, env, 0)

and call_func (name: string) (args: value list) : value option =
(* HARDCODE: Calling the function named `store` is always implicitly assumed to be the getting the global store, as if the variable named `s`. *)
if name = "store" then Some (Store.get ()) else

let builtin_name, is_builtin =
match find_hint name "builtin" with
| None -> name, false
Expand Down
2 changes: 1 addition & 1 deletion spectec/src/il2al/transpile.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1025,7 +1025,7 @@ let hide_state instr =
let access = { (mk_access ps s) with note } in
[ appendI (access, e) ~at:at ]
(* Return *)
| ReturnI (Some e) when is_state e || is_store e -> [ returnI None ~at:at ]
| ReturnI (Some ({it = VarE _; _} as e)) when is_state e || is_store e -> [ returnI None ~at:at ]
| _ -> [ instr ]

let remove_state algo =
Expand Down
Loading
Loading