Assert tracked tree holds nothing repository walkers skip (#170)

CHANGELOG.md

@@ -291,8 +291,10 @@ versions, and the entries below say what each tag does and does not claim.
   under a runtime namespace. `RT-02` recomputes the compiler-semantics IDs
   with each frozen file changed (1.0 and 1.1 unchanged, 1.2 changed). `RT-03`
   plants the second direction of the axiom check. Every directory that holds a
-  `CACHEDIR.TAG` is skipped by the repository walkers, so a build directory
-  beside the sources no longer reads as source. No compiled behavior changes.
+  `CACHEDIR.TAG` is skipped by every repository walker, so a build directory
+  beside the sources no longer reads as source, and `RP-03` (#170) asserts that
+  the tracked tree (`git ls-files`) holds no `CACHEDIR.TAG` and no walker-skipped
+  path component outside the sanctioned `expected/` oracle directories. No compiled behavior changes.
 - UOR Atlas is verified in CI as the parts of one run (SPEC.md §9.4, §22.11,
   `RP-14`, `VR-23`, #131; no new diagnostic code). The examples leg, 178
   minutes on `main` at 514e95ad (CI run 38716449420), was 156 minutes of

CONFORMANCE.md

@@ -452,7 +452,7 @@ the error registry does not sanction (R5, `ERRORS.md`).
 | --- | --- | --- |
 | `RP-01` | `build` | The repository, crate, executable, metadata, and licenses have the exact LexLean identity specified. |
 | `RP-02` | `build` | The repository is derived from the pinned UOR template commit and contains no inherited domain-specific claim logic. |
-| `RP-03` | `build` | The completed repository has the required file and crate layout. |
+| `RP-03` | `build` | The completed repository has the required file and crate layout, and the tracked tree holds no CACHEDIR.TAG or path component the repository walkers skip outside sanctioned expected/ oracle directories. |
 | `RP-04` | `build` | Only the lexlean crate is shipped and no shipped crate depends on repository-only tooling. |
 | `RP-05` | `build` | The just vv recipe runs every normative acceptance gate in the specified order. |
 | `RP-06` | `build` | CONFORMANCE.md and ERRORS.md are exact generated views of model files. |

SPEC.md

@@ -270,7 +270,7 @@ Every user-visible failure has a registered diagnostic code and a sanctioned exi
 
 ## 7. Repository layout
 
-The completed repository MUST have this layout. Additional files are allowed only when they have a defined role and are included by the repository audits.
+The completed repository MUST have this layout. Additional files are allowed only when they have a defined role and are included by the repository audits; the tracked tree MUST NOT hold any `CACHEDIR.TAG` file or any path component the repository walkers skip (`target`, `.git`, `.lexlean`, `.lake`, `node_modules`, or `expected` outside the sanctioned `expected/` oracle directories under `bootstrap/`, `compiler/`, `stdlib/`, `examples/<example>/`, `tests/negative/<case>/`, `tests/tooling/<suite>/<case>/`, and `tests/fixtures/<suite>/<case>/`).
 
 ```text
 .
@@ -9378,7 +9378,7 @@ Every row below is normative, has honesty level `build`, and MUST be copied byte
 |---|---|---|---|
 | `RP-01` | `repository` | The repository, crate, executable, metadata, and licenses have the exact LexLean identity specified. | §2 |
 | `RP-02` | `repository` | The repository is derived from the pinned UOR template commit and contains no inherited domain-specific claim logic. | §2.2 |
-| `RP-03` | `repository` | The completed repository has the required file and crate layout. | §7 |
+| `RP-03` | `repository` | The completed repository has the required file and crate layout, and the tracked tree holds no CACHEDIR.TAG or path component the repository walkers skip outside sanctioned expected/ oracle directories. | §7 |
 | `RP-04` | `repository` | Only the lexlean crate is shipped and no shipped crate depends on repository-only tooling. | §7, §8.4 |
 | `RP-05` | `repository` | The just vv recipe runs every normative acceptance gate in the specified order. | §9.2 |
 | `RP-06` | `repository` | CONFORMANCE.md and ERRORS.md are exact generated views of model files. | §27.5 |

VERIFICATION.md

@@ -8471,9 +8471,22 @@ none is claimed.
 grep of `SPEC.md` for the path; it now recomputes the three IDs from disk
 (`RP-10`'s recomputation, shared) and finds, with either frozen file changed
 by one byte, the language-1.0 and 1.1 IDs unchanged and the 1.2 ID changed.
-The repository walkers skip any directory that holds a `CACHEDIR.TAG`: with
-a Cargo target directory named `target-check` in the checkout, `RT-01` and
-`SP-12` failed on its Lean files before and pass now.
+The repository walkers skip any directory that holds a `CACHEDIR.TAG` (including
+`xtask/src/audit.rs`, `crates/conformance/src/lib.rs`, and
+`crates/conformance/src/cases/oracle.rs`): with a Cargo target directory named
+`target-check` in the checkout, `RT-01` and `SP-12` failed on its Lean files
+before and pass now. Conversely (`RP-03`, #170), the tracked tree (`git ls-files`)
+holds no `CACHEDIR.TAG` file and no path component the walkers skip (`target`,
+`.git`, `.lexlean`, `.lake`, `node_modules`, or `expected` outside the
+sanctioned `expected/` oracle directories). Planted in the git index and
+restored after each run (`cargo test -p repo-conformance --test conformance
+conformance_rp_03 -- --exact`):
+
+1. A tracked `examples/collections/CACHEDIR.TAG`:
+   `left: ["examples/collections/CACHEDIR.TAG: tracked `CACHEDIR.TAG` would cause repository walkers to skip `examples/collections`"]`
+2. A tracked `.lexlean` directory outside the ignored roots
+   (`crates/lexlean/.lexlean/planted.lean`):
+   `left: ["crates/lexlean/.lexlean/planted.lean: tracked path has walker-skipped component `.lexlean`"]`
 
 The fifth runtime module, `LexLeanRuntime.Laws` (#117), declares under the
 namespace `LexLeanLaws`, which the runtime cases' list of namespaces did not

crates/conformance/src/cases/oracle.rs

@@ -2391,7 +2391,11 @@ fn equivalent_renderings() {
 
 /// The pinned files of a checkout, copied to `to`.
 fn copy_used(from: &Path, to: &Path, pin: &Pin) {
-    for entry in walkdir::WalkDir::new(from).into_iter().flatten() {
+    for entry in walkdir::WalkDir::new(from)
+        .into_iter()
+        .filter_entry(|entry| !support::holds_cache_tag(entry))
+        .flatten()
+    {
         let relative = entry.path().strip_prefix(from).expect("under root");
         let text = relative
             .components()

crates/conformance/src/cases/repository.rs

@@ -532,6 +532,80 @@ pub(crate) fn run(id: &str) {
                     "{fixture}: the committed fixture project carries a build root; fixtures run from a temporary copy — remove it"
                 );
             }
+            // No tracked file is named `CACHEDIR.TAG` or sits under a path
+            // component the repository walkers skip (`target`, `.git`,
+            // `.lexlean`, `.lake`, `node_modules`, or `expected` outside the
+            // sanctioned `expected/` oracle directories), so no tracked subtree
+            // can hide from the walkers.
+            let is_sanctioned_expected = |parts: &[&str], index: usize| -> bool {
+                (index == 1 && matches!(parts[0], "bootstrap" | "compiler" | "stdlib"))
+                    || (index == 2 && parts[0] == "examples")
+                    || (index == 3
+                        && parts[0] == "tests"
+                        && matches!(parts[1], "negative" | "tooling"))
+                    || (index == 4 && parts[0] == "tests" && parts[1] == "fixtures")
+            };
+            let walker_skip_defect = |tracked: &str| -> Option<String> {
+                let parts: Vec<&str> = tracked.split('/').collect();
+                for (index, component) in parts.iter().copied().enumerate() {
+                    if component == "CACHEDIR.TAG" {
+                        return Some(format!(
+                            "{tracked}: tracked `CACHEDIR.TAG` would cause repository walkers to skip `{}`",
+                            parts[..index].join("/")
+                        ));
+                    }
+                    if matches!(
+                        component,
+                        "target" | ".git" | ".lexlean" | ".lake" | "node_modules"
+                    ) {
+                        return Some(format!(
+                            "{tracked}: tracked path has walker-skipped component `{component}`"
+                        ));
+                    }
+                    if component == "expected" && !is_sanctioned_expected(&parts, index) {
+                        return Some(format!(
+                            "{tracked}: tracked path has `expected` component outside sanctioned oracle directories"
+                        ));
+                    }
+                }
+                None
+            };
+            let ls_files = std::process::Command::new("git")
+                .args(["ls-files", "-z"])
+                .current_dir(root.as_std_path())
+                .output()
+                .expect("git ls-files runs in the repository");
+            assert!(ls_files.status.success(), "git ls-files succeeded");
+            let tracked: Vec<String> = ls_files
+                .stdout
+                .split(|byte| *byte == 0)
+                .filter(|entry| !entry.is_empty())
+                .map(|entry| String::from_utf8_lossy(entry).replace('\\', "/"))
+                .collect();
+            assert!(
+                tracked.len() > 1000,
+                "git ls-files returned {} tracked files",
+                tracked.len()
+            );
+            let defects: Vec<String> = tracked
+                .iter()
+                .filter_map(|path| walker_skip_defect(path))
+                .collect();
+            assert_eq!(
+                defects,
+                Vec::<String>::new(),
+                "§7 (RP-03): the tracked tree holds nothing the repository walkers skip"
+            );
+            for planted in [
+                "examples/collections/CACHEDIR.TAG",
+                "crates/lexlean/.lexlean/planted.lean",
+                "crates/lexlean/src/expected/planted.rs",
+            ] {
+                assert!(
+                    walker_skip_defect(planted).is_some(),
+                    "planted tracked path `{planted}` is refused by RP-03"
+                );
+            }
         }
         // §7, §8.4: shipped crates derive from `publish = false`, and the
         // shipped crate depends on no repository-only tooling.

crates/conformance/src/lib.rs

@@ -197,7 +197,9 @@ pub fn workspace_test_names_with_flags(root: &Path) -> (BTreeSet<String>, BTreeS
         for entry in entries.flatten() {
             let path = entry.path();
             if path.is_dir() {
-                if path.file_name().is_some_and(|name| name == "target") {
+                if path.file_name().is_some_and(|name| name == "target")
+                    || path.join("CACHEDIR.TAG").is_file()
+                {
                     continue;
                 }
                 stack.push(path);

features/suites/repository.feature

@@ -18,11 +18,12 @@ Feature: repository
     And none of the four tooling files still mentions the template's audit-limits remnant
 
   @RP-03 @build
-  Scenario: The completed repository has the required file and crate layout.
-    Given the section 7 layout tree parsed out of the SPEC.md text fence
-    When every tree row is resolved to a path under the repository root
+  Scenario: The completed repository has the required file and crate layout, and the tracked tree holds no CACHEDIR.TAG or path component the repository walkers skip outside sanctioned expected/ oracle directories.
+    Given the section 7 layout tree parsed out of the SPEC.md text fence and the tracked file list from git ls-files
+    When every tree row is resolved to a path under the repository root and every tracked path is inspected for CACHEDIR.TAG and walker-skipped components
     Then each row ending in a slash exists as a directory and every other row exists as a file
     And more than 80 rows were checked
+    And no tracked path is named CACHEDIR.TAG or has a walker-skipped component outside sanctioned expected/ oracle directories
 
   @RP-04 @build
   Scenario: Only the lexlean crate is shipped and no shipped crate depends on repository-only tooling.

model/ids.toml

@@ -24,7 +24,7 @@ statement = "The repository is derived from the pinned UOR template commit and c
 id = "RP-03"
 level = "build"
 suite = "repository"
-statement = "The completed repository has the required file and crate layout."
+statement = "The completed repository has the required file and crate layout, and the tracked tree holds no CACHEDIR.TAG or path component the repository walkers skip outside sanctioned expected/ oracle directories."
 
 [[id]]
 id = "RP-04"

xtask/src/audit.rs

@@ -21,6 +21,9 @@ fn gather(root: &Path, dirs: &[&str], extensions: &[&str], out: &mut Vec<PathBuf
         for entry in walkdir::WalkDir::new(&base)
             .follow_links(false)
             .into_iter()
+            .filter_entry(|entry| {
+                !(entry.file_type().is_dir() && entry.path().join("CACHEDIR.TAG").is_file())
+            })
             .flatten()
         {
             if entry.file_type().is_dir() {