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
13 changes: 8 additions & 5 deletions scripts/v4-glob-discovery-project.sh
Original file line number Diff line number Diff line change
Expand Up @@ -10,10 +10,13 @@

set -euo pipefail

v4_glob_discovery_default_claims_root() {
local root="${1:-}"
if [[ -n "$root" ]]; then
printf '%s/test/claim' "$root"
# Args: optional explicit claims_root directory. When omitted, default to repo
# src/v4/test/claim. Callers must not pass a source root — pass the claim tree
# root directly (e.g. .../test/claim/impossible_bug for perturb scans).
v4_glob_discovery_resolve_claims_root() {
local claims_root="${1:-}"
if [[ -n "$claims_root" ]]; then
printf '%s' "$claims_root"
return
fi
local repo
Expand Down Expand Up @@ -56,7 +59,7 @@ project_marker_file() {
# Exits 2 when projection is empty (fail-closed).
v4_glob_discovery_project_distributed_markers() {
local claims_root
claims_root="$(v4_glob_discovery_default_claims_root "${1:-}")"
claims_root="$(v4_glob_discovery_resolve_claims_root "${1:-}")"
V4_GLOB_DISCOVERY_ROWS=""
V4_GLOB_DISCOVERY_ROW_COUNT=0

Expand Down
3 changes: 3 additions & 0 deletions src/v4/test/claim/lens_affected_set/edit_locus_resolver.dag
Original file line number Diff line number Diff line change
Expand Up @@ -230,6 +230,9 @@ data edit_locus_source_provenance_parse_root_span_claim_passes: Bool = edit_locu
data edit_locus_source_provenance_affected_set_wire_claim_passes: Bool = edit_locus_source_provenance_affected_set_wire_holds()
data edit_locus_source_provenance_producer_rejects_malformed_source_claim_passes: Bool = edit_locus_source_provenance_producer_rejects_malformed_source_holds()

// Transport Symbol pin — independent authority for substrate-equivalence field-preservation laws.
data edit_locus_narrow_resolution_holds_symbol: Symbol = edit_locus_narrow_resolution_holds

// Consolidation #4553 Phase 2 distributed BoolWitnessClaim marker.
// Co-located with `edit_locus_narrow_resolution_holds` so glob discovery finds the witness without the central roster.
data unified_claim_edit_locus_narrow: UnifiedTestClaim = BoolWitnessClaim {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -19,12 +19,20 @@ import v4.std.verification {
unified_test_claim_bool_witness,
unified_test_claim_modality
}
import v4.test.claim.lens_affected_set.edit_locus_resolver { unified_claim_edit_locus_narrow }
import v4.test.claim.lens_affected_set.edit_locus_resolver {
edit_locus_narrow_resolution_holds_symbol,
unified_claim_edit_locus_narrow
}
import v4.std.text { String }
import v4.test.claim.manual.eval_runtime_mvp { claim_eval_mvp2_test_claim_route }
import v4.test.claim.workflow.glob_discovery {
glob_discovered_smoke_marker_count,
glob_discovery_smoke_marker_count_is_positive
}
// Independent transport authority for the sample marker (not read back from extraction).

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BLOCKING: This makes the equivalence proof a single sample-marker oracle, so it still cannot prove the discovered BoolWitness set equals the roster rows required by test-claim-consolidation design §6.2 C9 / INVARIANTS P2; a dropped row plus an added row can pass the count and sample checks.

data substrate_equivalence_sample_bool_witness_entry: String = "src/v4/test/claim/lens_affected_set/edit_locus_resolver.dag"


fn substrate_equivalence_sample_bool_unified_claim() -> UnifiedTestClaim {
unified_claim_edit_locus_narrow
}
Expand All @@ -41,12 +49,11 @@ fn substrate_equivalence_sample_node_corpus_claim() -> UnifiedTestClaim {
fn substrate_equivalence_glob_discovery_marker_preserves_entry_function() -> Bool {
match unified_test_claim_bool_witness(c: substrate_equivalence_sample_bool_unified_claim()) {
Accepted { value: w, diagnostics: None } =>
(w.entry == "src/v4/test/claim/lens_affected_set/edit_locus_resolver.dag")
&& bool_witness_matches_entry_function(
w: w,
entry: w.entry,
function: w.function
)
bool_witness_matches_entry_function(
w: w,
entry: substrate_equivalence_sample_bool_witness_entry,
function: edit_locus_narrow_resolution_holds_symbol
)
Rejected { diagnostics: _ } => false
}
}
Expand Down Expand Up @@ -75,8 +82,8 @@ fn substrate_equivalence_unified_claim_preserves_bool_fields() -> Bool {
Accepted { value: w, diagnostics: None } =>
bool_witness_matches_entry_function(
w: w,
entry: extracted.entry,
function: extracted.function
entry: substrate_equivalence_sample_bool_witness_entry,
function: edit_locus_narrow_resolution_holds_symbol
)
Rejected { diagnostics: _ } => false
}
Expand Down
7 changes: 7 additions & 0 deletions tools/ci_affected_components/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -143,6 +143,7 @@ pub fn ci_changed_path_affects_testclaim_corpus(path: &str) -> bool {
|| path.starts_with("src/v4/test/claim/")
|| path == "scripts/v4-testclaim-corpus-eval.sh"
|| path == "scripts/v4-testclaim-smoke-roster.sh"
|| path == "scripts/v4-glob-discovery-project.sh"
|| path == "scripts/v4-substrate-equivalence-gate.sh"
|| path == "src/v4/test/claim/workflow/glob_discovery.dag"
|| path == "src/v4/test/claim/workflow/unified_test_claim_substrate_equivalence.dag"
Expand Down Expand Up @@ -248,6 +249,12 @@ mod tests {
assert!(ci_changed_path_affects_testclaim_corpus(
"scripts/v4-testclaim-smoke-roster.sh"
));
assert!(ci_changed_path_affects_testclaim_corpus(
"scripts/v4-glob-discovery-project.sh"
));
assert!(ci_changed_path_affects_testclaim_corpus(
"scripts/v4-substrate-equivalence-gate.sh"
));
assert!(!ci_changed_path_affects_testclaim_corpus(
"scripts/other.sh"
));
Expand Down
Loading