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
4 changes: 3 additions & 1 deletion dag/gunbc/ci_materialization.dag
Original file line number Diff line number Diff line change
Expand Up @@ -170,7 +170,9 @@ data ci_floor_resolve_receipt_note: String = "The counted cold-resolve receipt o

data ci_floor_resolve_receipt_path: String = "target/floor-resolve-receipt.txt"

data ci_floor_declared_resolve_count: Nat = 1
data ci_floor_declared_resolve_count: Nat = 2

data ci_floor_native_batch_resolve_receipt_note: String = "RECEIPT 9 — CONSCIOUS RAISING 1 -> 2 (2026-08-02, native-bundle production enrollment): CI run 30767841790 refused exactly `floor resolve count 2 differs from declared 1` and wrote target/floor-resolve-receipt.txt with resolves_total=2, resolve_ms_total=79064. The cause is the empirical law above operating as designed: gunbc_pr_native_batch enrolls as a RunnableSingleClaim on its own entry file (src/v2/test/claim/pr_native_batch_test.dag), an entry class whose closure escapes the batch-1 whole-tree materialization, so it pays its own cold resolve — 1 anchor + 1 escaping entry = 2. Same run: the batch itself PASSED via the counted outage fallback (verdict fallback:native_realization_refused, transport causes located), so the resolve count is the sole finalization refusal. Ratchet direction unchanged: the persistent content-keyed store still owes the permanent pin at 1, and de-enrolling the native batch (or pooling its closure warm) lowers this row consciously in the PR that does it."

data floor_finalization_note: String = "The CI floor's post-batch contract, and it lives HERE rather than in std.realization_schedule because it is a fact about THIS floor's duplicate-computation budget, not about walks in general (review 2026-07-30): the generic carrier takes it as a type parameter, so gunbc_ci_floor_plan returns WalkPlan<FloorFinalization> and every other plan returns WalkPlan<NoWalkFinalization>. WHAT THAT BUYS, narrowly: the signature DECLARES which finalization family each plan intends, and the std-level coproduct fork is gone. It is NOT a construction wall today — probed by execution, the typechecker does not check a declared return type against the body, so a plan can still return the wrong family and typecheck. Until return-position and annotated-data checking are grounded, the enrolled value witnesses and the executor's parser are the wall; the witnesses dissolve when that checking lands (std.realization_schedule walk_finalization_note carries the probe and the dissolve-on).

Expand Down
5 changes: 4 additions & 1 deletion dag/gunbc/ci_spec.dag

Large diffs are not rendered by default.

3 changes: 2 additions & 1 deletion dag/gunbc/merge_admission.dag
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ import gunbc.commit_workflow {
CommitSpecGate, CommitWitnessClaim, CommitCargoFmtCheck,
}
import std.realization_schedule {
WitnessKind, CorpusWitnessKind, ExecutionWitnessKind,
WitnessKind, CorpusWitnessKind, ExecutionWitnessKind, NativeBundleWitnessKind,
WitnessSeam, WitnessSpan, SpanUndeclared, SpanSeams,
}
import gunbc.ci_gate {
Expand Down Expand Up @@ -127,6 +127,7 @@ fn witness_kind_content_hash_structural(kind: WitnessKind) -> Fnv1a64Structural
match kind {
CorpusWitnessKind => content_hash_atom(value: "CorpusWitnessKind")
ExecutionWitnessKind => content_hash_atom(value: "ExecutionWitnessKind")
NativeBundleWitnessKind => content_hash_atom(value: "NativeBundleWitnessKind")
}
}

Expand Down
21 changes: 19 additions & 2 deletions dag/std/realization_schedule.dag
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,7 @@ type RealizationObjective {
type WitnessKind
= CorpusWitnessKind
| ExecutionWitnessKind
| NativeBundleWitnessKind

type WitnessSeam {
producer: String
Expand All @@ -72,8 +73,21 @@ type WitnessSpan

fn witness_kind_eq(a: WitnessKind, b: WitnessKind) -> Bool {
match a {
CorpusWitnessKind => match b { CorpusWitnessKind => true ExecutionWitnessKind => false }
ExecutionWitnessKind => match b { ExecutionWitnessKind => true CorpusWitnessKind => false }
CorpusWitnessKind => match b {
CorpusWitnessKind => true
ExecutionWitnessKind => false
NativeBundleWitnessKind => false
}
ExecutionWitnessKind => match b {
ExecutionWitnessKind => true
CorpusWitnessKind => false
NativeBundleWitnessKind => false
}
NativeBundleWitnessKind => match b {
NativeBundleWitnessKind => true
CorpusWitnessKind => false
ExecutionWitnessKind => false
}
}
}

Expand Down Expand Up @@ -287,6 +301,7 @@ fn scoped_witness_kind_label(kind: WitnessKind) -> String {
match kind {
CorpusWitnessKind => "corpus"
ExecutionWitnessKind => "execution"
NativeBundleWitnessKind => "native-bundle"
}
}

Expand All @@ -295,6 +310,8 @@ fn scoped_witness_kind_from_label(label: String) -> WitnessKind? {
Present { value: CorpusWitnessKind }
} else if label == "execution" {
Present { value: ExecutionWitnessKind }
} else if label == "native-bundle" {
Present { value: NativeBundleWitnessKind }
} else {
none
}
Expand Down
53 changes: 53 additions & 0 deletions dag/std/selected_witness_bundle.dag
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ module std.selected_witness_bundle

import std.types { NonEmptyStr, List, Int, Bool }
import std.verification { NanosecondDuration }
import std.measure { ByteSize }
import std.content_hash {
Fnv1a64Structural,
content_hash_atom,
Expand Down Expand Up @@ -313,6 +314,58 @@ type NativeWitnessBundleExecutionReceipt {
interpreter_frontier_count: Int
}

type NativeProductionTransitionVerdict
= NativeProductionTransitionAccepted
| NativeProductionTransitionFallback { cause: NativeUnavailableCause }
| NativeProductionTransitionRefused { reason: NonEmptyStr }

type NativeWitnessProductionTransitionReceipt {
selected_count: Int
native_count: Int
interpreted_count: Int
unavailable_count: Int
bundle_count: Int
shard_count: Int
cold_compile_wall_nanos: NanosecondDuration
warm_artifact_hit_wall_nanos: NanosecondDuration
native_execution_wall_nanos: NanosecondDuration
interpreter_oracle_wall_nanos: NanosecondDuration
fallback_count: Int
rss_peak_bytes: ByteSize
cgroup_peak_bytes: ByteSize
verdict: NativeProductionTransitionVerdict
planted_red_equivalent: Bool
}

data native_production_transition_population_note: String = "🟡 The population law is a VALIDATOR over the flat-count receipt (review 47496): counts and verdict are authored separately, so an inconsistent pair is representable and this fn is what discriminates it. Executing consumers: the witness-unit controls in v2.test.claim.pr_native_batch_test — an accepted positive control plus discriminating REDs per verdict arm, enrolled in per-PR discovery. The seed's TSV transition-receipt projection does not yet route through this law; that wire belongs to native_selected_bundle_process_seed_deferral. dissolve-on: counts carried on the verdict variants so an inconsistent receipt is unwritable, or the executor walk emitting receipts from .dag — whichever lands first; then this validator and this note delete together."

fn native_production_transition_population_holds(
receipt: NativeWitnessProductionTransitionReceipt
) -> Bool {
receipt.selected_count > 0
&& receipt.bundle_count == 1
&& receipt.shard_count == 1
&& receipt.native_count >= 0
&& receipt.interpreted_count >= 0
&& receipt.unavailable_count >= 0
&& receipt.fallback_count >= 0
&& match receipt.verdict {
NativeProductionTransitionAccepted =>
receipt.native_count == receipt.selected_count
&& receipt.interpreted_count == 0
&& receipt.unavailable_count == 0
&& receipt.fallback_count == 0
NativeProductionTransitionFallback { cause: _ } =>
receipt.native_count + receipt.interpreted_count == receipt.selected_count
&& receipt.unavailable_count == receipt.fallback_count
&& receipt.fallback_count <= receipt.interpreted_count
NativeProductionTransitionRefused { reason: _ } =>
receipt.native_count + receipt.interpreted_count <= receipt.selected_count
&& receipt.unavailable_count <= receipt.selected_count
&& receipt.fallback_count <= receipt.interpreted_count
}
}

type NativeBundleFamilyCutoverEvidence {
planted_plan: SelectedWitnessPlan
execution: NativeWitnessBundleExecutionReceipt
Expand Down
Loading
Loading