feat(stdlib): Transaction.affine — affine-bounded write-set isolation — db-theory #2 (8 externs) by hyperpolymath · Pull Request #526 · hyperpolymath/affinescript

hyperpolymath · 2026-06-01T13:44:50Z

Summary

New stdlib/Transaction.affine module exposing SQL transactions as an affine-bounded resource: Tx opaque handle from tx_begin(d), consumed exactly once by tx_commit(t) or tx_rollback(t). Savepoint surface (tx_savepoint / tx_release / tx_rollback_to), tx_db aliasing, and tx_is_live introspection round out the 8-extern API.
Deno-ESM codegen wires __as_txBegin / Commit / Rollback / Savepoint / Release / RollbackTo / Db / IsLive JS prelude helpers + 8 deno_builtins lowerings. Host adapter contract documented inline.
Six-function smoke (tests/codegen-deno/transaction_smoke.{affine,harness.mjs}) witnesses all lifecycle shapes — including the rollback-discards-writes safety property (an INSERT issued during a Tx consumed by tx_rollback leaves only the pre-tx rows visible).

Proof obligation cross-doc

Per owner directive 2026-06-01 — every proof in AffineScript must first audit hyperpolymath/echo-types, reuse if applicable, extend upstream with proofs if not, then cross-document.

New docs/academic/proofs/db-theory-2-transaction-safety.md states three safety obligations:
- #DB-2.1 rollback-discards-writes (key invariant)
- #DB-2.2 commit-promotes-writes
- #DB-2.3 savepoint locality
Audit finding: echo-types carries EchoLinear.LEcho + weaken, EchoSecurity.Security record, and EchoNoSectionGeneric.no-section-of-collapsing-map — the latter is precisely the generic lemma the Transaction proof reduces to. Upstream extension required: a new TransactionMutations.agda module instantiating the generic no-section lemma. Issue to be filed on echo-types separately and back-linked here.

Test plan

dune runtest test/test_main.exe — 367 tests green, including the new AOT smoke for stdlib/Transaction.affine (row Rename AffineScript file extension from .as to .affine #15 in the AOT smoke output) and the regression test enforcing codegen ⊆ stdlib decls (no drift introduced).
tools/run_codegen_deno_tests.sh — transaction_smoke.harness.mjs passes all 6 assertions.
Mock adapter implements write-set isolation by snapshotting tables on txBegin and restoring on txRollback. Production adapter contract (Deno jsr:@db/sqlite / Node better-sqlite3) maps each extern to native BEGIN / COMMIT / ROLLBACK / SAVEPOINT / RELEASE / ROLLBACK TO.

🤖 Generated with Claude Code

github-actions · 2026-06-01T13:45:55Z

🔍 Hypatia Security Scan

Findings: 88 issues detected

Severity	Count
🔴 Critical	2
🟠 High	16
🟡 Medium	70

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action perpolymath/standards/.github/workflows/governance-reusable.yml@main\n needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action ons/checkout@v6\n    needs attention",
    "type": "unpinned_action",
    "file": "publish-jsr.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action land/setup-deno@v2\n    needs attention",
    "type": "unpinned_action",
    "file": "publish-jsr.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in affine-vscode-publish.yml",
    "type": "missing_timeout_minutes",
    "file": "affine-vscode-publish.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in ci.yml",
    "type": "missing_timeout_minutes",
    "file": "ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in ci.yml",
    "type": "missing_timeout_minutes",
    "file": "ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in ci.yml",
    "type": "missing_timeout_minutes",
    "file": "ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

github-actions · 2026-06-01T13:48:05Z

🔍 Hypatia Security Scan

Findings: 88 issues detected

Severity	Count
🔴 Critical	2
🟠 High	16
🟡 Medium	70

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action perpolymath/standards/.github/workflows/governance-reusable.yml@main\n needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action ons/checkout@v6\n    needs attention",
    "type": "unpinned_action",
    "file": "publish-jsr.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action land/setup-deno@v2\n    needs attention",
    "type": "unpinned_action",
    "file": "publish-jsr.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in affine-vscode-publish.yml",
    "type": "missing_timeout_minutes",
    "file": "affine-vscode-publish.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in ci.yml",
    "type": "missing_timeout_minutes",
    "file": "ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in ci.yml",
    "type": "missing_timeout_minutes",
    "file": "ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in ci.yml",
    "type": "missing_timeout_minutes",
    "file": "ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

…s — db-theory #3 (7 externs) (#527) ## Summary - New `stdlib/Aggregate.affine` module with 7 externs: `db_count`, `db_sum`, `db_min_int`, `db_max_int`, `db_avg`, `db_group_by` (whole result-set as JSON), `db_group_count` (key/count buckets as JSON). - Codegen + Deno-ESM JS prelude wired; smoke + harness witness all 7 externs with both single-row aggregates and grouped buckets. - Cross-doc proof obligation at `docs/academic/proofs/db-theory-3-aggregation-as-fold.md` — each aggregator is a commutative monoid, group-by is the indexed sum (Green/Karvounarakis/Tannen). - **Stacked on [#526](#526 (Transactions) — base will flip to `main` once #526 merges; auto-rebase will pick up cleanly. ## Echo-types audit cross-doc Per owner directive 2026-06-01, mandatory audit step. Found: no existing `Monoid`/`Semiring` infrastructure in echo-types. Closest scaffolding: `EchoCost.CostAlgebra` (left-identity only), `OmegaPow.additive-principal`. Filed [hyperpolymath/echo-types#175](hyperpolymath/echo-types#175) proposing new `EchoAggregation.agda` module with `Monoid` + `GroupAggregator` carriers + signature for `aggregation-as-fold` lemma. Sibling: [echo-types#174](hyperpolymath/echo-types#174) (Transaction safety). ## Aggregator monoid table | Aggregator | Elem | ε | ⊕ | Comm? | Idemp? | |------------|-----------------|----|----|-------|--------| | COUNT | ℕ | 0 | + | ✓ | ✗ | | SUM | ℕ (or ℤ, ℝ) | 0 | + | ✓ | ✗ | | MIN | ℕ ∪ {∞} | ∞ | min | ✓ | ✓ | | MAX | ℕ ∪ {-∞} | -∞ | max | ✓ | ✓ | | AVG | derived: SUM/COUNT (not a monoid — no identity) | ## Test plan - [x] `dune runtest test/test_main.exe` — 368 tests green (one more than baseline since AOT smoke picked up `Aggregate.affine`). - [x] `tools/run_codegen_deno_tests.sh` — `aggregate_smoke.harness.mjs` passes all 8 assertions (5 single-row + 3 grouped). - [x] Stack discipline: based on `feat/db-2-transactions`; will rebase onto main once #526 lands. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

github-actions · 2026-06-01T13:55:38Z

🔍 Hypatia Security Scan

Findings: 88 issues detected

Severity	Count
🔴 Critical	2
🟠 High	16
🟡 Medium	70

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action perpolymath/standards/.github/workflows/governance-reusable.yml@main\n needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action ons/checkout@v6\n    needs attention",
    "type": "unpinned_action",
    "file": "publish-jsr.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action land/setup-deno@v2\n    needs attention",
    "type": "unpinned_action",
    "file": "publish-jsr.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in affine-vscode-publish.yml",
    "type": "missing_timeout_minutes",
    "file": "affine-vscode-publish.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in ci.yml",
    "type": "missing_timeout_minutes",
    "file": "ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in ci.yml",
    "type": "missing_timeout_minutes",
    "file": "ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in ci.yml",
    "type": "missing_timeout_minutes",
    "file": "ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

… — db-theory #2 (8 externs) New `Transaction` module exposing SQL transactions as an affine-bounded resource: `tx_begin(d) -> Tx` returns an opaque handle consumed exactly once by `tx_commit` or `tx_rollback`. Adds savepoint surface (`tx_savepoint` / `tx_release` / `tx_rollback_to`), `tx_db` aliasing, and `tx_is_live` introspection. Codegen prelude adds `__as_tx*` helpers; Deno-ESM smoke witnesses the six lifecycle shapes including the rollback-discards-writes safety property (an insert during a `Tx` ending in rollback leaves only pre-tx rows visible). Cross-doc: docs/academic/proofs/db-theory-2-transaction-safety.md states three formal safety obligations (#DB-2.1 rollback-discards-writes, references the echo-types upstream extension shape — per owner directive 2026-06-01 the proof must reuse EchoNoSectionGeneric.no-section-of- collapsing-map via a new TransactionMutations.agda instantiation upstream (separate issue to follow). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Cross-doc seam now points to hyperpolymath/echo-types#174 (the TransactionMutations.agda upstream proposal) instead of a TBD placeholder. Path in module docstring corrected to docs/academic/proofs/ (the actual location). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…s — db-theory #3 (7 externs) (#527) ## Summary - New `stdlib/Aggregate.affine` module with 7 externs: `db_count`, `db_sum`, `db_min_int`, `db_max_int`, `db_avg`, `db_group_by` (whole result-set as JSON), `db_group_count` (key/count buckets as JSON). - Codegen + Deno-ESM JS prelude wired; smoke + harness witness all 7 externs with both single-row aggregates and grouped buckets. - Cross-doc proof obligation at `docs/academic/proofs/db-theory-3-aggregation-as-fold.md` — each aggregator is a commutative monoid, group-by is the indexed sum (Green/Karvounarakis/Tannen). - **Stacked on [#526](#526 (Transactions) — base will flip to `main` once #526 merges; auto-rebase will pick up cleanly. ## Echo-types audit cross-doc Per owner directive 2026-06-01, mandatory audit step. Found: no existing `Monoid`/`Semiring` infrastructure in echo-types. Closest scaffolding: `EchoCost.CostAlgebra` (left-identity only), `OmegaPow.additive-principal`. Filed [hyperpolymath/echo-types#175](hyperpolymath/echo-types#175) proposing new `EchoAggregation.agda` module with `Monoid` + `GroupAggregator` carriers + signature for `aggregation-as-fold` lemma. Sibling: [echo-types#174](hyperpolymath/echo-types#174) (Transaction safety). ## Aggregator monoid table | Aggregator | Elem | ε | ⊕ | Comm? | Idemp? | |------------|-----------------|----|----|-------|--------| | COUNT | ℕ | 0 | + | ✓ | ✗ | | SUM | ℕ (or ℤ, ℝ) | 0 | + | ✓ | ✗ | | MIN | ℕ ∪ {∞} | ∞ | min | ✓ | ✓ | | MAX | ℕ ∪ {-∞} | -∞ | max | ✓ | ✓ | | AVG | derived: SUM/COUNT (not a monoid — no identity) | ## Test plan - [x] `dune runtest test/test_main.exe` — 368 tests green (one more than baseline since AOT smoke picked up `Aggregate.affine`). - [x] `tools/run_codegen_deno_tests.sh` — `aggregate_smoke.harness.mjs` passes all 8 assertions (5 single-row + 3 grouped). - [x] Stack discipline: based on `feat/db-2-transactions`; will rebase onto main once #526 lands. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

github-actions · 2026-06-02T09:49:15Z

🔍 Hypatia Security Scan

Findings: 88 issues detected

Severity	Count
🔴 Critical	2
🟠 High	16
🟡 Medium	70

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action perpolymath/standards/.github/workflows/governance-reusable.yml@main\n needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action ons/checkout@v6\n    needs attention",
    "type": "unpinned_action",
    "file": "publish-jsr.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action land/setup-deno@v2\n    needs attention",
    "type": "unpinned_action",
    "file": "publish-jsr.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in affine-vscode-publish.yml",
    "type": "missing_timeout_minutes",
    "file": "affine-vscode-publish.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in ci.yml",
    "type": "missing_timeout_minutes",
    "file": "ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in ci.yml",
    "type": "missing_timeout_minutes",
    "file": "ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in ci.yml",
    "type": "missing_timeout_minutes",
    "file": "ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

Appends today's three db-theory stdlib PRs to the [Unreleased] section. Repo's changelog-reusable.yml automation isn't wired yet (manual append per the file's own header pointer). Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

## Summary Refresh the authoritative status surfaces in this repo to reflect the stdlib **db-theory triplet** that landed yesterday and today: - PR #525 — `Sqlite.affine` schema introspection + bulk I/O + error inspection (db-theory #1c, 6 externs) - PR #526 — `Transaction.affine` (db-theory #2, affine-bounded write-set isolation, 8 externs) - PR #527 — `Aggregate.affine` (db-theory #3, SQL group-by + aggregation primitives, 7 externs) - PR #528 — CHANGELOG sync (already merged) `CHANGELOG.md` is already up to date via #528, so this PR touches only the four files that ledger that work as status, not as history. ## What changed - `docs/CAPABILITY-MATRIX.adoc` — replace the stale "19/19 stdlib files" sentence (the AOT gate now discovers files dynamically) and call out the db-theory triplet as the current authoring frontier alongside Http / Json / Dict-Map. - `docs/TECH-DEBT.adoc` §C STDLIB — add a `STDLIB-05` row capturing the full Sqlite arc (#522 / #524 / #525), Transaction (#526), and Aggregate (#527), with pointers to the two academic proofs the PRs already shipped (`docs/academic/proofs/db-theory-{2,3}-*.md`). - `docs/stdlib-roadmap.adoc` — promote `Sqlite.affine` from `partial / Coverage audit needed` to `usable`, and add `Aggregate.affine` + `Transaction.affine` rows to the inventory snapshot. - `.machine_readable/6a2/STATE.a2ml` — bump `last-updated` to `2026-06-02` (this file mirrors, it does not lead — per its own drift-flag). ## What was deliberately *not* touched - `docs/ROADMAP.adoc` — language/compiler progress; the db-theory PRs are stdlib-side and don't move the language roadmap. - A `TEST-NEEDS` file — none exists at repo root; the three PRs each shipped their own Deno-ESM smoke harness under `tests/codegen-deno/` (`sqlite_introspect_bulk` / `transaction_smoke` / `aggregate_smoke`) and the AOT gate auto-picked the new modules up. - License / SPDX headers — per the estate's no-automated-licence-edits rule. ## Test plan - [x] `bash tools/check-doc-truthing.sh` passes locally — banner / primacy / mirror invariants intact, over-claim ratchet unchanged (no new baseline entry needed). - [x] Commit GPG-signed; verified `gpg: Good signature`. Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

hyperpolymath enabled auto-merge (squash) June 1, 2026 13:44

hyperpolymath mentioned this pull request Jun 1, 2026

Add TransactionMutations module — instantiate no-section-of-collapsing-map for SQL transaction rollback safety (consumer: affinescript db-theory #2) hyperpolymath/echo-types#174

Closed

5 tasks

hyperpolymath mentioned this pull request Jun 1, 2026

feat(stdlib): Aggregate.affine — SQL group-by + aggregation primitives — db-theory #3 (7 externs) #527

Merged

3 tasks

hyperpolymath and others added 3 commits June 2, 2026 10:39

hyperpolymath force-pushed the feat/db-2-transactions branch from f08fcc7 to 8c760d2 Compare June 2, 2026 09:40

hyperpolymath merged commit a00af13 into main Jun 2, 2026
15 of 24 checks passed

hyperpolymath deleted the feat/db-2-transactions branch June 2, 2026 09:41

hyperpolymath mentioned this pull request Jun 2, 2026

docs: refresh status after db-theory PRs #525/#526/#527/#528 #529

Merged

2 tasks

Navigation Menu

Uh oh!

feat(stdlib): Transaction.affine — affine-bounded write-set isolation — db-theory #2 (8 externs) - #526

feat(stdlib): Transaction.affine — affine-bounded write-set isolation — db-theory #2 (8 externs)#526
hyperpolymath merged 3 commits into
mainfrom
feat/db-2-transactions

hyperpolymath commented Jun 1, 2026

github-actions Bot commented Jun 1, 2026

github-actions Bot commented Jun 1, 2026

github-actions Bot commented Jun 1, 2026

Uh oh!

github-actions Bot commented Jun 2, 2026

Labels

1 participant

Uh oh!

Conversation

hyperpolymath commented Jun 1, 2026

Summary

Proof obligation cross-doc

Test plan

github-actions Bot commented Jun 1, 2026

🔍 Hypatia Security Scan

github-actions Bot commented Jun 1, 2026

🔍 Hypatia Security Scan

github-actions Bot commented Jun 1, 2026

🔍 Hypatia Security Scan

Uh oh!

github-actions Bot commented Jun 2, 2026

🔍 Hypatia Security Scan

Labels

1 participant