ABI Layer 2: prove ISU short-program well-formedness — flagship Idris2 proof (#41)

## Summary

Raises anvomidaviser's Idris2 ABI to **Layer 2** with its first flagship
semantic proof. anvomidaviser's headline is converting ISU notation to
formal figure-skating programs; the canonical structural rule is the
short-program element-count limit. This proves `WellFormed` — at most 7
elements — as a decidable proposition, so a conforming program is
provably valid and an over-length one is provably rejected.

Mirrors the estate flagship-proof pattern: program model, decidable
`WellFormed` (propositional `LTE`), sound+complete `Dec`, certifier
proven sound, positive + negative controls.

## Changes

- Adds `src/interface/abi/Anvomidaviser/ABI/Semantics.idr` —
`SkateElement`/`Program`, `WellFormed`/`decWellFormed`,
`certifyProgramSound`, positive control + negative control
(`overRejected`).
- Registers the module in `anvomidaviser-abi.ipkg`.

## RSR Quality Checklist

### Required
- [x] Tests pass — ABI builds clean (see Testing)
- [x] Linter clean — zero warnings
- [x] No banned language patterns
- [x] No banned functions — genuine proof
- [x] SPDX headers present
- [x] No secrets

### As Applicable
- [x] ABI/FFI changes validated — additive proof; FFI untouched

## Testing

Verified with **Idris2 0.7.0**: `idris2 --build anvomidaviser-abi.ipkg`
→ exit 0, zero warnings. **Adversarial check**: a deliberately-false
proof (accepting an 8-element program) was rejected. `build/` removed.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx

---
_Generated by [Claude
Code](https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx)_

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

src/interface/abi/Anvomidaviser/ABI/Semantics.idr

@@ -0,0 +1,102 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+||| Flagship semantic proof for Anvomidaviser (Idris2 ABI Layer 2).
+|||
+||| Anvomidaviser's headline is "convert ISU notation to formal figure skating
+||| programs". A formal program must satisfy ISU well-formedness rules; the
+||| canonical structural one is the element-count limit of a short program (at
+||| most seven elements). This module models a program as a sequence of skating
+||| elements and proves:
+|||
+|||   1. `WellFormed` — the ISU element-count rule — as a decidable proposition
+|||      (LTE the limit), with a sound+complete `Dec`;
+|||   2. a certifier proven sound; and
+|||   3. positive + negative controls (an over-length program is provably
+|||      rejected — the rule is non-vacuous).
+
+module Anvomidaviser.ABI.Semantics
+
+import Anvomidaviser.ABI.Types
+import Data.Nat
+
+%default total
+
+--------------------------------------------------------------------------------
+-- A minimal but faithful program model
+--------------------------------------------------------------------------------
+
+public export
+data SkateElement = Jump | Spin | StepSequence
+
+||| A program is an ordered sequence of elements (as parsed from ISU notation).
+public export
+Program : Type
+Program = List SkateElement
+
+||| The ISU short-program element limit.
+public export
+maxElements : Nat
+maxElements = 7
+
+--------------------------------------------------------------------------------
+-- ISU well-formedness as a decidable proposition
+--------------------------------------------------------------------------------
+
+-- NB: the limit is written as the literal `7` (= `maxElements`) in this
+-- constructor's type, because a lowercase name in a constructor signature is
+-- auto-bound as a fresh implicit (which would shadow the global constant).
+public export
+data WellFormed : Program -> Type where
+  WF : {0 p : Program} -> LTE (length p) 7 -> WellFormed p
+
+public export
+decWellFormed : (p : Program) -> Dec (WellFormed p)
+decWellFormed p = case isLTE (length p) maxElements of
+  Yes prf => Yes (WF prf)
+  No  no  => No (\(WF q) => no q)
+
+--------------------------------------------------------------------------------
+-- Certifier into the ABI Result, proven sound
+--------------------------------------------------------------------------------
+
+public export
+certifyProgram : Program -> Result
+certifyProgram p = case decWellFormed p of
+  Yes _ => Ok
+  No  _ => Error
+
+export
+certifyProgramSound : (p : Program) -> certifyProgram p = Ok -> WellFormed p
+certifyProgramSound p prf with (decWellFormed p)
+  certifyProgramSound p prf  | Yes wf = wf
+  certifyProgramSound p Refl | No _ impossible
+
+--------------------------------------------------------------------------------
+-- Positive control
+--------------------------------------------------------------------------------
+
+public export
+goodProgram : Program
+goodProgram = [Jump, Spin, StepSequence]
+
+export
+goodAccepts : certifyProgram Semantics.goodProgram = Ok
+goodAccepts = Refl
+
+export
+goodWellFormed : WellFormed Semantics.goodProgram
+goodWellFormed = certifyProgramSound Semantics.goodProgram goodAccepts
+
+--------------------------------------------------------------------------------
+-- Negative control: an over-length program is rejected (non-vacuity)
+--------------------------------------------------------------------------------
+
+||| Eight elements — one over the ISU short-program limit.
+public export
+overProgram : Program
+overProgram = [Jump, Jump, Jump, Jump, Spin, Spin, Spin, StepSequence]
+
+export
+overRejected : certifyProgram Semantics.overProgram = Error
+overRejected = Refl

src/interface/abi/anvomidaviser-abi.ipkg

@@ -1,4 +1,4 @@
 -- SPDX-License-Identifier: MPL-2.0
 package anvomidaviser-abi
 sourcedir = "."
-modules = Anvomidaviser.ABI.Types, Anvomidaviser.ABI.Layout, Anvomidaviser.ABI.Foreign, Anvomidaviser.ABI.Proofs
+modules = Anvomidaviser.ABI.Types, Anvomidaviser.ABI.Layout, Anvomidaviser.ABI.Foreign, Anvomidaviser.ABI.Proofs, Anvomidaviser.ABI.Semantics