Wasm-DSL · zilinc · Apr 19, 2025 · Apr 19, 2025 · Mar 21, 2025 · Jun 17, 2025
diff --git a/specification/wasm-3.0/0.2-aux.num.spectec b/specification/wasm-3.0/0.2-aux.num.spectec
@@ -6,6 +6,10 @@ def $min(nat, nat) : nat
 def $min(i, j) = i  -- if $(i <= j)
 def $min(i, j) = j  -- otherwise
 
+def $max(nat, nat) : nat
+def $max(i, j) = i  -- if $(i >= j)
+def $max(i, j) = j  -- otherwise
+
 def $sum(nat*) : nat  hint(show (+) %) hint(macro none)
 def $sum(eps) = 0
 def $sum(n n'*) = $(n + $sum(n'*))

diff --git a/specification/wasm-3.0/0.3-aux.seq.spectec b/specification/wasm-3.0/0.3-aux.seq.spectec
@@ -11,14 +11,62 @@ def $opt_(syntax X, w) = w
 
 ;; Concatenation
 
-def $concat_(syntax X, (X*)*) : X*  hint(show (++) %2)
+def $concat_(syntax X, (X*)*) : X*  hint(show (++) %2) hint(inverse $invconcat_)
 def $concat_(syntax X, eps) = eps
 def $concat_(syntax X, (w*) (w'*)*) = w* ++ $concat_(X, (w'*)*)
 
-def $concatn_(syntax X, (X*)*, nat) : X*  hint(show (++) %2)
+def $concatn_(syntax X, (X*)*, nat) : X*  hint(show (++) %2) hint(inverse $invconcatn_)
 def $concatn_(syntax X, eps, n) = eps
 def $concatn_(syntax X, (w^n) (w'^n)*, n) = w^n $concatn_(X, (w'^n)*, n)
 
+def $invconcat_(syntax X, X*) : (X*)*        hint(builtin "inverse_of_concat")
+def $invconcatn_(syntax X, nat, X*) : (X*)*  hint(builtin "inverse_of_concatn")
+
+
+;; List manipulation
+
+
+;; This version might be easier to define in theorem provers (eyeball close)
+def $rev_(syntax X, X*) : X*
+def $rev_(syntax X, []) = []
+def $rev_(syntax X, w_0 w*) = $rev_(X, w*) w_0
+
+;; This version is more succinct in SpecTec.
+def $rev'_(syntax X, X*) : X*
+def $rev'_(syntax X, w^N) = (w^N[N-1-i])^(i < N)
+
+def $filter_(syntax X, def $p(X) : bool, X*) : X*
+def $filter_(syntax X, $p, []) = []
+def $filter_(syntax X, $p, w_0 w*) = w_0 $filter_(X, $p, w*)  -- if $p(w_0)
+def $filter_(syntax X, $p, w_0 w*) = $filter_(X, $p, w*)  -- otherwise
+
+
+def $take_(syntax X, nat, X*) : X*
+def $take_(syntax X, 0, w*) = []
+def $take_(syntax X, n, []) = []
+def $take_(syntax X, n, w w'*) = w $take_(X, $(n-1), w'*)  -- if n > 0
+
+def $take'_(syntax X, nat, X*) : X*
+def $take'_(syntax X, n, w^n') = w^n'    -- if n' < n
+def $take'_(syntax X, n, w^n w'*) = w^n
+
+def $takeWhile_(syntax X, def $p(X) : bool, X*) : X*
+def $takeWhile_(syntax X, $p, []) = []
+def $takeWhile_(syntax X, $p, w_0 w*) = w_0 $takeWhile_(X, $p, w*)  -- if $p(w_0)
+def $takeWhile_(syntax X, $p, w_0 w*) = []                          -- otherwise
+
+
+def $drop_(syntax X, nat, X*) : X*
+def $drop_(syntax X, 0, w*) = w*
+def $drop_(syntax X, n, []) = []
+def $drop_(syntax X, n, w w'*) = $drop_(X, $(n-1), w'*)  -- if n > 0
+
+;; Doesn't work with the interpreter backend
+def $drop'_(syntax X, nat, X*) : X*
+def $drop'_(syntax X, n, w^n') = []      -- if n' < n
+def $drop'_(syntax X, n, w^n w'*) = w'*
+
+
 
 ;; Set functions
 

diff --git a/specification/wasm-3.0/1.1-syntax.values.spectec b/specification/wasm-3.0/1.1-syntax.values.spectec
@@ -22,6 +22,7 @@ syntax u64 = uN(64)
 syntax u128 = uN(128)
 syntax s33 = sN(33)
 
+var d : bit
 var b : byte
 
 

diff --git a/specification/wasm-3.0/1.2-syntax.types.spectec b/specification/wasm-3.0/1.2-syntax.types.spectec
@@ -203,12 +203,15 @@ def $JN(64) = I64
 
 ;; Size
 
-def $size(numtype) : nat       hint(show |%|)
+def $size(numtype) : nat       hint(show |%|) hint(inverse $invsize)
 def $vsize(vectype) : nat      hint(show |%|)
 def $psize(packtype) : nat     hint(show |%|)
-def $lsize(lanetype) : nat     hint(show |%|)
+def $lsize(lanetype) : nat     hint(show |%|) hint(inverse $invlsize)
 def $zsize(storagetype) : nat  hint(show |%|)
 
+def $invsize(nat) : numtype    hint(builtin "inverse_of_size")
+def $invlsize(nat) : lanetype  hint(builtin "inverse_of_lsize")
+
 def $size(I32) = 32
 def $size(I64) = 64
 def $size(F32) = 32
@@ -228,7 +231,7 @@ def $zsize(packtype) = $psize(packtype)
 
 
 ;; TODO(2, rossberg): get rid of these terrible hacks by defining $Inn(nat) hint(show I#%)
-def $sizenn(numtype) : nat     hint(show N)   hint(macro none)  ;; HACK!
+def $sizenn(numtype) : nat     hint(show N)   hint(macro none) hint(inverse $invsizenn)  ;; HACK!
 def $sizenn1(numtype) : nat    hint(show N_1) hint(macro none)  ;; HACK!
 def $sizenn2(numtype) : nat    hint(show N_2) hint(macro none)  ;; HACK!
 def $sizenn(nt) = $size(nt)
@@ -241,13 +244,16 @@ def $vsizenn(vt) = $vsize(vt)
 def $psizenn(packtype) : nat   hint(show N)   hint(macro none)  ;; HACK!
 def $psizenn(pt) = $psize(pt)
 
-def $lsizenn(lanetype) : nat   hint(show N)   hint(macro none)  ;; HACK!
+def $lsizenn(lanetype) : nat   hint(show N)   hint(macro none) hint(inverse $invlsizenn)  ;; HACK!
 def $lsizenn1(lanetype) : nat  hint(show N_1) hint(macro none)  ;; HACK!
 def $lsizenn2(lanetype) : nat  hint(show N_2) hint(macro none)  ;; HACK!
 def $lsizenn(lt) = $lsize(lt)
 def $lsizenn1(lt) = $lsize(lt)
 def $lsizenn2(lt) = $lsize(lt)
 
+def $invsizenn(nat) : numtype    hint(builtin "inverse_of_sizenn")
+def $invlsizenn(nat) : lanetype  hint(builtin "inverse_of_lsizenn")
+
 
 ;; Unpacking