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.

To first explain what this pass exactly does, we must first understand what specific functions we are converting to inductive relation:

• If it has any premises (note: at the moment it does not consider LetPr but it should in the future)
• It it has any non-linear patterns and definite length patterns (This should be handled by [Middlend] Non-linear and definite iteration pattern simplification #224)
• There are more binded variables than the ones utilized in the arguments (Note: this does consider LetPr, so the only binded variables left should just be random existentials that would be very unclear on how to deal with)
• The function is recursive (Note: would maybe be good to add a hint to force recursive functions to be actual functions when we know they will pass)
• It utilizes any function that has been converted to a relation

If a function fulfills any of these criterias, then it get transformed.

The transformation is done as such:

• It makes the parameters and return type be the relational signature, the last typ being the return type.
• It puts the function body as the last expression of the relation expression tuple, with everything before as the patterns of the clause, allowing the relation to pattern match on those.
• Other than that, it is a pretty 1:1 transformation, as they have a pretty similar structure. Once it has been created, it does one pass on all the new rules to see if there are any otherwise premise. If there is, it does a similar transformation as the otherwise removal pass.

The only other portion left is transforming the function calls. This portion is much trickier as we need to ensure the scope of the function call is preserved (i.e. when it is in an iterE). So the solution is as follows for each function call:

• We generate a fresh new variable to signify the return exp of the function
• We transform each function call into the relation utilizing the new fresh variable as the return exp.
• Then, utilizing a map made by collecting function calls, we go through all other premises replacing the function call into the return exp.
• We preserve and even make the new fresh variable into an iterated variable if need be (i.e. when the function call utilizes an iterated variable, that would mean the fresh variable also needs to be iterated upon). This also means we need to remove the iterated variable from the original iteration if it is not used anywhere else and add the fresh variable iteration.

To give a small example illustrating this, say we have:

def $foo(nat : nat) : nat
  def $foo(32) = 23
    -- if (320 = 320)
  def $foo(64) = 52

relation foo2: `%~>%`(nat*, nat*)
  rule test1{`a*` : nat*, `b*` : nat*}:
    `%~>%`(a*{a <- `a*`}, b*{b <- `b*`})
    -- (if ($foo(a) = $foo(b)))*{a <- `a*`, b <- `b*`}

This gets transformed into:

relation fun_foo: `%%`(nat, nat)
  rule fun_foo_case_0:
    `%%`(32, 23)
    -- if (320 = 320)

  rule fun_foo_case_1:
    `%%`(64, 52)

relation foo2: `%~>%`(nat*, nat*)
  rule test1{`a*` : nat*, `b*` : nat*, `var_1*` : nat*, `var_0*` : nat*}:
    `%~>%`(a*{a <- `a*`}, b*{b <- `b*`})
    -- (if (var_0 = var_1))*{var_0 <- `var_0*`, var_1 <- `var_1*`}
    -- (fun_foo: `%%`(b, var_1))*{var_1 <- `var_1*`, b <- `b*`}
    -- (fun_foo: `%%`(a, var_0))*{var_0 <- `var_0*`, a <- `a*`}

Notice how the new relational premises have preserved the iteration, and the if premise now has new iteration ids!

As you can probably see, this is a very complex pass.

Old 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)

[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).

[DCupello1]

Changed this to only do fallthrough whenever it spots an otherwise premise, instead of all the time. This is in line with what the actual semantics is supposed to be.

Other than maybe fixing names and reordering premises, this should be good to start being reviewed. It is a pretty complicated one to review though.

[nomeata]

It is a pretty complicated one to review though.

Yeah, I’m not sure if I can do a meaningful review :-/

[DCupello1]

It is a pretty complicated one to review though.

Yeah, I’m not sure if I can do a meaningful review :-/

Fair enough! I will probably just keep it as a draft until we make use of this pass in the mechanization backends.

Will also try to make it more readable!

[rossberg]

Just to understand this better: I'm a bit surprised that every function with premises is turned into a relation. That seems rather brittle, since a small source-level change to a definition might consist of adding a condition, but that would totally change the translation outcome. Naively, I would have expected that Boolean premises are fine for functions (as long as they don't involve free variables, which is already ruled out by the third condition). Is that because you want to translate Boolean expressions into something in prop?

[DCupello1]

Just to understand this better: I'm a bit surprised that every function with premises is turned into a relation. That seems rather brittle, since a small source-level change to a definition might consist of adding a condition, but that would totally change the translation outcome. Naively, I would have expected that Boolean premises are fine for functions (as long as they don't involve free variables, which is already ruled out by the third condition). Is that because you want to translate Boolean expressions into something in prop?

It is very restricting, I agree. However with boolean premises, the only way to translate it for ITPs would be to have if-then-else expressions. It should then be the case that the if-then-else-introduction pass should resolve this issue. But if it cannot, then we don't exactly have a good way to convert these functions into executable functions in ITPs.

Hopefully if we keep improving the ITE pass to cover all cases for boolean premises then it should never hit the case for functions that only have boolean premises. But it is still good to have that safety net in deftorel to ensure we can always compile in the mechanization side.

I would be fine with reporting some warning if this does happen though, as these functions are supposed to stay as functions.

(Also, I forgot a condition: if the function is recursive then it does get turned into a relation always as we cannot prove termination automatically in general! Will edit this)

[rossberg]

I see, makes sense!