-
Notifications
You must be signed in to change notification settings - Fork 97
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Builtin functions. #920
Builtin functions. #920
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,16 @@ | ||
/// This is a built-in function taking an array argument and returning | ||
/// the length of the array. | ||
/// This symbol is not an empty array, the actual semantics are overridden. | ||
let len = []; | ||
|
||
/// Evaluates to the array [f(0), f(1), ..., f(length - 1)]. | ||
let new = |length, f| std::utils::fold(length, f, [], |acc, e| (acc + [e])); | ||
|
||
/// Evaluates to the array [f(arr[0]), f(arr[1]), ..., f(arr[len(arr) - 1])]. | ||
let map = |arr, f| new(len(arr), |i| f(arr[i])); | ||
|
||
/// Computes folder(...folder(folder(initial, arr[0]), arr[1]) ..., arr[len(arr) - 1]) | ||
let fold = |arr, initial, folder| std::utils::fold(len(arr), |i| arr[i], initial, folder); | ||
|
||
/// Returns the sum of the array elements. | ||
let sum = [|arr| fold(arr, 0, |a, b| a + b)][0]; |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,12 @@ | ||
/// This is a built-in function taking a string argument and terminating | ||
/// evaluation unsuccessfully with this argument as explanation. | ||
/// This symbol is not an empty array, the actual semantics are overridden. | ||
let panic = []; | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This is quite confusing There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. The main other way I could think of is something like:
And then There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. although this would not pass strict type checking There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. ok, we could use something like There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. if it's already built-in, why not make it fully built-in? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. so we keep it like this for now? |
||
|
||
/// Checks the condition and panics if it is false. | ||
/// IMPORTANT: Since this does not generate any constraints, the verifier will not | ||
/// check these assertions. This function should only be used to verify | ||
/// prover-internal consistency. | ||
/// The panic message is obtained by calling the function `reason`. | ||
/// Returns an empty array on success, which allows it to be used at statement level. | ||
let assert = |condition, reason| if !condition { panic(reason()) } else { [] }; |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,6 @@ | ||
mod array; | ||
mod binary; | ||
mod check; | ||
mod hash; | ||
mod shift; | ||
mod split; | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,11 @@ | ||
use std::check; | ||
|
||
machine Empty { | ||
let line = |i| i - 7; | ||
col witness w; | ||
w = line; | ||
|
||
|
||
check::assert(line(7) == 0, || "This should succeed."); | ||
check::assert(line(7) != 0, || "This should fail."); | ||
} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is also confusing. Why is it done like this?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If I just use
let len;
, then it will be a witness column. I have to assign something.Although thinking about it, maybe it could work?
But in any case, since we don't have any annotations or stuff like this, it has to be weird in some way.