Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
73 changes: 66 additions & 7 deletions dag/gunbc/regen_receipt.dag
Original file line number Diff line number Diff line change
Expand Up @@ -2,19 +2,72 @@ module gunbc.regen_receipt

import std.types { String, Int, List, Bool }

data regen_receipt_note: String = "Typed receipt for a non-mutating stage0 regen verify run via claim_executor --required-regen. first_generation_equal and fixed_point_equal are DISTINCT questions and must never collapse. The host binary materializes this carrier at runtime; fixed_point_equal is answered by a second invocation (--required-regen-fixed-point), not a second code path inside one run."
// A RECEIPT MAY REFERENCE PRIOR EVIDENCE BUT MAY NOT IMPERSONATE PRIOR EVIDENCE AS SOMETHING IT
// MEASURED ITSELF (operator ruling, 2026-08-20). The two regen passes answer DISTINCT questions —
// first_generation_equal (does a fresh emit match the committed seed) and fixed_point_equal (does
// the emit reproduce itself on a second pass) — and they run as two separate process invocations
// against one receipt file at target/stage0-regen-receipt.json.
//
// WHAT WENT WRONG WITH ONE FLAT RECORD. A single eight-field record forced the second pass to
// populate fields it had not measured, and the only available source was the receipt the first
// pass left on disk. Four of six were therefore copied through verbatim:
// committed_generated_digest, first_generation_equal, changed_paths, candidate_artifact. The
// result is stamped with the SECOND pass commit_sha while carrying the FIRST pass answers, and it
// is internally consistent and schema-valid — which is exactly what makes it invisible. Nothing in
// the artifact says which tree four of its fields describe.
//
// The reachable arm is the ordinary local one rather than CI: the two modes are separate
// invocations, and nothing requires the first to have run in this process, at this commit, or at
// all. A developer iterating on the determinism half alone, over a warm target/ from an earlier
// commit, gets today commit_sha carrying yesterday changed_paths. In CI the arm is currently
// unreachable because actions/checkout default clean removes the ignored target/ each run —
// measured, two consecutive main runs each compiling 105 crates starting at proc-macro2, where a
// warm tree compiles zero — but that is a property of a checkout default nobody declared, and it
// is one cache-reuse change away from live on a required path.
//
// THE SHAPE BELOW MAKES THE FABRICATION UNWRITABLE RATHER THAN DETECTABLE. The two passes are two
// variants, and the second variant HAS NO first_generation_equal FIELD to fill in. There is no
// value to copy and no check to pass, because the invalid state has no constructor — DESIGN 4b
// structural impossibility, not the validation rung one below it. Choosing this over "compute all
// six in pass two" is deliberate: computing all six would make the second pass re-derive
// first_generation_equal against the committed tree, which is the FIRST pass question, fusing two
// authorities into one row (DESIGN 3).
//
// A REFERENCE IS ONLY HONEST IF IT NAMES ITS SUBJECT. PriorReceiptRef therefore carries the
// commit_sha the referenced evidence was measured at, so a consumer READS which tree those facts
// describe instead of inferring it from context. A ref that silently pointed at another tree would
// be the same defect with better vocabulary.

type RegenReceipt {
type PriorReceiptRef {
commit_sha: String
authority_digest: String
committed_generated_digest: String
candidate_generated_digest: String
first_generation_equal: Bool
fixed_point_equal: Bool
changed_paths: List<String>
candidate_artifact: String
}

// FIRST GENERATION measures everything it reports. FIXED POINT measures the pass-2 digest and its
// equality, and references the rest. The commit_sha on each variant is the tree THAT PASS ran
// against; prior.commit_sha is the tree the referenced evidence came from, and the host refuses
// when they differ.
type RegenReceipt
= FirstGeneration {
commit_sha: String
authority_digest: String
committed_generated_digest: String
candidate_generated_digest: String
first_generation_equal: Bool
changed_paths: List<String>
candidate_artifact: String
}
| FixedPoint {
commit_sha: String
authority_digest: String
candidate_generated_digest: String
fixed_point_equal: Bool
prior: PriorReceiptRef
}

data stage0_regen_candidate_dir_rel: String = "target/stage0-regen-candidate"

data stage0_regen_receipt_rel: String = "target/stage0-regen-receipt.json"
Expand All @@ -23,6 +76,12 @@ data stage0_regen_candidate_artifact_name: String = "stage0-regen-candidate"

data stage0_regen_receipt_artifact_name: String = "stage0-regen-receipt"

fn stage0_regen_receipt_is_green(receipt: RegenReceipt) -> Bool {
receipt.first_generation_equal && receipt.fixed_point_equal
// STALENESS IS DECIDABLE FROM THE CARRIER ALONE, which is the point of putting commit_sha on the
// ref. The host refuses a cross-tree reference on the required path; this predicate is the same
// question asked of an already-materialized receipt.
fn prior_reference_is_same_tree(receipt: RegenReceipt) -> Bool {
match receipt {
FirstGeneration { commit_sha: _, authority_digest: _, committed_generated_digest: _, candidate_generated_digest: _, first_generation_equal: _, changed_paths: _, candidate_artifact: _ } => true,
FixedPoint { commit_sha, authority_digest: _, candidate_generated_digest: _, fixed_point_equal: _, prior } => commit_sha == prior.commit_sha
}
}
82 changes: 82 additions & 0 deletions dag/test/claim/regen_receipt_prior_reference_witness_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,82 @@
module test.claim.regen_receipt_prior_reference_witness

import std.types { Bool, String, List }
import gunbc.regen_receipt { RegenReceipt, PriorReceiptRef, FirstGeneration, FixedPoint, prior_reference_is_same_tree }

// WHAT THIS WITNESS COVERS, AND WHAT IT DOES NOT — stated first because the gap is the point.
//
// COVERS: the model predicate. A FixedPoint receipt whose prior reference names a DIFFERENT tree
// is distinguishable from one that names the same tree, decidably, from the carrier alone.
//
// DOES NOT COVER: the host refusal arm in required_regen_host run_required_regen_fixed_point.
// That arm compares the on-disk prior receipt against git HEAD and returns an Err, and reaching it
// requires planting a receipt file at target/stage0-regen-receipt.json with a chosen commit_sha
// before invoking the binary. No witness form available here writes a file before running a
// process, so the host arm has no executing evidence and I am not claiming otherwise. Its
// next-rung trigger is a witness form that can stage a fixture file for a wet run; until then the
// host arm rests on review, which is strictly weaker than this predicate does.
//
// The reason the predicate is worth having anyway is that it is the SAME question the host asks.
// If the model says a cross-tree reference is detectable and the host later stops checking, the
// disagreement is between two things that both exist, rather than a rule that lives only in one
// unexecuted comment.

data same_tree_sha: String = "bd239370923f0000000000000000000000000000"

data other_tree_sha: String = "5a10ca7e01891e32f7568c3bac23878f2b3fdc5f"

fn a_prior_ref(at: String) -> PriorReceiptRef {
PriorReceiptRef {
commit_sha: at,
committed_generated_digest: "digest-committed",
first_generation_equal: true,
changed_paths: [],
candidate_artifact: "target/stage0-regen-candidate"
}
}

fn a_fixed_point_receipt(ran_at: String, referenced_at: String) -> RegenReceipt {
FixedPoint {
commit_sha: ran_at,
authority_digest: "digest-authority",
candidate_generated_digest: "digest-candidate",
fixed_point_equal: true,
prior: a_prior_ref(at: referenced_at)
}
}

// POSITIVE CONTROL. Without this, the RED below is satisfied by a predicate that returns false
// unconditionally — which is the failure mode that cost me a broken instrument earlier today, one
// that printed the right answer while being incapable of printing any other.
test fn a_fixed_point_receipt_referencing_its_own_tree_is_same_tree() -> Bool {
prior_reference_is_same_tree(
receipt: a_fixed_point_receipt(ran_at: same_tree_sha, referenced_at: same_tree_sha)
)
}

// THE DISCRIMINATING RED. This is the state the flat eight-field receipt could reach silently:
// stamped with the tree the second pass ran against, carrying evidence measured on another. It is
// internally consistent and schema-valid, and the ONLY thing that distinguishes it is that the
// reference names its subject.
test fn w_RED_a_fixed_point_receipt_referencing_another_tree_is_not_same_tree() -> Bool {
!prior_reference_is_same_tree(
receipt: a_fixed_point_receipt(ran_at: same_tree_sha, referenced_at: other_tree_sha)
)
}

// A FirstGeneration receipt has no prior reference to be wrong about, so the predicate is
// vacuously true there. Asserted rather than assumed: a predicate that answered false for the
// variant carrying no reference would refuse every first pass.
test fn a_first_generation_receipt_has_no_cross_tree_reference() -> Bool {
prior_reference_is_same_tree(
receipt: FirstGeneration {
commit_sha: same_tree_sha,
authority_digest: "digest-authority",
committed_generated_digest: "digest-committed",
candidate_generated_digest: "digest-candidate",
first_generation_equal: true,
changed_paths: [],
candidate_artifact: "target/stage0-regen-candidate"
}
)
}
45 changes: 39 additions & 6 deletions src/v1/stage0/src/bin/claim_executor.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10464,9 +10464,28 @@ fn run() -> Result<ExitCode, ExitCode> {
return match v1_compiler::cli_run::run_required_regen_fixed_point(&regen_receipt_path, None)
{
Ok(outcome) => {
// The provenance is printed, not just carried. This line previously read
// `first_generation_equal={}` off the receipt as though the fixed-point pass had
// measured it; it never does. Labelling it `referenced_` and naming the commit it
// came from means the log itself distinguishes measured from quoted -- and since
// the host refuses a cross-tree reference, `referenced_at` equals HEAD on every
// line that is allowed to print.
let (referenced_fge, referenced_at) = match outcome.receipt.prior() {
Some(prior) => (
prior.first_generation_equal.to_string(),
prior.commit_sha.clone(),
),
None => ("unavailable".to_string(), "unavailable".to_string()),
};
eprintln!(
"required-regen-fixed-point: fixed_point_equal={} first_generation_equal={}",
outcome.receipt.fixed_point_equal, outcome.receipt.first_generation_equal
"required-regen-fixed-point: fixed_point_equal={} referenced_first_generation_equal={} referenced_at={}",
outcome
.receipt
.fixed_point_equal()
.map(|v| v.to_string())
.unwrap_or_else(|| "unmeasured".to_string()),
referenced_fge,
referenced_at
);
for failure in &outcome.failures {
eprintln!("required-regen-fixed-point: FAIL {failure}");
Expand All @@ -10490,10 +10509,24 @@ fn run() -> Result<ExitCode, ExitCode> {
&regen_receipt_path,
) {
Ok(outcome) => {
eprintln!(
"required-regen: first_generation_equal={} candidate={}",
outcome.receipt.first_generation_equal, outcome.receipt.candidate_artifact
);
// Both values here ARE measured by this pass, so they print unqualified. Read
// through accessors rather than by matching the variant: the
// `required_regen_host` module is private to `cli_run`, so the type is usable here
// but not nameable. The accessors return Option because the sibling variant does
// not measure these fields; a `None` on this path would mean the first pass built
// the wrong variant, so it prints `unmeasured` rather than defaulting to a
// plausible-looking value.
let fge = outcome
.receipt
.first_generation_equal()
.map(|v| v.to_string())
.unwrap_or_else(|| "unmeasured".to_string());
let candidate = outcome
.receipt
.candidate_artifact()
.unwrap_or("unmeasured")
.to_string();
eprintln!("required-regen: first_generation_equal={fge} candidate={candidate}");
for failure in &outcome.failures {
eprintln!("required-regen: FAIL {failure}");
}
Expand Down
Loading