Skip to content

Commit

Permalink
chore: rollback call and chain to accept a single argument
Browse files Browse the repository at this point in the history 
Extra: build call expressions with the new `(<hash> arg)` way of writing
to save up iterations, since we had to write `((open <hash>) arg)` before.
  • Loading branch information
@arthurpaulino
arthurpaulino committed Mar 19, 2024
1 parent 54e9292 commit 3dd3b98
Show file tree
Hide file tree
Showing 5 changed files with 62 additions and 53 deletions.
8 changes: 4 additions & 4 deletions demo/bank.lurk
View file
Original file line number Diff line number Diff line change
Expand Up @@ -202,7 +202,7 @@ ledger2

;; We can verify the proof..

!(verify "supernova_bn256_10_11882126c5f0dd9a94f76ff58ea5c499cfe2364162585c320c55f53651e16ffd")
!(verify "supernova_bn256_10_2729492c67fc7d6adbd52705c714152979b65ac304f2679eb11e8eecc0eb09c5")

;; Unfortunately, this functional commitment doesn't let us maintain state.
;; Let's turn our single-transaction function into a chained function.
Expand All @@ -223,20 +223,20 @@ ledger2

!(prove)

!(verify "supernova_bn256_10_0b72908859e73ee3014067a5eaa557a995aea262cfb5f3621922024a176b8281")
!(verify "supernova_bn256_10_176d2e388b909d361746d7b9c5cb0a7c7d8f020e027729d53a8db12d025ed687")

;; Then we can transfer 5 more, proceeding from the new head of the chain.

!(chain 0x18b99c6b580d518129921ebf70023b5d757861b935f7f537460c99130eb4447d '(5 0 2))

!(prove)

!(verify "supernova_bn256_10_0d8159faab0d85855d4cf53c7e36a2357a1766a1540afbafb0ef93d7e1537ca8")
!(verify "supernova_bn256_10_1bca041de218e346bd36ae7a67233919bf748d8bb19fd949e84bfc3399cde03d")

;; And once more, this time we'll transfer 20 from Turing to Church.

!(chain 0x0b2d868fad0e6ec88e9ba6818ae9a0345aab06abc2c226200ff3ed45c60a41db '(20 1 0))

!(prove)

!(verify "supernova_bn256_10_0a253296edb4d6c204edd92e63176efed7c30e9f5928b52ba9be2b3f2e6e8b08")
!(verify "supernova_bn256_10_0c0b590f5a75d3232b270944e681dac76cce7802725d77f9ca06f93cd672a075")
6 changes: 3 additions & 3 deletions demo/chained-functional-commitment.lurk
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@

;; We can verify the proof.

!(verify "supernova_bn256_10_0f54f9e56fa6c436618597c971daa7b525ad80ac48be11226284fd4f8167e60a")
!(verify "supernova_bn256_10_258ef770ae37ce944a5c3e32c104f6715150276963dc3476af55407f0ed83a88")

;; Now let's chain another call to the new head, adding 12 to the counter.

Expand All @@ -35,7 +35,7 @@

;; And verify.

!(verify "supernova_bn256_10_281771b7af2f96cac51cb7579d94f0a6f56e9a9d951b753f8514b2b4ec6ce4db")
!(verify "supernova_bn256_10_180a27de7a650743500a90dd43517143f3cf65e813c8aa45cda7d03b1a572873")

;; One more time, we'll add 14 to the head commitment's internal state.

Expand All @@ -49,7 +49,7 @@

;; Verify.

!(verify "supernova_bn256_10_22ab68c1fa6e75f54d213a3ada71edd21331bf58826263a79e3fdd32f1c4c62d")
!(verify "supernova_bn256_10_01018a9231e97b1743ef5882beff1d0b4e2dec196de16e11b5af1a63efd3b171")

;; Repeat indefinitely.

Expand Down
6 changes: 3 additions & 3 deletions demo/functional-commitment.lurk
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,12 +18,12 @@

;; We can inspect the input/output expressions of the proof.

!(inspect "supernova_bn256_10_15c837e5040ac70c00030c228b61fde2c164d930ba6ea396353b3cfcaa16609d")
!(inspect "supernova_bn256_10_138686f709e302fd7334c96e4107e0026cc9a84137813a597f47c00d4803cabf")

;; Or the full proof claim

!(inspect-full "supernova_bn256_10_15c837e5040ac70c00030c228b61fde2c164d930ba6ea396353b3cfcaa16609d")
!(inspect-full "supernova_bn256_10_138686f709e302fd7334c96e4107e0026cc9a84137813a597f47c00d4803cabf")

;; Finally, and most importantly, we can verify the proof.

!(verify "supernova_bn256_10_15c837e5040ac70c00030c228b61fde2c164d930ba6ea396353b3cfcaa16609d")
!(verify "supernova_bn256_10_138686f709e302fd7334c96e4107e0026cc9a84137813a597f47c00d4803cabf")
72 changes: 35 additions & 37 deletions src/cli/repl/meta_cmd.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -77,18 +77,18 @@ where
format: "!(def <binding> <body>)",
description: &[
"Gets macroexpanded to this: (let ((foo (lambda () 123))) (current-env))",
"The state's env is set to the result.",
"The REPL's env is set to the result.",
],
example: &["!(def foo (lambda () 123))"],
run: |repl, args, _path| {
let (first, second) = repl.peek2(args)?;
let new_name = first.fmt_to_string(&repl.store, &repl.state.borrow());
let l = repl.store.intern_lurk_symbol("let");
let current_env = repl.store.intern_lurk_symbol("current-env");
let binding = repl.store.list(vec![first, second]);
let bindings = repl.store.list(vec![binding]);
let current_env_call = repl.store.list(vec![current_env]);
let expanded = repl.store.list(vec![l, bindings, current_env_call]);
let binding = repl.store.list([first, second]);
let bindings = repl.store.list([binding]);
let current_env_call = repl.store.list([current_env]);
let expanded = repl.store.list([l, bindings, current_env_call]);
let expanded_io = repl.eval_expr(expanded)?;
repl.env = expanded_io[0];
println!("{new_name}");
Expand All @@ -102,7 +102,7 @@ where
format: "!(defrec <binding> <body>)",
description: &[
"Gets macroexpanded to this: (letrec ((foo (lambda () 123))) (current-env))",
"The state's env is set to the result.",
"The REPL's env is set to the result.",
],
example: &[
"!(defrec sum (lambda (l) (if (eq l nil) 0 (+ (car l) (sum (cdr l))))))",
Expand All @@ -113,10 +113,10 @@ where
let new_name = first.fmt_to_string(&repl.store, &repl.state.borrow());
let l = repl.store.intern_lurk_symbol("letrec");
let current_env = repl.store.intern_lurk_symbol("current-env");
let binding = repl.store.list(vec![first, second]);
let bindings = repl.store.list(vec![binding]);
let current_env_call = repl.store.list(vec![current_env]);
let expanded = repl.store.list(vec![l, bindings, current_env_call]);
let binding = repl.store.list([first, second]);
let bindings = repl.store.list([binding]);
let current_env_call = repl.store.list([current_env]);
let expanded = repl.store.list([l, bindings, current_env_call]);
let expanded_io = repl.eval_expr(expanded)?;
repl.env = expanded_io[0];
println!("{new_name}");
Expand Down Expand Up @@ -296,7 +296,7 @@ where
],
run: |repl, args, _path| {
let hash_expr = repl.peek1(args)?;
let hash = *repl.get_comm_hash(hash_expr)?;
let (hash, _) = repl.get_comm_hash(hash_expr)?;
repl.fetch(&hash, false)
},
};
Expand All @@ -312,7 +312,7 @@ where
],
run: |repl, args, _path| {
let hash_expr = repl.peek1(args)?;
let hash = *repl.get_comm_hash(hash_expr)?;
let (hash, _) = repl.get_comm_hash(hash_expr)?;
repl.fetch(&hash, true)
},
};
Expand Down Expand Up @@ -531,29 +531,24 @@ where

fn call(repl: &mut Repl<F, C>, args: &Ptr, _path: &Utf8Path) -> Result<()> {
let (hash_expr, args) = repl.store.car_cdr_simple(args)?;
let hash = *repl.get_comm_hash(hash_expr)?;
let arg = repl.peek1(&args)?;
let (hash, call_head) = repl.get_comm_hash(hash_expr)?;
// check if the data is already available on the store before trying to
// fetch it from the file system
if repl.store.open(hash).is_none() {
repl.fetch(&hash, false)?;
}
let open = repl.store.intern_lurk_symbol("open");
let open_expr = repl.store.list(vec![open, repl.store.num(hash)]);
let (args_vec, _) = repl
.store
.fetch_list(&args)
.expect("list of arguments must have been interned");
let mut expr_vec = Vec::with_capacity(args_vec.len() + 1);
expr_vec.push(open_expr);
expr_vec.extend(args_vec);
repl.handle_non_meta(repl.store.list(expr_vec))
repl.handle_non_meta(repl.store.list([call_head, arg]))
}

const CALL: MetaCmd<F, C> = MetaCmd {
name: "call",
summary: "Open a functional commitment then apply arguments to it",
format: "!(call <hash> <args>)",
description: &[],
summary: "Open a functional commitment then apply an argument to it",
format: "!(call <hash> <arg>)",
description: &[
"Open a functional commitment then apply an argument to it.",
"If the commitment is not in memory, it will look for a persisted commitment.",
],
example: &[
"(commit (lambda (x) x))",
"!(call 0x2f31ee658b82c09daebbd2bd976c9d6669ad3bd6065056763797d5aaf4a3001b 0)",
Expand All @@ -563,12 +558,14 @@ where

const CHAIN: MetaCmd<F, C> = MetaCmd {
name: "chain",
summary: "Chain a functional commitment by applying the provided arguments to it",
format: "!(chain <hash> <args>)",
summary: "Chain a functional commitment by applying an argument to it",
format: "!(chain <hash> <arg>)",
description: &[
"Chain a functional commitment by applying the provided arguments to it.",
"Chain a functional commitment by applying an argument to it.",
"If the commitment is not in memory, it will look for a persisted commitment.",
"The chained function must return a pair whose first component is the actual result",
" and the second is a commitment to the next function",
"Important: the commitment to the next function is persisted",
],
example: &[
"!(commit (letrec ((add (lambda (counter x)
Expand All @@ -589,16 +586,17 @@ where
let (_, comm) = repl
.store
.fetch_cons(result)
.ok_or_else(|| anyhow!("Chained function must return a cons expression"))?;
let (Tag::Expr(ExprTag::Comm), RawPtr::Atom(hash)) = comm.parts() else {
.ok_or(anyhow!("Chained function must return a cons expression"))?;
let (Tag::Expr(ExprTag::Comm), RawPtr::Atom(hash)) = comm.into_parts() else {
bail!("Second component of a chain must be a commitment")
};
let hash = *repl.store.expect_f(*hash);
// retrieve from store to persist
let hash = *repl.store.expect_f(hash);
// retrieve from store
let (secret, fun) = repl
.store
.open(hash)
.expect("data must have been committed");
.ok_or(anyhow!("Could not open the next functional commitment"))?;
// and then persist
repl.hide(*secret, *fun)
},
};
Expand Down Expand Up @@ -738,7 +736,7 @@ where
)
}

let lambda = repl.store.list(vec![repl.store.intern_lurk_symbol("lambda"), vars, body]);
let lambda = repl.store.list([repl.store.intern_lurk_symbol("lambda"), vars, body]);
let io = repl.eval_expr_with_env(lambda, repl.store.intern_empty_env())?;
let fun = io[0];
if !fun.is_fun() {
Expand Down Expand Up @@ -792,7 +790,7 @@ where
)?;

// the standard format for a processed protocol as Lurk data
let protocol = repl.store.list(vec![fun, backend, rc, lang, description]);
let protocol = repl.store.list([fun, backend, rc, lang, description]);
repl.env = repl.store.push_binding(name, protocol, repl.env);
Ok(())
},
Expand Down Expand Up @@ -898,7 +896,7 @@ where
/// * If the predicate rejects the proof (evaluation returns nil)
fn post_verify_check(repl: &Repl<F, C>, post_verify: Ptr) -> Result<()> {
if !post_verify.is_nil() {
let call = repl.store.list(vec![post_verify]);
let call = repl.store.list([post_verify]);
let io = repl
.eval_expr_with_env(call, repl.store.intern_empty_env())
.with_context(|| "evaluating post-verify call")?;
Expand Down
23 changes: 17 additions & 6 deletions src/cli/repl/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -135,16 +135,25 @@ impl<F: LurkField, C: Coprocessor<F> + Serialize + DeserializeOwned> Repl<F, C>
}

fn peek1(&self, args: &Ptr) -> Result<Ptr> {
let (first, rest) = self.store.car_cdr_simple(args)?;
let (first, rest) = self
.store
.fetch_cons(args)
.ok_or(anyhow!("Missing argument"))?;
if !rest.is_nil() {
bail!("At most one argument is accepted")
}
Ok(first)
}

fn peek2(&self, args: &Ptr) -> Result<(Ptr, Ptr)> {
let (first, rest) = self.store.car_cdr_simple(args)?;
let (second, rest) = self.store.car_cdr_simple(&rest)?;
let (first, rest) = self
.store
.fetch_cons(args)
.ok_or(anyhow!("Missing first argument"))?;
let (second, rest) = self
.store
.fetch_cons(&rest)
.ok_or(anyhow!("Missing second argument"))?;
if !rest.is_nil() {
bail!("At most two arguments are accepted")
}
Expand Down Expand Up @@ -219,6 +228,7 @@ where
}
}

#[inline]
fn lang_setup(&self) -> (&Func, &[Func], &Lang<F, C>) {
(&self.lurk_step, &self.cprocs, &self.lang)
}
Expand Down Expand Up @@ -556,17 +566,18 @@ where
Ok((output, iterations))
}

/// Evaluates `hash_expr` and returns the resulting commitment hash
/// Evaluates `hash_expr` then returns the resulting commitment hash and the
/// resulting pointer
///
/// # Errors
/// Errors when `hash_expr` doesn't reduce to a Num or Comm pointer
fn get_comm_hash(&mut self, hash_expr: Ptr) -> Result<&F> {
fn get_comm_hash(&mut self, hash_expr: Ptr) -> Result<(F, Ptr)> {
let io = self.eval_expr(hash_expr)?;
let (Tag::Expr(ExprTag::Num | ExprTag::Comm), RawPtr::Atom(hash_idx)) = io[0].parts()
else {
bail!("Commitment hash expression must reduce to a Num or Comm pointer")
};
Ok(self.store.expect_f(*hash_idx))
Ok((*self.store.expect_f(*hash_idx), io[0]))
}

pub(crate) fn handle_non_meta(&mut self, expr_ptr: Ptr) -> Result<()> {
Expand Down

0 comments on commit 3dd3b98

Please sign in to comment.