sideconditions: also traverse function clauses

[nomeata]

The totalize pass can cause TheE expressions appear in the RHS of functions:

 ;; ../../../../specification/wasm-3.0/1.2-syntax.types.spectec
-def $inv_isize(nat : nat) : Inn
+def $inv_isize(nat : nat) : Inn?
   ;; ../../../../specification/wasm-3.0/1.2-syntax.types.spectec
-  def $inv_isize(32) = I32_Inn
+  def $inv_isize(32) = ?(I32_Inn)
   ;; ../../../../specification/wasm-3.0/1.2-syntax.types.spectec
-  def $inv_isize(64) = I64_Inn
+  def $inv_isize(64) = ?(I64_Inn)
+  def $inv_isize{x0 : nat}(x0) = ?()
 
 ;; ../../../../specification/wasm-3.0/1.2-syntax.types.spectec
-def $inv_jsize(nat : nat) : Jnn
+def $inv_jsize(nat : nat) : Jnn?
   ;; ../../../../specification/wasm-3.0/1.2-syntax.types.spectec
-  def $inv_jsize(8) = I8_Jnn
+  def $inv_jsize(8) = ?(I8_Jnn)
   ;; ../../../../specification/wasm-3.0/1.2-syntax.types.spectec
-  def $inv_jsize(16) = I16_Jnn
+  def $inv_jsize(16) = ?(I16_Jnn)
   ;; ../../../../specification/wasm-3.0/1.2-syntax.types.spectec
-  def $inv_jsize{n : nat}(n) = ($inv_isize(n) : addrtype <: Jnn)
+  def $inv_jsize{n : nat}(n) = ?((!($inv_isize(n)) : addrtype <: Jnn))
+  def $inv_jsize{x0 : nat}(x0) = ?()

Such TheE containing branches should not be taken if the the value is none, so we should add that as a side-condition in that pass. So this is is the new side-condition added here:

 ;; ../../../../specification/wasm-3.0/0.3-aux.seq.spectec
@@ -1352,6 +1353,7 @@
   def $inv_jsize(16) = ?(I16_Jnn)
   ;; ../../../../specification/wasm-3.0/1.2-syntax.types.spectec
   def $inv_jsize{n : nat}(n) = ?((!($inv_isize(n)) : addrtype <: Jnn))
+    -- if ($inv_isize(n) =/= ?())
   def $inv_jsize{x0 : nat}(x0) = ?()

(There are cleaner translations possible here, but at least that makes it correct)

[nomeata]

Maybe not the right approach, this affects the pose output, that’s probably not desirable.

[nomeata]

These inv functions seem to not be explicitly used:

../specification/wasm-3.0/1.2-syntax.types.spectec:def $isize(Inn) : nat          hint(show |%|) hint(inverse $inv_isize)
../specification/wasm-3.0/1.2-syntax.types.spectec:def $jsize(Jnn) : nat          hint(show |%|) hint(inverse $inv_jsize)
../specification/wasm-3.0/1.2-syntax.types.spectec:def $fsize(Fnn) : nat          hint(show |%|) hint(inverse $inv_fsize)
../specification/wasm-3.0/1.2-syntax.types.spectec:def $inv_isize(nat) : Inn hint(partial)
../specification/wasm-3.0/1.2-syntax.types.spectec:def $inv_jsize(nat) : Jnn hint(partial)
../specification/wasm-3.0/1.2-syntax.types.spectec:def $inv_fsize(nat) : Fnn hint(partial)
../specification/wasm-3.0/1.2-syntax.types.spectec:def $inv_isize(32) = I32
../specification/wasm-3.0/1.2-syntax.types.spectec:def $inv_isize(64) = I64
../specification/wasm-3.0/1.2-syntax.types.spectec:def $inv_fsize(32) = F32
../specification/wasm-3.0/1.2-syntax.types.spectec:def $inv_fsize(64) = F64
../specification/wasm-3.0/1.2-syntax.types.spectec:def $inv_jsize(8)  = I8
../specification/wasm-3.0/1.2-syntax.types.spectec:def $inv_jsize(16) = I16
../specification/wasm-3.0/1.2-syntax.types.spectec:def $inv_jsize(n)  = $inv_isize(n)
../specification/wasm-3.0/1.2-syntax.types.spectec:def $jsizenn(Jnn) : nat   hint(show N) hint(macro none) hint(inverse $inv_jsizenn) ;; HACK!
../specification/wasm-3.0/1.2-syntax.types.spectec:def $inv_jsizenn(nat) : Jnn hint(partial)
../specification/wasm-3.0/1.2-syntax.types.spectec:def $inv_jsizenn(n)  = $inv_jsize(n)

As far as I can tell these are used only by the interpreter, so maybe they can be ignored for the purpose of mechanization?

So maybe we need a tree shaking pass so that we can focus on the declarations relevant for the mechanization?
Maybe with a hint to mark the “roots”? Or, if that’s too tedious, some heuristics (all relations named *_ok and Eval_* or so).

[rossberg]

Well, or inv functions add proof obligations for mechanisations, to show that they actually are inverses. ;)

[nomeata]

Sure, but one step at a time.

I could also wait for Diego’s def-to-rel pass, which (if run before sidecondition introduction) would also solve present problem.