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
3 changes: 2 additions & 1 deletion .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -159,6 +159,7 @@ jobs:
run: |
echo "CARGO_HOME=$RUNNER_TEMP/cargo" >> "$GITHUB_ENV"
echo "RUSTUP_HOME=$RUNNER_TEMP/rustup" >> "$GITHUB_ENV"
echo "CARGO_BUILD_JOBS=2" >> "$GITHUB_ENV"

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 workflow edit changes the bytes pinned by dsl/gunbc/ci_github_actions_workflow.dag, but the carrier Source-SHA256 still does not match, violating INVARIANTS P2 boundary discipline and the existing checksum receipt.

# INTERIM sccache transport (operator 2026-06-01 override; "disregard the memo for now").
# Right-way fix is the modeled cache_interface projection consumer (dsl/std/cache_interface.dag
# sccache_local_facts; src/v4/workflow/ci.dag cache-projection note) -- NOT this hand-wire.
Expand Down Expand Up @@ -228,7 +229,7 @@ jobs:
gunbc-bin-${{ runner.os }}-${{ runner.arch }}-
- name: Build v2 compiler (v4 floor)
if: steps.v4-v2-bin.outputs.cache-hit != 'true'
run: cargo build -p v2-compiler --release
run: RUSTC_WRAPPER= cargo build -p v2-compiler --release
- name: M1 v4 full-tree rust emit probe (v2 emit)
timeout-minutes: 20
env:
Expand Down
4 changes: 2 additions & 2 deletions dsl/gunbc/ci_github_actions_workflow.dag
Original file line number Diff line number Diff line change
Expand Up @@ -211,7 +211,7 @@ data gunbc_ci_github_actions_workflow: Workflow = {
steps: [RunStep {
name: Some { value: "Isolate toolchain dirs (srv1/srv2 shared-$HOME concurrent-rustup race)" },
id: none,
run: "echo \"CARGO_HOME=$RUNNER_TEMP/cargo\" >> \"$GITHUB_ENV\"\necho \"RUSTUP_HOME=$RUNNER_TEMP/rustup\" >> \"$GITHUB_ENV\"\n# INTERIM sccache transport (operator 2026-06-01 override; \"disregard the memo for now\").\n# Right-way fix is the modeled cache_interface projection consumer (dsl/std/cache_interface.dag\n# sccache_local_facts; src/v4/workflow/ci.dag cache-projection note) -- NOT this hand-wire.\n# The runner provides an ISOLATED, ghrunner-owned sccache via systemd env (SCCACHE_DIR +\n# SCCACHE_SERVER_UDS, ctrl#1419). Do NOT hardcode SCCACHE_SERVER_UDS here: a job/step-level\n# env beats the runner default, so pinning the old shared socket forces EACCES and keeps\n# sccache inert. Inherit the runner's socket; only flip RUSTC_WRAPPER on. The server starts\n# LAZILY (sccache creates the socket on the first rustc call), so the socket does NOT exist yet\n# at this pre-cargo step -- gate on the socket's PARENT DIR being writable, not the socket file:\n# the runner provisions that dir ghrunner:ghrunner 0755 (ctrl#1419), so the gate passes pre-start\n# and sccache then binds its socket there on first rustc. Fails SAFE: a missing or non-writable\n# dir -> cold build (::warning), never silently / never fail-hard. dissolve-on-arrival.\nif [ -n \"$SCCACHE_SERVER_UDS\" ] && [ -w \"$(dirname \"$SCCACHE_SERVER_UDS\")\" ]; then\n echo \"RUSTC_WRAPPER=sccache\" >> \"$GITHUB_ENV\"\n echo \"CARGO_INCREMENTAL=0\" >> \"$GITHUB_ENV\"\nelse\n echo \"::warning::sccache socket (SCCACHE_SERVER_UDS=${SCCACHE_SERVER_UDS:-unset}) absent or not usable by runner user; building cold\"\nfi\n",
run: "echo \"CARGO_HOME=$RUNNER_TEMP/cargo\" >> \"$GITHUB_ENV\"\necho \"RUSTUP_HOME=$RUNNER_TEMP/rustup\" >> \"$GITHUB_ENV\"\necho \"CARGO_BUILD_JOBS=2\" >> \"$GITHUB_ENV\"\n# INTERIM sccache transport (operator 2026-06-01 override; \"disregard the memo for now\").\n# Right-way fix is the modeled cache_interface projection consumer (dsl/std/cache_interface.dag\n# sccache_local_facts; src/v4/workflow/ci.dag cache-projection note) -- NOT this hand-wire.\n# The runner provides an ISOLATED, ghrunner-owned sccache via systemd env (SCCACHE_DIR +\n# SCCACHE_SERVER_UDS, ctrl#1419). Do NOT hardcode SCCACHE_SERVER_UDS here: a job/step-level\n# env beats the runner default, so pinning the old shared socket forces EACCES and keeps\n# sccache inert. Inherit the runner's socket; only flip RUSTC_WRAPPER on. The server starts\n# LAZILY (sccache creates the socket on the first rustc call), so the socket does NOT exist yet\n# at this pre-cargo step -- gate on the socket's PARENT DIR being writable, not the socket file:\n# the runner provisions that dir ghrunner:ghrunner 0755 (ctrl#1419), so the gate passes pre-start\n# and sccache then binds its socket there on first rustc. Fails SAFE: a missing or non-writable\n# dir -> cold build (::warning), never silently / never fail-hard. dissolve-on-arrival.\nif [ -n \"$SCCACHE_SERVER_UDS\" ] && [ -w \"$(dirname \"$SCCACHE_SERVER_UDS\")\" ]; then\n echo \"RUSTC_WRAPPER=sccache\" >> \"$GITHUB_ENV\"\n echo \"CARGO_INCREMENTAL=0\" >> \"$GITHUB_ENV\"\nelse\n echo \"::warning::sccache socket (SCCACHE_SERVER_UDS=${SCCACHE_SERVER_UDS:-unset}) absent or not usable by runner user; building cold\"\nfi\n",
shell: Bash,
env: none,
working_directory: none,
Expand Down Expand Up @@ -277,7 +277,7 @@ data gunbc_ci_github_actions_workflow: Workflow = {
}, RunStep {
name: Some { value: "Build v2 compiler (v4 floor)" },
id: none,
run: "cargo build -p v2-compiler --release",
run: "RUSTC_WRAPPER= cargo build -p v2-compiler --release",
shell: Bash,
env: none,
working_directory: none,
Expand Down
107 changes: 107 additions & 0 deletions src/v4/test/claim/lens_parallelism/data_dependency.dag
Original file line number Diff line number Diff line change
Expand Up @@ -6,32 +6,61 @@
module v4.test.claim.lens_parallelism.data_dependency

import v4.compiler.infer { InferredFacts, InferredTree }
import v4.compiler.eval {
TestClaimEvalSubject,
TestClaimRun,
eval_test_claim_subject,
run_test_claim_assert,
run_test_claim
}
import v4.lens.parallelism {
DataDependent,
ParallelismFact,
parallelism_fact_eq,
parallelism_witness
}
import v4.std.diagnostic { Accepted, None }
import v4.std.dependency {
ClassifiedDependencyView,
DataDependsOn,
DependencyView
}
import v4.std.collection { List }
import v4.std.logic { Bool }
import v4.std.node { Atom, Edge, Named, Node, Symbol, TypeNode }
import v4.std.runtime { RuntimeValue }
import v4.std.verification {
ManualAnchorAbsent,
TestClassification,
TestClaim,
Tier1,
Integration,
EqualsClaim,
manual_claim_anchor
}
import v4.std.verdict { Verdict }
import v4.std.witness { Holds, Witness }
import v4.test.claim.lens_common.infer_fixture {
claim_atom_node,
claim_inferred_facts,
claim_inferred_tree
}
import v4.test.claim.manual.eval_runtime_mvp {
eval_mvp2_add_subgraph,
eval_mvp2_context,
eval_mvp2_evaluator_pin,
eval_mvp2_five_literal_node,
eval_mvp2_inferred_tree
}

data parallelism_root_symbol: Symbol = parallelism_root_symbol
data parallelism_child_symbol: Symbol = parallelism_child_symbol
data parallelism_edge_symbol: Symbol = parallelism_edge_symbol
data parallelism_type_symbol: Symbol = parallelism_type_symbol
data parallelism_algebra_symbol: Symbol = parallelism_algebra_symbol
data parallelism_descent_symbol: Symbol = parallelism_descent_symbol
data parallelism_claim_pass_symbol: Symbol = parallelism_claim_pass_symbol
data parallelism_claim_fail_symbol: Symbol = parallelism_claim_fail_symbol
data parallelism_child: Node = claim_atom_node(s: parallelism_child_symbol)

data parallelism_root: Node = Node {
Expand Down Expand Up @@ -66,6 +95,11 @@ type LensParallelismClaim {
actual: Witness<ParallelismFact>
}

type LensParallelismSubjectRosterContract {
run: TestClaimRun<Node, RuntimeValue>
unsupported_rows: List<Symbol>
}

data parallelism_data_dependency_claim: LensParallelismClaim = LensParallelismClaim {
input: parallelism_claim_tree(),
expected: ParallelismFact {
Expand All @@ -88,3 +122,76 @@ fn parallelism_data_dependency_claim_holds() -> Bool {
}

data parallelism_data_dependency_claim_passes: Bool = parallelism_data_dependency_claim_holds()

fn parallelism_claim_pass_node() -> Node {
Node {
kind: TypeNode { connective: Atom { identity: parallelism_claim_pass_symbol } },
children: []
}
}

fn parallelism_claim_fail_node() -> Node {
Node {
kind: TypeNode { connective: Atom { identity: parallelism_claim_fail_symbol } },
children: []
}
}

fn parallelism_claim_input(ok: Bool) -> Node {
if ok {
parallelism_claim_pass_node()
} else {
parallelism_claim_fail_node()
}
}

data claim_parallelism_data_dependency_receipt: TestClaim = EqualsClaim {
label: "lens_parallelism data dependency witness classifies DataDependsOn as DataDependent",
anchor: manual_claim_anchor(anchor: ManualAnchorAbsent),
lhs: parallelism_claim_input(ok: parallelism_data_dependency_claim_passes),
rhs: parallelism_claim_pass_node(),
classification: TestClassification { tier: Tier1, layer: Integration }
}

data verdict_parallelism_data_dependency_node_assert: Verdict<TestClaimEvalSubject<Node>, Node> = run_test_claim_assert(
claim: claim_parallelism_data_dependency_receipt,
actual: Accepted {
value: parallelism_claim_input(ok: parallelism_data_dependency_claim_passes),
diagnostics: None
},
at: parallelism_claim_pass_node()
)

fn parallelism_executable_claim_input(ok: Bool) -> Node {
if ok {
eval_mvp2_add_subgraph()
} else {
parallelism_claim_fail_node()
}
}

data claim_parallelism_data_dependency_run_test_claim_receipt: TestClaim = EqualsClaim {
label: "lens_parallelism data dependency witness gates run_test_claim executable receipt",
anchor: manual_claim_anchor(anchor: ManualAnchorAbsent),
lhs: parallelism_executable_claim_input(ok: parallelism_data_dependency_claim_passes),
rhs: eval_mvp2_five_literal_node(),
classification: TestClassification { tier: Tier1, layer: Integration }
}

data subject_parallelism_data_dependency_receipt: TestClaimEvalSubject<Node> = eval_test_claim_subject(
claim: claim_parallelism_data_dependency_run_test_claim_receipt,
context: eval_mvp2_context(),
tree: eval_mvp2_inferred_tree(),
evaluator_pin: eval_mvp2_evaluator_pin
)

data run_parallelism_data_dependency_receipt: TestClaimRun<Node, RuntimeValue> = run_test_claim(
subject: subject_parallelism_data_dependency_receipt
)

data lens_parallelism_unsupported_subject_rows: List<Symbol> = []

data lens_parallelism_data_dependency_subject_roster_contract: LensParallelismSubjectRosterContract = LensParallelismSubjectRosterContract {
run: run_parallelism_data_dependency_receipt,
unsupported_rows: lens_parallelism_unsupported_subject_rows
}
6 changes: 5 additions & 1 deletion src/v4/test/claim/manual/manual_corpus_roster.dag
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
// src/v4/test/claim/manual/manual_corpus_roster.dag
// Scope: T-38 manual TestClaim subject roster (RuntimeValue wedge).
// Status: wedge — four rows; expand per-A.
// Status: wedge — five rows; expand per-A.
// 🟡 gated — feature:t38-testclaim-corpus-eval — bind src/v4/TASKS.md T-38 — dissolve-on-arrival: item-registry reflection replaces explicit import roster when T-19 testclaim-coproduct-reflection lands.

module v4.test.claim.manual.manual_corpus_roster
Expand All @@ -9,6 +9,9 @@ module v4.test.claim.manual.manual_corpus_roster
import v4.compiler.eval { TestClaimEvalSubject }
import v4.std.collection { List }
import v4.std.node { Node }
import v4.test.claim.lens_parallelism.data_dependency {
subject_parallelism_data_dependency_receipt
}
import v4.test.claim.manual.dissolution_subsumption_reverification {
subject_rust_language_model_emit_mechanical_reverification_claim,
subject_rust_language_model_emit_subsumption_reverifies
Expand All @@ -21,6 +24,7 @@ import v4.test.claim.lens_effect.effect_depends_on {

data manual_corpus_node_subject_rows: List<TestClaimEvalSubject<Node>> = [
subject_eval_mvp2_test_claim_route,
subject_parallelism_data_dependency_receipt,
subject_lens_effect_depends_on_runtime_verdict,
subject_rust_language_model_emit_mechanical_reverification_claim,
subject_rust_language_model_emit_subsumption_reverifies
Expand Down
8 changes: 7 additions & 1 deletion src/v4/workflow/ci.dag
Original file line number Diff line number Diff line change
Expand Up @@ -124,6 +124,9 @@ import v4.test.claim.manual.dissolution_subsumption_reverification {
claim_rust_language_model_emit_subsumption_reverifies
}
import v4.test.claim.manual.eval_runtime_mvp { claim_eval_mvp2_test_claim_route }
import v4.test.claim.lens_parallelism.data_dependency {
claim_parallelism_data_dependency_run_test_claim_receipt
}
import v4.test.claim.lens_ownership.subject_roster {
lens_ownership_family_claim_ids,
lens_ownership_subject_rows
Expand Down Expand Up @@ -1108,6 +1111,7 @@ data ci_upsert_phase1_nat_semiring_rung_gate_execution: CiUpsertStepSymbol = ci_
// Forbidden: adding/removing manual corpus rows without the matching claim id here.
data ci_testclaim_corpus_eval_claim_ids: List<Symbol> = [
claim_eval_mvp2_test_claim_route,
claim_parallelism_data_dependency_run_test_claim_receipt,
claim_lens_effect_depends_on_runtime_verdict,
claim_rust_language_model_emit_mechanical_reverification,
claim_rust_language_model_emit_subsumption_reverifies
Expand Down Expand Up @@ -3101,6 +3105,8 @@ fn ci_glob_segment_matches_changed_path(segment: GlobSegment, path: RepoPath) ->
path == "src/v3/compiler/tests/boundary/v4_leaf_model_go_r1_r2_r3_external_test.rs"
} else if segment == "src/v4/test/claim/manual/**" {
ci_repo_path_has_prefix(path: path, prefix: "src/v4/test/claim/manual/")
} else if segment == "src/v4/test/claim/**" {
ci_repo_path_has_prefix(path: path, prefix: "src/v4/test/claim/")
} else if segment == "src/v4/test/claim/workflow/testclaim_corpus_runner.dag" {
path == "src/v4/test/claim/workflow/testclaim_corpus_runner.dag"
} else if segment == "src/v4/test/claim/workflow/manual_corpus_eval.dag" {
Expand Down Expand Up @@ -3153,7 +3159,7 @@ fn ci_upsert_input_ref_touches_git_diff(
ci_upsert_file_set_input_touches_git_diff(selector: selector, git_diff: git_diff)
TestClaimRef { claim_id: _ } =>
ci_glob_segment_matches_any_changed_path(
segment: "src/v4/test/claim/manual/**",
segment: "src/v4/test/claim/**",
paths: git_diff.changed_paths
)
LensOutputRef { lens: _, ports: _ } =>
Expand Down
3 changes: 3 additions & 0 deletions tools/ci_affected_components/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -215,6 +215,9 @@ mod tests {
assert!(ci_changed_path_affects_testclaim_corpus(
"src/v4/test/claim/manual/mvp1_rust_add_translate.dag"
));
assert!(ci_changed_path_affects_testclaim_corpus(
"src/v4/test/claim/lens_parallelism/data_dependency.dag"
));
assert!(ci_changed_path_affects_testclaim_corpus(
"src/v4/test/claim/lens_affected_set/irt1_leaf_claim_suite.dag"
));
Expand Down
Loading