Merge #169: Introduce typed holes; improve disconnect support in huma…

…n-readable encoding

5465612 human_encoding: output both CMR and IMR when disassembling programs; add more spacing (Andrew Poelstra)
7494aab simpcli: fixpoint example program, and `relabel` command (Andrew Poelstra)
2680e3e node: expose IMR in CommitData (Andrew Poelstra)
0fbddc6 human_readable: add fuzztest (Andrew Poelstra)
2ceb135 human_encoding: make disconnect a binary combinator with a hole for a right child (Andrew Poelstra)
3f974d0 human_encoding: add typed holes (Andrew Poelstra)
045a3c3 simpcli: add example programs directory (Andrew Poelstra)

Pull request description:

  This introduces the notion of "typed holes" which can be used as placeholders in the text encoding of Simplicity. It uses these holes for disconnect, so that at commitment time users can set their right children to placeholders. The old behavior, which allowed putting a complete expression into `disconnect` that wouldn't be committed to, was dangerous.

ACKs for top commit:
  uncomputable:
    5465612 ACK. Sanket's bug is already present on master.

Tree-SHA512: 08e2529cd7ddc4238635550e34aea1ab0d1dcaa8a83124701329f390624d218c9893948174e15ff04bd1431c5b6d320ed28e54aa470f18e752db5d76eee0a6a9

.github/workflows/fuzz.yml

@@ -19,6 +19,7 @@ jobs:
 c_rust_merkle,
 decode_natural,
 decode_program,
+parse_human,
         ]
     steps:
       - name: Install test dependencies

fuzz/Cargo.toml

@@ -27,3 +27,7 @@ path = "fuzz_targets/decode_natural.rs"
 [[bin]]
 name = "decode_program"
 path = "fuzz_targets/decode_program.rs"
+
+[[bin]]
+name = "parse_human"
+path = "fuzz_targets/parse_human.rs"

fuzz/fuzz_targets/parse_human.rs

@@ -0,0 +1,66 @@
+// Rust Simplicity Library
+// Written in 2023 by
+//   Andrew Poelstra <[email protected]>
+//
+// To the extent possible under law, the author(s) have dedicated all
+// copyright and related and neighboring rights to this software to
+// the public domain worldwide. This software is distributed without
+// any warranty.
+//
+// You should have received a copy of the CC0 Public Domain Dedication
+// along with this software.
+// If not, see <http://creativecommons.org/publicdomain/zero/1.0/>.
+//
+
+use std::str;
+use honggfuzz::fuzz;
+use simplicity::jet::Elements;
+use simplicity::human_encoding::Forest;
+
+fn do_test(data: &[u8]) {
+    let s = match str::from_utf8(data) {
+        Ok(s) => s,
+        Err(_) => return,
+    };
+
+    if let Ok(program) = Forest::<Elements>::parse(s) {
+        let reserialize= program.string_serialize();
+        let round_trip = Forest::<Elements>::parse(&reserialize).unwrap();
+        assert_eq!(program, round_trip);
+    }
+}
+
+fn main() {
+    loop {
+        fuzz!(|data| {
+            do_test(data);
+        });
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    fn extend_vec_from_hex(hex: &str, out: &mut Vec<u8>) {
+        let mut b = 0;
+        for (idx, c) in hex.as_bytes().iter().enumerate() {
+            b <<= 4;
+            match *c {
+                b'A'..=b'F' => b |= c - b'A' + 10,
+                b'a'..=b'f' => b |= c - b'a' + 10,
+                b'0'..=b'9' => b |= c - b'0',
+                _ => panic!("Bad hex"),
+            }
+            if (idx & 1) == 1 {
+                out.push(b);
+                b = 0;
+            }
+        }
+    }
+
+    #[test]
+    fn duplicate_crash() {
+        let mut a = Vec::new();
+        extend_vec_from_hex("00", &mut a);
+        super::do_test(&a);
+    }
+}

simpcli/example_programs/bip340.simpl

@@ -0,0 +1,12 @@
+-- Witnesses
+sig1 := witness : 1 -> 2^512
+
+-- Constants
+const1 := const 0xf9308a019258c31049344f85f89d5229b531c845836f99b08601f113bce036f90000000000000000000000000000000000000000000000000000000000000000 : 1 -> 2^512 -- f254d6e9
+
+-- Program code
+pr1 := pair const1 sig1  : 1 -> (2^512 * 2^512)   -- 31ae2960
+jt2 := jet_bip_0340_verify : (2^512 * 2^512) -> 1 -- af924cbe
+
+main := comp pr1 jt2       : 1 -> 1               -- 7bc56cb1
+

simpcli/example_programs/eq-plus-one.simpl

@@ -0,0 +1,8 @@
+-- Program which demands two 32-bit witnesses, the first one == the second + 1
+wit1 := comp iden witness : 1 -> 2^32
+wit2 := comp iden witness : 1 -> 2^32
+
+wit_diff := comp (comp (pair wit1 wit2) jet_subtract_32) (drop iden) : 1 -> 2^32
+diff_is_one := comp (pair wit_diff jet_one_32) jet_eq_32             : 1 -> 2
+main := comp diff_is_one jet_verify                                  : 1 -> 1
+

simpcli/example_programs/fixpoint.simpl

@@ -0,0 +1,32 @@
+
+-- Witnesses
+-- IMR: [none]
+wit_input := witness
+
+-- All jets have source type 1; but to use the `pair` combinator we want one
+-- with source type 2^256. To get this, we compose it with unit.
+sha256_init : 2^256 -> _
+sha256_init := comp unit jet_sha_256_ctx_8_init
+
+-- Using this, we can write a self-contained "take 32 bytes and compute their
+-- sha2 hash" function.
+-- IMR: 8e341445...
+sha256 : 2^256 -> 2^256
+sha256 := comp
+    comp
+        pair sha256_init iden
+        jet_sha_256_ctx_8_add_32
+    jet_sha_256_ctx_8_finalize
+
+-- Check eq
+assert_fixpoint : 2^256 -> 1
+assert_fixpoint := comp
+    comp
+        pair (comp iden sha256) iden
+        jet_eq_256
+    jet_verify
+
+-- IMR: [none]
+main := comp wit_input assert_fixpoint
+
+

simpcli/example_programs/twowit.simpl

@@ -0,0 +1,14 @@
+--
+-- Attempts to reuse a witness name.
+--
+-- By uncommenting wit2 and replacing one of the wit1 references with wit2,
+-- it'll work...but is it what you intended?
+--
+
+wit1 := witness : 1 -> 2^32
+--wit2 := witness : 1 -> 2^32
+wit_tuple := pair wit1 wit1 : 1 -> 2^64
+
+check_eq := comp wit_tuple jet_eq_32
+main := comp check_eq jet_verify
+

simpcli/src/main.rs

@@ -29,6 +29,7 @@ fn usage(process_name: &str) {
     eprintln!("Usage:");
     eprintln!("  {} assemble <filename>", process_name);
     eprintln!("  {} disassemble <base64>", process_name);
+    eprintln!("  {} relabel <base64>", process_name);
     eprintln!();
     eprintln!("For commands which take an optional expression, the default value is \"main\".");
     eprintln!();
@@ -43,6 +44,7 @@ fn invalid_usage(process_name: &str) -> Result<(), String> {
 enum Command {
     Assemble,
     Disassemble,
+    Relabel,
     Help,
 }
 
@@ -52,6 +54,7 @@ impl FromStr for Command {
         match s {
             "assemble" => Ok(Command::Assemble),
             "disassemble" => Ok(Command::Disassemble),
+            "relabel" => Ok(Command::Relabel),
             "help" => Ok(Command::Help),
             x => Err(format!("unknown command {}", x)),
         }
@@ -63,6 +66,7 @@ impl Command {
         match *self {
             Command::Assemble => false,
             Command::Disassemble => false,
+            Command::Relabel => false,
             Command::Help => false,
         }
     }
@@ -153,6 +157,10 @@ fn main() -> Result<(), String> {
             let prog = Forest::<DefaultJet>::from_program(commit);
             println!("{}", prog.string_serialize());
         }
+        Command::Relabel => {
+            let prog = parse_file(&first_arg)?;
+            println!("{}", prog.string_serialize());
+        }
         Command::Help => unreachable!(),
     }
 

src/human_encoding/error.rs

@@ -171,6 +171,8 @@ impl error::Error for ErrorSet {
             Error::BadWordLength { .. } => None,
             Error::EntropyInsufficient { .. } => None,
             Error::EntropyTooMuch { .. } => None,
+            Error::HoleAtCommitTime { .. } => None,
+            Error::HoleFilledAtCommitTime => None,
             Error::NameIllegal(_) => None,
             Error::NameIncomplete(_) => None,
             Error::NameMissing(_) => None,
@@ -243,6 +245,15 @@ pub enum Error {
     EntropyInsufficient { bit_length: usize },
     /// A "fail" node was provided with more than 512 bits of entropy
     EntropyTooMuch { bit_length: usize },
+    /// When converting to a `CommitNode`, there were unfilled holes which prevent
+    /// us from knowing the whole program.
+    HoleAtCommitTime {
+        name: Arc<str>,
+        arrow: types::arrow::Arrow,
+    },
+    /// When converting to a `CommitNode`, a disconnect node had an actual node rather
+    /// than a hole.
+    HoleFilledAtCommitTime,
     /// An expression name was not allowed to be used as a name.
     NameIllegal(Arc<str>),
     /// An expression was given a type, but no actual expression was provided.
@@ -295,6 +306,17 @@ impl fmt::Display for Error {
                 "fail node has too much entropy ({} bits, max 512)",
                 bit_length
             ),
+            Error::HoleAtCommitTime {
+                ref name,
+                ref arrow,
+            } => write!(
+                f,
+                "unfilled hole ?{} at commitment time; type arrow {}",
+                name, arrow
+            ),
+            Error::HoleFilledAtCommitTime => {
+                f.write_str("disconnect node has a non-hole child at commit time")
+            }
             Error::NameIllegal(ref s) => {
                 write!(f, "name `{}` is not allowed in this context", s)
             }

src/human_encoding/mod.rs

@@ -28,6 +28,7 @@ mod serialize;
 use crate::dag::{DagLike, MaxSharing};
 use crate::jet::Jet;
 use crate::node::{self, CommitNode};
+use crate::{Cmr, Imr};
 
 use std::collections::HashMap;
 use std::str;
@@ -66,6 +67,30 @@ impl From<santiago::lexer::Position> for Position {
     }
 }
 
+/// For named construct nodes, we abuse the `witness` combinator to support typed holes.
+///
+/// We do this because `witness` nodes have free source and target arrows, and
+/// allow us to store arbitrary data in them using the generic witness type of
+/// the node. Holes are characterized entirely by their source and target type,
+/// just like witnesses, and are labelled by their name.
+#[derive(Debug, PartialEq, Eq, Clone, Hash)]
+pub enum WitnessOrHole {
+    /// This witness is an actual witness combinator (with no witness data attached,
+    /// that comes later)
+    Witness,
+    /// This is a typed hole, with the given name.
+    TypedHole(Arc<str>),
+}
+
+impl WitnessOrHole {
+    pub fn shallow_clone(&self) -> Self {
+        match self {
+            WitnessOrHole::Witness => WitnessOrHole::Witness,
+            WitnessOrHole::TypedHole(name) => WitnessOrHole::TypedHole(Arc::clone(name)),
+        }
+    }
+}
+
 #[derive(Clone, Debug, PartialEq, Eq)]
 pub struct Forest<J: Jet> {
     roots: HashMap<Arc<str>, Arc<NamedCommitNode<J>>>,
@@ -93,22 +118,30 @@ impl<J: Jet> Forest<J> {
     /// Serialize the program in human-readable form
     pub fn string_serialize(&self) -> String {
         struct Print {
+            cmr: Cmr,
+            imr: Option<Imr>,
             expr_str: String,  // The X = Y part
             arrow_str: String, // The :: A -> B part
-            cmr_str: String,   // The -- <cmr> part
         }
         fn print_lines(lines: &[Print], skip_before_end: bool) -> String {
             let mut ret = String::new();
             let expr_width = lines.iter().map(|line| line.expr_str.len()).max().unwrap();
             let arrow_width = lines.iter().map(|line| line.arrow_str.len()).max().unwrap();
             let last_line = lines.len();
             for (n, line) in lines.iter().enumerate() {
+                ret += "\n";
                 if skip_before_end && n == last_line - 1 {
                     ret += "\n";
                 }
+                ret += &format!("-- CMR: {}\n", line.cmr);
+                if let Some(imr) = line.imr {
+                    ret += &format!("-- IMR: {}\n", imr);
+                } else {
+                    ret += "-- IMR: [undetermined]\n";
+                }
                 ret += &format!(
-                    "{0:1$} {2:3$} {4}\n",
-                    line.expr_str, expr_width, line.arrow_str, arrow_width, line.cmr_str
+                    "{0:1$} {2:3$}\n",
+                    line.expr_str, expr_width, line.arrow_str, arrow_width,
                 );
             }
             ret
@@ -117,6 +150,7 @@ impl<J: Jet> Forest<J> {
         let mut witness_lines = vec![];
         let mut const_lines = vec![];
         let mut program_lines = vec![];
+        let mut disc_idx = 0;
         // Pass 1: compute string data for every node
         for root in self.roots.values() {
             for data in root.as_ref().post_order_iter::<MaxSharing<_>>() {
@@ -141,22 +175,19 @@ impl<J: Jet> Forest<J> {
                 } else if let node::Inner::AssertL(_, cmr) = node.inner() {
                     expr_str.push_str(" #");
                     expr_str.push_str(&cmr.to_string());
+                } else if let node::Inner::Disconnect(_, node::NoDisconnect) = node.inner() {
+                    expr_str.push_str(&format!(" ?disc_expr_{}", disc_idx));
+                    disc_idx += 1;
                 }
 
                 let arrow = node.arrow();
                 let arrow_str = format!(": {} -> {}", arrow.source, arrow.target).replace('×', "*"); // for human-readable encoding stick with ASCII
 
-                // All witnesses have the same CMR so don't bother printing it
-                let cmr_str = if let node::Inner::Witness(..) = node.inner() {
-                    String::new()
-                } else {
-                    format!("-- cmr {:.8}...", node.cmr())
-                };
-
                 let print = Print {
+                    cmr: node.cmr(),
+                    imr: node.imr(),
                     expr_str,
                     arrow_str,
-                    cmr_str,
                 };
                 if let node::Inner::Witness(..) = node.inner() {
                     witness_lines.push(print);
@@ -171,18 +202,18 @@ impl<J: Jet> Forest<J> {
         // Pass 2: actually print everything
         let mut ret = String::new();
         if !witness_lines.is_empty() {
-            ret += "-- Witnesses\n";
+            ret += "--------------\n-- Witnesses\n--------------\n";
             ret += &print_lines(&witness_lines, false);
             ret += "\n";
         }
         if !const_lines.is_empty() {
             // FIXME detect scribes
-            ret += "-- Constants\n";
+            ret += "--------------\n-- Constants\n--------------\n";
             ret += &print_lines(&const_lines, false);
             ret += "\n";
         }
         if !program_lines.is_empty() {
-            ret += "-- Program code\n";
+            ret += "--------------\n-- Program code\n--------------\n";
             ret += &print_lines(&program_lines, true /* add a blank line before main */);
         }
         ret