lurk-lab / lurk-rs Goto Github PK

Currently we are not using Poseidon gadget to check the hash calculation is correct in the circuit. We need to fix that problem with high priority.

#7 implements a dummy var with name "_" for zero-arg functions. That works fine for now, but if/when _ becomes a legal symbol character (which it probably should), it will be possible to create bogus programs depending on the sugar. Like ((lambda () (+ _ 1)) 1).

This needs more thought if we stay with the dummy var approach.

#166 implements mod, but not in the circuit.

Now that we have the unop char, we have another reason to implement range checks, because we currently we have no mechanism to constrain (in the circuit) the input of char has 32 bits.

For instance, we have that (char 5000000000) is going to fail, which obviously must be fixed. In particular, in this situation, if the input doesn't belong to the range, we must have an error.

Range checks will also be important for implementation of other types in Lurk.

This will actually now be resolved by the latest commit in #135.

I modified a Lurk test to produce an intentional failure. Running the Lurk test caused a panic as expected but the message was uninformative.

thread 'main' panicked at 'assertion failed: `(left == right)`
  left: `Ptr(Num, RawPtr(5, PhantomData))`,
 right: `Ptr(Num, RawPtr(4, PhantomData))`', src/repl.rs:278:33
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

As noted in a comment on #183, we currently allow lambda forms that don't have exactly one body element. It would be better if this led to an error.

Examples:

Lurk REPL welcomes you.
> (lambda (x))
[1 iterations] => <FUNCTION (X) )>
> (lambda (x) 1)
[1 iterations] => <FUNCTION (X) 1)>
> (lambda (x) 1 2)
[1 iterations] => <FUNCTION (X) 1 2)>
> ((lambda (x) 1 2) 9)
[4 iterations] => 1

Since we want to avoid extra destructuring (car_cdr()), which incurs hashing costs in the circuit, the check should not come at the time of creating the function, but later (probably when handling Continuation::Call2 in apply_continuation().), when the body is being inspected.

The Nix build works, but when running the example you get:

~/lurk-rs master
❄ λ nix run .#lurk-example
error: builder for '/nix/store/na18s2l4c2vqf8nk5gvmxkgwbxnphw3z-lurk-deps-0.1.0.drv' failed with exit code 101;
       last 10 log lines:
       >   failed to clone into: /build/dummy-src/.cargo-home/git/db/bellperson-2a76e4554f04bda6
       >
       > Caused by:
       >   network failure seems to have happened
       >   if a proxy or similar is necessary `net.git-fetch-with-cli` may help here
       >   https://doc.rust-lang.org/cargo/reference/config.html#netgit-fetch-with-cli
       >
       > Caused by:
       >   failed to resolve address for github.com: Name or service not known; class=Net (12)
       > [naersk] cargo returned with exit code 101, exiting
       For full logs, run 'nix log /nix/store/na18s2l4c2vqf8nk5gvmxkgwbxnphw3z-lurk-deps-0.1.0.drv'.
error: 1 dependencies of derivation '/nix/store/4hfs7wjgyhp0mi778vfd1rvadjqp7y0p-lurk-0.1.0.drv' failed to build

Is this because of

[patch.crates-io]
bellperson = { git = "https://github.com/filecoin-project/bellperson", branch = "instance-aggregation" }
nova = { git = "https://github.com/porcuquine/nova", package = "nova-snark" }

in the Cargo.toml?

#160 implements eval, but not in the circuit.
Once merged, #165 will also need circuit.

Looks like REPL is taking paths relatively to target/release/ rather than from wherever it's called:

Trying to evaluate a cons pair like (1 . 1) causes panic.

~/workspace/lurk-rs $ lurkrs
Lurk REPL welcomes you.
> (1 . 1)
thread 'main' panicked at 'Can only extract car_cdr from Cons', /home/user/workspace/lurk-rs/src/store.rs:1943:17
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

circuit_frame::reduce_sym() needs careful attention. Naming could stand to be more principled and normalized. There may be latent bugs. A complete refactor might be in order, especially if that reduces (or at least doesn't increase) constraints.

Currently, running make fibonacci-proof.json on master causes the following error:

➜  examples git:(master) ✗ make fibonacci-proof
cargo run --release -- prove --expression fibonacci.lurk --proof fibonacci-proof.json
    Finished release [optimized] target(s) in 0.09s
     Running `/Users/jonat/lurk-rs/target/release/fcomm prove --expression fibonacci.lurk --proof fibonacci-proof.json`
thread 'main' panicked at 'failed to read file: Error("expected value", line: 1, column: 1)', /Users/jonat/lurk-rs/fcomm/src/lib.rs:413:44
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
make: *** [fibonacci-proof.json] Error 101

README instructions are here.

The above command does work on the fcomm-commitment branch. On master, you have to run the cargo command with --lurk added to make it work (cargo run --release -- prove --expression fibonacci.lurk --proof fibonacci-proof.json --lurk).

It seems like either the JSON needs to be fixed to work as it does on fcomm-commitment branch or the makefile on master needs to update to include --lurk.

I have the following error:

Lurk REPL welcomes you.
> "}"
Mismatched brackets: '}' is unpaired
> "\} "
Mismatched brackets: '}' is unpaired

Also happens with () and []. There's also an error with . interactions within strings too, but I haven't been able to minimize the example yet.

CI seems to have become very slow for mac and arm64 — so much so that we are seeing failures due to timeouts. Even without that, it's taking too long…

Prior to merging #143, master was performing well (at least status quo didn't exhibit this problem).

Previous:
b57acd5
https://app.circleci.com/pipelines/github/lurk-lang/lurk-rs/593/workflows/9e8547a0-f9ed-4859-8a05-ce620907496a

After #143 merged, we see the problem on master (and saw it on the branch, so it's not a surprise).

Slow:
00242f1
https://app.circleci.com/pipelines/github/lurk-lang/lurk-rs/613/workflows/0a04e249-c65e-49f1-b665-fc99a1001bf3

However, the same problem seems to have been affecting #152 — even before it was rebased to include the work from #143. This suggests maybe something else is going on, but it's not clear what.

I've seemingly ruled out the possibility that this is strictly due to some CI configuration or anything else entirely external, because I reran CI on the previous 'good' commit, and that did not display the problem:
https://app.circleci.com/pipelines/github/lurk-lang/lurk-rs/593/workflows/1ee45b5f-fd19-4081-9653-03e677ccd1ed

The expression '(cons # "")' doesn't give an error, as expected. Instead, it returns '("")', because symbol '#' is replaced by nothing, which means the expression is the same as '(cons "")'.

During code coverage exploration, I noticed that some functions with no coverage also have nothing referring to them in the lurkrs project (including fcomm).

Here is an example, in hash_witness.rs:

    pub fn get_named_cons(&self, name: &ConsName) -> HashStub<F> {
        for (slot_name, p) in &self.slots {
            if slot_name == name {
                return *p;
            }
        }

        Stub::Dummy
    }

The compiler is not flagging them as unused because of this (in lib.rs):

pub mod hash_witness;

I am not sure if the intention here is for consumers of lurkrs as a library to call this function (even though nothing in the fcomm examples does). Or it could be that this function is actually not needed.

The fact that all the modules have the pub modifier is a bit suspect. As long as that's the case, we can potentially leak unused functions without knowing it.

Example:

> (/ (u64 5) (u64 0))
[7 iterations] => ERROR!
> (% (u64 5) (u64 0))
thread 'main' panicked at 'attempt to calculate the remainder with a divisor of zero', src/uint.rs:80:55
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

As noted in #203, coercion to char with (char …) doesn't do any typechecking, which means its possible to create a proof of an evaluation whose output is a malformed Char.

For example:

(char (- 0 1))

This won't work in lurk-rs out of the box, since the evaluation will result in an error, but if the frame input were created 'maliciously', such a proof could still be generated.

Attempting to do this should either result in an explicit, provable error — or a truncated result guaranteed to be in range. The latter is probably preferable, by analogy to u64.

> (u64 (- 0 1))
[5 iterations] => 10108024940646105088u64

REPL example:

!(:assert someundefsymbol) = T 

!(:load...) command in the REPL not finding corresponding .lurk file (see error message below).

Lurk REPL welcomes you.
> !(:load “../lurk-lib/test.lurk”)
Loading from /Users/../lurk-rs/target/release/../lurk-lib/test.lurk.
Error: No such file or directory (os error 2)

We want to be able to embed Lurk code in our blog posts for the lurk-lang blog on Hugo.

Here are the desired features:

• In Hugo, blog post writer can use some kind of markup to create a runnable code block in the blog post. (runs with a button click in the REPL)
• Additional markup should be able to designate whether the reader is able to edit the code (if so, there should be a 'reset') feature
• While we will want to embed runnable code blocks in posts, we will also likely want to highlight specific lines of code for more specific discussion/explainer. As such, we'll want a markup feature that lets us hide the other lines of code from view, while still retaining them so that the code will run at the click of a button. A great example of this is in the Rust book. You can see whole blocks of runnable code, as well as a few lines of code (in the latter half of the page) that have a 'show/hide' button (as an eyeball icon) that does what I'm talking about in this bullet point.

@alvin-reyes is going to work on this August 1-5, minimally, but it would be ideal to have someone else who can support this work since his attention is notably split between this and other things.

(Just a note that whoever does this will need access to the lurk-lang-blog repo, which is currently private.)

This issue is for tracking / linking to PR 13 ("A non-trivial FinalSNARK implementation") in the Nova repo.

microsoft/Nova#13

This issue is for tracking / linking to PR 76 ("Refactor to allow non-determinisim.") in the Nova repo.

microsoft/Nova#76

Lurk currently allows binding any form at all as the 'variable' on the left-hand-side of a binding in let or letrec.

However, only symbols are ever looked up when evaluating.

It should be an evaluation-time syntax error to perform these useless bindings. Allowing them is confusing, can mask actual errors, and also has a performance cost (in other lookups).

Some example of the behavior we should eliminate follow. All of these should be explicit errors.

Lurk REPL welcomes you.
> (let (((a b) 123)) 1)
[3 iterations] => 1
> (let ((:a 123)) :a)
[3 iterations] => :A
> (let ((9 123)) 9)
[3 iterations] => 9

Because EMIT effectively produces order-dependent side effects, we 'need' BEGIN. This is not strictly true, since we can use IF (or LET, LAMBDA, etc.) for sequencing, but an explicit sequencing operator is very convenient. Moreover, it's in the spec and as implemented in api.lisp: https://github.com/lurk-lang/lurk/blob/master/spec/v0-1.md#begin

We should add a spec test in lurk-lib, then implement here and in circuit.

This relatedly suggests we should:

• synthesize and check circuits for spec tests
• add a mechanism for testing emitted values during evaluation

The above might best be treated discretely, in which case they can be broken into new issues.

Now that evaluation returns a Result (#144), we should update the REPL to fail gracefully rather than continue to panic because of unwrapping any errors which result.

@weissjeffm we'd like to have you work on parameter caching for Lurk. @samuelburnham should be able to help you orient, generally, and @porcuquine can add specific details were needed.

This should get integrated with zaps (and by extension the current website).

Currently, zero-arg functions are implemented using a dummy argument while multi-arg functions are implemented by auto-currying. Both of these representations have a bit of inefficiencies in number of iterations.

We could change the representation of call continuations for efficiency.

It would be useful to be able to pass such a limit in JSON together with source code in JSON. (discussed with @porcuquine)

This is a tracking issue for pending circuit support issues. Our current workflow is to first add non-circuit support for new features, then update the circuit accordingly (in a separate PR). Whenever such new functionality is added, we should create a corresponding circuit issue and add a link to the list below. When the issue is closed, the box in the checkbox-list below should be checked.

Let's keep this issue open as a master list to be done and historically completed.

• #161
• #163
• #167
• #178
• #184
• #186
• #204
• #219
• #421

> (cons (lambda (x y) nil) nil)
thread 'main' panicked at 'double booked: found Lambda when getting UnevaledArgs', /home/user/workspace/lurk-rs/src/hash_witness.rs:190:13

Tested on 270ac76

This issue exists for tracking and any discussion that may arise. Work is in progress (cc: @dignifiedquire).

See #51 for details. This is a placeholder description, with more detail in the linked PR.

Hi from Yatima. For the Yatima to Lurk transpiler, we would like to be able to use unicode characters so the translated names can be preserved.

We would like at least the greek alphabet α, β, ..., superscripts a¹, and subscripts a₁. Perhaps some math notation such as ∧ ∨ ∑, although these have much less priority. Let us know how much flexibility there is in the parser for these. Thanks!

From our discussion in discord: We would also like to have case sensitivity when symbol escaping.

Solve the following items:

• Refactor reduce_witness() to return Result<...>
• Create Lurk errors
• Replace panics by Lurk errors where applicable
• Review remaining panics in car_cdr_mut()
• Refactor car_cdr() as car_cdr_mut()

In some situations we are returning nil instead of proper dummy pointers. We need to take care because sometimes eval can be adapted to generate corrupted frames that lead to invalid proofs (breaking soundness). Moreover, using dummy pointers would improve readability of the code. We need to add:

• bogus dummy, for parts of the circuits that are not being exercised depending on some condition like a continuation tag or the head of an expression.
• blank dummy, for the initial phase of the circuit construction.

#162 implements U64, but not in the circuit.

Since the fcomm examples and readme are likely to change and develop, it would be great to have CI test(s) to ensure the entire process from committing to verifying works as intended.

As currently implemented, the largest Num that can be read is u64::MAX.

> 18446744073709551617
[1 iterations] => 1

This issue is a placeholder for a larger discussion.

This comment has some partial context, linked here to preserve it: https://github.com/lurk-lang/lurk-rs/pull/87/files#r857858272

See #148 for an example where these tests were broken but CI didn't tell us.

 (lambda () 1)

: Lurk REPL welcomes you.
: > [1 iterations] => <FUNCTION () 1)>
: > Exiting...

Note the last closing paren doesn't have an opening paren. Should probably look like this:

<(FUNCTION () 1)>

This is a tracking issue which should not be closed until all known circuit issues have been resolved.

Known issues:

• (fib 100) proofs fail to verify. [verified fixed in #113]
• test_create_open_and_verify_complicated_higher_order_functional_commitment2 fails (fcomm).
• Error handling: in some cases either eval or circuit synthesis panics in error cases. Both should return explicit error.
• FIXME: There are some cases in the circuit marked with FIXME because some known implementation detail has been deferred.

We from Yatima are working in the Yatima IR to Lurk transpiler and we'd like to be able to map underscores in Lean identifiers to underscores in Lurk identifiers because we're reserving dashes for Lean's dots.

Our previous solutions used colons, but that's not a good solution in terms of semantics for Lurk code.

As an example, the expression '(cons "")' should return an error, but instead it evaluates successfully because second argument is treated as NIL. We should not default the second argument to NIL. We must return an error instead.

(letrec ((fold (lambda (op acc l)
                 (if l
                     (fold op (op acc (car l)) (cdr l))
                     acc))))
  (fold (lambda (x y) (+ x y)) 0 '(1 2 3)))

thread 'main' panicked at 'double booked: found InnerBody when getting ClosedEnv', /home/user/workspace/lurk-rs/src/hash_witness.rs:190:13

This seems to be a regression, this version of fold worked before. Akosh (who's trying out our onboarding challenge) ran into this. Version I'm testing is bb98c334fed9b329cc3d1d35284ba986961948fb

Run the following:

 ~/ lurkrs
Lurk REPL welcomes you.
>  (lambda (|α|) nil)
thread 'main' panicked at 'assertion failed: !path.is_empty()', src/sym.rs:181:9
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
[1 iterations] => <FUNCTION (%
 ~/

#133 Implements relational operators outside the circuit. We need to support these in the circuit so they can be used in proofs. The tests in #133 cover the most important cases and should also be included when testing the circuit.