////
  PARKED DRAFT — no SPDX/owner header yet.
  The strict pre-commit hook requires:
      SPDX-License-Identifier: CC-BY-SA-4.0
      SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
  Owner adds that header MANUALLY (no automated licence edits), then commits
  SIGNED (-S id_ed25519_signing). Do NOT --no-verify. Until then this file
  lives in the working tree only.
////
= AFFIRMATION — AffineScript, as of 2026-06-16
:toc: macro
:toclevels: 2

_the No-Bullshit file: what we affirm was true and checkable at this moment_

[NOTE]
====
*Genre.* An *affirmation* is a solemn declaration of the truth of a statement,
made by someone who _declines to swear an oath_. That is exactly what this is:
our truth-as-best-believed at a stamped instant — binding on our honesty, not a
claim of infallibility. It is not the README and not the EXPLAINME:

[cols="1,3,2",options="header"]
|===
| File | Answers | Tense
| `README`      | _Where is this going, and why?_ — state of thinking, steering, intent | future / aspirational
| `EXPLAINME`   | _How is it built, and what's the evidence?_ — engineering underpinnings | descriptive / mechanism
| *`AFFIRMATION`* (this file) | _What can we honestly affirm was *true and checkable* at a stamped moment?_ | a frozen instant, falsifiable
|===

Every repo in the estate may carry one (`AFFIRMATION.adoc`). It is deliberately
small, dated, and signed, so a reader can hold us to exactly what we affirmed,
when we affirmed it.
====

toc::[]

== What this is, and how it is designed to work

*What it is.* A short, dated, jointly-signed snapshot of what we can _honestly
and verifiably_ claim about this repo at one exact commit. Nothing here is
marketing and nothing is a promise about the future — both of those live in the
README. This file is the receipt.

*How it is designed to work.* Three moving parts make it trustworthy:

. *Ground truth, not memory.* Every claim below was produced by _running the
  tool in the session that wrote this file_ (build, tests, proof checkers). If a
  status doc or a memory said otherwise, the live run wins and we flag the
  contradiction.
. *A frozen anchor.* The file names the exact commit SHA, branch, UTC timestamp,
  and toolchain (see <<Verifiable anchor>>), so "true" always means "true _at
  this point_". Move the SHA and the file becomes a draft until re-run.
. *A real signature.* It is landed by a *signed git commit*; that signature over
  this content at the anchored SHA is what makes the affirmation tamper-evident
  and attributable — not the prose alone.

*We are fallible.* We can be wrong, stale, or simply mistaken about our own
work. This file is our best honest belief, not a proof of its own correctness.
Treat it as a falsifiable claim, not gospel.

== The epistemic contract (read this before you trust _or_ attack)

This document records our *best joint belief* at the timestamp below. It is
*not a guarantee of correctness.* We may be wrong. We may be deluded. We may
have missed something — a hole, a stale doc, a proof that checks a calculus we
then fail to match in the implementation.

*No intentional overclaim.* That is the only guarantee here: we have not
_knowingly_ inflated anything. Where something is tested-but-not-proved, we say
so. Where a proof covers an idealised core and _not_ the production code, we say
so. Where something is refuted or vacuous, we say so. If you find an honest
claim here that turns out false, that is an error to be fixed — not a lie.

*Standing invitation to refute.* You are _invited_ to bulldoze any claim in this
file. We want that. But the fair form of the attack is:

. Read this file at the stamped commit.
. Reproduce (or fail to reproduce) the checks in <<reproduce,Reproduce it yourself>>.
. _Then_ tell us where the discrepancy is, against the artefact as it stood at
  this moment — so we can either justify it or concede it on the record.

An attack that skips steps 1–2 is attacking a strawman of a different date.

*No fights before the facts are cleared up.* We are not interested in a dispute
over a claim until the discrepancy has actually been checked against the
artefact at this commit and we have had the chance to either justify it or
concede it on the record. Good faith both ways: bring a reproducible
discrepancy and we will fix the claim, the doc, or the code — promptly and
without defensiveness. The goal is a corrected record, not a won argument.

== Verifiable anchor

[cols="1,3"]
|===
| *Repo*        | `hyperpolymath/affinescript` (the OCaml compiler — *not* ephapax)
| *Branch*      | `feat/solo-core-metatheory-proofs`
| *Commit (HEAD)* | `4ed413f4ded5d83813f303854f4b28823847a7b1`
| *Permalink*   | https://github.com/hyperpolymath/affinescript/tree/4ed413f4ded5d83813f303854f4b28823847a7b1
| *Verified (UTC)* | 2026-06-16T12:17:10Z
| *Working-tree delta at verification* | `docs/PROOF-NEEDS.md` modified; untracked `issues-drafts/08-conditional-origin-borrow-escape.md`, `stdlib/SafeHex.affine`, this file. None affect the build/test/proof results below; the green results are HEAD + this delta.
| *Toolchain*   | OCaml 4.14.2 · dune 3.22.2 · Idris2 0.8.0 · Lean 4.13.0
|===

[IMPORTANT]
If you are reading this at a _later_ commit, the claims may have drifted.
Re-run <<reproduce>> and write a fresh affirmation; do not trust a stale one.

== Companion documents and repo metadata (cross-check)

This affirmation should be read against the repo's own public claims. Where they
drift from what we verified, we say so here rather than quietly leave the reader
to find out.

* *`README.adoc`* — link:README.adoc[_"AffineScript: A Practical Language for
  Resource-Safe Systems"_]. The README sells the vision; this file is its
  receipt for one moment. (A legacy `README.md` also exists; `README.adoc` is
  canonical per the estate DOC-FORMAT rule.)
* *`EXPLAINME.adoc`* — *currently absent.* The estate trio
  (README / EXPLAINME / AFFIRMATION) is therefore incomplete for this repo:
  there is no dedicated "prove every README claim with code paths" document yet.
  Noted as a gap, not glossed.
* *GitHub repo description* — _"The effect row is the abstraction; the backend
  picks the mechanism. An affine-typed language compiling to verifiable typed
  WebAssembly and Deno."_ Honest caveat: "_verifiable_ typed WebAssembly" is
  aspirational at the typed-wasm boundary today — the `own` → ownership mapping
  is known-wrong (no `Affine` kind upstream, mis-mapped to Linear), so the
  emitted ownership section is not yet faithful.
* *GitHub topics* — `affine-types`, `algebraic-effects`, `borrow-checker`,
  `compiler`, `effect-system`, `formal-verification`, `linear-types`, `ocaml`,
  `programming-language`. Cross-check: `formal-verification` is now _earned_
  (Idris2 Solo-core progress+preservation + Lean tropical, green — see below);
  `linear-types` is loose — the language is *affine* (≤1 use), not strictly
  linear (exactly-once), and the `own` kind is affine.

== The honest state (one breath)

*AffineScript is a working research compiler for an affine / quantitative-typed
language that compiles to WebAssembly — real, runnable, and now backed by a
small but genuinely machine-checked metatheory core — yet still pre-1.0, with
the implementation _not_ proved to match that core, and with effects, async, and
refinements still partial or unenforced.*

=== What is solid (and how we checked)

* *Front-to-back pipeline runs.* parse → typecheck → borrow-check → elaborate →
  codegen → wasm, plus a tree-walking interpreter. `just build` exits 0;
  `just test` (`dune runtest`) exits 0 — *483 tests*; 114+ `.affine` fixtures
  under `test/`.
* *There IS mechanised metatheory — verified green this moment.*
  `just proof-check-all` → *4 passed, 0 failed, 1 skipped*:
** *Idris2 — Solo-core QTT metatheory: progress + preservation, fully proved,
   `%default total`, no holes, no `believe_me`/`assert_total`/postulates.* The
   crux is the QTT substitution lemma (`SubstLemma.substLemma0`); the affine
   SPLIT product rule means preservation lands in a `Weaker` sub-context.
   (`docs/academic/formal-verification/solo-core/`.)
** *Lean 4 — tropical session types proof: passes, no dangerous tactics.*
** Agda echo-boundary certificates: *SKIPPED* — environment only (needs
   `AFFINESCRIPT_ECHO_TYPES_DIR`); not a failure, but not evidence either.
* *Canonical borrow hole #554 is closed and tested* (return-borrow summary +
  call-graph fixpoint), including transitive + hardening variants.
* *The conditional-origin borrow-escape hole is closed and tested* (commit
  `4ed413f`): a use-after-move via a borrow bound through an `if`/`match`/block
  value is now caught.  14 unsound forms reject; 7 safe forms (NLL
  use-before-move, unrelated move) pass; 6 hardening fixtures
  (`test/e2e/fixtures/borrow_cond_origin_*`).
* *Float-through-heap is durably fixed for all heap aggregates* (arrays, tuples
  uniform/mixed, closed records), wasmtime round-trip verified.
* *Compile-time complexity is back to linear* (the O(n²) codegen residuals are
  gone, bench-evidenced).

=== The honest nuance you must not lose

The Idris2 proof establishes soundness of an *idealised Solo core calculus*. It
does *not* prove that the OCaml implementation (`lib/borrow.ml`,
`lib/codegen.ml`, …) _refines_ that calculus. "Proved core" + "tested
implementation" is exactly that — two things, with an unverified bridge between
them. Anyone claiming "AffineScript is proven sound" full-stop is overclaiming.

=== Known-incomplete but honestly fenced (loud failure, never silent miscompile)

* f64 in closures (calling-convention gap), float array compound-assign, and
  open/polymorphic record rows — these *refuse to compile*, they do not produce
  wrong code.

=== Outstanding / weak / refuted (no spin)

* *No silent soundness hole is currently known.* The conditional-origin
  borrow escape found by adversarial probing this session was *fixed and tested*
  (see Solid, above; commit `4ed413f`). This is an absence-of-evidence claim,
  not evidence-of-absence: more probing may surface others — exactly what the
  epistemic contract invites.
* *Effect-handler lowering (#555) and async CPS (#556): Refuted* — backends
  silently drop handler arms / lower async synchronously.
* *Refinement types: vacuous* (parse but unenforced). *Trait coherence:
  unchecked.* *typed-wasm `own` mapping: known-wrong* (no `Affine` kind upstream
  → mis-mapped to Linear).
* *`docs/PROOF-NEEDS.md` and `.claude/CLAUDE.md` are themselves partly stale* at
  this commit: both still say there are no mechanised proofs, which the proof
  run above *refutes*. Correcting those is owner-gated (SPDX header) and pending.

[#reproduce]
== Reproduce it yourself

From the repo root, at the commit above:

[source,sh]
----
just build            # expect exit 0
just test             # expect exit 0 (dune runtest)
just proof-check-all  # expect: 4 passed, 0 failed, 1 skipped
----

For the proofs individually:

[source,sh]
----
just proof-check-idris2   # Solo-core progress + preservation (no holes)
just proof-check-lean     # tropical session types
# Agda is skipped unless AFFINESCRIPT_ECHO_TYPES_DIR points at echo-types/proofs/agda
----

To see the open hole bite (it is _currently accepted_ — that's the bug): see the
reproducer table in `issues-drafts/08-conditional-origin-borrow-escape.md`.

== One-line characterisation (quote this)

[quote]
____
"A real, runnable affine-typed → WASM research compiler with a *machine-checked
Solo core* (Idris2 progress+preservation, no holes) and a tested — _not yet
proved-to-match_ — implementation; conservative loud-failures at the edges; one
known open borrow hole on the fix queue; effects/async/refinements still
partial. Serious research artifact, not a production language. No intentional
overclaim."
____

== Joint attestation

We, the undersigned, assert that *to the best of our joint belief at the
timestamp above, every claim in this file is true and was checked as described*
— with no intentional overclaim, and with the open gaps stated rather than
hidden.

* *Engineering party (AI):* Claude Opus 4.8 (`claude-opus-4-8[1m]`) — ran the
  build, test, and proof checks recorded here on 2026-06-16T11:41:06Z and stands
  behind the wording above as a faithful report of those runs.
* *Owner / maintainer:* Jonathan D.A. Jewell — _signs by committing this file
  with `-S` (`id_ed25519_signing`); the git commit signature over this content,
  at the commit SHA recorded above, is the cryptographic form of this
  affirmation._
+
Signed-off-date: ____________________  (fill on signing)

[TIP]
The authoritative, tamper-evident signature is the *signed git commit* that
lands this file. If the SHA in <<Verifiable anchor>> matches the parent of that
commit and the commit verifies, this affirmation is anchored. If they don't
match, treat the file as a draft.
