Deftorel pass

[DCupello1]

This pull request is made to introduce the pass "deftorel". This pass does as the name suggests: convert specific function definitions to relations.

Example:

syntax A = 
  | B{nat : nat}(nat : nat)
  | C

def $foo(A : A) : nat
  def $foo{n : n}(B_A(n)) = 10
    -- if (n < 5)
  def $foo{n : n}(B_A(n)) = 5
    -- if n = 10
  def $foo{varA : A}(varA) = 20

to

relation fun_foo_before_fun_foo_case_1: `%`(A)
  rule fun_foo_case_0{n : nat}:
    `%`(B_A(n))
    -- if (n < 5)

relation fun_foo_before_fun_foo_case_2: `%`(A)
  rule fun_foo_case_1{n : nat}:
    `%`(B_A(n))
    -- ~ fun_foo_before_fun_foo_case_1: `%`(B_A(n))
    -- if (n = 10)
  rule fun_foo_case_0{n : nat}:
    `%`(B_A(n))
    -- if (n < 5)

relation fun_foo: `%%`(A, nat)
  rule fun_foo_case_0{n : nat}:
    `%%`(B_A(n), 10)
    -- if (n < 5)
  rule fun_foo_case_1{n : nat}:
    `%%`(B_A(n), 5)
    -- ~ fun_foo_before_fun_foo_case_1: `%`(B_A(n))
    -- if (n = 10)
  rule fun_foo_case_2{varA : A}:
    `%%`(varA, 20)
    -- ~ fun_foo_before_fun_foo_case_2: `%`(varA)

This pass does not ensure the created relations that handle the fallthrough semantics have unique name (yet).

Currently a draft as its not meant to be mergable yet, since more testing should be done to ensure it does the right thing. But for now it should give a way to track what is happening with this pass.

Validates up to Wasm 3.0. Have not tested it in Rocq, but will probably not compile due to name clashes.

Some todos:

• Potentially resolve name clashes as I did in Else pass
• Make a new pass that simplifies these generated relations (and also the ones generated by otherwise). This might be tricky because for these you would ideally want:

relation fun_foo: `%%`(A, nat)
  rule fun_foo_case_0{n : nat}:
    `%%`(B_A(n), 10)
    -- if (n < 5)
  rule fun_foo_case_1{n : nat}:
    `%%`(B_A(n), 5)
    -- if n >= 5
    -- if n = 10 
  rule fun_foo_case_2{n : nat , varA : A}:
    `%%`(varA, 20)
    -- (varA != B_A(n) \/ n >= 5)
    -- (varA != B_A(n) \/ n != 10)

This would be possible for boolean conditions but not for anything else. Maybe thats fine?

• Only possible for functions with Exp params, since parametrised relations don't exist yet. Will modify once thats done.
• Want to order well the generated function-rel premises (since order matters if we make them implications).

[nomeata]

I’m trying to merge this into the lean4 branch, but trying to update the test-prose and test-splice test output hangs (or maybe just takes longer than I want to wait). Do you also observe that?

[DCupello1]

Just ran the tests locally again to make sure, it all seems fine to me. I haven't changed either of them, so thats very weird.

[DCupello1]

Also, for visibility (I put this in #207 but not here).

After some testing on the rocq output, it seems like some recursive functions turning into relations do not pass as it doesn't pass the strictly positive condition. Lean will likely exhibit a similar error on the function utf8.

[nomeata]

Lean will likely exhibit a similar error on the function utf8.

That function definition is in 5.1-binary.values.spectec – would it make sense to first focus on the other parts of the specification (types, validation and execution), and postpone issues related to the binary and text format?

[DCupello1]

Lean will likely exhibit a similar error on the function utf8.

That function definition is in 5.1-binary.values.spectec – would it make sense to first focus on the other parts of the specification (types, validation and execution), and postpone issues related to the binary and text format?

Fair enough, but did some more quick testing and it happens to most recursive functions (subst_typevar and subst_typeuse for example)

[nomeata]

Maybe we need to push harder to make them translate as functions.

At least when the premises are on identical patterns like in

def $subst_typevar(tv, eps, eps) = tv
def $subst_typevar(tv, tv_1 tv'*, tu_1 tu'*) = tu_1                            -- if tv = tv_1
def $subst_typevar(tv, tv_1 tv'*, tu_1 tu'*) = $subst_typevar(tv, tv'*, tu'*)  -- otherwise

and they are all booleans or otherwise, it should be possible to translate that as if-then-else, shouldn’t it?

[DCupello1]

Maybe we need to push harder to make them translate as functions.

At least when the premises are on identical patterns like in

def $subst_typevar(tv, eps, eps) = tv
def $subst_typevar(tv, tv_1 tv'*, tu_1 tu'*) = tu_1                            -- if tv = tv_1
def $subst_typevar(tv, tv_1 tv'*, tu_1 tu'*) = $subst_typevar(tv, tv'*, tu'*)  -- otherwise

and they are all booleans or otherwise, it should be possible to translate that as if-then-else, shouldn’t it?

Yes, that was one of the things I was thinking of doing as well, for premises that are boolean conditions. I wanted a more general approach first though to see if it worked.

In some functions by the way, you can also transform some of the if premises into let premises (look at growmem for example) and any iterpr with boolean conditions could be List.all

[DCupello1]

With the new changes, the fallthrough premises no longer cause a (big) problem. Wasm 3.0 was compiled in Rocq (with some spec changes for partial funcs).