Add composition terminology to website and otherwise improve docs (ri…

…sc0#1314)

This PR adds terminology entries to the website for terms/concepts
related to composition. Additionally is adds a bit more documentation to
types and methods related to composition, and additionally refactors the
`ExecutorEnv::add_assumption` method to accept `impl Into<Assumption>`
which allows the user to pass in a receipt without any transformation.

---------

Co-authored-by: Tim Zerrell <[email protected]>

bonsai/rest-api-mock/src/prover.rs

@@ -92,7 +92,7 @@ impl Prover {
                         continue;
                     }
                     let deserialized_receipt: Receipt = bincode::deserialize(&receipt)?;
-                    env.add_assumption(deserialized_receipt.into());
+                    env.add_assumption(deserialized_receipt);
                 }
 
                 let env = env

examples/composition/src/main.rs

@@ -26,7 +26,7 @@ fn main() {
     // chosen by Alice. This is like an RSA encryption from Bob to Alice, verified by the zkVM.
     let env = ExecutorEnv::builder()
         // add_assumption makes the receipt to be verified available to the prover.
-        .add_assumption(multiply_receipt.into())
+        .add_assumption(multiply_receipt)
         .write(&(n, 9u64, 100u64))
         .unwrap()
         .build()

risc0/build/src/docker.rs

@@ -233,15 +233,15 @@ mod test {
         build("../../risc0/zkvm/methods/guest/Cargo.toml");
         compare_image_id(
             "risc0_zkvm_methods_guest/multi_test",
-            "1e285559e2350e1bd5f72926c32c79333c83f3bbf438a5f43f4cc5b658dee49f",
+            "7cf76922134ecd86e4ad76508a7069afc3e9727e061c27ec2372bcbc2a5fcec8",
         );
         compare_image_id(
             "risc0_zkvm_methods_guest/hello_commit",
             "6efc912a71f11d152714774094c94e2a395b70cdeeb87bcb0e740ce8a321e9a4",
         );
         compare_image_id(
             "risc0_zkvm_methods_guest/slice_io",
-            "ce01ec8697f2cfbe01cc55a9d64d7a1a0340d18281d6ce54b277e804084482c1",
+            "d22f1a689dfc6b4a0fcf93b18d710b420b5416849ec9f6c64f97a56838518aab",
         );
     }
 }

risc0/zkvm/src/guest/env.rs

@@ -113,7 +113,7 @@ pub fn syscall(syscall: SyscallName, to_host: &[u8], from_host: &mut [u32]) -> s
 /// Calling this function in the guest is logically equivalent to verifying a receipt with the same
 /// image ID and journal. Any party verifying the receipt produced by this execution can then be
 /// sure that the receipt verified by this call is also valid. In this way, multiple receipts from
-/// potentially distinct guests can be combined into one. This feature is know as composition.
+/// potentially distinct guests can be combined into one. This feature is know as [composition].
 ///
 /// In order to be valid, the [crate::Receipt] must have `ExitCode::Halted(0)` or
 /// `ExitCode::Paused(0)`, an empty assumptions list, and an all-zeroes input hash. It may have any
@@ -127,6 +127,8 @@ pub fn syscall(syscall: SyscallName, to_host: &[u8], from_host: &mut [u32]) -> s
 /// # let HELLO_WORLD_ID = Digest::ZERO;
 /// env::verify(HELLO_WORLD_ID, b"hello world".as_slice()).unwrap();
 /// ```
+///
+/// [composition]: https://dev.risczero.com/terminology#composition
 pub fn verify(image_id: impl Into<Digest>, journal: &[impl Pod]) -> Result<(), VerifyError> {
     let image_id: Digest = image_id.into();
     let journal_digest: Digest = bytemuck::cast_slice::<_, u8>(journal).digest();
@@ -211,17 +213,19 @@ impl fmt::Display for VerifyError {
 impl std::error::Error for VerifyError {}
 
 /// Verify that there exists a valid receipt with the specified
-/// [ReceiptClaim].
+/// [crate::ReceiptClaim].
 ///
 /// Calling this function in the guest is logically equivalent to verifying a receipt with the same
-/// [ReceiptClaim]. Any party verifying the receipt produced by this execution can then be
+/// [crate::ReceiptClaim]. Any party verifying the receipt produced by this execution can then be
 /// sure that the receipt verified by this call is also valid. In this way, multiple receipts from
-/// potentially distinct guests can be combined into one. This feature is know as composition.
+/// potentially distinct guests can be combined into one. This feature is know as [composition].
 ///
 /// In order for a receipt to be valid, it must have a verifying cryptographic seal and
 /// additionally have no assumptions. Note that executions with no output (e.g. those ending in
 /// [ExitCode::SystemSplit]) will not have any encoded assumptions even if [verify] or
 /// [verify_integrity] is called.
+///
+/// [composition]: https://dev.risczero.com/terminology#composition
 pub fn verify_integrity(claim: &ReceiptClaim) -> Result<(), VerifyIntegrityError> {
     // Check that the assumptions list is empty.
     let assumptions_empty = claim.output.is_none()
@@ -253,7 +257,7 @@ pub fn verify_integrity(claim: &ReceiptClaim) -> Result<(), VerifyIntegrityError
 #[derive(Debug)]
 #[non_exhaustive]
 pub enum VerifyIntegrityError {
-    /// Provided [ReceiptClaim] struct contained a non-empty assumptions list.
+    /// Provided [crate::ReceiptClaim] struct contained a non-empty assumptions list.
     ///
     /// This is a semantic error as only unconditional receipts can be verified
     /// inside the guest. If there is a conditional receipt to verify, it's

risc0/zkvm/src/host/api/server.rs

@@ -627,12 +627,12 @@ fn build_env<'a>(
         match assumption.kind.as_ref().ok_or(malformed_err())? {
             pb::api::assumption::Kind::Proven(asset) => {
                 let receipt: Receipt = pb::core::Receipt::decode(asset.as_bytes()?)?.try_into()?;
-                env_builder.add_assumption(receipt.into())
+                env_builder.add_assumption(receipt)
             }
             pb::api::assumption::Kind::Unresolved(asset) => {
                 let claim: MaybePruned<ReceiptClaim> =
                     pb::core::MaybePruned::decode(asset.as_bytes()?)?.try_into()?;
-                env_builder.add_assumption(claim.into())
+                env_builder.add_assumption(claim)
             }
         };
     }

risc0/zkvm/src/host/api/tests.rs

@@ -263,7 +263,7 @@ fn lift_resolve() {
 
     // Execute the composition multitest
     let env = ExecutorEnv::builder()
-        .add_assumption(assumption_succinct_receipt.claim.clone().into())
+        .add_assumption(assumption_succinct_receipt.claim.clone())
         .write(&MultiTestSpec::SysVerify(vec![(
             HELLO_COMMIT_ID.into(),
             b"hello world".to_vec(),

risc0/zkvm/src/host/client/env.rs

@@ -324,13 +324,23 @@ impl<'a> ExecutorEnvBuilder<'a> {
         self
     }
 
-    /// Add an [Assumption] to the [ExecutorEnv] associated assumptions.
+    /// Add an [Assumption] to the [ExecutorEnv], for use in [composition].
     ///
     /// During execution, when the guest calls `env::verify` or
     /// `env::verify_integrity`, this collection will be searched for an
     /// [Assumption] that corresponds the verification call.
-    pub fn add_assumption(&mut self, assumption: Assumption) -> &mut Self {
-        self.inner.assumptions.borrow_mut().cached.push(assumption);
+    ///
+    /// Either a [crate::Receipt] or a [crate::ReceiptClaim] can be provided. If a [crate::Receipt]
+    /// is provided, then then an [Assumption::Proven] will be added to the [ExecutorEnv] and the
+    /// [crate::Receipt] generated by proving will be unconditional.
+    ///
+    /// [composition]: https://dev.risczero.com/terminology#composition
+    pub fn add_assumption(&mut self, assumption: impl Into<Assumption>) -> &mut Self {
+        self.inner
+            .assumptions
+            .borrow_mut()
+            .cached
+            .push(assumption.into());
         self
     }
 

risc0/zkvm/src/host/receipt.rs

@@ -45,10 +45,10 @@ use crate::{
     Assumptions, ExitCode, MaybePruned, Output, ReceiptClaim,
 };
 
-/// A receipt attesting to the execution of a Session.
+/// A receipt attesting to the execution of a guest program.
 ///
 /// A Receipt is a zero-knowledge proof of computation. It attests that the
-/// [Receipt::journal] was produced by executing a [crate::Session] based on a
+/// [Receipt::journal] was produced by executing a guest program based on a
 /// specified memory image. This image is _not_ included in the receipt; the
 /// verifier must provide an [ImageID](https://dev.risczero.com/terminology),
 /// a cryptographic hash corresponding to the expected image.
@@ -58,6 +58,7 @@ use crate::{
 /// from running specific code. Conversely, a verifier can inspect a receipt to
 /// confirm that its results must have been generated from the expected code,
 /// even when this code was run by an untrusted source.
+///
 /// # Example
 ///
 /// To create a [Receipt] attesting to the faithful execution of your code, run
@@ -81,6 +82,7 @@ use crate::{
 /// have been executed as a parameter. (See
 /// [risc0_build](https://docs.rs/risc0-build/latest/risc0_build/) for more
 /// information about how ImageIDs are generated.)
+///
 /// ```rust
 /// use risc0_zkvm::Receipt;
 /// # #[cfg(feature = "prove")]
@@ -97,10 +99,8 @@ use crate::{
 /// ```
 ///
 /// The public outputs of the [Receipt] are contained in the
-/// [Receipt::journal]. We provide serialization tools in the zkVM
-/// [serde](crate::serde) module, which can be used to read data from the
-/// journal as the same type it was written to the journal. If you prefer, you
-/// can also directly access the [Receipt::journal] as a `Vec<u8>`.
+/// [Receipt::journal]. You can use [Journal::decode] to deserialize the journal as typed and
+/// structured data, or access the [Journal::bytes] directly.
 #[derive(Clone, Debug, Deserialize, Serialize)]
 #[cfg_attr(test, derive(PartialEq))]
 pub struct Receipt {
@@ -252,7 +252,7 @@ impl Journal {
         Self { bytes }
     }
 
-    /// Decode the journal bytes by using the risc0 deserializer.
+    /// Decode the journal bytes by using the [risc0 deserializer](crate::serde).
     pub fn decode<T: DeserializeOwned>(&self) -> Result<T, Error> {
         from_slice(&self.bytes)
     }
@@ -592,7 +592,7 @@ impl CompositeReceipt {
 
 /// A receipt attesting to the execution of a Segment.
 ///
-/// A SegmentReceipt attests that a [crate::Segment] was executed in a manner
+/// A SegmentReceipt attests that a Segment was executed in a manner
 /// consistent with the [ReceiptClaim] included in the receipt.
 #[derive(Clone, Debug, Deserialize, Serialize)]
 #[cfg_attr(test, derive(PartialEq))]
@@ -659,11 +659,15 @@ impl SegmentReceipt {
     }
 }
 
-/// An assumption attached with a guest execution as a result of calling
+/// An assumption attached to a guest execution as a result of calling
 /// `env::verify` or `env::verify_integrity`.
 #[derive(Clone, Debug, Serialize, Deserialize)]
 pub enum Assumption {
     /// A [Receipt] for a proven assumption.
+    ///
+    /// Upon proving, this receipt will be used as proof of the assumption that results from a call
+    /// to `env::verify`, and the resulting receipt will be unconditional. As a result,
+    /// [Receipt::verify] will return true and the verifier will accept the receipt.
     Proven(Receipt),
 
     /// [ReceiptClaim] digest for an assumption that is not directly proven

risc0/zkvm/src/host/recursion/tests.rs

@@ -225,8 +225,8 @@ fn generate_composition_receipt(hashfn: &str) -> Receipt {
     tracing::info!("Done proving rv32im: echo 'execution B'");
 
     let env = ExecutorEnv::builder()
-        .add_assumption(assumption_receipt_a.clone().into())
-        .add_assumption(assumption_receipt_b.clone().into())
+        .add_assumption(assumption_receipt_a.clone())
+        .add_assumption(assumption_receipt_b.clone())
         .write(&MultiTestSpec::SysVerify(vec![
             (MULTI_TEST_ID.into(), b"execution A".to_vec()),
             (MULTI_TEST_ID.into(), b"execution B".to_vec()),

risc0/zkvm/src/host/server/exec/tests.rs

@@ -467,7 +467,7 @@ mod sys_verify {
         let env = ExecutorEnv::builder()
             .write(&spec)
             .unwrap()
-            .add_assumption(hello_commit_session.get_claim().unwrap().into())
+            .add_assumption(hello_commit_session.get_claim().unwrap())
             .build()
             .unwrap();
         let session = ExecutorImpl::from_elf(env, MULTI_TEST_ELF)
@@ -499,7 +499,7 @@ mod sys_verify {
             let env = ExecutorEnv::builder()
                 .write(&spec)
                 .unwrap()
-                .add_assumption(halt_session.get_claim().unwrap().into())
+                .add_assumption(halt_session.get_claim().unwrap())
                 .build()
                 .unwrap();
             let session = ExecutorImpl::from_elf(env, MULTI_TEST_ELF).unwrap().run();
@@ -523,7 +523,7 @@ mod sys_verify {
             let env = ExecutorEnv::builder()
                 .write(&spec)
                 .unwrap()
-                .add_assumption(pause_session.get_claim().unwrap().into())
+                .add_assumption(pause_session.get_claim().unwrap())
                 .build()
                 .unwrap();
             let session = ExecutorImpl::from_elf(env, MULTI_TEST_ELF).unwrap().run();
@@ -547,7 +547,7 @@ mod sys_verify {
         let env = ExecutorEnv::builder()
             .write(&spec)
             .unwrap()
-            .add_assumption(fault_session.get_claim().unwrap().into())
+            .add_assumption(fault_session.get_claim().unwrap())
             .build()
             .unwrap();
         assert!(ExecutorImpl::from_elf(env, MULTI_TEST_ELF)
@@ -568,7 +568,7 @@ mod sys_verify {
         let env = ExecutorEnv::builder()
             .write(&spec)
             .unwrap()
-            .add_assumption(hello_commit_session.get_claim().unwrap().into())
+            .add_assumption(hello_commit_session.get_claim().unwrap())
             .build()
             .unwrap();
         let session = ExecutorImpl::from_elf(env, MULTI_TEST_ELF)
@@ -602,7 +602,7 @@ mod sys_verify {
             let env = ExecutorEnv::builder()
                 .write(&spec)
                 .unwrap()
-                .add_assumption(halt_session.get_claim().unwrap().into())
+                .add_assumption(halt_session.get_claim().unwrap())
                 .build()
                 .unwrap();
             let session = ExecutorImpl::from_elf(env, MULTI_TEST_ELF)
@@ -626,7 +626,7 @@ mod sys_verify {
             let env = ExecutorEnv::builder()
                 .write(&spec)
                 .unwrap()
-                .add_assumption(pause_session.get_claim().unwrap().into())
+                .add_assumption(pause_session.get_claim().unwrap())
                 .build()
                 .unwrap();
             let session = ExecutorImpl::from_elf(env, MULTI_TEST_ELF)
@@ -650,7 +650,7 @@ mod sys_verify {
         let env = ExecutorEnv::builder()
             .write(&spec)
             .unwrap()
-            .add_assumption(fault_session.get_claim().unwrap().into())
+            .add_assumption(fault_session.get_claim().unwrap())
             .build()
             .unwrap();
         let session = ExecutorImpl::from_elf(env, MULTI_TEST_ELF)
@@ -676,7 +676,7 @@ mod sys_verify {
         let env = ExecutorEnv::builder()
             .write(&spec)
             .unwrap()
-            .add_assumption(hello_commit_session.get_claim().unwrap().into())
+            .add_assumption(hello_commit_session.get_claim().unwrap())
             .build()
             .unwrap();
 

risc0/zkvm/src/host/server/prove/tests.rs

@@ -535,7 +535,7 @@ mod sys_verify {
         let env = ExecutorEnv::builder()
             .write(&spec)
             .unwrap()
-            .add_assumption(HELLO_COMMIT_RECEIPT.clone().into())
+            .add_assumption(HELLO_COMMIT_RECEIPT.clone())
             .build()
             .unwrap();
         get_prover_server(&prover_opts_fast())
@@ -562,7 +562,7 @@ mod sys_verify {
         let env = ExecutorEnv::builder()
             .write(&spec)
             .unwrap()
-            .add_assumption(HELLO_COMMIT_RECEIPT.get_claim().unwrap().into())
+            .add_assumption(HELLO_COMMIT_RECEIPT.get_claim().unwrap())
             .build()
             .unwrap();
         // TODO(#982) Conditional receipts currently return an error on verification.
@@ -589,7 +589,7 @@ mod sys_verify {
         let env = ExecutorEnv::builder()
             .write(&spec)
             .unwrap()
-            .add_assumption(HELLO_COMMIT_RECEIPT.clone().into())
+            .add_assumption(HELLO_COMMIT_RECEIPT.clone())
             .build()
             .unwrap();
         get_prover_server(&prover_opts_fast())
@@ -616,7 +616,7 @@ mod sys_verify {
         let env = ExecutorEnv::builder()
             .write(&spec)
             .unwrap()
-            .add_assumption(HELLO_COMMIT_RECEIPT.get_claim().unwrap().into())
+            .add_assumption(HELLO_COMMIT_RECEIPT.get_claim().unwrap())
             .build()
             .unwrap();
         // TODO(#982) Conditional receipts currently return an error on verification.
@@ -640,7 +640,7 @@ mod sys_verify {
         let env = ExecutorEnv::builder()
             .write(&spec)
             .unwrap()
-            .add_assumption(halt_receipt.into())
+            .add_assumption(halt_receipt)
             .build()
             .unwrap();
         get_prover_server(&prover_opts_fast())
@@ -666,7 +666,7 @@ mod sys_verify {
         let env = ExecutorEnv::builder()
             .write(&spec)
             .unwrap()
-            .add_assumption(fault_receipt.into())
+            .add_assumption(fault_receipt)
             .build()
             .unwrap();
         get_prover_server(&prover_opts_fast())

website/api/zkvm/developer-guide/receipts.md

@@ -60,15 +60,13 @@ You can file an issue on [these docs] or the [examples], and we're happy to answ
 
 [zkVM application]: ../zkvm_overview.md
 [receipt]: /terminology#receipt
-[validity proof]: /terminology#proof
+[validity proof]: /terminology#validity-proof
 [execution]: /terminology#execution-trace
 [verified]: /terminology#verify
 [journal]: /terminology#journal
 [seal]: /terminology#seal
 [guest program]: /terminology#guest-program
 [Image ID]: /terminology#image-id
-[Sessions]: /terminology#session
-[segments]: /terminology#segment
 [receipt.verify()]: https://docs.rs/risc0-zkvm/*/risc0_zkvm/struct.Receipt.html#method.verify
 [receipt.journal]: https://docs.rs/risc0-zkvm/*/risc0_zkvm/struct.Receipt.html#structfield.journal
 [verify]: /terminology#verify

website/api_versioned_docs/version-0.18/zkvm/developer-guide/receipts.md

@@ -60,7 +60,7 @@ You can file an issue on [these docs] or the [examples], and we're happy to answ
 
 [zkVM application]: ../
 [receipt]: /terminology#receipt
-[validity proof]: /terminology#proof
+[validity proof]: /terminology#validity-proof
 [execution]: /terminology#execution-trace
 [verified]: /terminology#verify
 [journal]: /terminology#journal

website/api_versioned_docs/version-0.19/zkvm/developer-guide/receipts.md

@@ -60,7 +60,7 @@ You can file an issue on [these docs] or the [examples], and we're happy to answ
 
 [zkVM application]: ../zkvm_overview.md
 [receipt]: /terminology#receipt
-[validity proof]: /terminology#proof
+[validity proof]: /terminology#validity-proof
 [execution]: /terminology#execution-trace
 [verified]: /terminology#verify
 [journal]: /terminology#journal