Skip to content

Harden proof boundaries and close architecture drift#71

Merged
iperev merged 2 commits into
mainfrom
fix/architecture-audit-closure
Jul 12, 2026
Merged

Harden proof boundaries and close architecture drift#71
iperev merged 2 commits into
mainfrom
fix/architecture-audit-closure

Conversation

@iperev

@iperev iperev commented Jul 11, 2026

Copy link
Copy Markdown
Contributor

Summary

This change closes the confirmed architecture-audit gaps across Proofkit's trust, artifact, CLI, agent, planning, and self-hosting boundaries.

  • confines package execution-record reads, writes, invalidation, and atomic replacement to the repository root; rejects provider-derived candidate manifests before mutation
  • binds packed owner records and Python wheel binaries to current source bytes, and compares complete admitted self-evidence records instead of lossy projections
  • replaces partial CI package lists with the owner commands for generated catalog validation and the complete Go package set
  • makes generic command dispatch an exact descriptor-to-builder registry and removes unreachable special-runner branches
  • makes TypeScript public-API verification consume explicit package manifests and per-condition source paths, with a bounded top-level lexer that preserves byte offsets across comments, strings, templates, regex literals, and same-line exports
  • closes agent-envelope local references under truncation, preserves canonical changed-path pointer targets, and separates route-family vocabulary from command-family navigation
  • centralizes local-environment admission, path-pattern compilation, release-platform selection, and sorted-text admission in their existing owners
  • hardens the loopback browser server with Host/Origin checks, HTTP timeouts, and force-close fallback
  • preserves PID lifecycle proof under partial/stale fixture files and reduces release-closeout fixture runtime by copying one immutable base fixture
  • updates durable requirements, public CLI contract, proof bindings, and human routing documentation for every newly claimed invariant

Formal justification

For each changed boundary, the implementation follows the same proof form:

  1. If a decision consumes representation x, then x must be admitted by the named owner before the decision.
  2. If two artifacts claim the same identity, their complete canonical records or content digests must be equal.
  3. If a derived agent record references a local target, that target must remain present after bounding, or the reference must be removed and counted without double-counting the omitted semantic target.
  4. If a command descriptor selects a generic runner, exactly one generic builder must exist; non-generic commands must have none.
  5. If a filesystem scanner claims bounded explicit scope, every read path must originate in admitted caller input and remain under the selected root and package boundary.

The added falsifiers negate each conclusion independently: symlink escape, pre-mutation provider evidence, packed/source drift, wheel/source drift, lossy receipt collisions, dangling agent refs, invalid JSON pointers, unknown evidence vocabulary, descriptor/argv drift, Unicode/string/regex scanner offsets, foreign browser authority, partial PID files, and incomplete CI package coverage.

Breaking contract changes

  • typescript-public-api-surfaces now requires packageManifestPath and exportConditions[].sourcePath; implicit packages/, src/, and compiled-target inference were removed.
  • TSX is explicitly outside this scanner's claim; .ts, .mts, and .cts are admitted.
  • agent-route output uses selectedRouteFamily and guidance uses routeFamily, avoiding collision with command-family navigation.
  • unknown capability requiredEvidence values fail admission in every trust mode.
  • changed-path JSON output now exposes the canonical changed-path facts referenced by its agent envelope.

Validation

  • git show --check --format= HEAD
  • npm run check on committed object
    • formatting, all Go tests, vet, staticcheck, actionlint, govulncheck
    • package tarball and Python wheel build/verification
    • self-hosting receipts and coverage (59/59 requirements bound, 111 scenarios)
    • release closeout passed
  • go test -race for requirement browser, agent envelope, package execution record, TypeScript public API, Python package, and release closeout packages
  • requirement-browser and Python lifecycle packages repeated 20 times
  • semantic diff and raw diff reviewed against exact origin/main f3e41686849542087ed53863e6d56aaaeac41202

Release-closeout package tests decreased from about 9.9 seconds to about 4.3 seconds locally while preserving isolated copies and all existing falsifiers.

Non-claims

  • Local evidence does not prove provider-side CI success, branch protection, registry publication, deployment, rollout, or production readiness.
  • The TypeScript scanner does not parse JSX/TSX or prove compiler-output provenance.
  • Agent envelopes remain derived guidance and do not become proof or requirement authority.

@iperev
iperev marked this pull request as ready for review July 11, 2026 19:27
@iperev
iperev merged commit 10b4632 into main Jul 12, 2026
8 checks passed
@iperev
iperev deleted the fix/architecture-audit-closure branch July 12, 2026 00:20
@iperev iperev mentioned this pull request Jul 12, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Development

Successfully merging this pull request may close these issues.

1 participant