sandbox §13.1–13.2: what a park retains, and what an interval proves about waiting #582
8 changed files with 908 additions and 57 deletions
|
|
@ -409,7 +409,7 @@ A host **MUST NOT** advertise a part at a readiness it does not deliver.
|
|||
|
||||
## 10. Conformance
|
||||
|
||||
A host is **conformant** if it satisfies every **REQUIRED** clause of §1–§7 for the tiers it advertises and round-trips the conformance vectors in [`conformance/`](conformance/). The test obligations are enumerated in [`spec/conformance.md`](spec/conformance.md): canonicality (C1), capability enforcement / deny-by-default (C2), per-device receipt integrity and provenance coupling (C3), attestation signing and verification (C4), tier-minimization (C5), durable run records (C6, §13), environment-manifest ingestion and addressing (C7, §14), content-addressed process control (C8, §5.5), warm-pool idle-energy accounting (C9, §15), fleet merkle aggregation (C10, §16), the enforcement mechanism (C11, §7.9), locality evidence (C12, §7.7), and flow across a run's checkpoints (C13, §5.8). A conforming host **MUST** pass the full pack with no skips for its advertised tiers.
|
||||
A host is **conformant** if it satisfies every **REQUIRED** clause of §1–§7 for the tiers it advertises and round-trips the conformance vectors in [`conformance/`](conformance/). The test obligations are enumerated in [`spec/conformance.md`](spec/conformance.md): canonicality (C1), capability enforcement / deny-by-default (C2), per-device receipt integrity and provenance coupling (C3), attestation signing and verification (C4), tier-minimization (C5), durable run records (C6, §13), environment-manifest ingestion and addressing (C7, §14), content-addressed process control (C8, §5.5), warm-pool idle-energy accounting (C9, §15), fleet merkle aggregation (C10, §16), the enforcement mechanism (C11, §7.9), locality evidence (C12, §7.7), flow across a run's checkpoints (C13, §5.8), what a park retains (C14, §13.1), and what an interval proves about waiting (C15, §13.2). A conforming host **MUST** pass the full pack with no skips for its advertised tiers.
|
||||
|
||||
---
|
||||
|
||||
|
|
@ -425,7 +425,33 @@ A coding agent acts in many steps. A host that exposes a "build" capability **MU
|
|||
|
||||
## 13. Durable run records
|
||||
|
||||
Long-horizon work outlives the sandbox that started it. A host that suspends and resumes units **MUST** keep a **run record**: an append-only hash chain over the run's segments — executed intervals (by attestation address, §7), suspensions (by snapshot content addresses: filesystem root, optional memory image, environment manifest) and resumptions (same snapshot, plus the **idle energy** the retained state drew while parked). The genesis head binds `unit_id` and `grants_id`, so records cannot be spliced across units or grant sets. Resumption **MUST** be refused unless the offered snapshot is content-identical to the one recorded at suspension and the chain verifies from genesis. The run's total cost is its receipts' energy **plus** its idle energy — a parked run is not free, and a conformant host does not pretend it is. Conformance class **C6** exercises the chain, the refusals and the tamper-evidence. See [`spec/durable-runs.md`](spec/durable-runs.md); the reference `sandbox-attest::runrecord` implements it.
|
||||
Long-horizon work outlives the sandbox that started it. A host that suspends and resumes units **MUST** keep a **run record**: an append-only hash chain over the run's segments — executed intervals (by attestation address, §7), suspensions (by snapshot content addresses, in one of the two forms of §13.1, with the environment manifest) and resumptions (same snapshot, plus the **idle energy** the retained state drew while parked). The genesis head binds `unit_id` and `grants_id`, so records cannot be spliced across units or grant sets. Resumption **MUST** be refused unless the offered snapshot is content-identical to the one recorded at suspension and the chain verifies from genesis. The run's total cost is its receipts' energy **plus** its idle energy — a parked run is not free, and a conformant host does not pretend it is. Conformance class **C6** exercises the chain, the refusals and the tamper-evidence. See [`spec/durable-runs.md`](spec/durable-runs.md); the reference `sandbox-attest::runrecord` implements it.
|
||||
|
||||
### 13.1 What a park retains
|
||||
|
||||
A park retains state in one of **two forms**, and the record states which. The first retains **host state**: a filesystem root, and a memory image where the executor suspends resident state (an S5 snapshot). The second retains **nothing on the host** — for a unit whose resumable state is the record of what it has already done, that record *is* the continuation, and the park names only its content address. A snapshot reference **MUST** carry exactly one form. One naming neither, or both, or a transcript beside a resident memory image, **MUST** be refused rather than hashed: a park that cannot say what it retained cannot be resumed against, and a chain that accepted it would attest to an ambiguity.
|
||||
|
||||
The forms differ in two ways that a record must not blur.
|
||||
|
||||
**Where a run may resume.** The preconditions above apply unchanged to both. Because a transcript park names no host state, the content-identity precondition is satisfiable by any host that can fetch the transcript, so such a run resumes wherever its manifest (§14) holds. An image park additionally requires a host able to restore that image. The record therefore states not merely that a run *can* resume but where it can.
|
||||
|
||||
**What waiting costs.** A transcript park runs no computation and holds no resident memory. A host **MUST NOT** record its idle energy as zero on that ground. What it retains is bytes in storage, and storage draws power for as long as the park lasts; `idle_uj` **MUST** account for the retained transcript under the provenance discipline of §6.2 — measured where the host can measure it, labelled as estimated where it cannot. The honest claim for this form is that waiting costs no *computation*, not that waiting is free. A run parked for a week on a transcript is far cheaper than one parked on a volume, and neither is costless; §13's total stands for both.
|
||||
|
||||
Conformance class **C14** exercises both forms, the refusal of a malformed one, cross-form substitution at resume, and the idle accounting of a transcript park.
|
||||
|
||||
### 13.2 What an interval proves about waiting
|
||||
|
||||
§13 prices the wait a run spends **parked**. It says nothing about the wait a run spends **running**, and that is where the larger cost usually hides: an interval that dispatches an outward call and then sits until the result arrives holds its sandbox, and its receipt (§6) charges that sitting as computation. Two runs with identical work and identical receipts can differ by hours of it, and §13 could not tell them apart.
|
||||
|
||||
A host **MAY** therefore account, per executed interval, for the calls it **dispatched** and the results it **resolved**, each by call id. The presence of that account is the marker: an interval carrying no account is not an interval that made no calls — the second is an account of two empty sets, the first is a refusal to say. An interval recorded without an account hashes exactly as it did before this section existed.
|
||||
|
||||
A run is **non-blocking** when every executed interval accounts, and every interval resolves only calls that were **outstanding before it began**. An interval that resolves a call it dispatched itself did not hand off and return: it waited, and that wait is inside its receipt.
|
||||
|
||||
Where a record establishes this, it establishes something a host otherwise can only assert: **no receipt in the run contains a wait for an outward call**, so the run's whole cost of waiting is its idle energy under §13 and §13.1 — a figure the record already carries. A host **MUST NOT** describe a run as non-blocking unless its record establishes it. Where any executed interval does not account, or the run has no accounted interval at all, nothing is established and the claim is unavailable; a property of no intervals is not a property.
|
||||
|
||||
An account that does not add up — a result answering a call never dispatched, a call resolved twice, one id dispatched twice — is a fault in the record and **MUST** be reported as such, distinctly from blocking. The two say different things: one is a run that waited, the other a record that cannot be read.
|
||||
|
||||
Conformance class **C15** exercises the hand-off shape, the blocking interval, each way an account fails to add up, and the refusal to prove anything from an absent account.
|
||||
|
||||
## 14. The environment manifest
|
||||
|
||||
|
|
|
|||
|
|
@ -9,7 +9,7 @@ The v1 wire vectors. Each file is regenerated by `gen_vectors` and verified by t
|
|||
| `receipt.json` | C3 | a CPU+GPU receipt → canonical core (hex), content id, sealed JCR-1 envelope (hex), steward key |
|
||||
| `attestation.json` | C4 | an S5 attestation → JCS bytes, content id, Ed25519 signature (hex), supervisor key |
|
||||
| `tier.json` | C5 | grant set + isolation flags → required tier (S0–S7) |
|
||||
| `durable.json` | C6/C7/C10 | a run-record trace → head id; a devcontainer → manifest id; a fleet → merkle root (all `b3:`) |
|
||||
| `durable.json` | C6/C7/C10/C14/C15 | a run-record trace → head id, once parked on host state, once on a transcript (§13.1), and once with each interval accounting for its outward calls (§13.2); a devcontainer → manifest id; a fleet → merkle root (all `b3:`) |
|
||||
| `negative.json` | C-neg | malformed receipts + attestations a conformant host MUST reject |
|
||||
| `confidential.json` | C-tee | SEV-SNP report verify (valid + negatives) + audit-chain check |
|
||||
| `flow.json` | C13 | a run's calls in order → the origins each read adds, and whether each sink may be reached |
|
||||
|
|
|
|||
|
|
@ -2,5 +2,7 @@
|
|||
"devcontainer": "{\"image\":\"ghcr.io/acme/builder@sha256:0011aabb\",\"features\":{\"ghcr.io/devcontainers/features/rust:1\":{\"profile\":\"minimal\"}},\"containerEnv\":{\"B\":\"2\",\"A\":\"1\"}}",
|
||||
"expect_manifest_id": "b3:9sgqzur-bEpnB-3PNwQd0jMKtnzG6FOBSclU_BhdgEo",
|
||||
"expect_runrecord_head": "b3:mk3hGn1kCXPuMQNPGQxHsqu8TxsnGVPBTBcgcxrHYlA",
|
||||
"expect_transcript_head": "b3:XKKBf5hYdrSZoJN-GHLdZ_Bbg7CjN6P4DCRVD17GyUs",
|
||||
"expect_accounted_head": "b3:FINebhSRpv_1ncmpE3PaRG85MR8Ri1fDy4lmR1yI2DA",
|
||||
"expect_fleet_root": "b3:NZtu05H3fp7ZLOUJPjTE_-pYeIT25mTsZphfqGSLkis"
|
||||
}
|
||||
|
|
|
|||
|
|
@ -18,27 +18,129 @@
|
|||
//! true cost of the run, not just the cost of its active intervals.
|
||||
|
||||
use sandbox_schema::ContentId;
|
||||
use std::collections::BTreeSet;
|
||||
use serde::{Deserialize, Serialize};
|
||||
|
||||
/// Content addresses of the state retained at suspension.
|
||||
///
|
||||
/// A park retains state in one of two forms, and exactly one (§13.1):
|
||||
/// **host state** (`fs_root`, optionally `memory`), or a **transcript** whose
|
||||
/// content address is the run's continuation. A value carrying neither, or
|
||||
/// both, is malformed and is refused rather than hashed — see [`SnapshotKind`].
|
||||
#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
|
||||
pub struct SnapshotRef {
|
||||
/// Root of the unit's filesystem snapshot (content-addressed).
|
||||
pub fs_root: ContentId,
|
||||
/// Root of the unit's filesystem snapshot (content-addressed). Absent on
|
||||
/// a transcript continuation, where no host state is retained at all.
|
||||
#[serde(default, skip_serializing_if = "Option::is_none")]
|
||||
pub fs_root: Option<ContentId>,
|
||||
/// Memory image, if the executor suspends with resident state (S5
|
||||
/// microVM snapshot); pure filesystem suspends leave this `None`.
|
||||
#[serde(default, skip_serializing_if = "Option::is_none")]
|
||||
pub memory: Option<ContentId>,
|
||||
/// The run's transcript, content-addressed. Present exactly when no host
|
||||
/// state is retained: for a unit whose resumable state is the record of
|
||||
/// what it has done, the transcript *is* the continuation, so a park
|
||||
/// needs no filesystem and no memory image.
|
||||
#[serde(default, skip_serializing_if = "Option::is_none")]
|
||||
pub transcript: Option<ContentId>,
|
||||
/// Hash of the environment manifest the run was created from; resume on
|
||||
/// a host that cannot reproduce this manifest must be refused.
|
||||
pub manifest: ContentId,
|
||||
}
|
||||
|
||||
/// Which of the two forms of retained state a [`SnapshotRef`] carries.
|
||||
///
|
||||
/// The distinction is not cosmetic. An image park can only be resumed by a
|
||||
/// host able to restore that image; a transcript park names no host state, so
|
||||
/// any host satisfying the manifest can resume it. And their idle draws differ
|
||||
/// in kind: an image park holds a volume and possibly memory, a transcript
|
||||
/// park holds bytes in storage — less, never nothing.
|
||||
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
|
||||
pub enum SnapshotKind<'a> {
|
||||
/// Host state was retained: a filesystem root, optionally a memory image.
|
||||
Image {
|
||||
fs_root: &'a ContentId,
|
||||
memory: Option<&'a ContentId>,
|
||||
},
|
||||
/// No host state was retained; the continuation is the transcript.
|
||||
Transcript { transcript: &'a ContentId },
|
||||
}
|
||||
|
||||
impl SnapshotRef {
|
||||
/// A park that retained host state.
|
||||
pub fn image(fs_root: ContentId, memory: Option<ContentId>, manifest: ContentId) -> Self {
|
||||
SnapshotRef { fs_root: Some(fs_root), memory, transcript: None, manifest }
|
||||
}
|
||||
|
||||
/// A park that retained only the run's transcript (§13.1).
|
||||
pub fn transcript(transcript: ContentId, manifest: ContentId) -> Self {
|
||||
SnapshotRef { fs_root: None, memory: None, transcript: Some(transcript), manifest }
|
||||
}
|
||||
|
||||
/// Which form this is, or `None` if it is neither or both. Callers refuse
|
||||
/// on `None`; nothing malformed reaches the chain.
|
||||
pub fn kind(&self) -> Option<SnapshotKind<'_>> {
|
||||
match (&self.fs_root, &self.transcript, &self.memory) {
|
||||
(Some(fs_root), None, memory) => {
|
||||
Some(SnapshotKind::Image { fs_root, memory: memory.as_ref() })
|
||||
}
|
||||
// A memory image is host state, so it cannot accompany a
|
||||
// transcript: that would be a park claiming to retain nothing
|
||||
// while holding a resident image.
|
||||
(None, Some(transcript), None) => Some(SnapshotKind::Transcript { transcript }),
|
||||
_ => None,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// What an executed segment did with the calls it made outside itself.
|
||||
///
|
||||
/// Presence is the honesty marker (§13.2). `None` on a segment means the host
|
||||
/// did not account for its outward calls, which is **not** the same as a
|
||||
/// segment that made none — that is `Some` with two empty sets. Absent
|
||||
/// accounting proves nothing, and a host may not claim from it.
|
||||
#[derive(Clone, Debug, Default, PartialEq, Eq, Serialize, Deserialize)]
|
||||
pub struct CallAccount {
|
||||
/// Calls this segment handed off, by call id. The segment ends without
|
||||
/// their results.
|
||||
#[serde(default, skip_serializing_if = "Vec::is_empty")]
|
||||
pub dispatched: Vec<ContentId>,
|
||||
/// Results this segment consumed, by the id of the call each answers.
|
||||
#[serde(default, skip_serializing_if = "Vec::is_empty")]
|
||||
pub resolved: Vec<ContentId>,
|
||||
}
|
||||
|
||||
/// What a run's call accounting proves about where it waited (§13.2).
|
||||
#[derive(Clone, Debug, PartialEq, Eq)]
|
||||
pub enum WaitProof {
|
||||
/// Nothing is proved. Either some executed segment did not account for
|
||||
/// its outward calls, or the run has no accounted executed segment at
|
||||
/// all. A claim resting on this is a claim about an empty domain.
|
||||
Unproved,
|
||||
/// A segment consumed the result of a call it had itself dispatched, so
|
||||
/// it waited inside an executed interval and that wait is inside the
|
||||
/// interval's receipt.
|
||||
Blocked { segment: usize },
|
||||
/// The account does not add up: a result answering a call never
|
||||
/// dispatched, a call resolved twice, or one id dispatched twice.
|
||||
Malformed { segment: usize },
|
||||
/// Every segment resolved only calls that were outstanding before it
|
||||
/// began. No receipt in this run contains a wait for an outward call.
|
||||
NonBlocking,
|
||||
}
|
||||
|
||||
/// One link in a run record.
|
||||
#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
|
||||
pub enum Segment {
|
||||
/// An executed interval, by the content address of its attestation
|
||||
/// (which binds the interval's receipt, journal root and outcome).
|
||||
Executed { attestation_id: ContentId },
|
||||
Executed {
|
||||
attestation_id: ContentId,
|
||||
/// What the interval did with its outward calls, where the host
|
||||
/// accounts for them (§13.2).
|
||||
#[serde(default, skip_serializing_if = "Option::is_none")]
|
||||
calls: Option<CallAccount>,
|
||||
},
|
||||
/// A suspension: what was retained.
|
||||
Suspended { snapshot: SnapshotRef },
|
||||
/// A resumption: what was restored, and what the park cost.
|
||||
|
|
@ -53,38 +155,73 @@ pub enum Segment {
|
|||
}
|
||||
|
||||
impl Segment {
|
||||
/// Canonical bytes folded into the chain head.
|
||||
fn chain_bytes(&self) -> Vec<u8> {
|
||||
/// Canonical bytes folded into the chain head, or `None` if the segment
|
||||
/// carries a malformed snapshot. It is not a panic and not a silent
|
||||
/// encoding: a segment that cannot be canonicalized cannot be appended
|
||||
/// and cannot verify.
|
||||
fn chain_bytes(&self) -> Option<Vec<u8>> {
|
||||
let mut out = Vec::new();
|
||||
match self {
|
||||
Segment::Executed { attestation_id } => {
|
||||
Segment::Executed { attestation_id, calls } => {
|
||||
out.extend_from_slice(b"exec/1");
|
||||
out.extend_from_slice(attestation_id.0.as_bytes());
|
||||
// Folded only when the host accounted, so a segment without
|
||||
// an account hashes exactly as it did before §13.2 existed.
|
||||
// Each set is length-prefixed, so no id boundary is
|
||||
// ambiguous and no two accounts share bytes.
|
||||
if let Some(c) = calls {
|
||||
out.extend_from_slice(b"calls/1");
|
||||
push_ids(&mut out, &c.dispatched);
|
||||
push_ids(&mut out, &c.resolved);
|
||||
}
|
||||
}
|
||||
Segment::Suspended { snapshot } => {
|
||||
out.extend_from_slice(b"susp/1");
|
||||
push_snapshot(&mut out, snapshot);
|
||||
push_snapshot(&mut out, snapshot)?;
|
||||
}
|
||||
Segment::Resumed { snapshot, idle_uj } => {
|
||||
out.extend_from_slice(b"resm/1");
|
||||
push_snapshot(&mut out, snapshot);
|
||||
push_snapshot(&mut out, snapshot)?;
|
||||
out.extend_from_slice(&idle_uj.to_be_bytes());
|
||||
}
|
||||
}
|
||||
out
|
||||
Some(out)
|
||||
}
|
||||
}
|
||||
|
||||
fn push_snapshot(out: &mut Vec<u8>, s: &SnapshotRef) {
|
||||
out.extend_from_slice(s.fs_root.0.as_bytes());
|
||||
match &s.memory {
|
||||
Some(m) => {
|
||||
out.push(1);
|
||||
out.extend_from_slice(m.0.as_bytes());
|
||||
/// A set of call ids, length-prefixed so no id boundary is ambiguous.
|
||||
fn push_ids(out: &mut Vec<u8>, ids: &[ContentId]) {
|
||||
out.extend_from_slice(&(ids.len() as u64).to_be_bytes());
|
||||
for id in ids {
|
||||
out.extend_from_slice(id.0.as_bytes());
|
||||
}
|
||||
}
|
||||
|
||||
/// The image form's bytes are exactly what they were before the transcript
|
||||
/// form existed — `fs_root ‖ (1 ‖ memory | 0) ‖ manifest` — so every record
|
||||
/// and every conformance address written under the single-form chain still
|
||||
/// recomputes. The transcript form is introduced under its own tag, which
|
||||
/// cannot collide with a `ContentId`'s first bytes at the same offset because
|
||||
/// the two forms are never both reachable for one snapshot.
|
||||
fn push_snapshot(out: &mut Vec<u8>, s: &SnapshotRef) -> Option<()> {
|
||||
match s.kind()? {
|
||||
SnapshotKind::Image { fs_root, memory } => {
|
||||
out.extend_from_slice(fs_root.0.as_bytes());
|
||||
match memory {
|
||||
Some(m) => {
|
||||
out.push(1);
|
||||
out.extend_from_slice(m.0.as_bytes());
|
||||
}
|
||||
None => out.push(0),
|
||||
}
|
||||
}
|
||||
SnapshotKind::Transcript { transcript } => {
|
||||
out.extend_from_slice(b"cont/1");
|
||||
out.extend_from_slice(transcript.0.as_bytes());
|
||||
}
|
||||
None => out.push(0),
|
||||
}
|
||||
out.extend_from_slice(s.manifest.0.as_bytes());
|
||||
Some(())
|
||||
}
|
||||
|
||||
/// Why a segment could not be appended.
|
||||
|
|
@ -95,6 +232,9 @@ pub enum RunRecordError {
|
|||
WrongPhase(&'static str),
|
||||
/// The snapshot offered for resume is not the one recorded at suspend.
|
||||
SnapshotMismatch,
|
||||
/// The snapshot names neither host state nor a transcript, or names both
|
||||
/// (§13.1). A park must say what it retained, once.
|
||||
MalformedSnapshot,
|
||||
/// The run has already reached a terminal segment.
|
||||
Closed,
|
||||
}
|
||||
|
|
@ -142,13 +282,14 @@ impl RunRecord {
|
|||
ContentId::of_bytes(&self.head)
|
||||
}
|
||||
|
||||
fn fold(&mut self, seg: Segment) -> ContentId {
|
||||
fn fold(&mut self, seg: Segment) -> Result<ContentId, RunRecordError> {
|
||||
let bytes = seg.chain_bytes().ok_or(RunRecordError::MalformedSnapshot)?;
|
||||
let mut h = blake3::Hasher::new();
|
||||
h.update(&self.head);
|
||||
h.update(&seg.chain_bytes());
|
||||
h.update(&bytes);
|
||||
self.head = *h.finalize().as_bytes();
|
||||
self.segments.push(seg);
|
||||
self.head_id()
|
||||
Ok(self.head_id())
|
||||
}
|
||||
|
||||
/// Whether the run is currently parked (last segment is a suspension).
|
||||
|
|
@ -167,7 +308,72 @@ impl RunRecord {
|
|||
if self.is_parked() {
|
||||
return Err(RunRecordError::WrongPhase("execution while parked"));
|
||||
}
|
||||
Ok(self.fold(Segment::Executed { attestation_id: attestation_id.clone() }))
|
||||
self.fold(Segment::Executed { attestation_id: attestation_id.clone(), calls: None })
|
||||
}
|
||||
|
||||
/// Record an executed interval together with what it did about its
|
||||
/// outward calls (§13.2). An interval recorded this way can be reasoned
|
||||
/// about by [`RunRecord::wait_proof`]; one recorded by
|
||||
/// [`RunRecord::record_execution`] cannot, and makes the whole run's
|
||||
/// proof `Unproved` — an absent account is not an empty one.
|
||||
pub fn record_execution_accounted(
|
||||
&mut self,
|
||||
attestation_id: &ContentId,
|
||||
calls: CallAccount,
|
||||
) -> Result<ContentId, RunRecordError> {
|
||||
if self.closed {
|
||||
return Err(RunRecordError::Closed);
|
||||
}
|
||||
if self.is_parked() {
|
||||
return Err(RunRecordError::WrongPhase("execution while parked"));
|
||||
}
|
||||
self.fold(Segment::Executed {
|
||||
attestation_id: attestation_id.clone(),
|
||||
calls: Some(calls),
|
||||
})
|
||||
}
|
||||
|
||||
/// What this record proves about where the run waited (§13.2).
|
||||
///
|
||||
/// Walked in order, holding the calls outstanding at each segment's
|
||||
/// start. A segment may resolve only those. One that resolves a call it
|
||||
/// dispatched itself did not hand off and return — it waited, inside an
|
||||
/// executed interval, and that wait is inside the interval's receipt.
|
||||
pub fn wait_proof(&self) -> WaitProof {
|
||||
let mut outstanding: BTreeSet<&str> = BTreeSet::new();
|
||||
let mut ever_dispatched: BTreeSet<&str> = BTreeSet::new();
|
||||
let mut accounted = 0usize;
|
||||
for (i, seg) in self.segments.iter().enumerate() {
|
||||
let Segment::Executed { calls, .. } = seg else { continue };
|
||||
let Some(c) = calls else { return WaitProof::Unproved };
|
||||
accounted += 1;
|
||||
let mine: BTreeSet<&str> = c.dispatched.iter().map(|d| d.0.as_str()).collect();
|
||||
for r in &c.resolved {
|
||||
let id = r.0.as_str();
|
||||
if !outstanding.remove(id) {
|
||||
// Resolving one of its own dispatches is the blocking
|
||||
// case; anything else is an account that does not add up.
|
||||
return if mine.contains(id) {
|
||||
WaitProof::Blocked { segment: i }
|
||||
} else {
|
||||
WaitProof::Malformed { segment: i }
|
||||
};
|
||||
}
|
||||
}
|
||||
for d in &c.dispatched {
|
||||
let id = d.0.as_str();
|
||||
if !ever_dispatched.insert(id) {
|
||||
return WaitProof::Malformed { segment: i };
|
||||
}
|
||||
outstanding.insert(id);
|
||||
}
|
||||
}
|
||||
// A run with nothing accounted proves nothing, rather than proving a
|
||||
// property of no segments.
|
||||
if accounted == 0 {
|
||||
return WaitProof::Unproved;
|
||||
}
|
||||
WaitProof::NonBlocking
|
||||
}
|
||||
|
||||
/// Park the run, recording what was retained.
|
||||
|
|
@ -178,7 +384,7 @@ impl RunRecord {
|
|||
if self.is_parked() {
|
||||
return Err(RunRecordError::WrongPhase("suspend while parked"));
|
||||
}
|
||||
Ok(self.fold(Segment::Suspended { snapshot }))
|
||||
self.fold(Segment::Suspended { snapshot })
|
||||
}
|
||||
|
||||
/// Resume from a park. The offered snapshot must be content-identical to
|
||||
|
|
@ -200,8 +406,9 @@ impl RunRecord {
|
|||
}
|
||||
_ => return Err(RunRecordError::WrongPhase("resume while not parked")),
|
||||
}
|
||||
let head = self.fold(Segment::Resumed { snapshot, idle_uj })?;
|
||||
self.idle_uj += idle_uj;
|
||||
Ok(self.fold(Segment::Resumed { snapshot, idle_uj }))
|
||||
Ok(head)
|
||||
}
|
||||
|
||||
/// Close the record; nothing may be appended afterwards. A parked run
|
||||
|
|
@ -260,9 +467,12 @@ impl RunRecord {
|
|||
_ => return false,
|
||||
},
|
||||
}
|
||||
let Some(bytes) = seg.chain_bytes() else {
|
||||
return false;
|
||||
};
|
||||
let mut hh = blake3::Hasher::new();
|
||||
hh.update(&head);
|
||||
hh.update(&seg.chain_bytes());
|
||||
hh.update(&bytes);
|
||||
head = *hh.finalize().as_bytes();
|
||||
}
|
||||
head == self.head && idle == self.idle_uj
|
||||
|
|
@ -274,11 +484,15 @@ mod tests {
|
|||
use super::*;
|
||||
|
||||
fn snap(tag: &[u8]) -> SnapshotRef {
|
||||
SnapshotRef {
|
||||
fs_root: ContentId::of_bytes(tag),
|
||||
memory: Some(ContentId::of_bytes(b"mem")),
|
||||
manifest: ContentId::of_bytes(b"manifest"),
|
||||
}
|
||||
SnapshotRef::image(
|
||||
ContentId::of_bytes(tag),
|
||||
Some(ContentId::of_bytes(b"mem")),
|
||||
ContentId::of_bytes(b"manifest"),
|
||||
)
|
||||
}
|
||||
|
||||
fn tsnap(tag: &[u8]) -> SnapshotRef {
|
||||
SnapshotRef::transcript(ContentId::of_bytes(tag), ContentId::of_bytes(b"manifest"))
|
||||
}
|
||||
|
||||
#[test]
|
||||
|
|
@ -326,7 +540,7 @@ mod tests {
|
|||
// Rewrite the recorded snapshot after the fact ⇒ chain breaks.
|
||||
let mut forged = r.clone();
|
||||
if let Some(Segment::Suspended { snapshot }) = forged.segments.get_mut(1) {
|
||||
snapshot.fs_root = ContentId::of_bytes(b"fs-FORK");
|
||||
snapshot.fs_root = Some(ContentId::of_bytes(b"fs-FORK"));
|
||||
}
|
||||
assert!(!forged.verify());
|
||||
// Removing a segment breaks it too.
|
||||
|
|
@ -335,6 +549,246 @@ mod tests {
|
|||
assert!(!truncated.verify());
|
||||
}
|
||||
|
||||
/// The image form must hash exactly as it did before the transcript form
|
||||
/// existed, or every record and conformance address written under the
|
||||
/// single-form chain stops recomputing. The layout is pinned here against
|
||||
/// bytes written out by hand, so it is checked without reference to the
|
||||
/// code that produced it.
|
||||
#[test]
|
||||
fn the_image_forms_bytes_are_what_they_always_were() {
|
||||
let fs = ContentId::of_bytes(b"fs-1");
|
||||
let mem = ContentId::of_bytes(b"mem");
|
||||
let man = ContentId::of_bytes(b"manifest");
|
||||
|
||||
let mut want = Vec::new();
|
||||
want.extend_from_slice(fs.0.as_bytes());
|
||||
want.push(1);
|
||||
want.extend_from_slice(mem.0.as_bytes());
|
||||
want.extend_from_slice(man.0.as_bytes());
|
||||
let mut got = Vec::new();
|
||||
push_snapshot(&mut got, &SnapshotRef::image(fs.clone(), Some(mem), man.clone())).unwrap();
|
||||
assert_eq!(got, want, "an image park with a memory image");
|
||||
|
||||
let mut want_nomem = Vec::new();
|
||||
want_nomem.extend_from_slice(fs.0.as_bytes());
|
||||
want_nomem.push(0);
|
||||
want_nomem.extend_from_slice(man.0.as_bytes());
|
||||
let mut got_nomem = Vec::new();
|
||||
push_snapshot(&mut got_nomem, &SnapshotRef::image(fs, None, man)).unwrap();
|
||||
assert_eq!(got_nomem, want_nomem, "an image park with no memory image");
|
||||
}
|
||||
|
||||
/// A transcript park is a full lifecycle, not a special case: it chains,
|
||||
/// it verifies, and its park is priced.
|
||||
#[test]
|
||||
fn a_transcript_park_chains_and_is_priced() {
|
||||
let mut r = RunRecord::open(ContentId::of_bytes(b"unit"), ContentId::of_bytes(b"grants"));
|
||||
r.record_execution(&ContentId::of_bytes(b"att-1")).unwrap();
|
||||
r.suspend(tsnap(b"turns-1")).unwrap();
|
||||
assert!(r.is_parked());
|
||||
// Nothing is resident, but the transcript sits in storage: a park that
|
||||
// retains bytes is cheaper than one that retains a volume, never free.
|
||||
r.resume(tsnap(b"turns-1"), 42).unwrap();
|
||||
r.record_execution(&ContentId::of_bytes(b"att-2")).unwrap();
|
||||
assert_eq!(r.executions(), 2);
|
||||
assert_eq!(r.idle_uj(), 42);
|
||||
assert!(r.verify());
|
||||
}
|
||||
|
||||
/// The two forms are different parks even when the inner address is the
|
||||
/// same, so one cannot be substituted for the other.
|
||||
#[test]
|
||||
fn the_two_forms_never_collide() {
|
||||
let same = ContentId::of_bytes(b"same");
|
||||
let man = ContentId::of_bytes(b"manifest");
|
||||
let image = SnapshotRef::image(same.clone(), None, man.clone());
|
||||
let transcript = SnapshotRef::transcript(same, man);
|
||||
|
||||
let mut a = Vec::new();
|
||||
push_snapshot(&mut a, &image).unwrap();
|
||||
let mut b = Vec::new();
|
||||
push_snapshot(&mut b, &transcript).unwrap();
|
||||
assert_ne!(a, b);
|
||||
|
||||
// And a resume must offer the form that was parked.
|
||||
let mut r = RunRecord::open(ContentId::of_bytes(b"unit"), ContentId::of_bytes(b"grants"));
|
||||
r.suspend(image).unwrap();
|
||||
assert_eq!(r.resume(transcript, 0), Err(RunRecordError::SnapshotMismatch));
|
||||
}
|
||||
|
||||
/// A park must say what it retained, exactly once. Neither, both, or a
|
||||
/// transcript beside a resident memory image are refused before anything
|
||||
/// is hashed — and cannot be smuggled in by editing a record afterwards.
|
||||
#[test]
|
||||
fn a_malformed_snapshot_is_refused_and_never_verifies() {
|
||||
let man = ContentId::of_bytes(b"manifest");
|
||||
let bad = [
|
||||
SnapshotRef { fs_root: None, memory: None, transcript: None, manifest: man.clone() },
|
||||
SnapshotRef {
|
||||
fs_root: Some(ContentId::of_bytes(b"fs")),
|
||||
memory: None,
|
||||
transcript: Some(ContentId::of_bytes(b"turns")),
|
||||
manifest: man.clone(),
|
||||
},
|
||||
SnapshotRef {
|
||||
fs_root: None,
|
||||
memory: Some(ContentId::of_bytes(b"mem")),
|
||||
transcript: Some(ContentId::of_bytes(b"turns")),
|
||||
manifest: man,
|
||||
},
|
||||
];
|
||||
for s in &bad {
|
||||
assert_eq!(s.kind(), None);
|
||||
let mut r =
|
||||
RunRecord::open(ContentId::of_bytes(b"unit"), ContentId::of_bytes(b"grants"));
|
||||
assert_eq!(r.suspend(s.clone()), Err(RunRecordError::MalformedSnapshot));
|
||||
// The refusal left no segment behind.
|
||||
assert_eq!(r.segments().len(), 0);
|
||||
assert!(r.verify());
|
||||
}
|
||||
|
||||
// Forged in after the fact, it fails verification rather than hashing.
|
||||
let mut r = RunRecord::open(ContentId::of_bytes(b"unit"), ContentId::of_bytes(b"grants"));
|
||||
r.suspend(tsnap(b"turns-1")).unwrap();
|
||||
r.resume(tsnap(b"turns-1"), 7).unwrap();
|
||||
assert!(r.verify());
|
||||
let mut forged = r.clone();
|
||||
if let Some(Segment::Suspended { snapshot }) = forged.segments.get_mut(0) {
|
||||
snapshot.fs_root = Some(ContentId::of_bytes(b"fs"));
|
||||
}
|
||||
assert_eq!(forged.segments()[0], {
|
||||
let mut s = tsnap(b"turns-1");
|
||||
s.fs_root = Some(ContentId::of_bytes(b"fs"));
|
||||
Segment::Suspended { snapshot: s }
|
||||
});
|
||||
assert!(!forged.verify());
|
||||
}
|
||||
|
||||
/// A refused resume must not advance the idle total: a park that was never
|
||||
/// recorded has no energy to attribute.
|
||||
#[test]
|
||||
fn a_refused_resume_leaves_the_idle_total_alone() {
|
||||
let mut r = RunRecord::open(ContentId::of_bytes(b"unit"), ContentId::of_bytes(b"grants"));
|
||||
r.suspend(tsnap(b"turns-1")).unwrap();
|
||||
assert_eq!(r.resume(tsnap(b"turns-OTHER"), 1_000), Err(RunRecordError::SnapshotMismatch));
|
||||
assert_eq!(r.idle_uj(), 0);
|
||||
r.resume(tsnap(b"turns-1"), 11).unwrap();
|
||||
assert_eq!(r.idle_uj(), 11);
|
||||
assert!(r.verify());
|
||||
}
|
||||
|
||||
fn acct(dispatched: &[&[u8]], resolved: &[&[u8]]) -> CallAccount {
|
||||
CallAccount {
|
||||
dispatched: dispatched.iter().map(|d| ContentId::of_bytes(d)).collect(),
|
||||
resolved: resolved.iter().map(|r| ContentId::of_bytes(r)).collect(),
|
||||
}
|
||||
}
|
||||
|
||||
/// An interval recorded without an account must hash exactly as it did
|
||||
/// before §13.2 existed, or every head written before it stops
|
||||
/// recomputing. Pinned against bytes written out by hand.
|
||||
#[test]
|
||||
fn an_unaccounted_interval_hashes_as_it_always_did() {
|
||||
let att = ContentId::of_bytes(b"att-1");
|
||||
let mut want = Vec::new();
|
||||
want.extend_from_slice(b"exec/1");
|
||||
want.extend_from_slice(att.0.as_bytes());
|
||||
let got = Segment::Executed { attestation_id: att, calls: None }.chain_bytes().unwrap();
|
||||
assert_eq!(got, want);
|
||||
}
|
||||
|
||||
/// Accounting for no calls is a different statement from not accounting,
|
||||
/// so the two must not hash alike — otherwise the honesty marker is only
|
||||
/// a comment.
|
||||
#[test]
|
||||
fn an_empty_account_is_not_an_absent_one() {
|
||||
let att = ContentId::of_bytes(b"att-1");
|
||||
let absent = Segment::Executed { attestation_id: att.clone(), calls: None };
|
||||
let empty =
|
||||
Segment::Executed { attestation_id: att, calls: Some(CallAccount::default()) };
|
||||
assert_ne!(absent.chain_bytes(), empty.chain_bytes());
|
||||
}
|
||||
|
||||
/// The shape a hand-off takes: dispatch, end the interval, park, and
|
||||
/// resolve in a later one. Nothing waited inside a receipt.
|
||||
#[test]
|
||||
fn a_hand_off_resolved_later_is_non_blocking() {
|
||||
let mut r = RunRecord::open(ContentId::of_bytes(b"unit"), ContentId::of_bytes(b"grants"));
|
||||
r.record_execution_accounted(&ContentId::of_bytes(b"att-1"), acct(&[b"call-1"], &[]))
|
||||
.unwrap();
|
||||
r.suspend(tsnap(b"turns-1")).unwrap();
|
||||
r.resume(tsnap(b"turns-1"), 3).unwrap();
|
||||
r.record_execution_accounted(&ContentId::of_bytes(b"att-2"), acct(&[], &[b"call-1"]))
|
||||
.unwrap();
|
||||
assert_eq!(r.wait_proof(), WaitProof::NonBlocking);
|
||||
assert!(r.verify());
|
||||
}
|
||||
|
||||
/// The fault the class exists to catch: an interval that dispatched a
|
||||
/// call and then consumed its own result sat waiting, and its receipt
|
||||
/// carries that wait as computation.
|
||||
#[test]
|
||||
fn resolving_its_own_dispatch_is_blocking() {
|
||||
let mut r = RunRecord::open(ContentId::of_bytes(b"unit"), ContentId::of_bytes(b"grants"));
|
||||
r.record_execution_accounted(&ContentId::of_bytes(b"att-1"), acct(&[b"c"], &[]))
|
||||
.unwrap();
|
||||
r.record_execution_accounted(
|
||||
&ContentId::of_bytes(b"att-2"),
|
||||
acct(&[b"c2"], &[b"c2"]),
|
||||
)
|
||||
.unwrap();
|
||||
assert_eq!(r.wait_proof(), WaitProof::Blocked { segment: 1 });
|
||||
}
|
||||
|
||||
/// An absent account proves nothing, and neither does a run with nothing
|
||||
/// accounted at all: a property of no segments is not a property.
|
||||
#[test]
|
||||
fn an_absent_account_proves_nothing() {
|
||||
let mut mixed =
|
||||
RunRecord::open(ContentId::of_bytes(b"unit"), ContentId::of_bytes(b"grants"));
|
||||
mixed
|
||||
.record_execution_accounted(&ContentId::of_bytes(b"att-1"), acct(&[], &[]))
|
||||
.unwrap();
|
||||
mixed.record_execution(&ContentId::of_bytes(b"att-2")).unwrap();
|
||||
assert_eq!(mixed.wait_proof(), WaitProof::Unproved);
|
||||
|
||||
let empty = RunRecord::open(ContentId::of_bytes(b"unit"), ContentId::of_bytes(b"grants"));
|
||||
assert_eq!(empty.wait_proof(), WaitProof::Unproved);
|
||||
|
||||
let mut parked_only =
|
||||
RunRecord::open(ContentId::of_bytes(b"unit"), ContentId::of_bytes(b"grants"));
|
||||
parked_only.suspend(tsnap(b"turns-1")).unwrap();
|
||||
assert_eq!(parked_only.wait_proof(), WaitProof::Unproved);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn an_account_that_does_not_add_up_is_malformed() {
|
||||
// A result answering a call never dispatched.
|
||||
let mut a = RunRecord::open(ContentId::of_bytes(b"unit"), ContentId::of_bytes(b"grants"));
|
||||
a.record_execution_accounted(&ContentId::of_bytes(b"att"), acct(&[], &[b"ghost"]))
|
||||
.unwrap();
|
||||
assert_eq!(a.wait_proof(), WaitProof::Malformed { segment: 0 });
|
||||
|
||||
// The same call resolved twice.
|
||||
let mut b = RunRecord::open(ContentId::of_bytes(b"unit"), ContentId::of_bytes(b"grants"));
|
||||
b.record_execution_accounted(&ContentId::of_bytes(b"att-1"), acct(&[b"c"], &[]))
|
||||
.unwrap();
|
||||
b.record_execution_accounted(&ContentId::of_bytes(b"att-2"), acct(&[], &[b"c"]))
|
||||
.unwrap();
|
||||
b.record_execution_accounted(&ContentId::of_bytes(b"att-3"), acct(&[], &[b"c"]))
|
||||
.unwrap();
|
||||
assert_eq!(b.wait_proof(), WaitProof::Malformed { segment: 2 });
|
||||
|
||||
// One id dispatched twice: two calls cannot share an identity, or a
|
||||
// result cannot be matched to the call it answers.
|
||||
let mut c = RunRecord::open(ContentId::of_bytes(b"unit"), ContentId::of_bytes(b"grants"));
|
||||
c.record_execution_accounted(&ContentId::of_bytes(b"att-1"), acct(&[b"c"], &[]))
|
||||
.unwrap();
|
||||
c.record_execution_accounted(&ContentId::of_bytes(b"att-2"), acct(&[b"c"], &[]))
|
||||
.unwrap();
|
||||
assert_eq!(c.wait_proof(), WaitProof::Malformed { segment: 1 });
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn genesis_binds_unit_and_grants() {
|
||||
let a = RunRecord::open(ContentId::of_bytes(b"unit-a"), ContentId::of_bytes(b"grants"));
|
||||
|
|
|
|||
|
|
@ -28,7 +28,9 @@ use sandbox_attest::fleet::{FleetItem, FleetRecord};
|
|||
use sandbox_attest::Mechanism;
|
||||
use sandbox_attest::manifest::{EnvironmentManifest, ManifestError};
|
||||
use sandbox_attest::warmpool::WarmPool;
|
||||
use sandbox_attest::runrecord::{RunRecord, RunRecordError, SnapshotRef};
|
||||
use sandbox_attest::runrecord::{
|
||||
CallAccount, RunRecord, RunRecordError, SnapshotRef, WaitProof,
|
||||
};
|
||||
use sandbox_attest::{Attestation, DeviceIdentity, Outcome};
|
||||
use sandbox_capability::{Enforcer, Grants, HostService, KvDir, PathMode};
|
||||
use sandbox_meter::{DeviceEnergy, Provenance, Receipt};
|
||||
|
|
@ -228,10 +230,8 @@ fn c5() -> Result<(), String> {
|
|||
|
||||
/// C6 — durable run records (SPEC §13), with adversarial negatives.
|
||||
fn c6() -> Result<(), String> {
|
||||
let snap = |tag: &[u8]| SnapshotRef {
|
||||
fs_root: ContentId::of_bytes(tag),
|
||||
memory: None,
|
||||
manifest: ContentId::of_bytes(b"manifest"),
|
||||
let snap = |tag: &[u8]| {
|
||||
SnapshotRef::image(ContentId::of_bytes(tag), None, ContentId::of_bytes(b"manifest"))
|
||||
};
|
||||
let mut r = RunRecord::open(ContentId::of_bytes(b"unit"), ContentId::of_bytes(b"grants"));
|
||||
let h0 = r.head_id();
|
||||
|
|
@ -275,6 +275,190 @@ fn c6() -> Result<(), String> {
|
|||
Ok(())
|
||||
}
|
||||
|
||||
/// C14 — what a park retains (SPEC §13.1), with adversarial negatives.
|
||||
fn c14_park_forms() -> Result<(), String> {
|
||||
let man = ContentId::of_bytes(b"manifest");
|
||||
let image = |tag: &[u8]| SnapshotRef::image(ContentId::of_bytes(tag), None, man.clone());
|
||||
let transcript =
|
||||
|tag: &[u8]| SnapshotRef::transcript(ContentId::of_bytes(tag), man.clone());
|
||||
|
||||
// A transcript park is a full lifecycle, and its park is priced.
|
||||
let mut r = RunRecord::open(ContentId::of_bytes(b"unit"), ContentId::of_bytes(b"grants"));
|
||||
r.record_execution(&ContentId::of_bytes(b"att-1")).map_err(|e| format!("{e:?}"))?;
|
||||
r.suspend(transcript(b"turns-1")).map_err(|e| format!("{e:?}"))?;
|
||||
want(r.is_parked(), "a transcript park parks the run")?;
|
||||
r.resume(transcript(b"turns-1"), 42).map_err(|e| format!("{e:?}"))?;
|
||||
r.record_execution(&ContentId::of_bytes(b"att-2")).map_err(|e| format!("{e:?}"))?;
|
||||
want(r.verify(), "a transcript record verifies from genesis")?;
|
||||
want(r.idle_uj() == 42, "a transcript park's storage draw is accounted")?;
|
||||
|
||||
// The two forms are different parks over the same inner address, so one
|
||||
// cannot be offered to resume the other.
|
||||
let mut x = RunRecord::open(ContentId::of_bytes(b"unit"), ContentId::of_bytes(b"grants"));
|
||||
x.suspend(image(b"same")).map_err(|e| format!("{e:?}"))?;
|
||||
want(
|
||||
x.resume(transcript(b"same"), 0) == Err(RunRecordError::SnapshotMismatch),
|
||||
"a transcript reference must not resume an image park",
|
||||
)?;
|
||||
let mut y = RunRecord::open(ContentId::of_bytes(b"unit"), ContentId::of_bytes(b"grants"));
|
||||
y.suspend(transcript(b"same")).map_err(|e| format!("{e:?}"))?;
|
||||
want(
|
||||
y.resume(image(b"same"), 0) == Err(RunRecordError::SnapshotMismatch),
|
||||
"an image reference must not resume a transcript park",
|
||||
)?;
|
||||
|
||||
// A park must say what it retained, exactly once. Neither, both, and a
|
||||
// transcript beside a resident memory image are each refused, and the
|
||||
// refusal leaves no segment behind.
|
||||
let malformed = [
|
||||
("neither form", SnapshotRef { fs_root: None, memory: None, transcript: None, manifest: man.clone() }),
|
||||
(
|
||||
"both forms",
|
||||
SnapshotRef {
|
||||
fs_root: Some(ContentId::of_bytes(b"fs")),
|
||||
memory: None,
|
||||
transcript: Some(ContentId::of_bytes(b"turns")),
|
||||
manifest: man.clone(),
|
||||
},
|
||||
),
|
||||
(
|
||||
"a transcript beside a memory image",
|
||||
SnapshotRef {
|
||||
fs_root: None,
|
||||
memory: Some(ContentId::of_bytes(b"mem")),
|
||||
transcript: Some(ContentId::of_bytes(b"turns")),
|
||||
manifest: man.clone(),
|
||||
},
|
||||
),
|
||||
];
|
||||
for (why, s) in &malformed {
|
||||
want(s.kind().is_none(), &format!("{why} has no form"))?;
|
||||
let mut z = RunRecord::open(ContentId::of_bytes(b"unit"), ContentId::of_bytes(b"grants"));
|
||||
want(
|
||||
z.suspend(s.clone()) == Err(RunRecordError::MalformedSnapshot),
|
||||
&format!("{why} must be refused"),
|
||||
)?;
|
||||
want(z.segments().is_empty(), &format!("{why} leaves no segment"))?;
|
||||
}
|
||||
|
||||
// Edited into a record after the fact — through the wire form, as C6
|
||||
// tests tampering — a malformed reference fails verification rather than
|
||||
// hashing to something. Giving a parked transcript an `fs_root` makes it
|
||||
// carry both forms, which is exactly the ambiguity the chain must reject.
|
||||
let mut honest = RunRecord::open(ContentId::of_bytes(b"unit"), ContentId::of_bytes(b"grants"));
|
||||
honest.suspend(transcript(b"turns-1")).map_err(|e| format!("{e:?}"))?;
|
||||
honest.resume(transcript(b"turns-1"), 7).map_err(|e| format!("{e:?}"))?;
|
||||
want(honest.verify(), "the honest record verifies first")?;
|
||||
let mut wire: serde_json::Value =
|
||||
serde_json::to_value(&honest).map_err(|e| e.to_string())?;
|
||||
wire["segments"][0]["Suspended"]["snapshot"]["fs_root"] =
|
||||
serde_json::json!(ContentId::of_bytes(b"fs").0);
|
||||
let forged: RunRecord = serde_json::from_value(wire).map_err(|e| e.to_string())?;
|
||||
want(
|
||||
forged.segments()[0] != honest.segments()[0],
|
||||
"the wire edit landed on the recorded snapshot",
|
||||
)?;
|
||||
want(!forged.verify(), "a record carrying both forms must not verify")?;
|
||||
|
||||
// A refused resume must not advance the idle total.
|
||||
let mut q = RunRecord::open(ContentId::of_bytes(b"unit"), ContentId::of_bytes(b"grants"));
|
||||
q.suspend(transcript(b"turns-1")).map_err(|e| format!("{e:?}"))?;
|
||||
want(
|
||||
q.resume(transcript(b"turns-other"), 1_000) == Err(RunRecordError::SnapshotMismatch),
|
||||
"a mismatched resume is refused",
|
||||
)?;
|
||||
want(q.idle_uj() == 0, "a refused resume attributes no idle energy")?;
|
||||
Ok(())
|
||||
}
|
||||
|
||||
/// C15 — what an interval proves about waiting (SPEC §13.2).
|
||||
fn c15_wait_proof() -> Result<(), String> {
|
||||
let man = ContentId::of_bytes(b"manifest");
|
||||
let park = |tag: &[u8]| SnapshotRef::transcript(ContentId::of_bytes(tag), man.clone());
|
||||
let acct = |d: &[&[u8]], r: &[&[u8]]| CallAccount {
|
||||
dispatched: d.iter().map(|x| ContentId::of_bytes(x)).collect(),
|
||||
resolved: r.iter().map(|x| ContentId::of_bytes(x)).collect(),
|
||||
};
|
||||
let open =
|
||||
|| RunRecord::open(ContentId::of_bytes(b"unit"), ContentId::of_bytes(b"grants"));
|
||||
let e = |x: RunRecordError| format!("{x:?}");
|
||||
|
||||
// The hand-off shape: dispatch, end the interval, park, resolve later.
|
||||
let mut r = open();
|
||||
r.record_execution_accounted(&ContentId::of_bytes(b"att-1"), acct(&[b"call-1"], &[]))
|
||||
.map_err(e)?;
|
||||
r.suspend(park(b"turns-1")).map_err(e)?;
|
||||
r.resume(park(b"turns-1"), 3).map_err(e)?;
|
||||
r.record_execution_accounted(&ContentId::of_bytes(b"att-2"), acct(&[], &[b"call-1"]))
|
||||
.map_err(e)?;
|
||||
want(r.wait_proof() == WaitProof::NonBlocking, "a hand-off resolved later is non-blocking")?;
|
||||
want(r.verify(), "an accounted record verifies from genesis")?;
|
||||
|
||||
// Negative: an interval that consumed its own dispatch waited inside its
|
||||
// receipt, and must be reported as blocking rather than passed over.
|
||||
let mut b = open();
|
||||
b.record_execution_accounted(&ContentId::of_bytes(b"att"), acct(&[b"c"], &[b"c"]))
|
||||
.map_err(e)?;
|
||||
want(
|
||||
b.wait_proof() == WaitProof::Blocked { segment: 0 },
|
||||
"resolving its own dispatch is blocking",
|
||||
)?;
|
||||
|
||||
// Negative: an absent account proves nothing, and neither does a run with
|
||||
// no accounted interval. The claim must be unavailable, not vacuous.
|
||||
let mut mixed = open();
|
||||
mixed
|
||||
.record_execution_accounted(&ContentId::of_bytes(b"att-1"), acct(&[], &[]))
|
||||
.map_err(e)?;
|
||||
mixed.record_execution(&ContentId::of_bytes(b"att-2")).map_err(e)?;
|
||||
want(mixed.wait_proof() == WaitProof::Unproved, "one absent account unproves the run")?;
|
||||
want(open().wait_proof() == WaitProof::Unproved, "a run with no interval proves nothing")?;
|
||||
|
||||
// Negative: each way an account fails to add up is a malformed record,
|
||||
// reported distinctly from blocking.
|
||||
let mut ghost = open();
|
||||
ghost
|
||||
.record_execution_accounted(&ContentId::of_bytes(b"att"), acct(&[], &[b"ghost"]))
|
||||
.map_err(e)?;
|
||||
want(
|
||||
ghost.wait_proof() == WaitProof::Malformed { segment: 0 },
|
||||
"a result answering no dispatched call is malformed",
|
||||
)?;
|
||||
|
||||
let mut twice = open();
|
||||
twice
|
||||
.record_execution_accounted(&ContentId::of_bytes(b"att-1"), acct(&[b"c"], &[]))
|
||||
.map_err(e)?;
|
||||
twice
|
||||
.record_execution_accounted(&ContentId::of_bytes(b"att-2"), acct(&[], &[b"c"]))
|
||||
.map_err(e)?;
|
||||
twice
|
||||
.record_execution_accounted(&ContentId::of_bytes(b"att-3"), acct(&[], &[b"c"]))
|
||||
.map_err(e)?;
|
||||
want(
|
||||
twice.wait_proof() == WaitProof::Malformed { segment: 2 },
|
||||
"a call resolved twice is malformed",
|
||||
)?;
|
||||
|
||||
let mut dup = open();
|
||||
dup.record_execution_accounted(&ContentId::of_bytes(b"att-1"), acct(&[b"c"], &[]))
|
||||
.map_err(e)?;
|
||||
dup.record_execution_accounted(&ContentId::of_bytes(b"att-2"), acct(&[b"c"], &[]))
|
||||
.map_err(e)?;
|
||||
want(
|
||||
dup.wait_proof() == WaitProof::Malformed { segment: 1 },
|
||||
"one id dispatched twice is malformed",
|
||||
)?;
|
||||
|
||||
// Accounting for no calls is a different statement from not accounting,
|
||||
// so the two must not fold to the same bytes.
|
||||
let mut absent = open();
|
||||
absent.record_execution(&ContentId::of_bytes(b"att")).map_err(e)?;
|
||||
let mut empty = open();
|
||||
empty.record_execution_accounted(&ContentId::of_bytes(b"att"), acct(&[], &[])).map_err(e)?;
|
||||
want(absent.head_id() != empty.head_id(), "an empty account is not an absent one")?;
|
||||
Ok(())
|
||||
}
|
||||
|
||||
/// C7 — environment manifest (SPEC §14), with adversarial negatives.
|
||||
fn c7() -> Result<(), String> {
|
||||
|
|
@ -318,11 +502,8 @@ fn c7() -> Result<(), String> {
|
|||
)?;
|
||||
// Linkage with durable runs: a resume offering the same fs/memory but a
|
||||
// different environment manifest is a different snapshot — refused.
|
||||
let snap = |man: &ContentId| SnapshotRef {
|
||||
fs_root: ContentId::of_bytes(b"fs"),
|
||||
memory: None,
|
||||
manifest: man.clone(),
|
||||
};
|
||||
let snap =
|
||||
|man: &ContentId| SnapshotRef::image(ContentId::of_bytes(b"fs"), None, man.clone());
|
||||
let other = ContentId::of_bytes(b"other-manifest");
|
||||
let mut r = RunRecord::open(ContentId::of_bytes(b"unit"), ContentId::of_bytes(b"grants"));
|
||||
r.suspend(snap(&id)).map_err(|e| format!("{e:?}"))?;
|
||||
|
|
@ -574,6 +755,8 @@ pub fn run() -> Report {
|
|||
check("C11 enforcement-mechanism", c11_mechanism),
|
||||
check("C12 locality-evidence", c12_locality),
|
||||
check("C13 run-flow", || vectors::check_flow(&vectors::flow_vectors())),
|
||||
check("C14 park-forms", c14_park_forms),
|
||||
check("C15 wait-proof", c15_wait_proof),
|
||||
],
|
||||
}
|
||||
}
|
||||
|
|
@ -615,7 +798,7 @@ pub fn run_file_backed() -> Report {
|
|||
serde_json::from_str(&load("attestation.json")?).map_err(|e| e.to_string())?;
|
||||
check_attestation(&v)
|
||||
}),
|
||||
check("C6/C7/C10 durable.json", || {
|
||||
check("C6/C7/C10/C14/C15 durable.json", || {
|
||||
let v: DurableVectors =
|
||||
serde_json::from_str(&load("durable.json")?).map_err(|e| e.to_string())?;
|
||||
check_durable(&v)
|
||||
|
|
@ -708,10 +891,12 @@ mod tests {
|
|||
assert!(r.passed, "class {} failed: {}", r.class, r.detail);
|
||||
}
|
||||
assert!(report.ok());
|
||||
// C1–C13. Bump deliberately when a class is added, never to make a
|
||||
// C1–C15. Bump deliberately when a class is added, never to make a
|
||||
// red build green: a silently shrinking pack is a standard quietly
|
||||
// certifying less than it claims.
|
||||
assert_eq!(report.results.len(), 13);
|
||||
// certifying less than it claims. C14 (§13.1, what a park retains)
|
||||
// and C15 (§13.2, what an interval proves about waiting) are the
|
||||
// additions that took this from 13.
|
||||
assert_eq!(report.results.len(), 15);
|
||||
}
|
||||
|
||||
/// The committed pack is exactly what the builders emit, file for file
|
||||
|
|
|
|||
|
|
@ -10,7 +10,7 @@
|
|||
use ed25519_dalek::{SigningKey, VerifyingKey};
|
||||
use sandbox_attest::fleet::{FleetItem, FleetRecord};
|
||||
use sandbox_attest::manifest::EnvironmentManifest;
|
||||
use sandbox_attest::runrecord::{RunRecord, SnapshotRef};
|
||||
use sandbox_attest::runrecord::{CallAccount, RunRecord, SnapshotRef};
|
||||
use sandbox_attest::{
|
||||
replay_compare, Attestation, DeviceIdentity, Journal, JournalEntry, Outcome, Replay,
|
||||
};
|
||||
|
|
@ -920,8 +920,18 @@ pub struct DurableVectors {
|
|||
/// devcontainer document whose canonical manifest id is fixed.
|
||||
pub devcontainer: String,
|
||||
pub expect_manifest_id: String,
|
||||
/// The run-record head after a fixed execute/suspend/resume/execute trace.
|
||||
/// The run-record head after a fixed execute/suspend/resume/execute trace,
|
||||
/// parked on host state (SPEC §13.1, the image form).
|
||||
pub expect_runrecord_head: String,
|
||||
/// The head after the same trace parked on a transcript instead — the
|
||||
/// other form of §13.1. Pinned separately so an implementation cannot
|
||||
/// satisfy one form's address by producing the other's.
|
||||
pub expect_transcript_head: String,
|
||||
/// The head after the same trace with each interval accounting for its
|
||||
/// outward calls (§13.2). The account is folded into the chain, so this
|
||||
/// pins those bytes; the trace is otherwise the transcript one's, which
|
||||
/// is what makes the two addresses comparable.
|
||||
pub expect_accounted_head: String,
|
||||
/// The merkle root over a fixed fleet of three items.
|
||||
pub expect_fleet_root: String,
|
||||
}
|
||||
|
|
@ -929,11 +939,55 @@ pub struct DurableVectors {
|
|||
const VEC_DEVCONTAINER: &str = r#"{"image":"ghcr.io/acme/builder@sha256:0011aabb","features":{"ghcr.io/devcontainers/features/rust:1":{"profile":"minimal"}},"containerEnv":{"B":"2","A":"1"}}"#;
|
||||
|
||||
fn vec_runrecord() -> RunRecord {
|
||||
let snap = SnapshotRef {
|
||||
fs_root: ContentId::of_bytes(b"vec-fs"),
|
||||
memory: None,
|
||||
manifest: ContentId::of_bytes(b"vec-manifest"),
|
||||
};
|
||||
let snap = SnapshotRef::image(
|
||||
ContentId::of_bytes(b"vec-fs"),
|
||||
None,
|
||||
ContentId::of_bytes(b"vec-manifest"),
|
||||
);
|
||||
let mut r = RunRecord::open(ContentId::of_bytes(b"vec-unit"), ContentId::of_bytes(b"vec-grants"));
|
||||
r.record_execution(&ContentId::of_bytes(b"vec-att-1")).unwrap();
|
||||
r.suspend(snap.clone()).unwrap();
|
||||
r.resume(snap, 117).unwrap();
|
||||
r.record_execution(&ContentId::of_bytes(b"vec-att-2")).unwrap();
|
||||
r
|
||||
}
|
||||
|
||||
/// The transcript trace again, with each interval accounting for its outward
|
||||
/// calls (§13.2): the first hands off one call, the second resolves it after
|
||||
/// the park. Everything else is `vec_transcript_runrecord`'s, so the two
|
||||
/// pinned heads differ only by the account being folded in.
|
||||
fn vec_accounted_runrecord() -> RunRecord {
|
||||
let snap = SnapshotRef::transcript(
|
||||
ContentId::of_bytes(b"vec-turns"),
|
||||
ContentId::of_bytes(b"vec-manifest"),
|
||||
);
|
||||
let call = ContentId::of_bytes(b"vec-call-1");
|
||||
let mut r = RunRecord::open(ContentId::of_bytes(b"vec-unit"), ContentId::of_bytes(b"vec-grants"));
|
||||
r.record_execution_accounted(
|
||||
&ContentId::of_bytes(b"vec-att-1"),
|
||||
CallAccount { dispatched: vec![call.clone()], resolved: Vec::new() },
|
||||
)
|
||||
.unwrap();
|
||||
r.suspend(snap.clone()).unwrap();
|
||||
r.resume(snap, 117).unwrap();
|
||||
r.record_execution_accounted(
|
||||
&ContentId::of_bytes(b"vec-att-2"),
|
||||
CallAccount { dispatched: Vec::new(), resolved: vec![call] },
|
||||
)
|
||||
.unwrap();
|
||||
r
|
||||
}
|
||||
|
||||
/// The same trace, parked on a transcript instead of host state (§13.1). The
|
||||
/// unit ids, attestations, manifest and idle figure are deliberately those of
|
||||
/// `vec_runrecord`, so the only difference between the two pinned heads is
|
||||
/// which form the park retained — an implementation that confused the forms
|
||||
/// would produce one address where the other is expected.
|
||||
fn vec_transcript_runrecord() -> RunRecord {
|
||||
let snap = SnapshotRef::transcript(
|
||||
ContentId::of_bytes(b"vec-turns"),
|
||||
ContentId::of_bytes(b"vec-manifest"),
|
||||
);
|
||||
let mut r = RunRecord::open(ContentId::of_bytes(b"vec-unit"), ContentId::of_bytes(b"vec-grants"));
|
||||
r.record_execution(&ContentId::of_bytes(b"vec-att-1")).unwrap();
|
||||
r.suspend(snap.clone()).unwrap();
|
||||
|
|
@ -959,6 +1013,8 @@ pub fn durable_vector() -> DurableVectors {
|
|||
devcontainer: VEC_DEVCONTAINER.to_string(),
|
||||
expect_manifest_id: manifest.content_id().unwrap().0,
|
||||
expect_runrecord_head: vec_runrecord().head_id().0,
|
||||
expect_transcript_head: vec_transcript_runrecord().head_id().0,
|
||||
expect_accounted_head: vec_accounted_runrecord().head_id().0,
|
||||
expect_fleet_root: vec_fleet().root_id().0,
|
||||
}
|
||||
}
|
||||
|
|
@ -974,6 +1030,26 @@ pub fn check_durable(v: &DurableVectors) -> Result<(), String> {
|
|||
if got_head != v.expect_runrecord_head {
|
||||
return Err(format!("runrecord head drift: {got_head} != {}", v.expect_runrecord_head));
|
||||
}
|
||||
let got_transcript = vec_transcript_runrecord().head_id().0;
|
||||
if got_transcript != v.expect_transcript_head {
|
||||
return Err(format!(
|
||||
"transcript-park head drift: {got_transcript} != {}",
|
||||
v.expect_transcript_head
|
||||
));
|
||||
}
|
||||
if v.expect_transcript_head == v.expect_runrecord_head {
|
||||
return Err("the two park forms must not share a head".to_string());
|
||||
}
|
||||
let got_accounted = vec_accounted_runrecord().head_id().0;
|
||||
if got_accounted != v.expect_accounted_head {
|
||||
return Err(format!(
|
||||
"accounted-interval head drift: {got_accounted} != {}",
|
||||
v.expect_accounted_head
|
||||
));
|
||||
}
|
||||
if v.expect_accounted_head == v.expect_transcript_head {
|
||||
return Err("an accounted interval must not hash as an unaccounted one".to_string());
|
||||
}
|
||||
let f = vec_fleet();
|
||||
if !f.verify() {
|
||||
return Err("fleet self-check failed".into());
|
||||
|
|
|
|||
|
|
@ -42,6 +42,12 @@ An attestation without a `mechanism` canonicalizes to byte-identical JSON under
|
|||
### C13 — Flow across a run's checkpoints (§5.8)
|
||||
A run's calls, in order: a read from an untrusted source adds its origins to the run's taint, and a sink is decided against everything read before it. A clean run reaches every sink its capabilities allow. An untrusted read closes the egress and launch that follow it, except where the flow grant opens a sink to every origin the run carries. The taint only grows, so a later clean read restores nothing, and a second origin closes a sink opened to the first. A grant set without a flow grant is never tainted. The order is part of the vector, since no single query can show what a run may do after what it did.
|
||||
|
||||
### C14 — What a park retains (§13.1)
|
||||
A park retains host state or a transcript, and a record says which. A transcript park chains, verifies and accumulates idle energy like any other — nothing is resident, so the figure it owes is the draw of the bytes it kept, and zero is not that figure. A reference naming neither form, both, or a transcript beside a resident memory image is refused before anything is hashed and leaves no segment behind; edited into a record afterwards, through the wire form, it fails verification rather than hashing to something. The two forms over the same inner address are different parks, so offering one to resume the other is refused. The image form's bytes are pinned against a hand-written layout, and its committed head is unchanged from before the second form existed — a backwards-compatible extension is one whose old addresses still recompute, which is checkable rather than asserted.
|
||||
|
||||
### C15 — What an interval proves about waiting (§13.2)
|
||||
A run whose every executed interval accounts for its outward calls, and whose every interval resolves only calls outstanding before it began, is non-blocking: no receipt in it contains a wait for an outward call, so its whole cost of waiting is the idle energy §13 already records. The hand-off shape — dispatch, end the interval, resolve in a later one — proves it. An interval that resolves a call it dispatched itself is reported as blocking, because the wait is inside its receipt. An account that does not add up (a result answering a call never dispatched, a call resolved twice, one id dispatched twice) is reported as a malformed record, distinctly from blocking. An absent account proves nothing, and neither does a run with no accounted interval: a property of no intervals is not a property, and the claim is unavailable rather than vacuously true. An interval recorded without an account hashes exactly as it did before the section existed.
|
||||
|
||||
## Adversarial obligation
|
||||
|
||||
The most valuable vectors are **negatives** — runs a conformant host must reject. A standard whose vectors only assert the happy path certifies nothing. The committed pack ([`../conformance/v1/negative.json`](../conformance/v1/negative.json)) carries a **C-neg** class the harness asserts is rejected:
|
||||
|
|
|
|||
|
|
@ -28,13 +28,51 @@ Three segment kinds:
|
|||
attestation (§7), which already binds the interval's energy receipt (§6),
|
||||
replay-journal root (§8) and outcome. Nothing is re-stated; the record
|
||||
points at sealed objects.
|
||||
- **Suspended** — the run parked. Records a **snapshot reference**: the
|
||||
content addresses of the retained filesystem root, the memory image if the
|
||||
executor retains resident state (S5 snapshots), and the environment
|
||||
manifest the run was created from.
|
||||
- **Suspended** — the run parked. Records a **snapshot reference**: what was
|
||||
retained, in one of the two forms below, and the environment manifest the
|
||||
run was created from.
|
||||
- **Resumed** — the run un-parked. Records the snapshot reference restored
|
||||
and the **idle energy** the retained state drew while parked.
|
||||
|
||||
## What a park retains
|
||||
|
||||
There are two forms, and a snapshot reference carries exactly one.
|
||||
|
||||
**An image park** retains host state: a filesystem root, and a memory image
|
||||
where the executor suspends resident state. This is the form a shell, a build
|
||||
or a long-lived server needs, because its resumable state is spread across a
|
||||
filesystem and a process.
|
||||
|
||||
**A transcript park** retains nothing on the host. Some units — an agent
|
||||
driven by a model is the clear case — hold their resumable state entirely in
|
||||
the record of what they have already done. For those, that record *is* the
|
||||
continuation: restore it and the unit is where it left off, with no process to
|
||||
revive. The park names its content address and nothing else.
|
||||
|
||||
That is not a smaller version of the first form; it is a different claim about
|
||||
where the run lives, and it buys two things.
|
||||
|
||||
- **It resumes anywhere.** The content-identity precondition is satisfied by
|
||||
any host that can fetch the transcript, so a transcript park is portable
|
||||
across hardware by construction. An image park also needs a host able to
|
||||
restore its image. A record of the first kind says a run can resume; a
|
||||
record of the second says where.
|
||||
- **Its park is small, and priced.** What it holds is bytes, so the park's
|
||||
draw is the draw of storing them — orders below a retained volume, and
|
||||
bounded by a number the host already knows.
|
||||
|
||||
A reference naming neither form, or both, or a transcript beside a resident
|
||||
memory image, is **refused rather than hashed**. The last of those is the
|
||||
interesting one: it is a park claiming to retain nothing on the host while
|
||||
holding an image on it. Admitting any of the three would put an ambiguity
|
||||
inside a chain whose purpose is to remove ambiguity, so the refusal happens
|
||||
before the bytes are folded, and a reference edited into a record afterwards
|
||||
fails verification rather than hashing to something.
|
||||
|
||||
The image form's canonical bytes are unchanged from before the second form
|
||||
existed, so every record and every conformance address written under the
|
||||
single-form chain still recomputes.
|
||||
|
||||
## Resumption preconditions
|
||||
|
||||
A host **MUST** refuse to resume unless:
|
||||
|
|
@ -61,6 +99,61 @@ the host can measure, estimated and labelled where it cannot. The total cost
|
|||
of a run is the sum over its receipts **plus** its idle energy; a host that
|
||||
reports only active-interval joules for a week-long run does not conform.
|
||||
|
||||
A transcript park is where that rule earns its keep. Nothing is running and
|
||||
nothing is resident, and it is tempting to call the wait free — a claim that
|
||||
is nearly true and therefore worth stating precisely. What the park holds is
|
||||
a transcript in storage, and storage draws power for every hour of the wait.
|
||||
So a host **MUST NOT** record a transcript park's `idle_uj` as zero on the
|
||||
grounds that no computation happened: the figure it owes is the draw of the
|
||||
bytes it kept, under the same provenance discipline as any other. The claim
|
||||
this form supports is that **waiting costs no computation**. It does not
|
||||
support the claim that waiting costs nothing, and a record that says zero for
|
||||
a week of storage is not a cheaper run, only a less honest one.
|
||||
|
||||
## The wait inside a receipt
|
||||
|
||||
Everything above prices the wait a run spends parked. The wait it spends
|
||||
*running* is the larger number, and until an interval accounts for its outward
|
||||
calls, nothing in the record can see it.
|
||||
|
||||
An interval that dispatches a call and then sits until the result arrives holds
|
||||
its sandbox for the duration, and its receipt charges the sitting as
|
||||
computation. A build that takes twenty minutes, a review that comes back the
|
||||
next morning, an approval that never comes — each of those is, in a blocking
|
||||
runtime, an interval whose receipt is mostly waiting. Two runs doing identical
|
||||
work bill differently by hours, and the record as described so far reports both
|
||||
the same way.
|
||||
|
||||
So an executed segment may carry an **account** of the calls it dispatched and
|
||||
the results it resolved, each by call id. The shape that makes a run
|
||||
non-blocking is: dispatch, **end the interval**, park, and resolve in a later
|
||||
one. An interval that resolves a call it dispatched itself did not hand off and
|
||||
return — it waited.
|
||||
|
||||
Three things make this worth the two fields.
|
||||
|
||||
- **It is checkable, not promised.** Walk the segments in order holding the
|
||||
calls outstanding at each one's start; a segment may resolve only those. No
|
||||
trust in the implementation is required, and no instrumentation beyond the
|
||||
ids the host already has to match results to calls.
|
||||
- **It is what licenses the energy claim.** Where every interval accounts and
|
||||
every one resolves only what was outstanding, no receipt in the run contains
|
||||
a wait for an outward call. The run's whole cost of waiting is then its idle
|
||||
energy — which §13 already records, and which §13.1 makes small for a
|
||||
transcript park. That is the condition under which "waiting costs no
|
||||
computation" is a statement about this record rather than about the runtime
|
||||
that produced it.
|
||||
- **An absent account proves nothing.** Not accounting is not the same as
|
||||
accounting for no calls, and the two do not hash alike. A run with an
|
||||
unaccounted interval, or with no accounted interval at all, yields no
|
||||
verdict rather than a favourable one. A property of no intervals is not a
|
||||
property.
|
||||
|
||||
An account that does not add up is reported separately from blocking: a result
|
||||
answering a call never dispatched, a call resolved twice, or one id dispatched
|
||||
twice is a record that cannot be read, which is a different problem from a run
|
||||
that waited.
|
||||
|
||||
## Relation to the audit chain
|
||||
|
||||
The S7 audit chain (§7.7) orders *runs* within a steward's domain; the run
|
||||
|
|
@ -76,4 +169,13 @@ execute → suspend → resume → execute; refusal of forked snapshots
|
|||
idle-energy accumulation; tamper-evidence through the wire form (a modified
|
||||
recorded snapshot must fail verification); refusal of appends after close.
|
||||
|
||||
Class **C14**: the two forms a park may retain. A transcript park chains,
|
||||
verifies and accumulates idle energy like any other; a reference naming
|
||||
neither form, both, or a transcript beside a memory image is refused with
|
||||
`MalformedSnapshot` and leaves no segment behind; an image and a transcript
|
||||
reference over the same inner address are different parks, so offering one to
|
||||
resume the other is a `SnapshotMismatch`; and the image form's canonical bytes
|
||||
are pinned against a hand-written layout, so the chain written before the
|
||||
second form existed still recomputes.
|
||||
|
||||
The reference implementation is `sandbox_attest::runrecord`.
|
||||
|
|
|
|||
Loading…
Reference in a new issue