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
14 changes: 14 additions & 0 deletions dag/extdeps/rust/cargo_build.dag
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,20 @@ service cargo.Build {
}
}

operation BuildManifestMessages {
input { workdir: FilePath, manifest_path: FilePath, target_dir: FilePath, extra_args: List<String> = [] }
output {
success: Bool from "exit_success"
stdout: String from "stdout"
stderr: String from "stderr"
}
transport shell { argv: ["env", "-C", "{workdir}", "CARGO_TARGET_DIR={target_dir}", "cargo", "build", "--message-format=json", "--manifest-path", "{manifest_path}", extra_args] }
exit {
0 => Unit
101 => String "Compilation failed"
}
}

operation Test {
input { extra_args: List<String> = [] }
output {
Expand Down
9 changes: 9 additions & 0 deletions dag/gunbc/ci_layer_roots.dag
Original file line number Diff line number Diff line change
Expand Up @@ -303,6 +303,11 @@ data witness_exclusion_frontier: List<WitnessExclusionRow> = [
classification: OfflineLocalRecipe,
reason: excl_wet_integration_reason,
dissolution: excl_wet_integration_dissolve},
WitnessExclusionRow {
pattern: "self_host_artifact_materialization_real_execution_witness_test.dag",
classification: BinWitnessWet,
reason: excl_bin_wet_reason,
dissolution: excl_bin_wet_dissolve},
WitnessExclusionRow {
pattern: "typed_witness_invocation_test.dag",
classification: BinWitnessWet,
Expand Down Expand Up @@ -990,6 +995,10 @@ data excl_no_fake_anomalies_dissolve: DissolutionCondition = unbound_dissolution
data install_media_real_execution_wet_note: String = "The four srv3_install_media_fetch_real_execution_witness_test.dag / srv3_seeded_install_media_real_execution_witness_test.dag entries at the tail of bin_witness_wet_entries below share this lane with the bin-execution witnesses (same RunnableDiscoveryBatch Wet mechanism, not a forked one - DESIGN §3) though they are not bin-execution: they drive real shell.Mktemp.Dir/Filesystem.Write/shell.Remove.RecursiveForce effects that dag/extdeps/shell/shell.dag has no mock_response for (only shell.Exec.Run/Check do), so the Hermetic discovery corpus refuses them by construction (typed 'no mock_response for operation Dir' error). Split out of their parent files (shell-to-dag B1, 2026-07-14) so the parent files' pure classification witnesses keep hermetic per-PR discovery undiminished. Dissolve-on: shell.dag's file-effect operations gain mock_response coverage AND these fns' assertions are re-checked for correctness under a fixed mock (some assert behavior-dependent outcomes, e.g. matched == false on a wrong hash, which a naive fixed mock would falsify) - then they re-enroll as ordinary hermetic discovery rows and these rows delete."

data bin_witness_wet_entries: List<ScheduleWitnessEntry> = [
bin_wet(entry: "dag/test/claim/self_host_artifact_materialization_real_execution_witness_test.dag", f: "a_real_cargo_build_materializes_through_the_real_digest"),
bin_wet(entry: "dag/test/claim/self_host_artifact_materialization_real_execution_witness_test.dag", f: "the_materialized_path_is_the_one_the_real_cargo_stream_named"),
bin_wet(entry: "dag/test/claim/self_host_artifact_materialization_real_execution_witness_test.dag", f: "a_target_the_build_never_produced_refuses_and_does_not_materialize"),
bin_wet(entry: "dag/test/claim/self_host_artifact_materialization_real_execution_witness_test.dag", f: "the_digest_is_of_the_file_cargo_named_not_of_some_other_real_file"),
bin_wet(entry: "dag/test/claim/dag_collect_fingerprint_witness_test.dag", f: "dag_collect_fingerprint_witness_keystone_holds"),
bin_wet(entry: "dag/test/claim/dag_compile_clean_perturb_receipts_test.dag", f: "perturb_optional_skew_fixture_red_holds"),
bin_wet(entry: "dag/test/claim/dag_compile_clean_perturb_receipts_test.dag", f: "perturb_unresolved_import_fixture_red_holds"),
Expand Down
225 changes: 225 additions & 0 deletions dag/gunbc/self_host_artifact_materialization.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,225 @@
module gunbc.self_host_artifact_materialization

import std.types { Bool, FilePath, Int, List, NonEmptyStr, String }
import extdeps.cargo_build
import std.content_hash { Sha512Digest }
import extdeps.cargo_message {
CargoArtifactSelection,
CargoArtifactSelected,
CargoArtifactAbsent,
CargoArtifactAmbiguous,
CargoArtifactWithoutExecutable,
CargoArtifactExecutablePathEmpty,
CargoArtifactExecutableNotAString,
CargoMessageExecutableAbsent,
CargoMessageLineUnparseable,
CargoMessageLineNotAnObject,
CargoMessageReasonAbsent,
CargoMessageReasonNotAString,
CargoMessageMemberDuplicated,
CargoMessageTargetNotAnObject,
CargoMessageTargetNameAbsent,
CargoMessageTargetNameNotAString,
cargo_select_artifact_executable
}
import extdeps.tools.sha512sum {
Sha512FileObservation,
Sha512FileObserved,
Sha512FileObservationRefused,
sha512sum_observe_file
}
import v2.compiler.self_host.generation {
ArtifactIdentity,
ArtifactMaterialized,
ArtifactNotMaterialized,
observed_artifact_digest
}

data artifact_materialization_subject_note: String = "SH-C: turning a cargo build into the artifact axis of a compiler generation, with no step that predicts a path instead of observing one. The chain is build -> the path cargo NAMED -> a digest of THAT path -> ArtifactIdentity. The load-bearing property is that the digest and every later execution consume ONE path value, produced by extdeps.cargo_message from cargo's own --message-format=json output. A convention-derived path breaks that at both ends simultaneously: it digests one file while executing another, with each operation individually honest and the composition silently wrong, and it also makes the artifact axis a FUNCTION of the build-configuration axis, collapsing two of the six independent axes v2.compiler.self_host.generation keeps apart."

data artifact_materialization_decomposition_note: String = "The decision logic is deliberately split into two PURE folds with a thin wet composition between them, rather than one wet function. select_artifact_path decides what the build reported; materialization_from_digest decides what the digest observation means. Both are total folds over typed inputs, so both are witnessed hermetically on every PR, and the only part that needs a wet cadence is the three service calls that produce their inputs. The alternative — one wet function carrying the decisions — would put every refusal arm behind a cadence that does not run per PR, which is how a decision nobody executes reads as a decision that holds."

data artifact_materialization_unbuilt_note: String = "There is NO arm here that yields ArtifactMaterialized without a digest observation in hand. That is the whole point of the carrier: v2.compiler.self_host.generation makes ObservedArtifactDigest a sole_constructor over a validated Sha512Digest precisely so an artifact identity cannot be authored, and this module is the first producer that has to respect it. Every failure — build nonzero, no artifact message, ambiguous target, unreadable stream, digest refused — lands on its own arm and projects ArtifactNotMaterialized, which promotion admission already refuses BY NAME rather than treating as equivalent."

type ArtifactPathOutcome
= ArtifactPathReported { executable: FilePath }
| ArtifactPathBuildFailed { target_name: String }
| ArtifactPathRefused { selection: CargoArtifactSelection }

type ArtifactMaterializationOutcome
= ArtifactMaterializationObserved {
executable: FilePath
digest: Sha512Digest
}
| ArtifactMaterializationBuildFailed { target_name: String }
| ArtifactMaterializationPathRefused { selection: CargoArtifactSelection }
| ArtifactMaterializationDigestRefused {
executable: FilePath
cause: NonEmptyStr
}

// A build that exited nonzero is its own arm and never reaches the stream decode.
// The distinction matters downstream: "the candidate did not build" and "the candidate
// built but we cannot say what it produced" have different remedies, and the brief this
// lane answers requires build failure to stay separate from every other refusal so a
// later behavioural comparison cannot read one as the other.
fn select_artifact_path(
build_success: Bool,
build_stdout: String,
target_name: String
) -> ArtifactPathOutcome {
if !build_success {
ArtifactPathBuildFailed { target_name: target_name }
} else {
match cargo_select_artifact_executable(
stdout: build_stdout,
target_name: target_name
) {
CargoArtifactSelected { executable: exe } =>
ArtifactPathReported { executable: exe }
CargoArtifactAbsent { target_name: t } =>
ArtifactPathRefused { selection: CargoArtifactAbsent { target_name: t } }
CargoArtifactAmbiguous { target_name: t, count: c } =>
ArtifactPathRefused {
selection: CargoArtifactAmbiguous { target_name: t, count: c }
}
CargoArtifactWithoutExecutable { target_name: t } =>
ArtifactPathRefused {
selection: CargoArtifactWithoutExecutable { target_name: t }
}
CargoArtifactExecutablePathEmpty { target_name: t, line_number: n } =>
ArtifactPathRefused {
selection: CargoArtifactExecutablePathEmpty { target_name: t, line_number: n }
}
CargoArtifactExecutableNotAString { target_name: t, line_number: n } =>
ArtifactPathRefused {
selection: CargoArtifactExecutableNotAString { target_name: t, line_number: n }
}
CargoMessageExecutableAbsent { line_number: n } =>
ArtifactPathRefused {
selection: CargoMessageExecutableAbsent { line_number: n }
}
CargoMessageLineUnparseable { line_number: n } =>
ArtifactPathRefused { selection: CargoMessageLineUnparseable { line_number: n } }
CargoMessageLineNotAnObject { line_number: n } =>
ArtifactPathRefused { selection: CargoMessageLineNotAnObject { line_number: n } }
CargoMessageReasonAbsent { line_number: n } =>
ArtifactPathRefused { selection: CargoMessageReasonAbsent { line_number: n } }
CargoMessageReasonNotAString { line_number: n } =>
ArtifactPathRefused { selection: CargoMessageReasonNotAString { line_number: n } }
CargoMessageMemberDuplicated { line_number: n, key: k } =>
ArtifactPathRefused {
selection: CargoMessageMemberDuplicated { line_number: n, key: k }
}
CargoMessageTargetNotAnObject { line_number: n } =>
ArtifactPathRefused { selection: CargoMessageTargetNotAnObject { line_number: n } }
CargoMessageTargetNameAbsent { line_number: n } =>
ArtifactPathRefused { selection: CargoMessageTargetNameAbsent { line_number: n } }
CargoMessageTargetNameNotAString { line_number: n } =>
ArtifactPathRefused {
selection: CargoMessageTargetNameNotAString { line_number: n }
}
}
}
}

// Takes the path the previous fold reported ALONGSIDE the observation made of that same
// path. The two parameters are not independent inputs a caller may mix: the wet
// composition below obtains the observation by digesting exactly this executable, and
// the executable is carried into the result so a consumer can prove the digest and any
// later invocation refer to one file.
fn materialization_from_digest(
executable: FilePath,
observation: Sha512FileObservation
) -> ArtifactMaterializationOutcome {
match observation {
Sha512FileObserved { digest: d } =>
ArtifactMaterializationObserved { executable: executable, digest: d }
Sha512FileObservationRefused { cause: c } =>
ArtifactMaterializationDigestRefused { executable: executable, cause: c }
}
}

fn materialization_outcome_from_path(
path: ArtifactPathOutcome,
observation: Sha512FileObservation
) -> ArtifactMaterializationOutcome {
match path {
ArtifactPathBuildFailed { target_name: t } =>
ArtifactMaterializationBuildFailed { target_name: t }
ArtifactPathRefused { selection: s } =>
ArtifactMaterializationPathRefused { selection: s }
ArtifactPathReported { executable: exe } =>
materialization_from_digest(executable: exe, observation: observation)
}
}

// The wet composition, and the ONLY function here that reaches the host. It is thin on
// purpose: it makes three service calls and carries no decision the two pure folds above
// do not already make, so the per-PR hermetic corpus keeps every arm under execution and
// the wet cadence only has to prove that the real cargo and the real sha512sum reach them.
//
// THE DIGEST IS TAKEN ONLY FOR A PATH CARGO REPORTED, and the match below is what makes
// that structural rather than a discipline: the non-reported arms have no executable to
// hand sha512sum, so they produce a refusal that says exactly that. Those arms discard it
// — materialization_outcome_from_path answers from the path alone — but the cause is true
// as written, so if a later edit ever did consult it the result stays fail-closed instead
// of naming a file nothing observed.
fn materialize_artifact_wet(
workdir: FilePath,
manifest_path: FilePath,
target_dir: FilePath,
target_name: String,
extra_args: List<String>
) -> ArtifactMaterializationOutcome {
let build = cargo.Build.BuildManifestMessages(
workdir: workdir,
manifest_path: manifest_path,
target_dir: target_dir,
extra_args: extra_args
)
let path = select_artifact_path(
build_success: build.success,
build_stdout: build.stdout,
target_name: target_name
)
let observation = match path {
ArtifactPathReported { executable: exe } => sha512sum_observe_file(path: exe)
ArtifactPathBuildFailed { target_name: _ } =>
Sha512FileObservationRefused {
cause: "no artifact path was reported, so no file was digested" as NonEmptyStr
}
ArtifactPathRefused { selection: _ } =>
Sha512FileObservationRefused {
cause: "no artifact path was reported, so no file was digested" as NonEmptyStr
}
}
materialization_outcome_from_path(path: path, observation: observation)
}

// The projection into the generation carrier. ArtifactMaterialized is reachable from
// exactly one arm, and only through observed_artifact_digest, whose argument is a
// Sha512Digest that existed only because sha512sum reported it for this path.
fn artifact_identity_of(outcome: ArtifactMaterializationOutcome) -> ArtifactIdentity {
match outcome {
ArtifactMaterializationObserved { executable: _, digest: d } =>
ArtifactMaterialized { digest: observed_artifact_digest(observed: d) }
ArtifactMaterializationBuildFailed { target_name: _ } => ArtifactNotMaterialized
ArtifactMaterializationPathRefused { selection: _ } => ArtifactNotMaterialized
ArtifactMaterializationDigestRefused { executable: _, cause: _ } =>
ArtifactNotMaterialized
}
}

// The executable a consumer may invoke, available ONLY when the artifact was observed.
// A consumer that wants to run the candidate takes the path from here, so the file it
// executes is the file that was digested, by construction rather than by discipline.
fn materialized_executable(outcome: ArtifactMaterializationOutcome) -> FilePath? {
match outcome {
ArtifactMaterializationObserved { executable: exe, digest: _ } =>
Present { value: exe }
ArtifactMaterializationBuildFailed { target_name: _ } => none
ArtifactMaterializationPathRefused { selection: _ } => none
ArtifactMaterializationDigestRefused { executable: _, cause: _ } => none
}
}
Loading
Loading