Skip to content

docs(repo-batcher): correct to verified-accurate state (no V ever; Zig stub unimplemented)#58

Merged
hyperpolymath merged 1 commit into
mainfrom
docs/repo-batcher-accurate-state
May 18, 2026
Merged

docs(repo-batcher): correct to verified-accurate state (no V ever; Zig stub unimplemented)#58
hyperpolymath merged 1 commit into
mainfrom
docs/repo-batcher-accurate-state

Conversation

@hyperpolymath
Copy link
Copy Markdown
Owner

Supersedes the PR #57 banners after deeper investigation for #56.

Finding: the "port V→Zig" premise is false.

  • git log --all --diff-filter=A -- src/v/* is empty — no V ever existed in source.
  • ffi/zig/ is an unsubstituted RSR template stub: literal {{project}} placeholders, build.zig uses removed addSharedLibrary (fails under Zig 0.15.2), does not bind the ATS2 c_exports ABI, references nonexistent files. Not an implementation.
  • Real source = ATS2 verified core (11 files, exports a C ABI) + the unimplemented Zig stub. The tool is not functional / not production-ready.

All 10 docs rewritten to that accurate state; load-bearing false claims (README headline, ROADMAP "v1.0.0 Production Ready", ARCHITECTURE V layer + table + ASCII diagram) corrected. Dated snapshot bodies left intact but banner-flagged as un-built historical plans. No fabricated code — the real Zig FFI/CLI is greenfield work, re-scoped on #56.

Refs #56, #53.

…ig stub unimplemented (Refs #56, #53)

Supersedes the #57 banners. Deeper investigation for #56 found the
'V→Zig port' premise is false:

- git history has NO src/v/ — no V implementation ever existed in source.
- ffi/zig/ is an unsubstituted RSR template stub ({{project}} placeholders,
  stale build API that fails under Zig 0.15.2, does not bind the ATS2
  c_exports ABI). It is not an implementation.
- Real source = ATS2 verified core (11 files, C ABI) + unimplemented Zig
  stub. Tool is NOT functional; not production-ready.

All 10 docs' banners + the load-bearing false claims (README headline,
ROADMAP 'v1.0.0 Production Ready', ARCHITECTURE V layer/table) rewritten
to the accurate state. Snapshot bodies left intact but banner-flagged as
un-built historical plans, not shipped code. No fabricated implementation.

Refs #56, #53.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@hyperpolymath hyperpolymath merged commit 9ba62ae into main May 18, 2026
10 of 11 checks passed
@hyperpolymath hyperpolymath deleted the docs/repo-batcher-accurate-state branch May 18, 2026 09:53
hyperpolymath added a commit that referenced this pull request May 18, 2026
Refs #56

> **Honest disclosure correction (fiction-review, 2026-05-18 — commit
`e07c207`).**
> "Fully verified" below means **type-checks under the canonical
> cross-module invocation** (`just tc-ats2`, `just ats2-lib`, exit 0).
> It does **NOT** mean machine-proven linear-memory safety: 55 ad-hoc
> `$UNSAFE` borrow casts were collapsed into a single audited combinator
> set (string_utils ×9, effects/types/github_settings ×1 each, 15 casts
> in 4 files; 6 of 10 modules now `$UNSAFE`-free with machine-checked
> linearity). Soundness of that set is **hand-verified proof-debt**
> (copy-before-free / read-only borrow, freed-once, no escape), not
> machine-proven. Layers 7–8 (Zig FFI/CLI, end-to-end Justfile) are
> NOT done. This PR stays **draft** until L7–L8 land and are
> fiction-reviewed.

From-scratch rebuild of `scaffoldia/repo-batcher/` (see disclosure
above). Prior
code was fictional pseudo-ATS2 that never compiled (corrected context:
merged
PRs #57/#58). Anti-fiction rule strictly applied: a layer is only marked
verified with the exact passing `patsopt`/`zig`/`idris2` command +
output
pasted in its commit.

## Toolchain (sanity-checked)

```
ATS/Postiats version 0.4.2
zig 0.15.2
Idris 2, version 0.8.0
patscc -> gcc 13.3.0
```

## Layer checklist (bottom-up)

- [x] **Layer 1 — `src/ats2/utils/string_utils.{sats,dats}`**
`patsopt -tc -s utils/string_utils.sats -d utils/string_utils.dats` →
exit 0, no diagnostics.
      Full rewrite to real linear/length-indexed Postiats; sound bound &
      termination proofs; documented `$UNSAFE` borrow boundaries only.
- [x] **Layer 2 — `src/ats2/operations/types.{sats,dats}`**
`patsopt -tc -s types.sats -d types.dats` (from `operations/`) → exit 0.
Split into interface + impl. **Honest proof-debt disclosure**: prior
value-string-indexed witnesses are *unrepresentable* in real Postiats
      (string index sort does not exist); replaced with sound opaque
constructor-controlled abstypes; effectful FS witnesses labelled as
such.
- [ ] Layer 3 — `validation/spdx.dats`
- [ ] Layer 4 — remaining `operations/*.dats`
- [ ] Layer 5 — `ffi/c_exports.dats` + `patscc` static lib
- [ ] Layer 6 — `src/abi/` Idris2 ABI
- [ ] Layer 7 — `ffi/zig/` build + CLI + tests (Zig 0.15.2)
- [ ] Layer 8 — `Justfile` end-to-end + real binary run

## Status

DRAFT — work continues bottom-up; only compile-verified layers are
checked.
Unverifiable layers will be reported honestly with compiler errors
rather than
faked.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath added a commit that referenced this pull request May 18, 2026
) (#61)

## Why

PRs #57/#58 correctly described repo-batcher as an unimplemented stub.
**PR #59 then implemented and merged the full L1–L8 build-out**, so
README.adoc / IMPLEMENTATION-STATUS.md / docs/ARCHITECTURE.adoc are now
wrong in the *opposite* direction ("not functional", "unimplemented RSR
template stub", "no working end-to-end CLI yet") — the inverse of the
original anti-fiction defect.

## What

Corrects the **live** status framing to the independently
fiction-reviewed reality:

- L1–L4 ATS2 core — `just tc-ats2`=0
- L5 self-contained C archive — `just ats2-lib`=0 (`ATS_DYNLOADFLAG 0`
link-completeness fix)
- L6 Idris2 typed ABI, machine-checked theorems — `just abi-check`=0
- L7 `patscc`-linked Zig CLI binding the genuine ATS2 C ABI (no Zig
reimpl)
- L8 fixture-backed `just e2e`=0 (real temp git repo; dry-run
byte-identical; real on-disk mutation via the ATS2 core; audit)

"No V ever existed" is **retained** (true history). The dated 2026-02-06
body in IMPLEMENTATION-STATUS.md is left intact; its banner now
correctly fences it as historical planning fiction, not status —
rewriting that artifact would itself be revisionism.

Refs #56 (CLOSED-COMPLETED — docs-truth follow-up, not a reopen).

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@github-actions
Copy link
Copy Markdown

🔍 Hypatia Security Scan

Findings: 195 issues detected

Severity Count
🔴 Critical 14
🟠 High 112
🟡 Medium 69

⚠️ Action Required: Critical security issues found!

View findings
[
  {
    "reason": "Issue in quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in security-policy.yml",
    "type": "missing_workflow",
    "file": "security-policy.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/reposystem/reposystem/tools/rsr-certified/extensions/vscode/src/extension.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "innerHTML assignment -- XSS risk, use textContent or SafeDOM (5 occurrences, CWE-79)",
    "type": "js_innerhtml",
    "file": "/home/runner/work/reposystem/reposystem/stateful-artefacts/browser-extension/scripts/popup.js",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "innerHTML assignment -- XSS risk, use textContent or SafeDOM (1 occurrences, CWE-79)",
    "type": "js_innerhtml",
    "file": "/home/runner/work/reposystem/reposystem/stateful-artefacts/browser-extension/scripts/content.js",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "innerHTML assignment -- XSS risk, use textContent or SafeDOM (4 occurrences, CWE-79)",
    "type": "js_innerhtml",
    "file": "/home/runner/work/reposystem/reposystem/stateful-artefacts/dashboard/js/dashboard.js",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "innerHTML assignment -- XSS risk, use textContent or SafeDOM (5 occurrences, CWE-79)",
    "type": "js_innerhtml",
    "file": "/home/runner/work/reposystem/reposystem/stateful-artefacts/annotation-layer/annotations.js",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "innerHTML assignment -- XSS risk, use textContent or SafeDOM (7 occurrences, CWE-79)",
    "type": "js_innerhtml",
    "file": "/home/runner/work/reposystem/reposystem/web/app.js",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "HTTP URL in code -- use HTTPS for non-localhost (16 occurrences, CWE-319)",
    "type": "js_http_url_in_code",
    "file": "/home/runner/work/reposystem/reposystem/web/app.js",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant