Skip to content

docs: fix README architecture drift (routes + packages match code) - #286

Merged
telleroutlook merged 1 commit into
mainfrom
docs/fix-readme-architecture-drift
Jul 30, 2026
Merged

docs: fix README architecture drift (routes + packages match code)#286
telleroutlook merged 1 commit into
mainfrom
docs/fix-readme-architecture-drift

Conversation

@telleroutlook

Copy link
Copy Markdown
Contributor

The Architecture block described endpoints and packages that do not exist, and contradicted the README itself.

Verified against cmd/symkerneld/routes.go and the internal/ tree on main:

  • Routes — removed phantom /v1/sandbox/run and /v1/verify/batch; added the real /v1/health, /v1/verify/smt, /v1/verify/symbolic.
  • Packagesinternal/composeinternal/composed (real name); removed nonexistent internal/explain and internal/batch; added internal/criterion, internal/z3, internal/verify.
  • CGO contradictioninternal/smt was labelled a "go-z3 CGO binding", but the README already states symkerneld does not use CGO and shells out to z3 -in. Corrected to the subprocess reality (both internal/z3 and internal/smt shell out to z3).
  • Batch section/v1/verify/batch (and SYMKERNEL_BATCH_CONCURRENCY) exist nowhere in code; reframed the section as planned rather than documenting a 404 as a live endpoint.

Docs only.

The Architecture block listed endpoints and packages that do not exist and
contradicted the repo itself:
- Routes: dropped phantom /v1/sandbox/run and /v1/verify/batch; added the real
  /v1/health, /v1/verify/smt, /v1/verify/symbolic (verified against
  cmd/symkerneld/routes.go).
- Packages: internal/compose -> internal/composed (real name); removed
  nonexistent internal/explain and internal/batch; added internal/criterion,
  internal/z3, internal/verify.
- Corrected internal/smt from "go-z3 CGO binding" to the z3 subprocess reality
  -- README already states symkerneld does NOT use CGO and shells out to
  "z3 -in", so the old line was self-contradictory.
- Batch verification section reframed as planned (no /v1/verify/batch route or
  SYMKERNEL_BATCH_CONCURRENCY exists in code), matching the repo's planned
  convention rather than documenting a 404 as live.

Docs only; verified every route/package against main.
@telleroutlook
telleroutlook merged commit d4d4d34 into main Jul 30, 2026
1 check passed
@telleroutlook
telleroutlook deleted the docs/fix-readme-architecture-drift branch July 30, 2026 07:19
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