Skip to content

Fix DESIGN §4c body-position source annotation violations (2 blocks) #7918

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
briansrls merged 2 commits into from
Aug 6, 2026
Merged

Fix DESIGN §4c body-position source annotation violations (2 blocks) #7918

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
aecd2bb
Fix DESIGN §4c body-position source annotation violations (2 blocks)
Aug 6, 2026
44be228
Fix prose regression from relocation: refusal_causes_token, not heal_…
Aug 6, 2026
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
9 changes: 5 additions & 4 deletions dag/extdeps/systems/nvidia.dag
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -88,6 +88,11 @@ data dgx_spark_network_ports: List<SystemNetworkPort> = [
SystemNetworkPort { medium: ShortRangeWireless, product_name: "Bluetooth 5.4", bandwidth: none },
]

// dgx_spark_catalog_row's IntegratedComputeSystemCatalogRow.memory and .memory_bandwidth
// fields: on a UnifiedShared SoC the GPU-facing and system-facing memory are one physical
// fact, not two independent ones, so both fields below derive from the already-cited
// nvidia_gb10_gpu_catalog row instead of re-asserting the same 128 GiB / 273 GB/s
// literals a second time (review 49122; DESIGN §3 parallel-representation).
fn dgx_spark_catalog_row(storage_capacity: ByteSize) -> IntegratedComputeSystemCatalogRow {
IntegratedComputeSystemCatalogRow {
vendor: nvidia,
Expand All @@ -96,10 +101,6 @@ fn dgx_spark_catalog_row(storage_capacity: ByteSize) -> IntegratedComputeSystemC
cpu_architecture: Aarch64,
cpu_core_clusters: dgx_spark_cpu_core_clusters,
gpu: nvidia_gb10_gpu_catalog,
// On a UnifiedShared SoC the GPU-facing and system-facing memory are one physical
// fact, not two independent ones: derive both fields from the already-cited
// nvidia_gb10_gpu_catalog row instead of re-asserting the same 128 GiB / 273 GB/s
// literals a second time (review 49122; DESIGN §3 parallel-representation).
memory: nvidia_gb10_gpu_catalog.memory,
memory_bus_width: bit_width(count: 256),
memory_data_rate: hertz(count: 4266000000),
Expand Down
11 changes: 6 additions & 5 deletions dag/test/claim/generated_artifact_drift_test.dag
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -358,6 +358,12 @@ test fn witness_binding_refusal_retains_its_locator() -> Bool {
}
}

// witness_refusal_cause_tokens_are_pairwise_distinct's fold_list cons lambda, third clause
// (t != "HealPushRefusalPopulationEmpty"): this pins what refusal_causes_token's
// fold relies on. It reuses the empty-population marker as its own "nothing accumulated
// yet" state, so a cause token colliding with that marker would make the first joined
// cause silently replace the marker instead of appending. Safe today by coincidence;
// this makes it safe by execution (review 49204).
test fn witness_refusal_cause_tokens_are_pairwise_distinct() -> Bool {
let causes = [
ActionsJobCredentialScopeUnavailable, ActionsJobCredentialScopeNotGranted,
Expand All @@ -373,11 +379,6 @@ test fn witness_refusal_cause_tokens_are_pairwise_distinct() -> Bool {
xs: tokens,
empty: true,
cons: fn(ok, t) {
// The third clause pins what refusal_causes_token's fold relies on:
// it reuses the empty-population marker as its own "nothing accumulated
// yet" state, so a cause token colliding with that marker would make the
// first joined cause silently replace the marker instead of appending.
// Safe today by coincidence; this makes it safe by execution (review 49204).
ok && (count(filter(tokens, u => u == t)) == 1) && (t != "")
&& (t != "HealPushRefusalPopulationEmpty")
}
Expand Down
Loading