Skip to content

Commit

Permalink
Distinguish between and avoid use of ExitCode::Fault and SessionLimit (
Browse files Browse the repository at this point in the history
…risc0#1317)

Currently our code does not distinguish between guest-reported/proven
and host-reported/unproven exit codes. This PR addresses this issue by
giving `ExitCode::SystemSplit`, `Fault` and `SessionLimit` distinct exit
codes.

The rv32im circuit does not support exiting with with a verified status
of `SessionLimit` or `Fault`. As a result, these exit codes should be
unused and reserved for future revision of the circuit. This PR
refactors the executor to reflect this and align with the fact that the
prover will never write these statuses to the seal.

Supersedes: risc0#1313
Resolves: risc0#1306

---------

Co-authored-by: Frank Laub <[email protected]>
  • Loading branch information
nategraf and flaub authored Jan 17, 2024
1 parent 2342cc1 commit 3a6cb52
Show file tree
Hide file tree
Showing 10 changed files with 57 additions and 162 deletions.
2 changes: 1 addition & 1 deletion examples/groth16-verifier/groth16/tests/groth16.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// Copyright 2023 RISC Zero, Inc.
// Copyright 2024 RISC Zero, Inc.
//
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
Expand Down
2 changes: 1 addition & 1 deletion examples/groth16-verifier/methods/build.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// Copyright 2023 RISC Zero, Inc.
// Copyright 2024 RISC Zero, Inc.
//
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// Copyright 2023 RISC Zero, Inc.
// Copyright 2024 RISC Zero, Inc.
//
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
Expand Down
2 changes: 1 addition & 1 deletion examples/groth16-verifier/methods/src/lib.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// Copyright 2023 RISC Zero, Inc.
// Copyright 2024 RISC Zero, Inc.
//
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
Expand Down
2 changes: 1 addition & 1 deletion examples/groth16-verifier/src/main.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// Copyright 2023 RISC Zero, Inc.
// Copyright 2024 RISC Zero, Inc.
//
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
Expand Down
6 changes: 3 additions & 3 deletions risc0/build/src/docker.rs
Original file line number Diff line number Diff line change
Expand Up @@ -233,15 +233,15 @@ mod test {
build("../../risc0/zkvm/methods/guest/Cargo.toml");
compare_image_id(
"risc0_zkvm_methods_guest/multi_test",
"7cf76922134ecd86e4ad76508a7069afc3e9727e061c27ec2372bcbc2a5fcec8",
"0cc188f58e21ed5050c997422c6bd509e5c131e88b353f144f97e0f1bdbc9e1d",
);
compare_image_id(
"risc0_zkvm_methods_guest/hello_commit",
"6efc912a71f11d152714774094c94e2a395b70cdeeb87bcb0e740ce8a321e9a4",
"579580ec878a1bd935d111f2b6af196aacb021fd5e57aa6825433de5cbd269dc",
);
compare_image_id(
"risc0_zkvm_methods_guest/slice_io",
"d22f1a689dfc6b4a0fcf93b18d710b420b5416849ec9f6c64f97a56838518aab",
"fa60a80cf1b23d64aa5e6c9eead5eb973a5754f65148252ad71b7f51ca7891b0",
);
}
}
25 changes: 7 additions & 18 deletions risc0/zkvm/src/host/server/exec/executor.rs
Original file line number Diff line number Diff line change
Expand Up @@ -239,8 +239,8 @@ impl<'a> ExecutorImpl<'a> {
self.run_with_callback(|segment| Ok(Box::new(FileSegmentRef::new(&segment, &path)?)))
}

/// Run the executor until [ExitCode::Halted], [ExitCode::Paused], or
/// [ExitCode::Fault] is reached, producing a [Session] as a result.
/// Run the executor until [ExitCode::Halted] or [ExitCode::Paused] is reached, producing a
/// [Session] as a result.
pub fn run_with_callback<F>(&mut self, mut callback: F) -> Result<Session>
where
F: FnMut(Segment) -> Result<Box<dyn SegmentRef>>,
Expand Down Expand Up @@ -285,7 +285,8 @@ impl<'a> ExecutorImpl<'a> {
let segment = Segment::new(
pre_image,
SystemState::from(&post_image),
// NOTE: On the last segment, the output is added outside this loop.
// NOTE: On the last segment, the output is added outside this loop, before
// it is sent to the callback and pushed into the Session object.
None,
faults,
syscalls,
Expand All @@ -304,11 +305,6 @@ impl<'a> ExecutorImpl<'a> {
self.segments.push(segment_ref);
self.split(Some(post_image.into()))?
}
ExitCode::SessionLimit => {
let segment_ref = callback(segment)?;
self.segments.push(segment_ref);
bail!("Session limit exceeded")
}
ExitCode::Paused(inner) => {
tracing::debug!("Paused({inner}): {}", self.segment_cycle);
// Set the pre_image so that the Executor can be run again to resume.
Expand All @@ -322,10 +318,7 @@ impl<'a> ExecutorImpl<'a> {
tracing::debug!("Halted({inner}): {}", self.segment_cycle);
return Ok((exit_code, segment, post_image));
}
ExitCode::Fault => {
tracing::debug!("Fault: {}", self.segment_cycle);
return Ok((exit_code, segment, post_image));
}
_ => bail!("execution reached unexpected exit code {:?}", exit_code),
};
};
}
Expand Down Expand Up @@ -418,7 +411,7 @@ impl<'a> ExecutorImpl<'a> {
pub fn step(&mut self) -> Result<Option<ExitCode>> {
if let Some(limit) = self.env.session_limit {
if self.session_cycle() >= (limit as usize) {
return Ok(Some(ExitCode::SessionLimit));
bail!("Session limit exceeded")
}
}

Expand Down Expand Up @@ -485,11 +478,7 @@ impl<'a> ExecutorImpl<'a> {
err
);
self.monitor.undo()?;
if cfg!(feature = "fault-proof") {
return Ok(Some(ExitCode::Fault));
} else {
bail!("rrs instruction executor failed with {:?}", err);
}
bail!("execution encountered a fault: {:?}", err);
}

if let Some(idx) = hart.last_register_write {
Expand Down
73 changes: 12 additions & 61 deletions risc0/zkvm/src/host/server/exec/tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -440,20 +440,6 @@ mod sys_verify {
session
}

fn exec_fault() -> Session {
let env = ExecutorEnvBuilder::default()
.write(&MultiTestSpec::Fault)
.unwrap()
.build()
.unwrap();
let session = ExecutorImpl::from_elf(env, MULTI_TEST_ELF)
.unwrap()
.run()
.unwrap();
assert_eq!(session.exit_code, ExitCode::Fault);
session
}

#[test]
fn sys_verify() {
let hello_commit_session = exec_hello_commit();
Expand Down Expand Up @@ -536,26 +522,6 @@ mod sys_verify {
}
}

#[test]
fn sys_verify_fault() {
// NOTE: ReceiptClaim for this Session won't differentiate Fault and SystemSplit,
// since these cannot be distinguished from the circuit's point of view.
let fault_session = exec_fault();

let spec = &MultiTestSpec::SysVerify(vec![(MULTI_TEST_ID.into(), Vec::new())]);

let env = ExecutorEnv::builder()
.write(&spec)
.unwrap()
.add_assumption(fault_session.get_claim().unwrap())
.build()
.unwrap();
assert!(ExecutorImpl::from_elf(env, MULTI_TEST_ELF)
.unwrap()
.run()
.is_err());
}

#[test]
fn sys_verify_integrity() {
let hello_commit_session = exec_hello_commit();
Expand Down Expand Up @@ -637,29 +603,6 @@ mod sys_verify {
}
}

#[test]
fn sys_verify_integrity_fault() {
// NOTE: ReceiptClaim for this Session won't differentiate Fault and SystemSplit,
// since these cannot be distinguished from the circuit's point of view.
let fault_session = exec_fault();

let spec = &MultiTestSpec::SysVerifyIntegrity {
claim_words: to_vec(&fault_session.get_claim().unwrap()).unwrap(),
};

let env = ExecutorEnv::builder()
.write(&spec)
.unwrap()
.add_assumption(fault_session.get_claim().unwrap())
.build()
.unwrap();
let session = ExecutorImpl::from_elf(env, MULTI_TEST_ELF)
.unwrap()
.run()
.unwrap();
assert_eq!(session.exit_code, ExitCode::Halted(0));
}

#[test]
fn sys_verify_integrity_pruned_claim() {
let hello_commit_session = exec_hello_commit();
Expand Down Expand Up @@ -853,8 +796,8 @@ fn fault() {
.build()
.unwrap();
let mut exec = ExecutorImpl::from_elf(env, MULTI_TEST_ELF).unwrap();
let session = exec.run().unwrap();
assert_eq!(session.exit_code, ExitCode::Fault);
let err = exec.run().err().unwrap();
assert!(err.to_string().contains("fault"));
}

#[test]
Expand Down Expand Up @@ -970,8 +913,16 @@ fn memory_access() {
Ok(session.exit_code)
}

assert_eq!(access_memory(0x0000_0000).unwrap(), ExitCode::Fault);
assert_eq!(access_memory(0x0C00_0000).unwrap(), ExitCode::Fault);
assert!(access_memory(0x0000_0000)
.err()
.unwrap()
.to_string()
.contains("fault"));
assert!(access_memory(0x0C00_0000)
.err()
.unwrap()
.to_string()
.contains("fault"));
assert_eq!(access_memory(0x0B00_0000).unwrap(), ExitCode::Halted(0));
}

Expand Down
64 changes: 10 additions & 54 deletions risc0/zkvm/src/host/server/prove/tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -232,13 +232,21 @@ fn memory_io() {
assert_eq!(run_memio(&[(POS, 1)]).unwrap(), ExitCode::Halted(0));

// Unaligned write is bad
assert_eq!(run_memio(&[(POS + 1001, 1)]).unwrap(), ExitCode::Fault);
assert!(run_memio(&[(POS + 1001, 1)])
.err()
.unwrap()
.to_string()
.contains("fault"));

// Aligned read is fine
assert_eq!(run_memio(&[(POS, 0)]).unwrap(), ExitCode::Halted(0));

// Unaligned read is bad
assert_eq!(run_memio(&[(POS + 1, 0)]).unwrap(), ExitCode::Fault);
assert!(run_memio(&[(POS + 1, 0)])
.err()
.unwrap()
.to_string()
.contains("fault"));
}

#[test]
Expand Down Expand Up @@ -493,32 +501,6 @@ mod sys_verify {
halt_receipt
}

fn prove_fault() -> Receipt {
let opts = ProverOpts {
hashfn: "sha-256".to_string(),
prove_guest_errors: true,
};

let env = ExecutorEnvBuilder::default()
.write(&MultiTestSpec::Fault)
.unwrap()
.build()
.unwrap();
let fault_receipt = get_prover_server(&opts)
.unwrap()
.prove(env, MULTI_TEST_ELF)
.unwrap();

// Double check that the receipt verifies with the expected image ID and exit code.
fault_receipt
.verify_integrity_with_context(&Default::default())
.unwrap();
let fault_claim = fault_receipt.get_claim().unwrap();
assert_eq!(fault_claim.pre.digest(), MULTI_TEST_ID.into());
assert_eq!(fault_claim.exit_code, ExitCode::Fault);
fault_receipt
}

lazy_static::lazy_static! {
static ref HELLO_COMMIT_RECEIPT: Receipt = prove_hello_commit();
}
Expand Down Expand Up @@ -650,30 +632,4 @@ mod sys_verify {
.verify(MULTI_TEST_ID)
.unwrap();
}

#[test]
fn sys_verify_integrity_fault() {
// Generate a receipt for a execution ending in fault.
// NOTE: This is not really a "proof of fault". Instead it is simply verifying a receipt
// that ended in SystemSplit for which the host claims a fault is about to occur.
let fault_receipt = prove_fault();

let spec = &MultiTestSpec::SysVerifyIntegrity {
claim_words: to_vec(&fault_receipt.get_claim().unwrap()).unwrap(),
};

// Test that proving results in a success execution and unconditional receipt.
let env = ExecutorEnv::builder()
.write(&spec)
.unwrap()
.add_assumption(fault_receipt)
.build()
.unwrap();
get_prover_server(&prover_opts_fast())
.unwrap()
.prove(env, MULTI_TEST_ELF)
.unwrap()
.verify(MULTI_TEST_ID)
.unwrap();
}
}
41 changes: 20 additions & 21 deletions risc0/zkvm/src/receipt_claim.rs
Original file line number Diff line number Diff line change
Expand Up @@ -160,32 +160,34 @@ impl std::error::Error for DecodeError {}
/// Indicates how a Segment or Session's execution has terminated
#[derive(Clone, Copy, Debug, Serialize, Deserialize, PartialEq)]
pub enum ExitCode {
/// This indicates when a system-initiated split has occurred due to the
/// segment limit being exceeded.
SystemSplit,

/// This indicates that the session limit has been reached.
///
/// NOTE: This state is reported by the host prover and results in the same proof as an
/// execution ending in `SystemSplit`.
// TODO(1.0): Refine how we handle the difference between proven and unproven exit codes.
SessionLimit,
/// This indicates normal termination of a program with an interior exit
/// code returned from the guest.
Halted(u32),

/// A user may manually pause a session so that it can be resumed at a later
/// time, along with the user returned code.
Paused(u32),

/// This indicates normal termination of a program with an interior exit
/// code returned from the guest.
Halted(u32),
/// This indicates when a system-initiated split has occurred, stopping execution of a segment.
///
/// Splits are initiated by the host. The most common reason a host will initiate a split is if
/// the number of cycles is approaching the limit for a single segment. The host may also
/// initiate a split if the next instruction will trigger a fault, or if the session limit is
/// reached.
SystemSplit,

/// This indicates termination of a program where the next instruction will
/// fail due to a machine fault (e.g. out of bounds memory read).
///
/// NOTE: This state is reported by the host prover and results in the same proof as an
/// execution ending in `SystemSplit`.
// TODO(1.0): Refine how we handle the difference between proven and unproven exit codes.
/// NOTE: The current version of the RISC Zero zkVM will never exit with an exit code of Fault.
/// This is because the system cannot currently prove that a fault has occured.
Fault,

/// This indicates that the guest exited upon reaching the session limit set by the host.
///
/// NOTE: The current version of the RISC Zero zkVM will never exit with an exit code of SessionLimit.
/// This is because the system cannot currently prove that the session limit as been reached.
SessionLimit,
}

impl ExitCode {
Expand All @@ -194,11 +196,8 @@ impl ExitCode {
ExitCode::Halted(user_exit) => (0, user_exit),
ExitCode::Paused(user_exit) => (1, user_exit),
ExitCode::SystemSplit => (2, 0),
// NOTE: SessionLimit and Fault result in the same exit code set by the rv32im
// circuit. As a result, this conversion is lossy. This factoring results in Fault,
// SessionLimit, and SystemSplit all having the same digest.
ExitCode::SessionLimit => (2, 0),
ExitCode::Fault => (2, 0),
ExitCode::Fault => (2, 1),
ExitCode::SessionLimit => (2, 2),
}
}

Expand Down

0 comments on commit 3a6cb52

Please sign in to comment.