Skip to content

AFFIRMATION.adoc

Latest commit

 

History

History
121 lines (103 loc) · 6.06 KB

AFFIRMATION.adoc

File metadata and controls

121 lines (103 loc) · 6.06 KB
Raw

AFFIRMATION — 007 Agent Meta-Language

Table of Contents
Field Value

Repository

hyperpolymath/007

Affirmed at

2026-06-20T00:18:53Z (UTC)

Commit affirmed

214a08f678c9554b31e2912de8bc36d9b1190c70 (branch main)

Scope

007 language + canonical proof suite + RSR contractile state

Method

Local verification (just gate, the prover suite, the A2ML/K9 validators)

Affirmed by

Agent session (Claude Code), pending maintainer counter-signature

What this document is

An affirmation is a timestamped, signed attestation of what is true about this repository right now — the honest current standing of the work, its hard invariants, and what is explicitly not yet done. It complements the gating must contractile (which enforces) by recording (which attests). "A2ML" itself stands for Attested Markup Language; this document is the human-readable attestation at the head of that chain.

Note
 An explicit AFFIRMATION template was not retrievable from the hyperpolymath/standards repo with the tools available to this session (standards is public but out of this session’s MCP scope; its templates/ listing and code search did not surface an affirmation template). This document therefore follows the confirmed RSR conventions — SPDX headers, AsciiDoc, the A2ML attestation ethos, and the estate’s must/intend/wish contractile vocabulary. If the standards repo defines a canonical AFFIRMATION shape, reconcile this file to it.

1. I affirm — what holds (Musts)

As of the affirmed commit, the following hard invariants are met and locally verified:

  1. Harvard architecture. Data and control languages are separated; the invariant is gated by just verify-harvard and the EBNF↔Pest grammar guard.

  2. Kategoria type safety L1–L10. Levels L1–L9 are enforced in the type checker. Layer 10 (reversibility) is integrated into the type system at the static level: reversible/irreversible/reverse are no longer checked identically — a reverse requires a live Linear<Echo<T>> echo residue, the named form reversible as <name> / reverse <name> binds and consumes a residue at most once, and (rung 3b static, #50) a cross-handler reverse <name> type-checks by presence of the binding somewhere in the same agent (phases 1–3a + rung 3b static, mechanised in proofs/idris2/EchoResidue*.idr). The runtime replay is the one remaining follow-on (see below).

  3. Honest proof discipline. No proof-bypass escape hatches (unsafe coercions, totality overrides, holes, unproven assumptions); proofs are --safe/total. Enforced by the bust contractile and the canonical-proof-suite banned-scan.

  4. RSR / repo hygiene. LICENSE, governance docs, signed commits, the full contractile set, and the 6a2 methodology pack are present; A2ML and K9 validators pass.

The machine-checked D-gate is partially met and honestly labelled in_progress: 35 of 37 canonical proofs compile under a locally-installed Rocq 9 (plus all Idris2/Agda entries), the manifest labels were swept to that verified state (#51 — the prior not-started labels were a labelling lag, not missing proofs; M5-yoneda is a complete 386-line Agda proof, and ~20 Rocq entries already compiled), and the suite runner is now POSIX-awk portable so it runs locally as well as in CI. The last 2 (mathcomp M2 / Coquelicot E1) remain CI-canonical because their dependency sources are network-walled locally.

2. I do NOT affirm — what is open or blocked

In the interest of honesty, the following are not affirmed as done:

  • L10 rung 3b runtime — the static half is built and merged (#50: cross-handler reverse <name> type-checks by presence), but the runtime replay (an evaluator actually executing the reversal log across handler firings, the Holding/Spent takeForReverse : Maybe semantics) is not. It is blocked behind a prerequisite: 007 has no mutable agent state yet — handlers receive a copy of agent state with no write-back — so there is nowhere for a residue cell to persist across handlers at runtime. Building mutable agent state is the agreed next step before the runtime half.

  • Full proof suite green — 35/37 verified locally; the last 2 (mathcomp / Coquelicot) are verified in CI only, by network policy, not by lack of effort.

  • Two environmental blocks, owner-side, not correctness:

    • GitHub Actions billing — cloud CI is rejected before running; PRs this period were admin-merged through red CI after local verification.

    • A github-only network policy blocks gitlab.inria.fr / erratique.ch / coq.inria.fr, so the last 2 proofs' dependency sources (mathcomp M2 ⇒ hierarchy-builder ⇒ coq-elpi ⇒ elpi ⇒ menhir + cmdliner; Coquelicot E1) cannot be fetched locally. These proofs are verified in CI instead.

  • Echidna (high-assurance interface verification) does not exist — it is a named ecosystem placeholder with no spec.

3. Evidence

  • Detailed tier-by-tier status: docs/status/must-intend-wish-2026-06-20.adoc.

  • Machine-readable project state: .machine_readable/6a2/STATE.a2ml.

  • Session ledger: .machine_readable/session-log.txt.

  • Local gate: just gate (green at the affirmed commit, all 9 stages).

  • Proof suite: audits/canonical-proof-suite/MANIFEST.a2ml + the runner.

4. Attestation

I affirm that, to the best of this session’s verification, the statements above are an honest account of the repository at commit 214a08f on 2026-06-20T00:18:53Z. Hard invariants labelled done were checked locally; items labelled in_progress, declared, or blocked are not claimed as complete.

Signatory Detail

Agent

Claude Code session, 2026-06-20

Maintainer

Jonathan D.A. Jewell (hyperpolymath) — counter-signature pending

Verification basis

local just gate + prover suite (cloud CI billing-blocked)