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

Human-readable encoding 2: cleanups and syntax changes #158

Merged
merged 10 commits into from
Jul 18, 2023
6 changes: 3 additions & 3 deletions jets-bench/benches/elements/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -471,7 +471,7 @@ fn bench(c: &mut Criterion) {
let (src_ty, tgt_ty) = jet_arrow(jet);
let env = env_sampler.env();

let mut group = c.benchmark_group(&format!("{}", jet.to_string()));
let mut group = c.benchmark_group(&jet.to_string());
for i in 0..NUM_RANDOM_SAMPLES {
let params = JetParams::with_rand_aligns(InputSampling::Random);
let name = format!("{}", i);
Expand Down Expand Up @@ -531,7 +531,7 @@ fn bench(c: &mut Criterion) {
let (src_ty, tgt_ty) = jet_arrow(jet);
let env = EnvSampling::Null.env();

let mut group = c.benchmark_group(&format!("{}", jet.to_string()));
let mut group = c.benchmark_group(&jet.to_string());
for i in 0..NUM_RANDOM_SAMPLES {
let params = JetParams::with_rand_aligns(InputSampling::Custom(inp_fn.clone()));
let name = format!("{}", i);
Expand Down Expand Up @@ -612,7 +612,7 @@ fn bench(c: &mut Criterion) {
for (jet, index, env_type) in arr {
let (src_ty, tgt_ty) = jet_arrow(jet);
let env = env_type.env();
let mut group = c.benchmark_group(&format!("{}", jet.to_string()));
let mut group = c.benchmark_group(&jet.to_string());

for i in 0..NUM_RANDOM_SAMPLES {
// We always select the current input because this is where we
Expand Down
5 changes: 4 additions & 1 deletion src/analysis.rs
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,10 @@

use crate::jet::Jet;
use crate::Value;
use std::{cmp, fmt, io};
use std::{cmp, fmt};

#[cfg(feature = "elements")]
use std::io;

#[cfg(feature = "elements")]
use elements::encode::Encodable;
Expand Down
2 changes: 1 addition & 1 deletion src/bit_encoding/decode.rs
Original file line number Diff line number Diff line change
Expand Up @@ -410,7 +410,7 @@ mod tests {
#[test]
fn root_unit_to_unit() {
// main = jet_eq_32 :: 2^64 -> 2 # 7387d279
let justjet = vec![0x6d, 0xb8, 0x80];
let justjet = [0x6d, 0xb8, 0x80];
// Should be able to decode this as an expression...
let mut iter = BitIter::from(&justjet[..]);
decode_expression::<_, Core>(&mut iter).unwrap();
Expand Down
6 changes: 3 additions & 3 deletions src/bit_machine/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -528,23 +528,23 @@ mod tests {
prog.cmr().to_string(),
cmr_str,
"CMR mismatch (got {} expected {}) for program {}",
prog.cmr().to_string(),
prog.cmr(),
cmr_str,
prog_hex,
);
assert_eq!(
prog.imr().to_string(),
imr_str,
"IMR mismatch (got {} expected {}) for program {}",
prog.imr().to_string(),
prog.imr(),
imr_str,
prog_hex,
);
assert_eq!(
prog.amr().to_string(),
amr_str,
"AMR mismatch (got {} expected {}) for program {}",
prog.amr().to_string(),
prog.amr(),
amr_str,
prog_hex,
);
Expand Down
14 changes: 11 additions & 3 deletions src/human_encoding/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -52,8 +52,8 @@ and EXPRESSION is
* `unit`, `iden`, or `witness`;
* `injl`, `injr`, `take`, or `drop` followed by another EXPRESSION;
* `case`, `comp`, or `pair` followed by two EXPRESSIONs;
* `assertl` followed by an EXPRESSION, a literal `#`, and another EXPRESSION;
* `assertr` followed by a literal `#` and two EXPRESSIONs;
* `assertl` followed by an EXPRESSION and a CMR (defined below);
* `assertr` followed by CMR and an EXPRESSION;
* a jet, which begins with `jet_` and must belong to the list of jets (FIXME define this list);
* `const` followed by a VALUE (defined below);
* `fail` followed by an ENTROPY (defined below); or
Expand All @@ -63,6 +63,14 @@ Note that while we allow parenthesis to help group parts of expressions for huma
understanding, they are never needed for disambiguation and are essentially
ignored by the parser.

A CMR is

* `#{` followed by an expression followed by `}`; or
* `#` followed by 64 hex bytes.

The first case indicates that an expression should be replaced by its commitment
Merkle root; the second case just directly encodes the Merkle root.

A HOLE is the literal `?` followed by a NAME. It indicates an expression that has
yet to be defined. Holes have a different namespace than other names.

Expand Down Expand Up @@ -151,7 +159,7 @@ Expressions may be
* one of the core combinators `unit`, `iden`, `comp`, `injl`, `injr`, `case`, `take`, `drop`, `pair`, followed by subexpression(s) as needed;
* the `disconnect` combinator followed by an expression and a hole;
* the `witness` combinator which currently allows no subexpressions;
* the assertions, `assertl` or `assertr`, which take two subexpressions, one of which will be hidden in the decoded program. The hidden subexpression should be prefixed by `#` which indicates to the parser to take the CMR of that expression, not the expression itself.
* the assertions, `assertl` or `assertr`, which take a subexpressions and a CMR. The CMR is encoded as a full expression prefixed by `#{` and suffixed by `}`; but in the bit-encoding the expression does not appear, only its CMR;
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

64c6ea4: Typo, and the definition of CMR was extended. I would leave out the latter part because it is already explained in an earlier section.

Suggested change
* the assertions, `assertl` or `assertr`, which take a subexpressions and a CMR. The CMR is encoded as a full expression prefixed by `#{` and suffixed by `}`; but in the bit-encoding the expression does not appear, only its CMR;
the assertions, `assertl` or `assertr`, which take a subexpression and a CMR;

* `fail` followed by a 128-to-512-bit entropy value, which should occur only in the pruned branch of an assertion, though this is not enforced;
* `const` followed by a value, which is a "constant-word jet" and is equivalent to constructing the given value by a tree of `pair`s whose leaves are `injl unit` (0) or `injr unit` (1);

Expand Down
4 changes: 4 additions & 0 deletions src/human_encoding/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -80,6 +80,7 @@ impl<J: Jet> Forest<J> {
let node = data.node;
let name = node.name();
let mut expr_str = match node.inner() {
node::Inner::AssertR(cmr, _) => format!("{} := assertr #{}", name, cmr),
node::Inner::Fail(entropy) => format!("{} := fail {}", name, entropy),
node::Inner::Jet(ref j) => format!("{} := jet_{}", name, j),
node::Inner::Word(ref v) => {
Expand All @@ -94,6 +95,9 @@ impl<J: Jet> Forest<J> {
if let Some(child) = node.right_child() {
expr_str.push(' ');
expr_str.push_str(child.name());
} else if let node::Inner::AssertL(_, cmr) = node.inner() {
expr_str.push_str(" #");
expr_str.push_str(&cmr.to_string());
}

let arrow = node.arrow();
Expand Down
2 changes: 1 addition & 1 deletion src/node/commit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -314,7 +314,7 @@ mod tests {
prog.cmr().to_string(),
cmr_str,
"CMR mismatch (got {} expected {}) for program {}",
prog.cmr().to_string(),
prog.cmr(),
cmr_str,
prog_hex,
);
Expand Down
40 changes: 37 additions & 3 deletions src/node/inner.rs
Original file line number Diff line number Diff line change
Expand Up @@ -303,7 +303,7 @@ impl<C, J, X: Disconnectable<C>, W> Inner<C, J, X, W> {
}
}

impl<C, J, X, W> Inner<Option<C>, J, Option<X>, W> {
impl<C, J, X, W> Inner<Option<C>, J, X, W> {
/// Convert an `Inner<Option<C>, J, W>` to an `Option<Inner<C, J, W>>`.
pub fn transpose(self) -> Option<Inner<C, J, X, W>> {
Some(match self {
Expand All @@ -318,7 +318,31 @@ impl<C, J, X, W> Inner<Option<C>, J, Option<X>, W> {
Inner::AssertL(c, cmr) => Inner::AssertL(c?, cmr),
Inner::AssertR(cmr, c) => Inner::AssertR(cmr, c?),
Inner::Pair(cl, cr) => Inner::Pair(cl?, cr?),
Inner::Disconnect(cl, cr) => Inner::Disconnect(cl?, cr?),
Inner::Disconnect(cl, cr) => Inner::Disconnect(cl?, cr),
Inner::Witness(w) => Inner::Witness(w),
Inner::Fail(entropy) => Inner::Fail(entropy),
Inner::Jet(j) => Inner::Jet(j),
Inner::Word(w) => Inner::Word(w),
})
}
}

impl<C, J, X, W> Inner<C, J, Option<X>, W> {
/// Convert an `Inner<Option<C>, J, W>` to an `Option<Inner<C, J, W>>`.
pub fn transpose_disconnect(self) -> Option<Inner<C, J, X, W>> {
Some(match self {
Inner::Iden => Inner::Iden,
Inner::Unit => Inner::Unit,
Inner::InjL(c) => Inner::InjL(c),
Inner::InjR(c) => Inner::InjR(c),
Inner::Take(c) => Inner::Take(c),
Inner::Drop(c) => Inner::Drop(c),
Inner::Comp(cl, cr) => Inner::Comp(cl, cr),
Inner::Case(cl, cr) => Inner::Case(cl, cr),
Inner::AssertL(c, cmr) => Inner::AssertL(c, cmr),
Inner::AssertR(cmr, c) => Inner::AssertR(cmr, c),
Inner::Pair(cl, cr) => Inner::Pair(cl, cr),
Inner::Disconnect(cl, cr) => Inner::Disconnect(cl, cr?),
Inner::Witness(w) => Inner::Witness(w),
Inner::Fail(entropy) => Inner::Fail(entropy),
Inner::Jet(j) => Inner::Jet(j),
Expand Down Expand Up @@ -351,7 +375,7 @@ impl<C, J, X, W> Inner<C, J, X, Option<W>> {
}
}

impl<C, J: Clone, X, W: Clone> Inner<C, J, X, &W> {
impl<C, J: Clone, X, W: Copy> Inner<C, J, X, &W> {
/// Copies witness data.
///
/// Useful in conjunction with [`Inner::as_ref`] when you don't want to
Expand All @@ -361,6 +385,16 @@ impl<C, J: Clone, X, W: Clone> Inner<C, J, X, &W> {
}
}

impl<C, J: Clone, X: Copy, W> Inner<C, J, &X, W> {
/// Copies disconnect data.
///
/// Useful in conjunction with [`Inner::as_ref`] when you don't want to
/// take a reference to disconnect data.
pub fn copy_disconnect(self) -> Inner<C, J, X, W> {
self.map_disconnect(X::clone)
}
}

impl<C, J: fmt::Display, X, W> fmt::Display for Inner<C, J, X, W> {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
match self {
Expand Down
10 changes: 5 additions & 5 deletions src/node/redeem.rs
Original file line number Diff line number Diff line change
Expand Up @@ -366,7 +366,7 @@ mod tests {
prog.cmr().to_string(),
cmr_str,
"CMR mismatch (got {} expected {}) for program {}",
prog.cmr().to_string(),
prog.cmr(),
cmr_str,
prog_hex,
);
Expand All @@ -375,15 +375,15 @@ mod tests {
prog.amr().to_string(),
amr_str,
"AMR mismatch (got {} expected {}) for program {}",
prog.amr().to_string(),
prog.amr(),
amr_str,
prog_hex,
);
assert_eq!(
prog.imr().to_string(),
imr_str,
"IMR mismatch (got {} expected {}) for program {}",
prog.imr().to_string(),
prog.imr(),
imr_str,
prog_hex,
);
Expand Down Expand Up @@ -426,7 +426,7 @@ mod tests {
//
// wits_are_equal = comp (pair wit1 wit2) jet_eq_32 :: 1 -> 2
// main = comp wits_are_equal jet_verify :: 1 -> 1
let eqwits = vec![0xcd, 0xdc, 0x51, 0xb6, 0xe2, 0x08, 0xc0, 0x40];
let eqwits = [0xcd, 0xdc, 0x51, 0xb6, 0xe2, 0x08, 0xc0, 0x40];
let mut iter = BitIter::from(&eqwits[..]);
let eqwits_prog = CommitNode::<Core>::decode(&mut iter).unwrap();

Expand Down Expand Up @@ -474,7 +474,7 @@ mod tests {
#[test]
fn witness_consumed() {
// "main = unit", but with a witness attached. Found by fuzzer.
let badwit = vec![0x27, 0x00];
let badwit = [0x27, 0x00];
let mut iter = BitIter::from(&badwit[..]);
if let Err(Error::InconsistentWitnessLength) =
RedeemNode::<crate::jet::Core>::decode(&mut iter)
Expand Down
32 changes: 28 additions & 4 deletions src/types/final_data.rs
Original file line number Diff line number Diff line change
Expand Up @@ -114,11 +114,29 @@ impl fmt::Display for Final {
(CompleteBound::Unit, _) => {
f.write_str("1")?;
}
// special-case 1 + A as A?
(CompleteBound::Sum(ref left, _), 0)
if matches!(left.bound, CompleteBound::Unit) =>
{
skipping = Some(Tmr::unit());
}
(CompleteBound::Sum(ref left, _), 1)
if matches!(left.bound, CompleteBound::Unit) => {}
(CompleteBound::Sum(ref left, _), 2)
if matches!(left.bound, CompleteBound::Unit) =>
{
f.write_str("?")?;
}
// other sums and products
(CompleteBound::Sum(..), 0) | (CompleteBound::Product(..), 0) => {
f.write_str("(")?;
if data.index > 0 {
f.write_str("(")?;
}
}
(CompleteBound::Sum(..), 2) | (CompleteBound::Product(..), 2) => {
f.write_str(")")?;
if data.index > 0 {
f.write_str(")")?;
}
}
(CompleteBound::Sum(..), _) => f.write_str(" + ")?,
(CompleteBound::Product(..), _) => f.write_str(" × ")?,
Expand Down Expand Up @@ -216,9 +234,15 @@ mod tests {
assert_eq!(ty1.to_string(), "2^1024");

let sum = Final::sum(Final::two_two_n(5), Final::two_two_n(10));
assert_eq!(sum.to_string(), "(2^32 + 2^1024)");
assert_eq!(sum.to_string(), "2^32 + 2^1024");

let prod = Final::product(Final::two_two_n(5), Final::two_two_n(10));
assert_eq!(prod.to_string(), "(2^32 × 2^1024)");
assert_eq!(prod.to_string(), "2^32 × 2^1024");

let ty1 = Final::two_two_n(0);
assert_eq!(ty1.to_string(), "2");

let ty1 = Final::sum(Arc::new(Final::unit()), Final::two_two_n(2));
assert_eq!(ty1.to_string(), "2^4?");
}
}
12 changes: 10 additions & 2 deletions src/types/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -332,8 +332,16 @@ impl fmt::Display for Bound {
match (&*data.node, data.n_children_yielded) {
(Bound::Free(ref s), _) => f.write_str(s)?,
(Bound::Complete(ref comp), _) => fmt::Display::fmt(comp, f)?,
(Bound::Sum(..), 0) | (Bound::Product(..), 0) => f.write_str("(")?,
(Bound::Sum(..), 2) | (Bound::Product(..), 2) => f.write_str(")")?,
(Bound::Sum(..), 0) | (Bound::Product(..), 0) => {
if data.index > 0 {
f.write_str("(")?
}
}
(Bound::Sum(..), 2) | (Bound::Product(..), 2) => {
if data.index > 0 {
f.write_str(")")?
}
}
(Bound::Sum(..), _) => f.write_str(" + ")?,
(Bound::Product(..), _) => f.write_str(" × ")?,
}
Expand Down