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
2 changes: 2 additions & 0 deletions dag/gunbc/ci_layer_roots.dag
Original file line number Diff line number Diff line change
Expand Up @@ -999,6 +999,8 @@ data bin_witness_wet_entries: List<ScheduleWitnessEntry> = [
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/self_host_artifact_materialization_real_execution_witness_test.dag", f: "changing_only_the_source_bytes_names_exactly_the_artifact_axis"),
bin_wet(entry: "dag/test/claim/self_host_artifact_materialization_real_execution_witness_test.dag", f: "rebuilding_identical_source_in_place_moves_no_axis"),
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
6 changes: 3 additions & 3 deletions dag/gunbc/self_host_artifact_materialization.dag
Original file line number Diff line number Diff line change
Expand Up @@ -29,13 +29,13 @@ import extdeps.tools.sha512sum {
sha512sum_observe_file
}
import v2.compiler.self_host.generation {
ArtifactIdentity,
GeneratedArtifactIdentity,
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_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 -> GeneratedArtifactIdentity. 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."

Expand Down Expand Up @@ -200,7 +200,7 @@ fn materialize_artifact_wet(
// 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 {
fn artifact_identity_of(outcome: ArtifactMaterializationOutcome) -> GeneratedArtifactIdentity {
match outcome {
ArtifactMaterializationObserved { executable: _, digest: d } =>
ArtifactMaterialized { digest: observed_artifact_digest(observed: d) }
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,17 @@ import extdeps.filesystem.filesystem_io
import extdeps.shell
import extdeps.cargo_build
import gunbc.self_host_artifact_materialization
import v2.compiler.self_host.generation {
ArtifactIdentity,
ArtifactMaterialized,
ArtifactNotMaterialized,
GenerationIdentity,
MaterializedArtifactAxis,
generation_axis_symbol,
generation_identity_mismatched_axes
}
import v2.std.algebra { for_all, length }
import v2.std.node { symbol_identity_digest }

data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree

Expand All @@ -28,6 +39,10 @@ type BuiltFixture
| FixtureSetupRefused { cause: String }

fn build_fixture_once(target_name: String) -> BuiltFixture {
build_fixture_from_source(target_name: target_name, main_source: crate_main)
}

fn build_fixture_from_source(target_name: String, main_source: String) -> BuiltFixture {
let dir = shell.Mktemp.Dir()
if !dir.success {
FixtureSetupRefused { cause: "mktemp -d failed" }
Expand All @@ -36,7 +51,7 @@ fn build_fixture_once(target_name: String) -> BuiltFixture {
let manifest = "{root}/Cargo.toml"
let main_rs = "{root}/main.rs"
let wrote_manifest = Filesystem.Write(path: manifest, content: crate_manifest)
let wrote_main = Filesystem.Write(path: main_rs, content: crate_main)
let wrote_main = Filesystem.Write(path: main_rs, content: main_source)
if !wrote_manifest.success || !wrote_main.success {
FixtureSetupRefused { cause: "fixture crate write failed" }
} else {
Expand Down Expand Up @@ -132,3 +147,149 @@ test fn the_digest_is_of_the_file_cargo_named_not_of_some_other_real_file() -> B
}
}
}

data crate_main_variant: String = "fn main() \{ println!(\"gunbc artifact axis fixture, second program\"); \}\n"

type TwoBuilds
= TwoBuilds { first: ArtifactIdentity, second: ArtifactIdentity }
| TwoBuildsSetupRefused { cause: String }

// MEASURED, and it is why both claims below build in ONE directory. A Rust debug binary
// embeds its build path, so the SAME source compiled in two different temp directories
// produces DIFFERENT bytes and therefore a different digest, while the same directory
// rebuilt produces byte-identical output. Verified directly: two mktemp dirs, one source,
// two digests; one dir built twice, one digest.
//
// THAT INVALIDATES THE OBVIOUS FIXTURE SHAPE. A claim that builds source A in dir 1 and
// source B in dir 2 and observes the artifact axis move proves nothing about the source,
// because the path difference alone accounts for it — the claim would pass unchanged if
// both sources were identical. That is the same non-discriminating shape as asserting a
// field is populated: something moved, and the fixture cannot say what. Holding the
// directory fixed and varying only main.rs makes the byte difference attributable to the
// source, which is the whole point of a per-axis derivation claim.
//
// CONSEQUENCE, AND IT IS AN INCOMPLETENESS IN THE IDENTITY RATHER THAN A CAVEAT ON
// COMPARING IT. Two generations can agree on all five model-side axes — same producer
// compiler, same source closure, same target model, same toolchain, same DECLARED build
// configuration — and still produce different artifact bytes, because build path is an
// input to the artifact that no axis names. So the axis set does not DETERMINE the
// artifact; it identifies a generation up to build location. The promotion mechanism's
// premise is that these axes identify a generation, and that premise is true only modulo
// this. Exactly two honest remedies exist: --remap-path-prefix (or equivalent) removes path
// from the output, and the five axes become an actual determinant; or build path joins
// build_configuration, and the axis tells the truth about what it covers. The third option
// — leaving it implicit and absorbing it in a comparison — is the one this lane does not
// take. NOT URGENT, because the direction is fail-closed: an identical build at a different
// path reports as a MOVED artifact axis, a false invalidation, never a false agreement, so
// nothing is silently admitted. It is recorded here because it was measured here; the
// carrier-side row belongs with the identity in v2.compiler.self_host.generation, not with
// the witness that found it.
fn build_twice_in_one_dir(first_source: String, second_source: String) -> TwoBuilds {
let dir = shell.Mktemp.Dir()
if !dir.success {
TwoBuildsSetupRefused { cause: "mktemp -d failed" }
} else {
let root = trim(dir.path as String)
let manifest = "{root}/Cargo.toml"
let main_rs = "{root}/main.rs"
let wrote_manifest = Filesystem.Write(path: manifest, content: crate_manifest)
let wrote_first = Filesystem.Write(path: main_rs, content: first_source)
if !wrote_manifest.success || !wrote_first.success {
TwoBuildsSetupRefused { cause: "fixture crate write failed" }
} else {
let first = gunbc.self_host_artifact_materialization.artifact_identity_of(
outcome: gunbc.self_host_artifact_materialization.materialize_artifact_wet(
workdir: root, manifest_path: manifest, target_dir: "{root}/target",
target_name: fixture_target_name, extra_args: []
)
)
let wrote_second = Filesystem.Write(path: main_rs, content: second_source)
if !wrote_second.success {
TwoBuildsSetupRefused { cause: "second fixture source write failed" }
} else {
TwoBuilds {
first: first,
second: gunbc.self_host_artifact_materialization.artifact_identity_of(
outcome: gunbc.self_host_artifact_materialization.materialize_artifact_wet(
workdir: root, manifest_path: manifest, target_dir: "{root}/target",
target_name: fixture_target_name, extra_args: []
)
)
}
}
}
}
}

fn axis_is_materialized(a: ArtifactIdentity) -> Bool {
match a {
ArtifactMaterialized { digest: _ } => true
ArtifactNotMaterialized => false
}
}

fn axis_identity(artifact: ArtifactIdentity) -> GenerationIdentity {
GenerationIdentity {
producer_compiler: symbol_identity_digest(sym: "axis-derivation-producer-compiler"),
source_closure: symbol_identity_digest(sym: "axis-derivation-source-closure"),
target_model: symbol_identity_digest(sym: "axis-derivation-target-model"),
toolchain: symbol_identity_digest(sym: "axis-derivation-toolchain"),
build_configuration: symbol_identity_digest(sym: "axis-derivation-build-configuration"),
materialized_artifact: artifact
}
}

fn moved_axis_count(both: TwoBuilds) -> Int {
match both {
TwoBuildsSetupRefused { cause: _ } => 0 - 1
TwoBuilds { first: f, second: s } =>
if !axis_is_materialized(a: f) || !axis_is_materialized(a: s) {
0 - 1
} else {
length(
xs: generation_identity_mismatched_axes(
left: axis_identity(artifact: f),
right: axis_identity(artifact: s)
)
)
}
}
}

test fn changing_only_the_source_bytes_names_exactly_the_artifact_axis() -> Bool {
let both = build_twice_in_one_dir(
first_source: crate_main,
second_source: crate_main_variant
)
match both {
TwoBuildsSetupRefused { cause: _ } => false
TwoBuilds { first: f, second: s } =>
axis_is_materialized(a: f)
&& axis_is_materialized(a: s)
&& moved_axis_count(both: both) == 1
&& for_all(
xs: generation_identity_mismatched_axes(
left: axis_identity(artifact: f),
right: axis_identity(artifact: s)
),
predicate: fn(named) {
generation_axis_symbol(axis: named) ==
generation_axis_symbol(axis: MaterializedArtifactAxis)
}
)
}
}

test fn rebuilding_identical_source_in_place_moves_no_axis() -> Bool {
let both = build_twice_in_one_dir(
first_source: crate_main,
second_source: crate_main
)
match both {
TwoBuildsSetupRefused { cause: _ } => false
TwoBuilds { first: f, second: s } =>
axis_is_materialized(a: f)
&& axis_is_materialized(a: s)
&& moved_axis_count(both: both) == 0
}
}
Loading