// 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, Weeks 1–12)

. *Progress*: a closed, well-typed Solo term is either a value or
  steps.
. *Preservation*: reduction preserves typing.
. *Affine preservation*: reduction preserves the quantity semiring
  accounting — a term typed in context `Γ` steps to a term typed in
  the same `Γ`, and `1`-quantity bindings are consumed exactly once.

This file-set is the *week 1-2* deliverable: syntax, contexts,
typing judgement, and *statements* (not proofs) of progress and
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 weekly against Track A's test fixtures:

* `examples/affine_basic.affine`
* `examples/affine_violation.affine`

If the mechanization and the compiler 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`.
  Rules only; no meta-theorems yet.

| `Soundness.idr`
| *Statements* of `progress` and `preservation` with
  `?todo_progress` / `?todo_preservation` holes. Proofs are
  weeks 3-12 work.
|===

== Status Block

[source]
----
Phase:       Track F1, week 1-2 (syntax + statements)
Last sync:   2026-04-10
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)
Dangerous:   none (no believe_me, no assert_total, no really_believe_me)
Holes:       ?todo_progress, ?todo_preservation (intentional)
----

== 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.
