From 8e239591e5cd6124db31eff36f0d21bd86529d62 Mon Sep 17 00:00:00 2001 From: Andrew Poelstra Date: Sat, 17 Oct 2026 04:45:48 +0000 Subject: [PATCH 1/3] human_encoding: serialize fail entropy with `0x` prefix `FailEntropy`'s `Display` impl renders bare hex, but the human-readable lexer only accepts hex literals with a `0x` prefix. So any program containing a `fail` node was serialized by `Forest::string_serialize` into a string that `Forest::parse` rejected ("unexpected character `0`"), breaking the parse/serialize round-trip in the same way as issue #394. Emit `fail 0x...` so the output re-parses. Written by GLM-5.3-Flash in Hermes Agent. --- src/human_encoding/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/human_encoding/mod.rs b/src/human_encoding/mod.rs index 7bbba011..c981731d 100644 --- a/src/human_encoding/mod.rs +++ b/src/human_encoding/mod.rs @@ -133,7 +133,7 @@ impl Forest { 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::Fail(entropy) => format!("{} := fail 0x{}", name, entropy), node::Inner::Jet(ref j) => format!("{} := jet_{}", name, j), node::Inner::Word(ref word) => { format!("{} := const {}", name, word) From a292d5976c492f29e690444e8c1603a34d160314 Mon Sep 17 00:00:00 2001 From: Andrew Poelstra Date: Sat, 17 Oct 2026 04:30:47 +0000 Subject: [PATCH 2/3] human_encoding: parse the `A?` optional notation The type `Display` implementations (`types::Final` and `types::Incomplete`) render the sum `1 + A` as `A?`. But the parser didn't accept this notation. Update the parser and document the new syntax in the human encoding README. Fixes #394. Written by GLM-5.3-Flash in Hermes Agent. --- src/human_encoding/README.md | 5 ++++- src/human_encoding/parse/ast.rs | 11 ++++++++++- 2 files changed, 14 insertions(+), 2 deletions(-) diff --git a/src/human_encoding/README.md b/src/human_encoding/README.md index 7d600846..2e5b9ff9 100644 --- a/src/human_encoding/README.md +++ b/src/human_encoding/README.md @@ -87,11 +87,14 @@ Finally, TYPE is * a literal `1`, indicating the unit type; * a literal `2`, indicating the bit type; * `2^n`, where `n` is any power of two, in decimal with no spaces or punctuation; +* another TYPE, followed by `?`, which is shorthand for `1 +` followed by that TYPE + (this matches how such types are displayed by the type `Display` implementations); * `(` followed by another TYPE followed by `)`; * another TYPE, followed by `+`, followed by another TYPE; or * another TYPE, followed by `*`, followed by another TYPE. -Here `*` has higher precedence than `+`, and both `+` and `*` are left-associative. +Here `?` binds more tightly than `+` and `*`; `*` has higher precedence than `+`, +and both `+` and `*` are left-associative. ## Namespaces diff --git a/src/human_encoding/parse/ast.rs b/src/human_encoding/parse/ast.rs index cfad2fe0..f60321b9 100644 --- a/src/human_encoding/parse/ast.rs +++ b/src/human_encoding/parse/ast.rs @@ -679,8 +679,17 @@ fn parse_type(p: &mut Parser) -> Result, ErrorSet> { Ok(lhs) } -/// Parse a type atom +/// Parse a type atom, including one or more `?`s. fn parse_type_atom(p: &mut Parser) -> Result, ErrorSet> { + let mut atom = parse_type_atom_inner(p)?; + // Repeated `?` denotes nested optionals, e.g. `2??` is 1 + (1 + 2). + while atom.is_some() && p.eat(&Token::Question) { + atom = atom.map(|ty| Type::Sum(Box::new(Type::One), Box::new(ty))); + } + Ok(atom) +} + +fn parse_type_atom_inner(p: &mut Parser) -> Result, ErrorSet> { match p.peek().cloned() { Some(Token::One) => { p.advance(); From 07ebcbbce3f46517801eefb8da3c6f40788b781f Mon Sep 17 00:00:00 2001 From: Andrew Poelstra Date: Sat, 17 Oct 2026 04:30:47 +0000 Subject: [PATCH 3/3] human_encoding: regression test for parsing `A?` and '`ail` Add tests covering the two serialization bugs fixed in the previous commits: * `parse::ast`: assert that the `A?` display shorthand parses to `1 + A`, binds tighter than `+`/`*`, supports nesting (`2??`), and is accepted in expression type ascriptions. * `human_encoding`: assert that `Forest::string_serialize` output re-parses to an equal forest for the issue #394 reproducer (`- := ?` / `a: v+2 -> v`), for the shorthand in nested and compound type positions, and for a program containing a `fail` node (including the `0x` prefix on the entropy). Written by GLM-5.3-Flash in Hermes Agent. --- src/human_encoding/mod.rs | 42 ++++++++++++++++++++++++++++++++- src/human_encoding/parse/ast.rs | 39 ++++++++++++++++++++++++++++++ 2 files changed, 80 insertions(+), 1 deletion(-) diff --git a/src/human_encoding/mod.rs b/src/human_encoding/mod.rs index c981731d..86f8d849 100644 --- a/src/human_encoding/mod.rs +++ b/src/human_encoding/mod.rs @@ -209,7 +209,7 @@ impl Forest { #[cfg(test)] mod tests { use crate::human_encoding::Forest; - use crate::jet::{CoreEnv, JetEnvironment}; + use crate::jet::{Core, CoreEnv, JetEnvironment}; use crate::types; use crate::{BitMachine, Value}; use std::collections::HashMap; @@ -361,6 +361,46 @@ mod tests { ); } + #[test] + fn string_serialize_round_trip() { + // Regression test for issue #394: the type `Display` shorthand `A?` + // (meaning `1 + A`) was not accepted by the parser, so re-parsing + // serialized programs failed whenever a free type variable was + // resolved to unit, making the source type `1 + 2`, displayed `2?`. + let program = Forest::parse::("- := ?\na: v+2 -> v\n").expect("parse"); + let reserialize = program.string_serialize(); + let round_trip = Forest::parse::(&reserialize).unwrap_or_else(|e| { + panic!("serialized program should re-parse: {}\n{}", e, reserialize) + }); + assert_eq!(program, round_trip); + + // Same shorthand in nested and compound positions. + for ty in ["(v + 2) * 2^2", "v + (1 + w)", "v + (1 + (1 + w))"] { + let s = format!("- := ?h : {} -> 1\n", ty); + let program = Forest::parse::(&s).expect("parse"); + let reserialize = program.string_serialize(); + let round_trip = Forest::parse::(&reserialize).unwrap_or_else(|e| { + panic!("serialized program should re-parse: {}\n{}", e, reserialize) + }); + assert_eq!(program, round_trip); + } + + // Fail nodes serialize their entropy with a `0x` prefix, which the + // lexer requires; previously they emitted bare hex and did not re-parse. + let s = "- := fail 0x000102030405060708090a0b0c0d0e0f101112131415161718191a1b1c1d1e1f\n"; + let program = Forest::parse::(s).expect("parse"); + let reserialize = program.string_serialize(); + assert!( + reserialize.contains("fail 0x00010203"), + "serialized program should contain 0x-prefixed entropy:\n{}", + reserialize, + ); + let round_trip = Forest::parse::(&reserialize).unwrap_or_else(|e| { + panic!("serialized program should re-parse: {}\n{}", e, reserialize) + }); + assert_eq!(program, round_trip); + } + #[test] fn witness_name_override() { let s = " diff --git a/src/human_encoding/parse/ast.rs b/src/human_encoding/parse/ast.rs index f60321b9..b95cf9a5 100644 --- a/src/human_encoding/parse/ast.rs +++ b/src/human_encoding/parse/ast.rs @@ -818,4 +818,43 @@ mod tests { ) .unwrap(); } + + #[test] + fn display_optional_type() { + // The `?` type shorthand (see the `Display` impls for `types::Final` + // and `types::Incomplete`) means `1 + `. + let lines = parse_line_vector::("U : 2? -> 1").unwrap(); + assert_eq!(lines.len(), 1); + assert_eq!( + lines[0].arrow, + ( + Some(Type::Sum(Box::new(Type::One), Box::new(Type::Two))), + Some(Type::One), + ), + ); + + // `?` binds tighter than `*` and `+`, mirroring the type `Display` + // implementations; e.g. `2? * 2^2` is `(1 + 2) * 2^2`. + let lines = parse_line_vector::("U : 2? * 2^2 -> 1").unwrap(); + assert_eq!( + lines[0].arrow.0, + Some(Type::Product( + Box::new(Type::Sum(Box::new(Type::One), Box::new(Type::Two))), + Box::new(Type::TwoTwoN(1)), + )), + ); + + // Repeated `?` denotes nested optionals: `2??` is `1 + (1 + 2)`. + let lines = parse_line_vector::("U : 2?? -> 1").unwrap(); + assert_eq!( + lines[0].arrow.0, + Some(Type::Sum( + Box::new(Type::One), + Box::new(Type::Sum(Box::new(Type::One), Box::new(Type::Two))), + )), + ); + + // The shorthand may also appear inside expression type ascriptions. + parse_line_vector::("U := witness : v + 2? -> v").unwrap(); + } }