Skip to content
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

Environment optimization #1035

Merged
merged 14 commits into from
Jan 12, 2024
12 changes: 8 additions & 4 deletions benches/common/fib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -56,14 +56,18 @@ fn lurk_fib<F: LurkField>(store: &Store<F>, n: usize) -> Ptr {
// saved_env: (((.lurk.user.next . <FUNCTION (.lurk.user.a .lurk.user.b) (.lurk.user.next .lurk.user.b (+ .lurk.user.a .lurk.user.b))>))),
// body: (.lurk.user.fib), continuation: Outermost }

let (_, rest_bindings) = store.car_cdr(target_env).unwrap();
let (second_binding, _) = store.car_cdr(&rest_bindings).unwrap();
store.car_cdr(&second_binding).unwrap().1
let [_, _, rest_bindings] = store.pop_binding(*target_env).unwrap();
let [_, val, _] = store.pop_binding(rest_bindings).unwrap();
val
}

// Returns the linear and angular coefficients for the iteration count of fib
fn compute_coeffs<F: LurkField>(store: &Store<F>) -> (usize, usize) {
let mut input = vec![fib_expr(store), store.intern_nil(), store.cont_outermost()];
let mut input = vec![
fib_expr(store),
store.intern_empty_env(),
store.cont_outermost(),
];
let lang: Lang<F, Coproc<F>> = Lang::new();
let mut coef_lin = 0;
let coef_ang;
Expand Down
16 changes: 8 additions & 8 deletions demo/bank.lurk
Original file line number Diff line number Diff line change
Expand Up @@ -192,7 +192,7 @@ ledger2

;; Now we can open the committed ledger transfer function on a transaction.

!(call 0x3be53fdb5946af9449e4f7063fd8d60a6acc7ccdea8da8b575facedcb2b1291d '(1 0 2))
!(call 0x348a2e97903fff808be52461d19c3192b6868830598be397b361a21bfc8a45f9 '(1 0 2))

;; And the record reflects that Church sent one unit to Satoshi.

Expand All @@ -202,7 +202,7 @@ ledger2

;; We can verify the proof..

!(verify "Nova_Pallas_10_0bac4e49ef06a34fd1a6a18d6d7bff8770e6acbf6a4624783af29ad8cd780b14")
!(verify "Nova_Pallas_10_398a87b5f99157b86abde88a67754791f72fed93ccd8db68d693bc9f7e26738c")

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

;; Now we can transfer one unit from Church to Satoshi like before.

!(chain 0x01ad5587273aed89dca2527f7a9a235e1ee74ba2519d39adc7b4c521c66f9dbb '(1 0 2))
!(chain 0x0e484bf02f72ad529ebb9ded8fc2f4c2b1519a758e0f0238973bf0cd8dd97f72 '(1 0 2))

!(prove)

!(verify "Nova_Pallas_10_2def0d8894789eda3fdbafe6216b9d38c1d73c39964780fff407596dca93535a")
!(verify "Nova_Pallas_10_11df37aff14b2fc8c1fea85fcc07ebececa4ef3e974764c73c49a2ce64eeb8f1")

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

!(chain 0x07172fda01948387c25038beb5738a12bf88cfb3317180cf5894319c16276c78 '(5 0 2))
!(chain 0x3cb56c66573d29a478b62ff6d59df557dd2e6a924ff408644e61e31c3847a9cd '(5 0 2))

!(prove)

!(verify "Nova_Pallas_10_2def0d8894789eda3fdbafe6216b9d38c1d73c39964780fff407596dca93535a")
!(verify "Nova_Pallas_10_3541178de43221c6d12f82ff6da37807971079d11ced58e3564ba2f34e77cfc4")

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

!(chain 0x261e0afd81be78f88bc638c79d6530f341517ff5fdb368e575407bd701c712cc '(20 1 0))
!(chain 0x38172b9b6212b557d94b9896ea569e77fa35ac979700bedcc97f711322169905 '(20 1 0))

!(prove)

!(verify "Nova_Pallas_10_2d3c73be45dce3971cf9208a6ec538238fc4a01328342d2b3aa501e5709ea2c5")
!(verify "Nova_Pallas_10_2dd41df4b593c4f8b4a0a058d94b8dbcded8343f829d1aaf2765f0b8e0eda03b")
12 changes: 6 additions & 6 deletions demo/chained-functional-commitment.lurk
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@

;; We chain a next commitment by applying the committed function to a value of 9.

!(chain 0x07978f48203798156497b7fdef995301644c10b16de71c98a9c3c5d5c80e5cb9 9)
!(chain 0x3e47de9fb674019306d566345ab360d92f955e29e015432b10ecb58476f42f01 9)

;; The new counter value is 9, and the function returns a new functional commitment.

Expand All @@ -21,11 +21,11 @@

;; We can verify the proof.

!(verify "Nova_Pallas_10_29077a93c626166dfe527acb4665eeaa0a2945965db1d984d111fdb04d7f6cb4")
!(verify "Nova_Pallas_10_1b894ae4e13a74970afb9ff982fd0e9c4dc439a8317ac85eeaf97ab6c3d8f35e")

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

!(chain 0x09d46102bcc9faaf2d8dbfabe72b5142a1788538129e4826e0e30015f594e035 12)
!(chain 0x17165f98bc83b64b47c4e030ae621c94edcb10cc3bd68e9dcc5c796283bda34c 12)

;; Now the counter is 21, and we have a new head commitment.

Expand All @@ -35,11 +35,11 @@

;; And verify.

!(verify "Nova_Pallas_10_18beccbc88887d27b074b782525d2c3d5cfafb7f553877513b167b8bb45017e4")
!(verify "Nova_Pallas_10_29a1a6b7ceca05a40f92883dc7d3c11dd8e7cca698665bc7a9faaaa96cdde96a")

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

!(chain 0x3b0ed1000667da8ce73779a52e4dfe17638f359fcb77f0aad1a6322c1fcef599 14)
!(chain 0x2c4c9d86f79bb575a1427ead9c14cb5226b79a6339dd1f8f8dc00354da677bfa 14)

;; 21 + 14 = 35, as expected.

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

;; Verify.

!(verify "Nova_Pallas_10_034258d4a0c61bc5fff43cc2e912a88f341abca00c4149c0ed85ab02b33d45dc")
!(verify "Nova_Pallas_10_13f092af20ac415822a0528d41e5c1f5565bfa6d0ec376445e677f411eb3ddd4")

;; Repeat indefinitely.

Expand Down
8 changes: 4 additions & 4 deletions demo/functional-commitment.lurk
Original file line number Diff line number Diff line change
Expand Up @@ -10,20 +10,20 @@

;; We open the functional commitment on input 5: Evaluate f(5).

!(call 0x3636a3820b53c834ce46a2d608c3b732681ccbc343b5154862f11f989d1a41e5 5)
!(call 0x05adecdb07d3d8d4a9d8027c163a70ef66c18ec311abc8381c2df92c58e216b5 5)

;; We can prove the functional-commitment opening.

!(prove)

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

!(inspect "Nova_Pallas_10_2f90a649f3a2a7861fdf6499309edc0c8e72b61ff3f40f2a11bd027749df4b04")
!(inspect "Nova_Pallas_10_1c3654a2491282df9c31cba2d104649a496b3d1bac4bb5352004a21c94554027")

;; Or the full proof claim

!(inspect-full "Nova_Pallas_10_2f90a649f3a2a7861fdf6499309edc0c8e72b61ff3f40f2a11bd027749df4b04")
!(inspect-full "Nova_Pallas_10_1c3654a2491282df9c31cba2d104649a496b3d1bac4bb5352004a21c94554027")

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

!(verify "Nova_Pallas_10_2f90a649f3a2a7861fdf6499309edc0c8e72b61ff3f40f2a11bd027749df4b04")
!(verify "Nova_Pallas_10_1c3654a2491282df9c31cba2d104649a496b3d1bac4bb5352004a21c94554027")
2 changes: 1 addition & 1 deletion demo/protocol.lurk
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
(mk-open-expr (lambda (hash) (cons 'open (cons hash nil)))))
(cons
(if (= (+ (car pair) (cdr pair)) 30)
(list6 (mk-open-expr hash) nil :outermost pair nil :terminal)
(list6 (mk-open-expr hash) (empty-env) :outermost pair (empty-env) :terminal)
nil)
(lambda () (> (car pair) 10))))
:rc 10
Expand Down
2 changes: 1 addition & 1 deletion demo/vdf.lurk
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@

!(prove)

!(verify "Nova_Pallas_10_04ebf402c8345327dbb271b393325f4d360372784e4d1e625e707235a8736dad")
!(verify "Nova_Pallas_10_3d385361e08449cad361ccbe45d4c41685bcee7ece87b33c47b8953309002f64")

!(def timelock-encrypt (lambda (secret-key plaintext rounds)
(let ((ciphertext (+ secret-key plaintext))
Expand Down
20 changes: 11 additions & 9 deletions src/cli/repl/meta_cmd.rs
Original file line number Diff line number Diff line change
Expand Up @@ -313,7 +313,7 @@ where
description: &[],
example: &["!(def a 1)", "(current-env)", "!(clear)", "(current-env)"],
run: |repl, _args, _path| {
repl.env = repl.store.intern_nil();
repl.env = repl.store.intern_empty_env();
Ok(())
},
};
Expand All @@ -327,7 +327,11 @@ where
run: |repl, args, _path| {
let first = repl.peek1(args)?;
let (first_io, ..) = repl.eval_expr(first)?;
repl.env = first_io[0];
let env = first_io[0];
if *env.tag() != Tag::Expr(ExprTag::Env) {
return Err(anyhow!("Value must be an environment"));
}
repl.env = env;
Ok(())
},
};
Expand Down Expand Up @@ -660,8 +664,7 @@ where
let path = get_path(repl, &path)?;
let LurkData::<F> { z_ptr, z_dag } = load(&path)?;
let ptr = z_dag.populate_store(&z_ptr, &repl.store, &mut Default::default())?;
let binding = repl.store.cons(sym, ptr);
repl.env = repl.store.cons(binding, repl.env);
repl.env = repl.store.push_binding(sym, ptr, repl.env);
Ok(())
},
};
Expand Down Expand Up @@ -716,7 +719,7 @@ where
}

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

// the standard format for a processed protocol as Lurk data
let protocol = repl.store.list(vec![fun, rc, lang, description]);
let binding = repl.store.cons(name, protocol);
repl.env = repl.store.cons(binding, repl.env);
repl.env = repl.store.push_binding(name, protocol, repl.env);
Ok(())
},
};
Expand Down Expand Up @@ -824,7 +826,7 @@ where
.list(vec![*repl.get_apply_fn(), fun, quoted_args]);

let (io, ..) = repl
.eval_expr_with_env(apply_call, repl.store.intern_nil())
.eval_expr_with_env(apply_call, repl.store.intern_empty_env())
.with_context(|| "evaluating protocol function call")?;

let (Tag::Expr(ExprTag::Cons), RawPtr::Hash4(idx)) = &io[0].parts() else {
Expand Down Expand Up @@ -858,7 +860,7 @@ where
if !post_verify.is_nil() {
let call = repl.store.list(vec![post_verify]);
let (io, ..) = repl
.eval_expr_with_env(call, repl.store.intern_nil())
.eval_expr_with_env(call, repl.store.intern_empty_env())
.with_context(|| "evaluating post-verify call")?;
if io[0].is_nil() {
bail!("Post-verification predicate rejected the input")
Expand Down
4 changes: 2 additions & 2 deletions src/cli/repl/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -185,7 +185,7 @@ where
let current_dir = std::env::current_dir().expect("couldn't capture current directory");
let pwd_path =
Utf8PathBuf::from_path_buf(current_dir).expect("path contains invalid Unicode");
let env = store.intern_nil();
let env = store.intern_empty_env();
let lurk_step = make_eval_step_from_config(&EvalConfig::new_ivc(&lang));
let cprocs = make_cprocs_funcs_from_lang(&lang);
Repl {
Expand Down Expand Up @@ -224,7 +224,7 @@ where
)
.unwrap();
let (io, ..) = self
.eval_expr_with_env(ptr, self.store.intern_nil())
.eval_expr_with_env(ptr, self.store.intern_empty_env())
.unwrap();
io[0]
})
Expand Down
73 changes: 59 additions & 14 deletions src/cli/zstore.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,9 @@ use crate::{
lem::{
pointers::{Ptr, RawPtr, ZPtr},
store::{expect_ptrs, intern_ptrs_hydrated, Store},
tag::Tag,
},
tag::ExprTag::{Env, Sym},
};

use super::field_data::HasFieldModulus;
Expand All @@ -21,6 +23,7 @@ pub(crate) enum ZPtrType<F: LurkField> {
Tuple2(ZPtr<F>, ZPtr<F>),
Tuple3(ZPtr<F>, ZPtr<F>, ZPtr<F>),
Tuple4(ZPtr<F>, ZPtr<F>, ZPtr<F>, ZPtr<F>),
Env(ZPtr<F>, ZPtr<F>, ZPtr<F>),
}

/// Holds a mapping from `ZPtr`s to their `ZPtrType`s
Expand All @@ -47,20 +50,44 @@ impl<F: LurkField> ZDag<F> {
z_ptr
}
RawPtr::Hash4(idx) => {
let [a, b] = expect_ptrs!(store, 2, *idx);
let a = self.populate_with(&a, store, cache);
let b = self.populate_with(&b, store, cache);
let z_ptr = ZPtr::from_parts(
*tag,
store.poseidon_cache.hash4(&[
a.tag_field(),
*a.value(),
b.tag_field(),
*b.value(),
]),
);
self.0.insert(z_ptr, ZPtrType::Tuple2(a, b));
z_ptr
if let Tag::Expr(Env) = tag {
let [sym_pay, val_tag, val_pay, env_pay] = store.expect_raw_ptrs(*idx);
let sym = Ptr::new(Tag::Expr(Sym), *sym_pay);
let val = Ptr::new(
store.fetch_tag(val_tag).expect("Couldn't fetch tag"),
*val_pay,
);
let env = Ptr::new(Tag::Expr(Env), *env_pay);
let sym = self.populate_with(&sym, store, cache);
let val = self.populate_with(&val, store, cache);
let env = self.populate_with(&env, store, cache);
let z_ptr = ZPtr::from_parts(
*tag,
store.poseidon_cache.hash4(&[
*sym.value(),
val.tag_field(),
*val.value(),
*env.value(),
]),
);
self.0.insert(z_ptr, ZPtrType::Env(sym, val, env));
z_ptr
} else {
let [a, b] = expect_ptrs!(store, 2, *idx);
let a = self.populate_with(&a, store, cache);
let b = self.populate_with(&b, store, cache);
let z_ptr = ZPtr::from_parts(
*tag,
store.poseidon_cache.hash4(&[
a.tag_field(),
*a.value(),
b.tag_field(),
*b.value(),
]),
);
self.0.insert(z_ptr, ZPtrType::Tuple2(a, b));
z_ptr
}
}
RawPtr::Hash6(idx) => {
let [a, b, c] = expect_ptrs!(store, 3, *idx);
Expand Down Expand Up @@ -146,6 +173,18 @@ impl<F: LurkField> ZDag<F> {
let ptr4 = self.populate_store(z4, store, cache)?;
intern_ptrs_hydrated!(store, *z_ptr.tag(), *z_ptr, ptr1, ptr2, ptr3, ptr4)
}
Some(ZPtrType::Env(sym, val, env)) => {
let sym = self.populate_store(sym, store, cache)?;
let val = self.populate_store(val, store, cache)?;
let env = self.populate_store(env, store, cache)?;
let raw = store.intern_raw_ptrs([
*sym.raw(),
store.tag(*val.tag()),
*val.raw(),
*env.raw(),
]);
Ptr::new(Tag::Expr(Env), raw)
}
};
cache.insert(*z_ptr, ptr);
Ok(ptr)
Expand Down Expand Up @@ -187,6 +226,12 @@ impl<F: LurkField> ZDag<F> {
self.populate_z_dag(z4, z_dag, cache)?;
z_dag.0.insert(*z_ptr, ZPtrType::Tuple4(*z1, *z2, *z3, *z4));
}
Some(ZPtrType::Env(sym, val, env)) => {
self.populate_z_dag(sym, z_dag, cache)?;
self.populate_z_dag(val, z_dag, cache)?;
self.populate_z_dag(env, z_dag, cache)?;
z_dag.0.insert(*z_ptr, ZPtrType::Env(*sym, *val, *env));
}
};
cache.insert(*z_ptr);
}
Expand Down
Loading
Loading