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
174 changes: 174 additions & 0 deletions dag/gunbc/floor/floor_materialization.dag
Original file line number Diff line number Diff line change
Expand Up @@ -206,3 +206,177 @@ fn floor_typecheck_store_materialization_without_provider() -> ValueMaterializat
providers: floor_typecheck_store_no_providers
)
}

// C3 — the HOST-PERSISTED tier over the SAME identity as C2. C2 discharges typed-module
// plurality inside ONE executor process; this row says where the value lives when that process is
// gone. The frame is UnboundedSiblingsFrame, not SharedStateFrame: recurring invocations of the
// fold on a runner host are successive siblings with no shared mutable state to rewire — there is
// no LCA process in which the repetition could have been carried, which is precisely the ladder's
// isolation-LCA obligation that only a STORE tier can discharge. ArtifactTier, not CasTier:
// tier_axes assigns CasTier the RemoteNetwork placement, and this store is a host-local directory
// (LocalFilesystem) — the same axis reading that puts extdeps.realization.resolved_graph's
// per-host content-addressed store at ArtifactTier.
//
// NOT A SECOND STORE BESIDE extdeps.realization.resolved_graph.resolved_graph_cache. That store is
// content-addressed and per-host too, and the question "why two" is the right one to ask. They key
// DIFFERENT COMPUTATIONS: resolved_graph_cache keys a whole entry's resolved graph by its closure
// subject, and this row keys ONE TYPED MODULE by its own content. The grains are not
// interchangeable — a one-module edit invalidates a whole closure subject and only that module and
// its dependents here, which is the entire reason a per-module grain buys anything the whole-graph
// grain does not. They also share the compiler-identity term rather than each deriving one
// (resolved_graph_cache transform_content_digest), which is the fnv1a64 dual-surface discipline
// applied: two providers, one identity authority, no second key scheme.

// WHAT THIS DELIVERS TODAY, named so the row is not read as more than it is: the typed-module
// content key's compiler-identity term is the running binary's content digest, and build.rs embeds
// the checkout's commit in that binary, so a rebuild at ANY new commit — including a corpus-only
// .dag commit — re-keys every entry. The relief therefore covers SAME-BUILD, CROSS-PROCESS reuse:
// the witness fold and the generated-artifact drift gate are two processes over one corpus running
// one built binary, and the second pays typecheck preparation again today. Cross-push reuse is a
// separate change to how compiler identity is derived and is NOT claimed by this row.

data floor_typecheck_store_persist_provider_id: String = "host_persisted_typecheck_store"

fn floor_runner_host_frame() -> std.materialization_ladder.Frame {
std.materialization_ladder.Frame { name: "runner-host", kind: UnboundedSiblingsFrame }
}

// The ladder refuses ReleasedNever with CapacityUnbounded (RetentionUnbounded) and with
// CapacityUnobserved (RetentionUnobserved), so a byte ceiling and an at-capacity disposition are
// OBLIGATIONS this row discharges rather than options it selects. ByteCapacity and not
// EntryCountCapacity: the ceiling that matters on a runner host is disk, and an entry bound over a
// payload whose size is not fixed establishes no byte bound. RefuseNewStore and not
// ReplaceExisting: replacement is a second mechanism with its own correctness surface, and this
// bridge does not need one — a full store declines publication, counts the refusal, and the run is
// merely cold. Its realization is shared_typecheck_store PersistentTypedStore, held in lockstep by
// persist_cap_matches_modeled_authority.

data floor_typecheck_store_persist_cap_bytes: ByteSize = byte_size(count: 8589934592)

data floor_typecheck_store_persist_provider: CacheProvider = provider_row(
id: floor_typecheck_store_persist_provider_id,
scope: [floor_runner_host_frame()],
coverage: CoversIdentities { identities: [floor_typecheck_store_identity] },
tier: ArtifactTier { keying: ContentKeyed },
retention: persistent_retention(capacity: CapacityBounded {
limit: ByteCapacity { limit: ExactLimit { value: floor_typecheck_store_persist_cap_bytes } },
at_capacity: RefuseNewStore
})
)

// The two sibling processes that each demand union-typecheck-store(dag,src/v2) over one corpus
// under one built binary. They execute apart by construction, so the repetition between them is
// not authored duplication a rewire could remove — their obligation LCA is the runner host, which
// is not a shared-state frame, and only a STORE tier reaches across it. The demand nature is
// PureComputation: same module text, same resolved dependency closure, same compiler binary ⇒ same
// typed result, which is what makes ContentKeyed reuse sound here without declaring any staleness
// envelope. Nothing is read from the world.

fn floor_witness_fold_process_frame() -> std.materialization_ladder.Frame {
std.materialization_ladder.Frame { name: "witness-fold-process", kind: SharedStateFrame }
}

fn floor_drift_gate_process_frame() -> std.materialization_ladder.Frame {
std.materialization_ladder.Frame { name: "drift-gate-process", kind: SharedStateFrame }
}

fn floor_typecheck_store_cross_process_demands() -> List<FrameDemand> {
[
FrameDemand {
identity: floor_typecheck_store_identity,
site: [floor_runner_host_frame(), floor_witness_fold_process_frame()],
nature: PureComputation
},
FrameDemand {
identity: floor_typecheck_store_identity,
site: [floor_runner_host_frame(), floor_drift_gate_process_frame()],
nature: PureComputation
}
]
}

data floor_typecheck_store_persist_providers: List<CacheProvider> = [floor_typecheck_store_persist_provider]

data floor_typecheck_store_no_cost_floor_exemptions: List<String> = []

fn floor_typecheck_store_persist_verdicts() -> List<LadderVerdict> {
materialization_ladder(
demands: floor_typecheck_store_cross_process_demands(),
providers: floor_typecheck_store_persist_providers,
cost_floor_exempt: floor_typecheck_store_no_cost_floor_exemptions
)
}

// RED CONTROLS. Each is the SAME demand set with exactly one obligation withdrawn from the
// provider, so the green above is green because the ladder looked and admitted it, never because
// nothing looked. Each red names the DISTINCT refusal it must produce, so a provider that fails
// for the wrong reason does not pass as the right one.

data floor_typecheck_store_persist_provider_unbounded: CacheProvider = provider_row(
id: floor_typecheck_store_persist_provider_id,
scope: [floor_runner_host_frame()],
coverage: CoversIdentities { identities: [floor_typecheck_store_identity] },
tier: ArtifactTier { keying: ContentKeyed },
retention: persistent_retention(capacity: CapacityUnbounded)
)

data floor_typecheck_store_persist_provider_unobserved: CacheProvider = provider_row(
id: floor_typecheck_store_persist_provider_id,
scope: [floor_runner_host_frame()],
coverage: CoversIdentities { identities: [floor_typecheck_store_identity] },
tier: ArtifactTier { keying: ContentKeyed },
retention: persistent_retention(capacity: CapacityUnobserved)
)

// Scope too narrow: the in-process row cannot answer a cross-process demand. A reference does not
// survive the process that holds it, which is the whole reason this tier exists — so the existing
// C2 provider, offered alone against these two demands, must REFUSE rather than appear to cover
// them.

fn floor_typecheck_store_persist_verdicts_unbounded() -> List<LadderVerdict> {
materialization_ladder(
demands: floor_typecheck_store_cross_process_demands(),
providers: [floor_typecheck_store_persist_provider_unbounded],
cost_floor_exempt: floor_typecheck_store_no_cost_floor_exemptions
)
}

fn floor_typecheck_store_persist_verdicts_unobserved() -> List<LadderVerdict> {
materialization_ladder(
demands: floor_typecheck_store_cross_process_demands(),
providers: [floor_typecheck_store_persist_provider_unobserved],
cost_floor_exempt: floor_typecheck_store_no_cost_floor_exemptions
)
}

// The scope control is the SAME store row with only its scope withdrawn to one process — not the
// C2 ReferenceTier share, which is not a store tier at all and would refuse for the unrelated
// reason that no store provider exists. Withdrawing one obligation at a time is what makes each
// red name its own refusal.

data floor_typecheck_store_persist_provider_process_scoped: CacheProvider = provider_row(
id: floor_typecheck_store_persist_provider_id,
scope: [floor_executor_process_frame()],
coverage: CoversIdentities { identities: [floor_typecheck_store_identity] },
tier: ArtifactTier { keying: ContentKeyed },
retention: persistent_retention(capacity: CapacityBounded {
limit: ByteCapacity { limit: ExactLimit { value: floor_typecheck_store_persist_cap_bytes } },
at_capacity: RefuseNewStore
})
)

fn floor_typecheck_store_persist_verdicts_process_scoped() -> List<LadderVerdict> {
materialization_ladder(
demands: floor_typecheck_store_cross_process_demands(),
providers: [floor_typecheck_store_persist_provider_process_scoped],
cost_floor_exempt: floor_typecheck_store_no_cost_floor_exemptions
)
}

fn floor_typecheck_store_persist_verdicts_without_provider() -> List<LadderVerdict> {
materialization_ladder(
demands: floor_typecheck_store_cross_process_demands(),
providers: floor_typecheck_store_no_providers,
cost_floor_exempt: floor_typecheck_store_no_cost_floor_exemptions
)
}
79 changes: 77 additions & 2 deletions dag/test/claim/floor/floor_materialization_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -14,11 +14,23 @@ import gunbc.floor_materialization {
floor_typecheck_store_share_provider_id,
floor_typecheck_store_materialization,
floor_typecheck_store_materialization_without_provider,
floor_typecheck_store_reader_count
floor_typecheck_store_reader_count,
floor_typecheck_store_persist_provider_id,
floor_typecheck_store_persist_verdicts,
floor_typecheck_store_persist_verdicts_unbounded,
floor_typecheck_store_persist_verdicts_unobserved,
floor_typecheck_store_persist_verdicts_process_scoped,
floor_typecheck_store_persist_verdicts_without_provider
}
import std.materialization_ladder {
LadderVerdict,
value_verdict_is_shared_by_reference,
value_verdict_is_refused_needing_reference
value_verdict_is_refused_needing_reference,
verdict_is_discharged_by,
verdict_is_refused_retention_unbounded,
verdict_is_refused_retention_unobserved,
verdict_is_refused_scope_too_narrow,
verdict_is_refused_no_provider
}
import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }

Expand Down Expand Up @@ -75,3 +87,66 @@ test fn floor_typecheck_store_reds_without_reference_provider() -> Bool {
identity: floor_typecheck_store_identity
)
}

// C3 — the HOST-PERSISTED tier. The demand set is the two sibling PROCESSES over one corpus under
// one built binary (the witness fold and the generated-artifact drift gate), whose obligation LCA
// is the runner host. That LCA is not shared state, so the repetition is not a rewire the ladder
// would refuse; it is the isolation obligation only a store tier discharges. Four REDs follow, one
// per withdrawn obligation, each naming the DISTINCT refusal it must produce — so the green is
// green because the ladder admitted this provider, and a provider failing for another reason
// cannot pass as this one.

fn first_persist_verdict(vs: List<LadderVerdict>) -> LadderVerdict? {
vs.first()
}

test fn floor_typecheck_store_persist_is_discharged() -> Bool {
match first_persist_verdict(vs: floor_typecheck_store_persist_verdicts()) {
Absent => false
Present { value: v } =>
verdict_is_discharged_by(
v: v,
identity: floor_typecheck_store_identity,
provider_id: floor_typecheck_store_persist_provider_id
)
}
}

// The ladder refuses ReleasedNever with CapacityUnbounded. Without this red, a persistent provider
// with no ceiling would read as discharged and the boundedness obligation would be decoration.
test fn floor_typecheck_store_persist_reds_when_unbounded() -> Bool {
match first_persist_verdict(vs: floor_typecheck_store_persist_verdicts_unbounded()) {
Absent => false
Present { value: v } =>
verdict_is_refused_retention_unbounded(v: v, provider_id: floor_typecheck_store_persist_provider_id)
}
}

// And refuses ReleasedNever with CapacityUnobserved: a ceiling nobody measures is not a ceiling.
test fn floor_typecheck_store_persist_reds_when_occupancy_unobserved() -> Bool {
match first_persist_verdict(vs: floor_typecheck_store_persist_verdicts_unobserved()) {
Absent => false
Present { value: v } =>
verdict_is_refused_retention_unobserved(v: v, provider_id: floor_typecheck_store_persist_provider_id)
}
}

// The same store row scoped to ONE PROCESS, offered against a CROSS-PROCESS demand, must refuse as
// scope-too-narrow. This is the discriminating red for the whole tier: if it passed, the
// process-scoped provider would be answering a cross-process question, and C3 would be redundant
// with C2 rather than reaching a boundary C2 cannot.
test fn floor_typecheck_store_persist_reds_when_only_process_scoped() -> Bool {
match first_persist_verdict(vs: floor_typecheck_store_persist_verdicts_process_scoped()) {
Absent => false
Present { value: v } =>
verdict_is_refused_scope_too_narrow(v: v, provider_id: floor_typecheck_store_persist_provider_id)
}
}

test fn floor_typecheck_store_persist_reds_without_any_provider() -> Bool {
match first_persist_verdict(vs: floor_typecheck_store_persist_verdicts_without_provider()) {
Absent => false
Present { value: v } =>
verdict_is_refused_no_provider(v: v, identity: floor_typecheck_store_identity)
}
}
Loading