// SPDX-License-Identifier: CC-BY-SA-4.0
// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>

= Solo Core — Idris2 Mechanization
Jonathan D.A. Jewell
:toc: left
:source-highlighter: rouge

== Scope

This directory holds the Idris2 mechanization of the *Solo* core of
AffineScript — the minimal fragment sufficient to prove affine
preservation. Solo is:

* Simply-typed lambda calculus
* Unit type
* Product (pair) types
* Sum types
* `let` binding
* Each binder annotated with a QTT quantity `q ∈ {0, 1, ω}`

Solo deliberately *excludes* traits, effects, row polymorphism,
refinement types, dependent types, ownership (`own`/`ref`/`mut`),
records, arrays, modules, and the entire effect system. Those belong
to *Duet* (traits + effects) and *Ensemble* (full language), which
will be mechanized in later tracks.

== Proof Goals (Track F1) — STATUS: PROVED

. *Progress*: a closed, well-typed Solo term is either a value or
  steps. — *proved* (`Soundness.progress`, total, hole-free).
. *Preservation* (affine): reduction preserves typing up to dropping
  resources — the reduct is typed in a `Weaker` SUB-context `g' ≤ g`
  (pointwise `qLe`, same shape/types). — *proved*
  (`Soundness.preservation`).
. *Affine preservation*: same statement (`Soundness.affinePreservation`).

All three are mechanically checked: `idris2 --check Soundness.idr`
exits 0, every definition is `total`, and there is no `believe_me`,
`assert_total`, `really_believe_me`, `postulate` or `?`-hole.

[NOTE]
====
*Why the conclusion is a sub-context, not the same `Γ`.* The original
week-1-2 statement asked for the reduct in the *same* `Γ` (and "`1`
consumed exactly once" — a *linear* phrasing). Mechanisation showed
that is *false* for the Solo core as designed: `TPair` introduces
multiplicatively (`AddCtx g1 g2 g`, resources split) but is eliminated
by the projections `Fst`/`Snd`. `Snd (Pair x y) → y` (with `x` linear)
leaves `y` typed in a *smaller* context — the projected-away component's
resources are dropped. Every β-rule preserves the context *exactly*
(via the substitution lemma); only the two projections shrink it.

Per the owner decision (2026-06-15) this is resolved the *affine* way —
AffineScript is affine (the OCaml `q_le observed declared` check permits
under-use), so dropping is legitimate and the honest theorem is the
sub-context one above. The language is unchanged (split product +
projections + eager CBV kept). See the per-rung discussion in
`dev-notes/2026-06-15-affinescript-solo-core-preservation/`.
====

== Ground-Truth Rule

[IMPORTANT]
====
The proof must *track the OCaml implementation*, not an idealized
QTT. When the Idris2 formalisation and `lib/quantity.ml` +
`lib/typecheck.ml` disagree, *the OCaml implementation is ground
truth* until an ADR is filed that explicitly reverses this.

Track F re-verifies against Track A's affine test fixtures (under
`test/e2e/fixtures/`):

* `affine_let_valid_sugar.affine`, `linear_arrow.affine` — accepted.
* `linear_arrow_violation.affine`,
  `slice_d_captured_linear_{param,let}_rejected.affine` — rejected.
* `affine_violation.affine` (`fn double_use(x) = x + x`) — *accepted*
  via the surface `check` because `x` is unannotated (quantity ω;
  `qAdd One One = Omega`); the linear double-use is exercised
  *programmatically* by `test_quantity_affine_violation` in
  `test/test_e2e.ml`.

Verified 2026-06-15: the compiler accepts linear-used-once and
ω-used-many, rejects linear-used-twice — consistent with the proven
Solo rules. If the mechanization and the compiler ever diverge on
these fixtures, the proof is wrong, not the compiler.
====

== Files

[cols="1,3"]
|===
| File | Status

| `Quantity.idr`
| Semiring `{0, 1, ω}` — definitions + semiring laws.
  *Mirrors* `lib/quantity.ml` `q_add` / `q_mul` / `q_le` exactly.

| `Syntax.idr`
| Solo types and terms with de Bruijn indices.

| `Context.idr`
| Snoc-list contexts of `(Ty, Q)` entries, pointwise addition and
  scalar multiplication.

| `Typing.idr`
| QTT-style typing judgement `Has : Ctx -> Tm -> Ty -> Type`.
  Split contexts of T-App/T-Pair/T-Case/T-Let are explicit `AddCtx`
  premises; T-Var/T-Unit use an analysable `IsZero` premise. (Encoding
  change from the statement-only version so the judgement is provable
  in Idris2 — same set of derivations.)

| `ContextLemmas.idr`
| The QTT context algebra: the inductive additive split `AddCtx`
  (type-tracking, Maybe-free), `IsZero`, the scaling/commutativity/
  associativity/interchange laws (reusing `Quantity.idr`), and the
  `Weaker` sub-context order with its monotonicity lemmas.

| `Subst.idr`
| de Bruijn `shift` / single-variable `subst` / `subst0`.

| `SubstLemma.idr`
| Weakening (`weakenAt`) + the QTT substitution lemma
  (`substGen` / `substLemma0`), proved by induction on the body's
  typing derivation, generalised over a `cross` context of crossed
  binders.

| `Soundness.idr`
| `Value`, the CBV `Step` relation (16 rules, spec §4.2-4.3), and the
  *proved* `progress` / `preservation` / `affinePreservation`.
|===

== Status Block

[source]
----
Phase:       Track F1 COMPLETE — progress + (affine) preservation proved
Last sync:   2026-06-15
OCaml refs:  lib/quantity.ml, lib/types.ml, lib/typecheck.ml
Spec refs:   docs/spec.md §3.1-3.6 (Solo-relevant rules only)
Idris2 ver:  0.8.0 (verified locally; idris2 --check Soundness.idr exit 0)
Dangerous:   none (no believe_me / assert_total / really_believe_me / postulate)
Holes:       none (all definitions total)
Decision:    preservation is AFFINE (reduct in a Weaker sub-context);
             split product + projections kept (owner decision 2026-06-15)
Check:       just proof-check-idris2
----

== Out of Scope (Tracks F2, F3, …)

* Duet: traits, effects, effect rows, handlers, resume
* Ensemble: row polymorphism, refinements, dependent types,
  ownership/borrowing, modules, `unsafe`
* Compiler-level soundness (backend / codegen)
* Termination of non-`total` functions

== Weekly Check

Each week, re-run `idris2 --check` on every file in this directory
and re-run the compiler against the two `examples/affine_*.affine`
fixtures. Divergence = file an ADR, not a silent fix.
