Skip to content
Closed
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
8 changes: 5 additions & 3 deletions dag/extdeps/transports/rest.dag
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
module extdeps.transports.rest

import std.types { HttpMethod, GET, POST, PUT, PATCH, DELETE, HEAD, OPTIONS, FermiDepth, NonEmptyStr, HttpStatus, Bool, String, Int, List }
import std.content_hash { ContentHash }
import std.content_hash { Fnv1a64Structural }
import std.serialization { WireFormat }
import std.fidelity { TransportFidelity }
import std.effect_grant { Envelope, HandlerBinding, Read, Write, CoveredBy, NoCoveringGrant, covering_grant, NamespacePosition, ServiceOpTree }
Expand Down Expand Up @@ -78,15 +78,17 @@ type RestExchangeObservation

type RestAuthSensitiveIdentity
= RestUnauthenticated
| RestAuthenticated { scheme: NonEmptyStr, digest: ContentHash }
| RestAuthenticated { scheme: NonEmptyStr, digest: Fnv1a64Structural }

data rest_authenticated_digest_witness_note: String = "AUTHENTICATED ARM: EXECUTED PIN, REPLAY-PATH DEFERRAL TYPED (review 47041, gunbc#7648). RestAuthenticated.digest is Fnv1a64Structural and the seed mint rest_auth_identity_value produces it via atom_identity_hash over '<scheme>\\0<secret>' - the SAME fnv1a64 primitive std.content_hash.content_hash_atom realizes, so an authored fixture reproduces the digest through the modeled surface (content_hash_atom(value: \"<scheme>\\0<secret>\")); an earlier spelling hashed with the host DefaultHasher, a value from outside the family this carrier names, which no dag fixture could ever author. EXECUTED EVIDENCE: rest_authenticated_identity_matches_dag_constructed_value (src/v1/tests/src/cross_representation_equality_test.rs) pins the seed mint ==-equal to the dag-authored identity - RED under a bare-text digest, RED under a non-fnv1a64 digest - plus a secret-inequality control. WHAT REMAINS DEFERRED, AND WHY, TYPED: a full replay-path authenticated witness (fixture matched against a seed-produced invocation through the service dispatch) additionally requires the invocation input_digest, whose per-param limbs content_hash_service_inputs still derives via the host value_hash - not reproducible from .dag - so authoring the matching fixture is blocked on that limb pipeline migrating to the fnv1a64 primitives; that migration also moves the recorded-fixture store keys, so it is its own lane, not a fixture edit here. RUNG, CORRECTED FOR CI ENROLLMENT (calm-badger-682, verified against .github/workflows/ci.yml and gunbc.ci_layer_roots witness_layer_roots): the pin executes LOCALLY and is enrolled in NO executing CI path, so it is evidence a human can run rather than a mechanism that blocks. CI's only contact with that crate is the step named 'cargo check -p v1-compiler-tests --tests (compile gate; no test execution)', and witness_layer_roots is dag plus src/v2, so floor discovery never reaches src/v1/tests either; measured, the pin passes locally in 1.66s and reds nothing anywhere. DESIGN 4b defines mechanically preventable as a mechanism that reliably exposes AND blocks, with safety depending on it executing and staying enrolled - so the mint seam sits BELOW that rung, and calling it mechanically prevented is rung inflation, which 4b names as worse than sitting low because an inflated class never ranks for climbing. Deleting the seam guard would leave this control present, compiling, and mute. NOT NEW DEBT FROM THIS PR: content_hash_cross_family_eq_v1_seed_bridge_note cites the same unexecuted crate for the cross-family backstop, so the whole family of seed-bridge controls shares this gap and it is recorded here rather than fixed. The end-to-end authenticated replay path remains unexecuted and must not be reported above either. HAND-RUST RECEIPT (review 47065): the ROADMAP row 'Work through the remaining hand-written files the products need' (authority dag/gunbc/v1_deletion_plan.dag, v1-hand-queue-drain lane) owns the interim seed bridge in rest_auth_identity_value, fnv1a64_structural_value, and rest_authenticated_identity_for_witness. DISSOLVE-ON: that row migrates REST invocation construction out of v1_interpreter; the checkable receipt is deletion of those three hand-Rust symbols while this discriminating equality/inequality witness remains enrolled against the replacement realization. Independently, the input-digest limb migration lands and an authenticated replay witness executes against a seed-produced invocation; this note then deletes."

data rest_bound_invocation_note: String = "REST needs a specialization of v2.std.operation_argv.BoundOperationInvocation rather than pretending its shell-only binding list is enough. OperationRef remains the declaration identity authority. The specialization adds the HTTP method, fully realized URI target, the digest of every declared input, and an auth-sensitive digest whose preimage never enters the fixture. Together those facts make a replay exact: a fixture for another operation, path/query/body input, method, target, or credential identity cannot satisfy this invocation. Query and body values are already in the declared-input digest; constants are fixed by OperationRef."

type RestBoundOperationInvocation {
at: OperationRef
method: HttpMethod
target: Uri
input_digest: ContentHash
input_digest: Fnv1a64Structural
auth_identity: RestAuthSensitiveIdentity
}

Expand Down
6 changes: 2 additions & 4 deletions dag/test/claim/rest_exchange_replay_test.dag
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
module test.claim.rest_exchange_replay_test

import std.types { Bool, String, List, GET }
import std.content_hash { as_content_hash_structural, structural_content_hash }
import std.content_hash { Fnv1a64Structural }
import std.materialization_ladder { Frame, SharedStateFrame }
import std.effect_grant {
Read, ServiceOpTree, NamespacePosition,
Expand Down Expand Up @@ -42,9 +42,7 @@ fn probe_invocation(operation: String) -> RestBoundOperationInvocation {
}
method: GET
target: probe_target
input_digest: as_content_hash_structural(
structural: structural_content_hash(digest: "0000000000000000")
)
input_digest: Fnv1a64Structural { digest: "0000000000000000" }
auth_identity: RestUnauthenticated
}
}
Expand Down
79 changes: 48 additions & 31 deletions src/v1/stage0/src/v1_interpreter.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7868,22 +7868,59 @@ fn rest_auth_identity_value(
Some((scheme, secret)) => {
// Only the hash crosses into the authored fixture carrier. The secret is
// never persisted in, or made displayable through, a replay identity.
let digest = format!(
"{:016x}",
value_hash_public(&Value::Str(format!("{}\0{}", scheme, secret)))
);
//
// The digest is minted through `v1_rt::atom_identity_hash` — the SAME fnv1a64
// primitive `std.content_hash.content_hash_atom` is realized by — for two
// load-bearing reasons: (1) the model types `RestAuthenticated.digest` as
// `Fnv1a64Structural`, and a `DefaultHasher` (SipHash) hex here would be a value
// from outside that family wearing the family's carrier (the labeling the
// constructor-wall note forbids); (2) an authored fixture can reproduce this
// digest through the modeled surface — `content_hash_atom(value:
// "<scheme>\0<secret>")` — so authenticated replay identities are expressible
// in .dag without pinning opaque literals. Pinned by
// `rest_authenticated_identity_matches_dag_constructed_value` in
// src/v1/tests/src/cross_representation_equality_test.rs.
let digest = v1_rt::atom_identity_hash(format!("{}\0{}", scheme, secret));
Value::Variant {
type_name: ctx.sym("RestAuthSensitiveIdentity"),
variant_name: ctx.sym("RestAuthenticated"),
fields: Rc::new(sorted_fields(vec![
(ctx.sym("scheme"), Value::Str(scheme)),
(ctx.sym("digest"), Value::Str(digest)),
(ctx.sym("digest"), fnv1a64_structural_value(digest, ctx)),
])),
}
}
}
}

/// The runtime `Value` shape of `std.content_hash.Fnv1a64Structural` — the single mint
/// for every seed-side crossing into a `Fnv1a64Structural`-typed carrier of the REST
/// replay model (`RestBoundOperationInvocation.input_digest`, `RestAuthenticated.digest`).
/// A bare `Value::Str` at either position is the model↔realization fork: fixture matching
/// compares a record against a string and silently never matches (DESIGN §5).
fn fnv1a64_structural_value(digest: String, ctx: &InterpContext) -> Value {
Value::Record {
type_name: ctx.sym("Fnv1a64Structural"),
fields: Rc::new(sorted_fields(vec![(ctx.sym("digest"), Value::Str(digest))])),
}
}

/// Witness export: lets the tests crate pin `rest_auth_identity_value`'s authenticated arm
/// `==`-equal to a dag-authored `RestAuthenticated { scheme, digest: content_hash_atom(…) }`,
/// so a drift on either side of the seam (mint shape, hash family, or preimage layout) goes
/// red instead of silently failing every authenticated fixture match.
#[cfg(any(test, feature = "interp_test_witness"))]
pub fn rest_authenticated_identity_for_witness(token: &str, ctx: &InterpContext) -> Value {
rest_auth_identity_value(
&AuthResolution::Resolved {
header: "Authorization".to_string(),
token: token.to_string(),
},
None,
ctx,
)
}

fn rest_uri_value(url: &str, ctx: &InterpContext) -> InterpResult<Value> {
let (scheme, locator) = if let Some(locator) = url.strip_prefix("https://") {
("Https", locator)
Expand All @@ -7903,31 +7940,6 @@ fn rest_uri_value(url: &str, ctx: &InterpContext) -> InterpResult<Value> {
})
}

/// Seed bridge for the `.dag`-owned `ContentHash` family carrier. REST input identity is
/// the structural FNV-1a digest produced by `content_hash_service_inputs`; the interpreter
/// must realize that modeled value, not leak its wire string across the typed dispatch seam.
///
/// This is the model↔realization fork DESIGN's open threads name: `#7480` made `ContentHash`
/// a coproduct in `.dag` while this site kept minting the pre-#7480 branded string, so a
/// fixture invocation built in `.dag` could never equal one built here. Every
/// `rest_exchange_replay` witness that requires a fixture to MATCH failed; the ones requiring
/// no match passed, which is the signature of an equality that is always false rather than of
/// a broken lookup. Recovered from the closed PR #7650, which had this right.
///
/// DISSOLVE-ON: REST service dispatch is evaluated by the emitted transport handler and this
/// host-side `RestBoundOperationInvocation` construction is deleted.
fn rest_structural_content_hash_value(digest: String, ctx: &InterpContext) -> Value {
let structural = Value::Record {
type_name: ctx.sym("Fnv1a64Structural"),
fields: Rc::new(sorted_fields(vec![(ctx.sym("digest"), Value::Str(digest))])),
};
Value::Variant {
type_name: ctx.sym("ContentHash"),
variant_name: ctx.sym("Fnv1a64"),
fields: Rc::new(vec![(ctx.sym("0"), structural)]),
}
}

fn rest_bound_invocation_value(
service_node: &Rc<Node>,
op_node: &Rc<Node>,
Expand All @@ -7951,7 +7963,12 @@ fn rest_bound_invocation_value(
(ctx.sym("target"), rest_uri_value(url, ctx)?),
(
ctx.sym("input_digest"),
rest_structural_content_hash_value(input_digest, ctx),
// Grounding, gunbc#7480 Phase A: RestBoundOperationInvocation.input_digest is
// modelled as std.content_hash Fnv1a64Structural (the structural family member
// content_hash_service_inputs actually produces), not as bare text. The realization
// must construct the SAME shape the model declares, or fixture matching compares a
// record against a string and silently never matches -- the model/realization fork.
fnv1a64_structural_value(input_digest, ctx),
),
(
ctx.sym("auth_identity"),
Expand Down
79 changes: 77 additions & 2 deletions src/v1/tests/src/cross_representation_equality_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,9 +6,18 @@ use v1_compiler::v1_interpreter::{self, ExecutionMode, InterpError, Value};

use crate::helpers::{resolve_imports_transitively_with_source_roots, workspace_root};

// Every dag source in this file imports `std.occurrence_identity` even though no test
// references it directly: the closures all reach `v2.std.node`, whose occurrence facade
// references `std.occurrence_identity.*` by bare namespace path (no import), and this
// helper's pool is import-driven — the bare references bind only if something drags the
// module into the pool (the #6985 Class-B pool-membership shape, used here deliberately).
// Without it every ctx in this module fails resolution with "unresolved type
// 'std.occurrence_identity.…'" — which is how the whole module sat red, unnoticed
// because the rust suite is local-only (CI removed 2026-07-11).
const RECEIPTS_SOURCE: &str = r#"
module test.xrepr

import std.occurrence_identity
import v2.std.logic { Bool }
import v2.std.nat { Nat, Succ, Zero, nat_add }
import v2.std.algebra { Cons, Empty }
Expand Down Expand Up @@ -38,7 +47,15 @@ fn assert_resolved(resolved: &ResolvedPipelineResult) {
.diagnostics
.iter()
.map(|d| v1_compiler::v1_std_core::diagnostic_to_message(d.diagnostic.clone()))
.filter(|m| !m.starts_with("complexity: ") && !m.starts_with("unlisted import use "))
// `where-refinement unenforced:` is filtered for the same reason
// `assert_content_hash_resolved` filters it: std.content_hash's refined hex
// carriers entered every closure via v2.std.node, and those advisory rows are
// not what these witnesses discriminate.
.filter(|m| {
!m.starts_with("complexity: ")
&& !m.starts_with("unlisted import use ")
&& !m.starts_with("where-refinement unenforced:")
})
.collect();
assert!(
msgs.is_empty() && resolved.graph.is_some(),
Expand Down Expand Up @@ -126,6 +143,7 @@ fn genuine_inequalities_stay_false_not_errors() {
const CALL_CONTRACT_SOURCE: &str = r#"
module v2.test.callcontract

import std.occurrence_identity
import v2.std.logic { Bool }

fn takes_tag(tag: Bool) -> Bool { tag }
Expand All @@ -143,7 +161,11 @@ fn assert_call_contract_resolved(resolved: &ResolvedPipelineResult) {
.diagnostics
.iter()
.map(|d| v1_compiler::v1_std_core::diagnostic_to_message(d.diagnostic.clone()))
.filter(|m| !m.starts_with("complexity: ") && !m.starts_with("unlisted import use "))
.filter(|m| {
!m.starts_with("complexity: ")
&& !m.starts_with("unlisted import use ")
&& !m.starts_with("where-refinement unenforced:")
})
.collect();
assert!(
msgs.is_empty() && resolved.graph.is_some(),
Expand Down Expand Up @@ -217,17 +239,34 @@ fn valid_application_sites_are_unaffected() {
const CONTENT_HASH_CROSS_FAMILY_SOURCE: &str = r#"
module test.contenthashxfamily

import std.occurrence_identity
import std.content_hash {
ContentHash,
Sha256Digest,
Sha256DigestHex,
content_hash_of_value,
content_hash_atom,
as_content_hash_cryptographic,
content_hash_eq_structural,
}
import std.types { Bool }
import extdeps.transports.rest { RestAuthSensitiveIdentity, RestAuthenticated }

data structural: ContentHash = content_hash_of_value(value: "fp-a")

fn authed_identity() -> RestAuthSensitiveIdentity {
RestAuthenticated {
scheme: "BearerToken"
digest: content_hash_atom(value: "BearerToken\0test-replay-token")
}
}

fn other_token_identity() -> RestAuthSensitiveIdentity {
RestAuthenticated {
scheme: "BearerToken"
digest: content_hash_atom(value: "BearerToken\0other-token")
}
}
data sha256_row: ContentHash = as_content_hash_cryptographic(
digest: Sha256Digest {
hex: "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855" as Sha256DigestHex,
Expand Down Expand Up @@ -305,6 +344,42 @@ fn cross_family_content_hash_bare_eq_refuses() {
});
}

/// Discriminating witness for the authenticated half of the REST replay identity seam
/// (gunbc#7648, second finding — review 47017 item 1 on #7650). The model types
/// `RestAuthenticated.digest` as `Fnv1a64Structural`; before this pin the seed minted
/// `(sym("digest"), Value::Str(<DefaultHasher hex>))` — a bare string OUTSIDE the fnv1a64
/// family, so no dag-authored authenticated fixture could ever match a runtime invocation
/// (the same silent-false fork as `input_digest`, one field over, invisible to the 9/9
/// unauthenticated replay witnesses).
///
/// RED under either half of the old mint: a `Value::Str` digest fails the shape equality;
/// a DefaultHasher digest fails the value equality against the modeled
/// `content_hash_atom("<scheme>\0<secret>")` chain. The inequality arm guards that the
/// digest actually discriminates secrets (a constant digest would pass the first assert
/// on the wrong grounds).
#[test]
fn rest_authenticated_identity_matches_dag_constructed_value() {
with_content_hash_ctx(|ctx| {
let dag_side = v1_interpreter::run_in_context(ctx, "authed_identity", false)
.expect("authed_identity must evaluate");
let seed_side =
v1_interpreter::rest_authenticated_identity_for_witness("test-replay-token", ctx);
assert_eq!(
dag_side, seed_side,
"seed authenticated-identity mint diverged from the dag-authored \
RestAuthenticated (content_hash_atom digest); every authenticated replay \
fixture would silently fail to match its runtime invocation"
);
let other_token = v1_interpreter::run_in_context(ctx, "other_token_identity", false)
.expect("other_token_identity must evaluate");
assert_ne!(
other_token, seed_side,
"identities for different secrets must differ — a constant digest would make \
the equality arm above pass without discriminating credentials"
);
});
}

#[test]
fn cross_family_content_hash_homonym_variant_names_do_not_trigger_guard() {
with_content_hash_ctx(|ctx| {
Expand Down
Loading