feat(repo-batcher): from-scratch verified build-out

scaffoldia/repo-batcher/Justfile

@@ -1,96 +1,124 @@
 # SPDX-License-Identifier: PMPL-1.0-or-later
 # justfile for repo-batcher
+#
+# CANONICAL ATS2 BUILD CONVENTION
+# -------------------------------
+# Every ATS2 module is typechecked/compiled with CWD = src/ats2 and the
+# single include flag `-IATS .` so that ROOT-RELATIVE staload paths
+# (e.g. `staload "utils/string_utils.sats"`) resolve regardless of the
+# compiler's working directory. Per-file isolated typechecking with
+# `../`-relative staloads is FORBIDDEN: it silently masked a real
+# cross-module regression (PR #59). All proofs use the recipes below,
+# which exercise the real cross-module invocation. Module list is
+# EXPLICIT (never a wildcard) so scratch/probe files cannot enter a
+# build.
+
+ats2_root := justfile_directory() / "src/ats2"
+build_dir := justfile_directory() / "build"
+
+# Modules in dependency order (sats checked with its dats).
+# layer1: utils/string_utils   layer2: operations/types
+# effects: operations/effects  layer3: validation/spdx
+# layer4: operations/<op>      layer5: ffi/c_exports
 
-# Default recipe
 default:
     @just --list
 
-# Build the project
-build:
-    @echo "Building repo-batcher..."
-    # Compile ATS2 core
-    cd src/ats2 && patscc -o ../../build/librepobatcher.a operations/*.dats
-    # Build Zig FFI layer
-    cd ffi/zig && zig build -Doptimize=ReleaseSafe
-    @echo "Build complete"
-
-# Build in development mode (faster, less optimized)
-build-dev:
-    @echo "Building repo-batcher (dev mode)..."
-    cd ffi/zig && zig build
-    @echo "Build complete"
-
-# Run smoke test (structure validation, no build required)
-test-smoke:
-    @echo "Running smoke test..."
-    ./tests/smoke_test.sh
-
-# Run tests
-test:
-    @echo "Running tests..."
-    cd ffi/zig && zig build test && zig build test-integration
-    @echo ""
-    @echo "All tests passed!"
-
-# Run real repository tests (dry-run only)
-test-real:
-    @echo "Running real repository tests (dry-run)..."
-    ./tests/real_repo_test.sh
-
-# Run performance benchmark
-benchmark:
-    @echo "Running performance benchmark..."
-    ./benchmark/performance_test.sh
-
-# Clean build artifacts
+# ---- Layer-by-layer cross-module typecheck (the canonical proof) ----
+
+# L1 + L2 + effects + L3: the verified core.
+tc-core:
+    cd {{ats2_root}} && patsopt -tc -s utils/string_utils.sats -d utils/string_utils.dats -IATS .
+    cd {{ats2_root}} && patsopt -tc -s operations/types.sats -d operations/types.dats -IATS .
+    cd {{ats2_root}} && patsopt -tc -s operations/effects.sats -d operations/effects.dats -IATS .
+    cd {{ats2_root}} && patsopt -tc -s validation/spdx.sats -d validation/spdx.dats -IATS .
+    @echo "tc-core: ATS2 core typechecks (cross-module, -IATS .)"
+
+# L4: each operation module typechecks against its .sats.
+tc-operations: tc-core
+    cd {{ats2_root}} && patsopt -tc -s operations/file_replace.sats -d operations/file_replace.dats -IATS .
+    cd {{ats2_root}} && patsopt -tc -s operations/git_sync.sats -d operations/git_sync.dats -IATS .
+    cd {{ats2_root}} && patsopt -tc -s operations/github_settings.sats -d operations/github_settings.dats -IATS .
+    cd {{ats2_root}} && patsopt -tc -s operations/license_update.sats -d operations/license_update.dats -IATS .
+    cd {{ats2_root}} && patsopt -tc -s operations/spdx_audit.sats -d operations/spdx_audit.dats -IATS .
+    cd {{ats2_root}} && patsopt -tc -s operations/workflow_update.sats -d operations/workflow_update.dats -IATS .
+    @echo "tc-operations: all Layer-4 operation modules typecheck"
+
+# L5: the C-export surface typechecks.
+tc-ffi: tc-operations
+    cd {{ats2_root}} && patsopt -tc -d ffi/c_exports.dats -IATS .
+    @echo "tc-ffi: Layer-5 C-export surface typechecks"
+
+# Full ATS2 proof.
+tc-ats2: tc-ffi
+    @echo "tc-ats2: full ATS2 stack typechecks under canonical invocation"
+
+# ---- Compilation to a C archive (Layer 5 link surface) ----
+
+# Compile every ATS2 module to .o then bundle a static archive.
+ats2-lib: tc-ffi
+    mkdir -p {{build_dir}}
+    cd {{ats2_root}} && patscc -DATS_MEMALLOC_LIBC -IATS . -c \
+        utils/string_utils.dats operations/types.dats \
+        operations/effects.dats validation/spdx.dats \
+        operations/file_replace.dats operations/git_sync.dats \
+        operations/github_settings.dats operations/license_update.dats \
+        operations/spdx_audit.dats operations/workflow_update.dats \
+        ffi/c_exports.dats
+    cd {{ats2_root}} && ar rcs {{build_dir}}/librepobatcher.a *_dats.o
+    @echo "ats2-lib: {{build_dir}}/librepobatcher.a built"
+
+# ---- Idris2 ABI (Layer 6) ----
+
+# The estate idris2 0.8.0 is a relocated Chez install; its baked
+# package prefix points at a non-existent ~/.asdf path. Idris2's
+# documented relocation override is IDRIS2_PREFIX, which makes it
+# resolve its OWN bundled stdlib at $PREFIX/idris2-0.8.0/*-0.8.0.
+# No .ttc is hand-located or staged.
+idris2_home := "/home/hyperpolymath/dev/tools/provers/idris2/0.8.0"
+
+abi-check:
+    cd {{justfile_directory()}}/src/abi && \
+        IDRIS2_PREFIX={{idris2_home}} {{idris2_home}}/bin/idris2 --check Abi.idr
+    @echo "abi-check: Idris2 ABI contract typechecks"
+
+# ---- Zig CLI (Layer 7): patscc owns the final link ----
+
+# `zig build` emits build/rb_cli.o (PIC, Zig front-end only). patscc
+# then links the ATS2 core (per-module *_dats.o from ats2-lib) +
+# ffi/cli_root.dats (the ATS2 program-bootstrap root) + rb_cli.o +
+# libatslib into the real binary. patscc MUST own this link: it injects
+# the Postiats prelude/libats/runtime/dynload bootstrap that a bare Zig
+# link cannot supply.
+cli: ats2-lib
+    cd {{justfile_directory()}}/ffi/zig && zig build
+    cd {{ats2_root}} && patscc -DATS_MEMALLOC_LIBC -IATS . \
+        -o {{build_dir}}/repo-batcher \
+        ffi/cli_root.dats *_dats.o {{build_dir}}/rb_cli.o -latslib \
+        -Wl,-z,noexecstack
+    @echo "cli: {{build_dir}}/repo-batcher built (Zig CLI + real ATS2 core)"
+
+# ---- Layer 8: fixture-backed end-to-end gate ----
+
+# Real git-repo fixture: dry-run no-mutation + genuine on-disk mutation
+# + spdx-audit, all driven through the real binary. NOT a smoke test.
+e2e: cli
+    bash {{justfile_directory()}}/ffi/zig/test/fixture.sh {{build_dir}}/repo-batcher
+    {{build_dir}}/repo-batcher --version
+    @echo "e2e: fixture-backed integration gate passed"
+
+# Aggregate build.
+build: ats2-lib cli
+    @echo "build: ATS2 archive + patscc-linked repo-batcher binary"
+
 clean:
-    rm -rf build/
-    find . -name "*.o" -delete
-    find . -name "*.a" -delete
-    find . -name "*.so" -delete
-
-# Install to system
-install:
-    @echo "Installing repo-batcher..."
-    sudo cp build/repo-batcher /usr/local/bin/
-    sudo chmod +x /usr/local/bin/repo-batcher
-    mkdir -p ~/.config/repo-batcher/watch
-    mkdir -p ~/.local/share/repo-batcher/logs
-    mkdir -p ~/.local/share/repo-batcher/backups
-    @echo "Installed to /usr/local/bin/repo-batcher"
-
-# Uninstall from system
-uninstall:
-    sudo rm -f /usr/local/bin/repo-batcher
-    @echo "Uninstalled repo-batcher"
-
-# Format code
+    rm -rf {{build_dir}}
+    find {{ats2_root}} -name "*_dats.o" -delete
+    find {{ats2_root}} -name "*.c" -path "*_dats.c" -delete
+    rm -rf {{justfile_directory()}}/ffi/zig/zig-out {{justfile_directory()}}/ffi/zig/.zig-cache
+
+# Backward-compatible check recipe (now the real cross-module proof).
+check: tc-ats2
+
 fmt:
-    zig fmt ffi/zig/src/ ffi/zig/test/
-
-# Check code quality
-check:
-    @echo "Checking ATS2 code..."
-    patsopt -tc -d src/ats2/operations/*.dats
-
-# Create example config
-setup-config:
-    mkdir -p ~/.config/repo-batcher
-    cp templates/config.example.toml ~/.config/repo-batcher/config.toml
-    @echo "Config created at ~/.config/repo-batcher/config.toml"
-
-# Run in dry-run mode (safe testing)
-dry-run operation targets:
-    ./build/repo-batcher {{operation}} --targets {{targets}} --dry-run
-
-# Quick git-sync (ported from sync_repos.sh)
-git-sync parallel="4" depth="2":
-    ./build/repo-batcher git-sync --parallel {{parallel}} --depth {{depth}}
-
-# Watch mode (daemon)
-watch:
-    ./build/repo-batcher watch
-
-# Show version and help
-help:
-    ./build/repo-batcher --help
+    zig fmt {{justfile_directory()}}/ffi/zig/src/ {{justfile_directory()}}/ffi/zig/test/

scaffoldia/repo-batcher/docs/RESUME-L7-L8.adoc

@@ -0,0 +1,107 @@
+// SPDX-License-Identifier: PMPL-1.0-or-later
+= repo-batcher #56 — Resume Runbook for Layers 7–8
+:toc: macro
+:reproducible:
+
+Machine- and human-readable handoff. Authoritative resume point for
+`hyperpolymath/reposystem#56` after the L1–L6 + `$UNSAFE` remediation
+landed. Branch: `feat/repo-batcher-fullbuild-56`. PR: #59 (DRAFT — must
+stay draft until L7/L8 land AND are fiction-reviewed).
+
+toc::[]
+
+== State (verified, committed, pushed)
+
+[cols="1,3,1"]
+|===
+| Layer | What | Proof
+
+| L1 string_utils | real Postiats 0.4.2 | `just tc-ats2` exit 0
+| L2 types | cross-module regression fixed (root-relative staload, `-IATS .`) | `just tc-ats2` exit 0
+| effects / L3 spdx | real Postiats | `just tc-ats2` exit 0
+| L4 (6 operation modules) | real Postiats | `just tc-ats2` exit 0
+| L5 c_exports | C-export surface + archive | `just ats2-lib` exit 0 (`build/librepobatcher.a`)
+| L6 Idris2 ABI | typed ABI contract | `just abi-check` exit 0
+| `$UNSAFE` remediation | 55 ad-hoc casts → 15 in one audited PROOF-DEBT boundary; 6/10 modules `$UNSAFE`-free | commit `e07c207`, `just tc-ats2`+`just ats2-lib` exit 0
+|===
+
+Commits on branch: `09682ec`(L1) `872d8f8`(L2) `c1ba394`(fix+L3)
+`4bcb883`(L4) `cf9df0b`(L5) `91887a9`(L6) `e07c207`(`$UNSAFE` remediation).
+
+== Honest disclosure (do not overstate)
+
+The ATS2 stack *type-checks* under the canonical cross-module invocation.
+It is NOT machine-proven memory-safe: linear-memory safety rests on a
+single audited `$UNSAFE` combinator set — *hand-verified proof-debt*
+(copy-before-free / read-only borrow, freed-once, no escape). The audit
+contract is the `PROOF-DEBT` banner block in
+`src/ats2/utils/string_utils.sats` (+ `system_owned` in
+`operations/types.dats`, `sys_run_owned` in `operations/effects.dats`,
+`gh_setting_owned` in `operations/github_settings.dats`). Auditing
+repo-batcher memory safety == auditing ONLY those ~15 casts.
+
+== Canonical build invocation (the ONLY accepted proof)
+
+[source,sh]
+----
+cd scaffoldia/repo-batcher
+just tc-ats2      # full cross-module typecheck (CWD=src/ats2, -IATS .)
+just ats2-lib     # patscc -> build/librepobatcher.a
+just abi-check    # Idris2 ABI (IDRIS2_PREFIX override; see Justfile)
+----
+Per-file isolated `patsopt -tc` with `../`-relative staloads is FORBIDDEN
+(it masked the L2 regression). Capture exit codes directly:
+`just tc-ats2 ; echo "EXIT=$?"` — never pipe through `tail`/`head`
+(returns tail's exit, not the compiler's — this caused a false "verified"
+claim earlier).
+
+== Remaining work
+
+=== L7 — Zig FFI/CLI (`ffi/zig/`)  — THE genuine unknown
+
+Build `ffi/zig/build.zig` (Zig 0.15.2 — `addSharedLibrary` was REMOVED;
+use `addLibrary` + `.linkage`, or static lib + exe), `ffi/zig/src/main.zig`
+(real CLI linking `build/librepobatcher.a`), `ffi/zig/test/integration_test.zig`.
+
+Hard part: the ATS2 archive needs the Postiats *runtime* at link time.
+The C-export surface is `src/ats2/ffi/c_exports.dats` (compiled into the
+archive by `just ats2-lib`). The Zig link must also resolve the Postiats
+libats runtime — locate it via `$PATSHOME/ccomp/runtime` /
+`$PATSHOME/ccomp/atslib/lib` (discover `PATSHOME` through the `just`-spawned
+shell; system `patsopt` is at `/usr/bin`, so query
+`patsopt -d 2>/dev/null` env or `dirname $(command -v patsopt)`-relative).
+The archive was built with `-DATS_MEMALLOC_LIBC`, so link against libc
+malloc (no GC lib needed). Expect trial-and-error here; that is normal.
+
+Acceptance: `just zig-build` and `just zig-test` exit 0.
+
+=== L8 — end-to-end
+
+`just e2e` (recipe already drafted in `Justfile`: ats2-lib → zig build →
+run real `repo-batcher --version` + `repo-batcher validate-spdx MIT`).
+Acceptance: `just e2e` exit 0 AND the produced binary actually runs.
+
+=== Cleanup (trivial)
+
+`rm` / gitignore any `src/ats2/*_dats.{c,o}` and
+`src/ats2/validation/_probe*` scratch (none are committed; they appear in
+a build/probe working tree, not in this clone).
+
+== Environment hazards (cost prior agents hours)
+
+* *Sandbox path*: ONLY paths under `/home/hyperpolymath/dev/repos/`
+  persist across Bash tool calls. Clone the working tree there
+  (e.g. `/home/hyperpolymath/dev/repos/.rb56-work`), never `~/dev` or
+  `/tmp` (those roll back). Background sub-agents inherit this and ALSO
+  hit a Write/Edit lockout — prefer doing L7/L8 in the main session.
+* *`git checkout -- .` destroys uncommitted work*: commit/stash before
+  ANY tree-wide clean. (Reverted this remediation once; reapplied.)
+* Toolchains are permission-live: `patsopt`/`patscc` `/usr/bin` (0.4.2),
+  `idris2` `~/dev/tools/provers/idris2/0.8.0/bin`, `zig` 0.15.2, `just`.
+
+== Definition of done for #56
+
+L7 + L8 build and their proofs (`just zig-build`, `just zig-test`,
+`just e2e`) exit 0, captured directly; each fiction-reviewed (compile
+claim independently reproduced, no pseudo-code, proof-debt labelled);
+PR #59 body updated; THEN and only then PR #59 marked ready / merged.