Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 13 additions & 0 deletions docs/PROGRAM_BOARD.md
Original file line number Diff line number Diff line change
Expand Up @@ -122,6 +122,17 @@ gates do not shrink.
- libcrux fits as the verified crypto link. It needs an owner-approved
RUSTSEC-2026-0173 exception, decided when phase 2 starts.
- Phases 0–1 can start now.
- **063 Generalized gateway.** Spec:
[AP-SPEC-063](specs/0063-generalized-gateway.md) (draft, not started).
- It covers five things: per-recipe recovery capability, the provider
capabilities the Stripe vertical proved necessary, one spend limit, an
operator plane the application cannot interfere with, and evidence and
assurance.
- It has eight epics; epic 8 runs only under §12 option A.
- Owner decision, 2026-09-27: §12 option A. The gateway becomes the single
provider-write path, and epic 8 retires the five local-agent effect
profiles.
- §13's readings are PROVISIONAL.
- **Reads through the gateway.** Read recipes, response projection
(`allowed_fields`, `maximum_response_bytes` as in 0024 §10), disclosure
receipts. Confidentiality additionally needs hermetic agent egress.
Expand Down Expand Up @@ -202,6 +213,8 @@ gates do not shrink.
| 2026-09-25 | Owner direction: the 2026-09-24 review pass is implemented as PRs in priority order, without filing public issues; a security weakness goes to a private advisory first. Decisions inside that work that the owner has not taken follow rule 8 (narrower reading, logged PROVISIONAL). | §3 "Review pass 2026-09-24"; `docs/audit/settled.md` |
| 2026-09-25 | PROVISIONAL, taken unattended as the narrower readings for package 2.5 (kernel conformance) of the 2026-09-24 review, whose check-precedence decision the owner delegated: native's current order is codified, and only the attachment-limit line changes in Rust. (1) The canonical action is decoded, with its input, body, and detached-attachment bounds, before the proof, and a failure there carries no plan digest. The Go and TypeScript verifiers decode it the same way and return the native codes: fields read in key order, each bound checked as its field is read, the canonical encoding checked last. (2) Detached attachments are bounded by the aggregate attachment limit, as the spec and CDDL already said; native used the bundle limit, which denied attachments between the two limits and ignored a lowered attachment limit in process. (3) One check precedence, native's: decode (context, canonical action, proof), reference resolution, principal control (registry manifest and configuration first), action binding before any branch, authority branches, then plan and composition. Binding runs the carried body, each action's fields, profile, audience, challenge, evaluation time, channel, shared meaning, extensions, and observation attachments, then attachments, then the profile policy. Each branch runs root control, anchor acceptance, statuses (the anchor, then each grant's status and subject), the resource matcher, namespaces, the budget chain, the delegation walk, terminal coverage, the action's control, assurance, and observation. A statement's control failure is deferred to the branch that needs it. (4) Every grant permission's resource, not only the action's, must lie inside the anchor's namespaces, as native requires. (5) A budget algebra is resolved only where a bounded ceiling is compared, and a value in another algebra is local-policy-denied, the algebra rejecting its input; Go and TypeScript had resolved every algebra up front, including those of unrelated anchors, and returned indeterminate. (6) For a grant after the first, the observation-requirement drop check and the attenuation laws run before any handler evaluates the grant's extensions, so a malformed or over-limit child payload is `observation-requirement-dropped` under a parent with requirements and `delegation-expanded` otherwise, never the handler's code; `protocol.md` now defers to the per-extension laws instead of byte-for-byte preservation. | `core/spec/v1/verification-algorithm.md` "Stages"; `core/spec/v1/registry.md` "Attenuation laws"; `core/spec/v1/protocol.md` "Trust anchor", "Grant"; `core/spec/v1/error-codes.md`; `docs/LIMIT_COVERAGE.md` |
| 2026-09-25 | PROVISIONAL, taken unattended as the narrower readings for package 2.6 (status statements) of the 2026-09-24 review, whose `purpose` decision the owner left open: (1) `purpose` is removed from principal-status statements rather than given purpose-scoped selection, which would add role semantics no spec defines. The wire loses key 3 and the later keys move down one, one direct cutover with no reader for the old shape (a ten-entry statement is `malformed-proof`); the carried-status rollback check keys on the principal alone, as selection does; the Python and WASM authoring APIs and the TypeScript engine contract drop the argument. (2) The accepted-extension rule covers every statement about a principal or grant whose status a branch evaluates, whatever its method or issuer and whether or not selection would pick it, checked after the statement's control and before selection; statements about subjects the branch does not evaluate are not checked. (3) As for actions and grants, the first extension in canonical order decides: an identifier the context does not accept is `critical-extension-unknown`, an accepted one `unsupported-critical-extension`. (4) No registered extension, `exact-marker-v1` included, has a status handler, so an accepted extension on an evaluated status statement is never evaluated and is always `unsupported-critical-extension`; a status extension needs a protocol review, an executable model, and a new manifest. | `core/spec/v1/protocol.md` "Evidence and status"; `core/spec/v1/verification-algorithm.md` "Principal status", "Grant status"; `core/spec/v1/registry.md` "Status-statement extensions"; `core/spec/v1/auths-proof.cddl` |
| 2026-09-25 | Owner directed AP-SPEC-063 (the generalized gateway) to be written as a draft before its epic starts. Writing it does not start an epic; the WIP limit still governs. The single-provider-write-path choice is left to the owner (§12), and §13's readings are PROVISIONAL. | 0063 §12, §13 |
| 2026-09-27 | Owner decision on AP-SPEC-063 §12: option A. The gateway becomes the single provider-write path. Epic 8 removes the five local-agent effect profiles in one cutover, and the PostgreSQL and OpenTofu production paths end with them, since they have no HTTP equivalent. The domain crates stay as test-only references, and §12's table lists what production gives up. | 0063 §12, §15 |
| 2026-09-26 | The owner delegated the choice between two fixes. Taken: when protected-base translation evidence is missing, `formal translation` runs two clean reproductions in the same job, rather than also reusing base runs where only the translation job succeeded. Six of the last eight `main` push runs were cancelled by newer merges, which the second fix cannot cover. Evidence that is found but fails binding still fails the job, and every pull-request reproduction still packages generated drift. | `docs/ci/formal-translation-evidence.md`; `.github/workflows/ci.yml` |
| 2026-09-26 | The owner delegated whether `formal Lean authoritative` fails when it packages an assurance update. Taken: it fails, as `formal translation` does, so the job that found the drift is the red one; the `formal-translation` gate and `CI qualified` were already red, and the updater keys off the update artifact, not job status. The job now declares the `update_required` output that `formal evidence` gates on, so aggregation is skipped instead of failing on a missing Lean artifact, and xtask requires both. | `.github/workflows/ci.yml`; `xtask/src/formal_qualification.rs` |

Expand Down
Loading
Loading