Geb generates incorrect function for the identity lambda-abstraction #93
Comments
|
For reference, here is the current syntax taking the above term to Vamp-IR under the name "name":
The current output is
|
|
Although the current output differs from the original, I still get a proof verification error from it during the |
You'll need to send in |
You mean give |
|
It doesn't work with |
|
You can speed up a setup using the Or better yet, skip the setup altogether and use |
|
Also, if the setup size is too small you will get an error about the trimming degree rather than proof verification. A proof verification error should only mean the circuit is not satisfied. |
|
This problem still exists, but the fix in #99 does change the output circuit, so for reference, here's the new one: I've tried several constraints and none of them has worked, so I don't know what this circuit is actually outputting yet. @lopeetall is working on debug features that should make this easy to determine, and @AHartNtkn is doing some refactoring for using multivariate polynomials which I suspect might also make it straightforward (particularly in conjunction with my forthcoming cat-spec API) for us to write an interpreter for the subset of VampIR that we use in Geb itself, which would not only help with debugging issues such as this, but would also help with formally verifying the whole pipeline throughout Geb. |
|
Here's the new |
|
I can probably write the interpreter for the parts of vampir we use, it'd be woefully incomplete, but I could just quickly draft up an interpreter for the vampir we use like #98 does for the other categories we have |
That'd certainly be great if it's not too much work! We could port it (along with everything else) to the new, modular cat-spec API once I have that in (and itself ported). I think this bug must be in I guess the divisions aren't reducing yet? Even if they were, though, these wouldn't be the right answers. So I think that this particular bug is happening before we get to the translation to VampIR. (Hence we don't need any VampIR-level debug features to address this specific issue.) |
|
I tried to figure out how to get I was trying to apply the checked term (which ought to be equivalent to the identity) to |
what is the If so, then actually inject-left
is all you should need. We use realized-objects here. See this example GEB> (gapply (pair (<-left so1 geb-bool:bool)
(<-right so1 geb-bool:bool))
(list so1 (left geb-bool:true-obj)))
(s-1 (left GEB-BOOL:TRUE)) |
|
Just checked: previous STLC logic also does not work. Working in https://github.com/anoma/geb/tree/mariari/interpreter and changing the
and
|
|
I just realized something -- this is generating a function that returns a lambda abstraction. It's not returning a function that applies the lambda abstraction. What it's returning is the quoted value of the identity function. |
|
I'm not sure what This does what I'd expect. The way the Idris is written is that the STLC context is where the inputs to the circuit come from; if the STLC context is empty then you get a constant value. The constant value of a lambda abstraction, in particular, is just the I'm not sure what we're doing in the Lisp yet with the latest STLC code. |
|
Assigning to @agureev as he knows what to do. :) |
|
Update: apologies for a very silly error. The new API does not change the value of the function we feed it in. I simply supplied a context when it did not need to be supplied. In particular, the appropriate code to reproducing Lukasz's original entry/output is.
Note the empty context here. Adding in a boolean to the context is what caused the incremental change in the Vamp-IR code. Moreover, using the uncurry API as well as @mariari interpreter one can check that the STLC -> Geb compilation actually works well, i.e. pointwise produces an identity function. In other words, the mistake seems to linger in the polynomial part of the compilation. |
|
If I understand the above comment correctly, then #107 will fix this specific bug because the |
|
No, even in this case after uncurrying, the |
Okay, that makes sense. In that case, would you please file a separate issue for the |
|
With #108 the code seems to work GEB-TEST> (bitc:to-circuit (geb:to-bitc (geb.lambda:compile-checked-term
(list (coprod so1 so1))
(coprod so1 so1)
(geb.lambda:lamb (coprod so1 so1)
(coprod so1 so1)
(geb.lambda:index 1))))
:foo)
def foo x1 = {
((1 - 0) * x1) + (0 * x1);
((1 - 1) * x1) + (1 * x1)
};if handed 1 it should return 1, if handed 0, it'd return 0 |
|
Are de Bruijn indices in the GEB STLC front-end 0-based or 1-based? I thought they're 0-based and that's what we generate. |
they are 0 based, however, due to the way |
|
I'm asking because you have |
it points to the top context, which is non ideal. Once the code changed it will be properly index 0 with a null starting context |
I compile the following
with
The output is:
At the end I add a constraint to test this:
I run:
I get:
By the way, the encoding of the identity function needs 2^14 parameters which seems a bit too much.
The text was updated successfully, but these errors were encountered: