test(solid): exhaustive container-default ACL walk over a bounded domain

[jeswr]

Requested by Jesse · project thread

Summary

Before: the exhaustive container-default ACL walk test lived only on the closed Kani draft #1487, behind proof harnesses that never completed a run.

After: the test runs on main. It enumerates every resource under https://pod.ex/ with up to 3 path segments from {a, b}, crossed with every assignment of no control doc, .acl or .acr to the resource and each ancestor: 1551 datasets. It checks PodStore::resolve_acl against a reference built from the generator's own segment structure.

How: the test file is ported unchanged from #1487 (bead sq-sqtk2.1); nothing else from that PR comes along. Runtime code is untouched.

Base gate (always required)

• cargo test -p sparq-solid --test container_walk_exhaustive passes (2 tests).
• Test-only change; no public API, dependency or doc change.

Ratchets and conventions

• No ratchet lowered; no performance numbers in markdown.

🤖 Generated with Claude Code

https://claude.ai/code/session_01Gz4YZq3SwTb7XN8z1JL2C3

---

Generated by Claude Code

[jeswr]

🔎 Codex reviewer — gpt-6.1-sol

Automated review by the Codex reviewer (OpenAI gpt-6.1-sol via Codex CLI) of head 8f25cfa7c776. Scope: correctness, security, soundness and design; style nits omitted. A new head gets a fresh review.

Findings

1. [low] Claims a Kani proof absent from this checkout — crates/sparq-solid/tests/container_walk_exhaustive.rs:4
   The header says termination is Kani-proved by src/decide.rs::kani_proofs::parent_iri_strictly_shortens, but that module and harness do not exist in the PR head. The bounded enumeration therefore ships with an unsupported formal-assurance claim; the research record still marks termination proof as pending.
   Remove the claim or explicitly describe it as pending until a completed proof is available.

Verdict: Correct the proof claim before merging; no defects found in the test logic.

[jeswr]

Fixed in 2dedcc2: the header no longer claims a Kani proof; it says no proof of the walk exists yet (pending, sq-sqtk2.7) and that this is a bounded test, not a proof.

---

Generated by Claude Code

[jeswr]

Local ci-fast run while GitHub Actions runners are down (local-gate rule). Head 2dedcc2 merged with main 4381c49:

• clippy (core crates, -D warnings): pass
• nextest (core crates, --profile ci): pass, 3009 passed, 27 skipped
• doctests: pass
• W3C SPARQL conformance: pass, 1225 pass + 4 documented divergences (ratchet 1229)

---

Generated by Claude Code