Verify machine-checkable source claims

ARCHITECTURE.md

@@ -98,6 +98,14 @@ acquire diff --> parse supported lockfiles --> parse + index --> bounded evidenc
   Only a complete receipt with no positive counterexample supports a universal claim.
   Incomplete repository evidence cannot confirm a fresh claim, so the claim is suppressed;
   a prior-ledger claim remains open until exact-head adjudication resolves it.
+  Typed Rust source claims cover Copy move-out premises, exact symbol absence, and normalized
+  signature mismatch. The source verifier parses bounded regular Rust module blobs under `src/`,
+  including `src/lib.rs` and `src/main.rs` but excluding separate `src/bin` crate roots, from the
+  immutable reviewed GitHub tree with `syn`; it does not compile, execute, expand macros, follow
+  symlinks, or infer names. Complete receipts bind the verifier version, head and tree identities,
+  normalized claim hash, verdict, and hash-only source evidence. Fresh claims without a conclusive
+  receipt are suppressed. Carried claims require an exact-head refutation to resolve and otherwise
+  remain visible as deferred, nonblocking findings.
   Every surviving generated candidate, plus applicable baseline candidates during a full
   rereview, enters one bounded adjudication operation before scoring and publication. The
   operation admits the complete candidate set or fails closed before provider contact. Its
@@ -280,6 +288,12 @@ additions (violations are `kind: contentPolicy`). Content policy is on by defaul
     cannot expand or enter schema repair. Confirmation and refutation require exact supplied
     evidence; repository-wide conclusions additionally require a complete receipt for the exact
     snapshot. Public rewrites describe only the defect, impact, and correction.
+16. Typed machine claims never substitute model prose for source proof. Verification parses a
+    bounded immutable Rust source snapshot without compilation or execution, rejects ambiguous
+    symbols and unsupported syntax, and emits only hash-bound evidence. A fresh unsupported,
+    unresolved, unavailable, exhausted, or refuted claim cannot reach the gate. A carried claim
+    remains visible but nonblocking until an exact-head refutation resolves it. Fresh independently
+    generated claims still require a supported receipt.
 
 ## Residual prompt-injection surface
 

Cargo.toml

@@ -38,6 +38,7 @@ serde_json = { version = "1.0.150", features = ["raw_value"] }
 sha1 = "0.11.0"
 sha2 = "0.11.0"
 similar = "3.1.1"
+syn = { version = "2", features = ["full", "visit"] }
 tempfile = "3.27.0"
 time = { version = "0.3.54", features = ["parsing", "formatting"] }
 tokio = { version = "1.52.3", features = ["rt-multi-thread", "macros", "process", "time"] }

bench/review-contract-sources.json

@@ -25,6 +25,7 @@
   "src/llm.rs",
   "src/local.rs",
   "src/login.rs",
+  "src/machine_claim.rs",
   "src/main.rs",
   "src/output.rs",
   "src/plan.rs",

docs/automation.md

@@ -4,7 +4,7 @@
 
 `postil review --output json` and `--output yaml` emit the complete versioned review envelope. `--output csv` emits a flattened findings table with review and gate fields repeated on each row. `--output-file <path>` keeps structured output separate from human-readable output.
 
-The JSON and YAML envelope contains the summary, findings, resolved findings, policy counts, gate result, model and scorer metadata, token usage, per-model usage, and reviewed SHAs. `usageAccountingComplete` is false when a provider request can have unknown billed usage.
+The JSON and YAML envelope contains the summary, findings, resolved findings, policy counts, gate result, model and scorer metadata, token usage, per-model usage, and reviewed SHAs. A finding can include a typed `machineClaim`; `claimVerification` records its exact-head, hash-only source receipt, and `machineClaimDeferred` marks a carried claim that remains visible without blocking. Both fields are optional during deserialization. `usageAccountingComplete` is false when a provider request can have unknown billed usage.
 
 `--sarif <path>` writes SARIF 2.1.0 for code-scanning ingestion.
 

src/adjudication.rs

@@ -1646,6 +1646,8 @@ mod tests {
             scorer_kind: None,
             scorer_reason: None,
             repository_claim: None,
+            machine_claim: None,
+            machine_claim_deferred: false,
             title: title.into(),
             body: body.into(),
             evidence: Some("uses: action@old".into()),

src/brevity.rs

@@ -146,6 +146,8 @@ mod tests {
             scorer_kind: None,
             scorer_reason: None,
             repository_claim: None,
+            machine_claim: None,
+            machine_claim_deferred: false,
             title: "Keep the stable finding metadata".to_string(),
             body,
             evidence: Some("changed_call();".to_string()),

src/envelope.rs

@@ -114,6 +114,14 @@ pub struct Finding {
         default
     )]
     pub repository_claim: Option<RepositoryClaim>,
+    /// Optional deterministic source premise that Postil can verify against
+    /// the immutable reviewed repository without compiling or executing it.
+    #[serde(skip_serializing_if = "Option::is_none", default)]
+    pub machine_claim: Option<MachineClaim>,
+    /// Carried machine claims stay visible when current source cannot settle
+    /// them, but they do not block until a fresh supported receipt exists.
+    #[serde(skip_serializing_if = "is_false", default)]
+    pub machine_claim_deferred: bool,
     pub title: String,
     pub body: String,
     /// Exact new-side text canonicalized from the cited prompt line. This is
@@ -127,6 +135,115 @@ pub struct Finding {
     pub id: Option<String>,
 }
 
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
+pub enum MachineClaimKind {
+    #[serde(rename = "rust.copy_move_out")]
+    RustCopyMoveOut,
+    #[serde(rename = "symbol.absent")]
+    SymbolAbsent,
+    #[serde(rename = "signature.mismatch")]
+    SignatureMismatch,
+}
+
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
+#[serde(rename_all = "camelCase")]
+pub enum MachineReceiver {
+    None,
+    Shared,
+    Mutable,
+    Value,
+}
+
+/// Bounded function shape accepted by `signature.mismatch`.
+///
+/// Parameter and return types use a deliberately small Rust type grammar:
+/// paths, references without explicit lifetimes, tuples, slices, and generic
+/// type arguments composed from those forms.
+#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
+#[serde(rename_all = "camelCase")]
+pub struct MachineSignature {
+    pub receiver: MachineReceiver,
+    #[serde(default)]
+    pub parameters: Vec<String>,
+    pub returns: String,
+    #[serde(rename = "async", default, skip_serializing_if = "is_false")]
+    pub is_async: bool,
+    #[serde(rename = "unsafe", default, skip_serializing_if = "is_false")]
+    pub is_unsafe: bool,
+}
+
+#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
+#[serde(rename_all = "camelCase")]
+pub struct MachineClaim {
+    pub kind: MachineClaimKind,
+    /// Exact regular Rust source file in the immutable repository tree.
+    pub path: String,
+    /// Exact `crate::`-qualified type, item, trait member, or inherent method.
+    pub symbol: String,
+    #[serde(skip_serializing_if = "Option::is_none", default)]
+    pub expected_signature: Option<MachineSignature>,
+}
+
+#[derive(Debug, Clone, Copy, Default, PartialEq, Eq, Serialize, Deserialize)]
+#[serde(rename_all = "camelCase")]
+pub enum ClaimVerificationState {
+    Complete,
+    Exhausted,
+    #[default]
+    Unavailable,
+}
+
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
+#[serde(rename_all = "camelCase")]
+pub enum ClaimVerificationVerdict {
+    Supported,
+    Refuted,
+    Unresolved,
+    Unsupported,
+}
+
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
+#[serde(rename_all = "camelCase")]
+pub enum ClaimEvidenceRole {
+    CopyDerive,
+    CopyImplementation,
+    SymbolDefinition,
+    Signature,
+    SourceScope,
+}
+
+/// Hash-only source evidence. No repository source text is serialized.
+#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
+#[serde(rename_all = "camelCase")]
+pub struct ClaimVerificationEvidence {
+    pub role: ClaimEvidenceRole,
+    pub path_sha256: String,
+    pub source_sha256: String,
+    pub span_sha256: String,
+}
+
+#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
+#[serde(rename_all = "camelCase")]
+pub struct VerifiedMachineClaim {
+    pub claim_input_sha256: String,
+    pub verdict: ClaimVerificationVerdict,
+    #[serde(default, skip_serializing_if = "Vec::is_empty")]
+    pub evidence: Vec<ClaimVerificationEvidence>,
+}
+
+#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
+#[serde(rename_all = "camelCase")]
+pub struct ClaimVerificationReceipt {
+    pub verifier: String,
+    #[serde(skip_serializing_if = "Option::is_none", default)]
+    pub head_sha: Option<String>,
+    #[serde(skip_serializing_if = "Option::is_none", default)]
+    pub tree_sha256: Option<String>,
+    pub state: ClaimVerificationState,
+    #[serde(default, skip_serializing_if = "Vec::is_empty")]
+    pub claims: Vec<VerifiedMachineClaim>,
+}
+
 #[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
 #[serde(rename_all = "camelCase")]
 pub enum RepositoryClaimKind {
@@ -1182,6 +1299,10 @@ pub enum SuppressionReason {
     /// A repository-wide absence or mismatch claim was not supported by one
     /// complete immutable-head receipt, or a positive counterexample refuted it.
     RepositoryClaimUnsupported,
+    /// A deterministic exact-head source proof contradicted the claim.
+    MachineClaimRefuted,
+    /// The source verifier could not produce a bounded conclusive proof.
+    MachineClaimUnverified,
 }
 
 #[derive(Debug, Clone, Serialize, Deserialize)]
@@ -1580,6 +1701,10 @@ pub struct Envelope {
     /// mismatch claims. Historical v1 envelopes deserialize as unavailable.
     #[serde(default)]
     pub repository_search: RepositorySearchReceipt,
+    /// Bounded deterministic source verification for typed machine claims.
+    /// Historical v1 envelopes omit this additive field.
+    #[serde(skip_serializing_if = "Option::is_none", default)]
+    pub claim_verification: Option<ClaimVerificationReceipt>,
     /// False when any sent provider request can have unknown billed usage,
     /// including timeouts and ambiguous transport failures.
     #[serde(default)]
@@ -1628,6 +1753,9 @@ pub fn finding_blocks_gate(
     block_on_kinds: &[String],
     provider_error_is_advisory: bool,
 ) -> bool {
+    if finding.machine_claim_deferred {
+        return false;
+    }
     if fail_on.eq_ignore_ascii_case("never") {
         return false;
     }
@@ -1732,6 +1860,8 @@ pub(crate) fn incomplete_review_finding(reason: IncompleteReviewReason) -> Findi
         scorer_kind: None,
         scorer_reason: None,
         repository_claim: None,
+        machine_claim: None,
+        machine_claim_deferred: false,
     }
 }
 
@@ -1766,6 +1896,8 @@ pub fn operational_failure_finding(detail: &str) -> Finding {
         scorer_kind: None,
         scorer_reason: None,
         repository_claim: None,
+        machine_claim: None,
+        machine_claim_deferred: false,
     }
 }
 
@@ -1797,6 +1929,8 @@ pub fn fail_closed_finding(detail: &str) -> Finding {
         scorer_kind: None,
         scorer_reason: None,
         repository_claim: None,
+        machine_claim: None,
+        machine_claim_deferred: false,
     }
 }
 
@@ -1832,6 +1966,8 @@ pub fn narrated_risk_finding(summary: &str) -> Finding {
         scorer_kind: None,
         scorer_reason: None,
         repository_claim: None,
+        machine_claim: None,
+        machine_claim_deferred: false,
     }
 }
 
@@ -1856,6 +1992,8 @@ pub fn provider_error_finding(_detail: &str) -> Finding {
         scorer_kind: None,
         scorer_reason: None,
         repository_claim: None,
+        machine_claim: None,
+        machine_claim_deferred: false,
     }
 }
 
@@ -2028,6 +2166,8 @@ mod tests {
             scorer_kind: None,
             scorer_reason: None,
             repository_claim: None,
+            machine_claim: None,
+            machine_claim_deferred: false,
             title: "t".into(),
             body: "b".into(),
             evidence: None,
@@ -2381,6 +2521,25 @@ mod tests {
         assert_eq!(contextual_value["repositoryContext"]["claim"], "absence");
         assert!(contextual_value.get("repositoryClaim").is_none());
 
+        let mut machine_finding = finding(Severity::Warn, 0.8);
+        machine_finding.machine_claim = Some(MachineClaim {
+            kind: MachineClaimKind::RustCopyMoveOut,
+            path: "src/identity.rs".into(),
+            symbol: "crate::identity::IdentityFailure".into(),
+            expected_signature: None,
+        });
+        let machine_value = serde_json::to_value(&machine_finding).unwrap();
+        assert_eq!(machine_value["machineClaim"]["kind"], "rust.copy_move_out");
+        assert!(machine_value.get("machineClaimDeferred").is_none());
+        let mut legacy_machine_value = machine_value;
+        legacy_machine_value
+            .as_object_mut()
+            .unwrap()
+            .remove("machineClaim");
+        let legacy_machine_finding: Finding = serde_json::from_value(legacy_machine_value).unwrap();
+        assert!(legacy_machine_finding.machine_claim.is_none());
+        assert!(!legacy_machine_finding.machine_claim_deferred);
+
         let mut env = Envelope {
             version: 1,
             summary: String::new(),
@@ -2405,6 +2564,7 @@ mod tests {
             review_coverage: None,
             review_admission: None,
             repository_search: RepositorySearchReceipt::default(),
+            claim_verification: None,
             usage_accounting_complete: true,
             duration_ms: 0,
             base_sha: None,
@@ -2454,6 +2614,7 @@ mod tests {
             historical.repository_search.state,
             RepositorySearchState::Unavailable
         );
+        assert!(historical.claim_verification.is_none());
 
         v.as_object_mut().unwrap().remove("modelIncidents");
         let decoded: Envelope = serde_json::from_value(v).unwrap();