ABI: make Idris2 proofs genuinely compile + add machine-checked theorems (#34)

* Add SPDX header to LICENSE and set Cargo.toml license field

The governance/licence-consistency check requires an SPDX-License-Identifier
header on the LICENSE file and a `license` field in the manifest. The LICENSE
body is MPL-2.0 text, so stamp `SPDX-License-Identifier: MPL-2.0` (matching the
actual body) and set `license = "MPL-2.0"` (replacing `license-file`).

Verified with standards/scripts/check-licence-consistency.sh (passes).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01DF9CcCuL4YJoqs26eHsYiA

* Normalize licensing to MPL-2.0 (code) + CC-BY-SA-4.0 (docs)

Make the repo's licensing single and consistent, matching the wokelangiser
reference policy and the merged iseriser pattern:

- Remove contradictory PMPL-1.0-or-later / Palimpsest self-claims from README
  badges/footers, QUICKSTART, RSR_OUTLINE, STATE-VISUALIZER, and machine-readable
  governance (META, stapeln, deny.toml allow-list, copilot/AGENTIC SPDX
  directives, Trust/Must LICENSE-content checks, per-project CLAUDE.md).
- Encode the docs split in REUSE dep5: *.adoc/*.md/docs/** -> CC-BY-SA-4.0,
  everything else -> MPL-2.0.
- READMEs show MPL-2.0 (code) + CC-BY-SA-4.0 (docs) badges; full texts live in
  LICENSES/; root LICENSE stays MPL-2.0 for GitHub's licence chip.

Preserves legitimate non-self references: cargo-deny's AGPL deny-list, the
"never use AGPL" estate policy, and the Contributor Covenant CoC.

Verified: standards/scripts/check-licence-consistency.sh passes; no residual
PMPL/Palimpsest self-claims remain.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01DF9CcCuL4YJoqs26eHsYiA

* fix(abi): make Idris2 ABI proofs genuinely compile and verify under 0.7.0

The src/interface/abi Idris2 ABI was scaffolded from a template and never
compiler-checked. This makes all three modules typecheck cleanly and adds a
machine-checked Proofs module, with zero errors and zero warnings under
Idris2 0.7.0 (idris2 --build tlaiser-abi.ipkg).

Systemic fixes:
- Types: replace the non-compiling `decEq _ _ = No absurd` catch-all in the
  `DecEq Result` instance with explicit off-diagonal `No (\case Refl impossible)`
  cases for all 8 constructors.
- Types: `createHandle` now derives a real `So (ptr /= 0)` via `choose` instead
  of leaving the `MkHandle` auto-implicit unsolved.
- Types: `thisPlatform` is a plain `Linux` value (the `%runElab` stub required
  ElabReflection and did not compile).
- Layout: `paddingFor` uses `minus` (Nat has no `-`); imports Data.Nat.
- Layout: add sound `decDivides`/`decFieldsAligned`; `checkCABI` builds a real
  `CABICompliant` witness instead of a `?fieldsAlignedProof` hole.
- Layout: `offsetInBounds` returns `Maybe (So ...)` via `choose` (the universal
  `So` return type was unsound); `alignUpDivides` decides divisibility soundly.
- Layout: concrete/parameterised StructLayouts supply genuine erased proofs.
  For the parameterised state-space/trace-step layouts the `sizeCorrect`
  obligation is discharged by an inductive `foldlSizes8` lemma (no axioms),
  and `aligned` by `DivideBy` with multiplication that reduces at the type level.

Pre-existing template bugs also fixed in Types:
- rename local `NonEmpty` (on StateMachine) to `StateMachineNonEmpty` so the
  trace obligation resolves to the Prelude list `NonEmpty` (import Data.List);
- `CPtr` matches on Platform (was `Bits (ptrSize p)`, ill-typed);
- `cSizeOf`/`cAlignOf` match on concrete primitive types (could not match on the
  `CInt`/`CSize` type-level functions).

Buildability:
- git mv flat files into Tlaiser/ABI/ nested namespace layout;
- add src/interface/abi/tlaiser-abi.ipkg;
- .gitignore now ignores **/build/, *.ttc, *.ttm.

New Tlaiser.ABI.Proofs theorems (export, machine-checked):
- modelCheckRequestCompliant : CABICompliant of the concrete FFI struct, built
  directly from per-field DivideBy witnesses;
- okIsZero, stateSpaceExhaustedIsSeven : result-code encoding pins;
- okDistinctFromTlcError : the encoding is injective on the switched codes.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01DF9CcCuL4YJoqs26eHsYiA

---------

Co-authored-by: Jonathan D.A. Jewell <paraordinate@yahoo.co.uk>
Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

Author: 3 people

.gitignore

@@ -18,6 +18,11 @@ Thumbs.db
 /dist/
 /out/
 
+# Idris2 ABI proof build artifacts
+**/build/
+*.ttc
+*.ttm
+
 # Dependencies
 /node_modules/
 /vendor/