FixtureAudit.lean

import FPRDTransfer.PEG.TableEval
import FPRDTransfer.Theorem16.Grammar

/-!
# Executable anti-vacuity fixtures for LMR Theorem 16

These fixtures are deliberately hand-built at degree one and depth two. They
exercise the generated grammar through the rank-ordered table evaluator without
using either compiler or an automaton decision procedure inside `evalTable`.
-/

namespace FPRD.Theorem16.FixtureAudit

abbrev FixtureAutomaton := Automaton Bool Bool Unit 1 2

/-- A nontrivial control-only language: words with odd Boolean parity. -/
def controlMachine : FixtureAutomaton where
  delta control symbol _ := (Bool.xor control symbol, (), fun _ => .missing)
  init := false
  accept control := control

theorem controlDistance : controlMachine.DistanceOk := by
  intro control symbol neighbourhood port path hpath
  simp [controlMachine] at hpath

/-- The same parity language, with every appended edge using `SELF`. -/
def selfMachine : FixtureAutomaton where
  delta control symbol _ := (Bool.xor control symbol, (), fun _ => .self)
  init := false
  accept control := control

theorem selfDistance : selfMachine.DistanceOk := by
  intro control symbol neighbourhood port path hpath
  simp [selfMachine] at hpath

/-- Detect whether the sole child is a present node rather than `missing`. -/
def childPresent (neighbourhood : Unfold 1 Unit 2) : Bool :=
  match neighbourhood.child 0 with
  | .missing => false
  | .node _ _ => true

/-- The next control observes whether the preceding node points to the
present-but-unlabelled base. The current symbol chooses whether the new edge
will expose that distinction to the following transition. -/
def neighbourhoodMachine : FixtureAutomaton where
  delta _ symbol neighbourhood :=
    (childPresent neighbourhood, (), fun _ =>
      if symbol = true then .path [] else .missing)
  init := false
  accept control := control

theorem neighbourhoodDistance : neighbourhoodMachine.DistanceOk := by
  intro control symbol neighbourhood port path hpath
  simp [neighbourhoodMachine] at hpath
  split at hpath <;> simp_all

abbrev FixtureNT := Fin (FiniteEnum.card (NT Bool Unit 1 2))

def grammarResult (machine : FixtureAutomaton)
    (hdistance : machine.DistanceOk) (word : List Bool) : Result Bool :=
  evalTable (canonicalGrammar machine hdistance)
    (canonicalGrammar_rankSchedule machine hdistance) word.reverse

/-- All Boolean words of one exact length. -/
def boolWordsExact : Nat → List (List Bool)
  | 0 => [[]]
  | length + 1 =>
      (boolWordsExact length).flatMap fun word =>
        [false :: word, true :: word]

/-- All Boolean words through the inclusive length bound. -/
def boolWordsUpTo (bound : Nat) : List (List Bool) :=
  (List.range (bound + 1)).flatMap boolWordsExact

structure FixtureCounts where
  accepted : Nat := 0
  rejected : Nat := 0
  partialSuccesses : Nat := 0
  mismatches : Nat := 0
  deriving Repr, DecidableEq

def tally (expected : Bool) (result : Result Bool)
    (counts : FixtureCounts) : FixtureCounts :=
  match result with
  | .ok [] =>
      if expected = true then
        { counts with accepted := counts.accepted + 1 }
      else
        { counts with mismatches := counts.mismatches + 1 }
  | .ok (_ :: _) =>
      { counts with partialSuccesses := counts.partialSuccesses + 1 }
  | .err =>
      if expected = false then
        { counts with rejected := counts.rejected + 1 }
      else
        { counts with mismatches := counts.mismatches + 1 }

def auditFixture (machine : FixtureAutomaton)
    (hdistance : machine.DistanceOk) (bound : Nat) : FixtureCounts :=
  (boolWordsUpTo bound).foldl
    (fun counts word => tally (machine.decides word)
      (grammarResult machine hdistance word) counts)
    {}

def controlGrammar : Grammar FixtureNT Bool :=
  canonicalGrammar controlMachine controlDistance

def controlSchedule : RankSchedule controlGrammar :=
  canonicalGrammar_rankSchedule controlMachine controlDistance

def directMissingName : FixtureNT :=
  canonicalEquiv
    (.neighbourhood (.missing : Unfold 1 Unit 2))

/-- Direct table-evaluator outcome for the impossible top-level missing
neighbourhood. This is `some err` only because `Path([])` is epsilon. -/
def directMissingResult : Option (Result Bool) :=
  TableEval.lookup (TableEval.fillSuffixes controlGrammar controlSchedule [])
    [] directMissingName

theorem directMissingResult_eq : directMissingResult = some .err := by decide

structure CorpusReport where
  bound : Nat
  wordsPerFixture : Nat
  languageCases : Nat
  alphabetCarrier : Nat
  controlCarrier : Nat
  labelCarrier : Nat
  unfoldDepth0 : Nat
  unfoldDepth1 : Nat
  unfoldDepth2 : Nat
  boundedPaths : Nat
  nonterminals : Nat
  maxSuffixes : Nat
  maxTableCells : Nat
  directMissingPassed : Bool
  control : FixtureCounts
  selfEdge : FixtureCounts
  neighbourhood : FixtureCounts
  deriving Repr, DecidableEq

def auditCorpus (bound : Nat) : CorpusReport :=
  let words := boolWordsUpTo bound
  let nonterminals := FiniteEnum.card (NT Bool Unit 1 2)
  {
    bound
    wordsPerFixture := words.length
    languageCases := 3 * words.length
    alphabetCarrier := FiniteEnum.card Bool
    controlCarrier := FiniteEnum.card Bool
    labelCarrier := FiniteEnum.card Unit
    unfoldDepth0 := FiniteEnum.card (Unfold 1 Unit 0)
    unfoldDepth1 := FiniteEnum.card (Unfold 1 Unit 1)
    unfoldDepth2 := FiniteEnum.card (Unfold 1 Unit 2)
    boundedPaths := FiniteEnum.card (BoundedPath 1 2)
    nonterminals
    maxSuffixes := bound + 1
    maxTableCells := (bound + 1) * nonterminals
    directMissingPassed := directMissingResult == some .err
    control := auditFixture controlMachine controlDistance bound
    selfEdge := auditFixture selfMachine selfDistance bound
    neighbourhood := auditFixture neighbourhoodMachine neighbourhoodDistance bound
  }

def emitFixtureRow (name : String) (counts : FixtureCounts) : IO Unit :=
  IO.println s!"LMR16_FIXTURE_V1 name={name} accepted={counts.accepted} rejected={counts.rejected} partial={counts.partialSuccesses} mismatches={counts.mismatches}"

/-- Emit carrier and maximum-table dimensions without evaluating a language
fixture. This lets the audit harness evaluate the three independent fixtures
concurrently and combine their named rows deterministically. -/
def emitCorpusHeader (bound : Nat) : IO Unit := do
  let wordsPerFixture := (boolWordsUpTo bound).length
  let nonterminals := FiniteEnum.card (NT Bool Unit 1 2)
  IO.println s!"LMR16_CORPUS_V1 bound={bound} words_per_fixture={wordsPerFixture} language_cases={3 * wordsPerFixture} alphabet={FiniteEnum.card Bool} controls={FiniteEnum.card Bool} labels={FiniteEnum.card Unit} unfold0={FiniteEnum.card (Unfold 1 Unit 0)} unfold1={FiniteEnum.card (Unfold 1 Unit 1)} unfold2={FiniteEnum.card (Unfold 1 Unit 2)} paths={FiniteEnum.card (BoundedPath 1 2)} nonterminals={nonterminals} max_suffixes={bound + 1} max_table_cells={(bound + 1) * nonterminals} direct_missing={directMissingResult == some .err}"

def emitControlReport (bound : Nat) : IO Unit :=
  emitFixtureRow "control" (auditFixture controlMachine controlDistance bound)

def emitSelfReport (bound : Nat) : IO Unit :=
  emitFixtureRow "self" (auditFixture selfMachine selfDistance bound)

def emitNeighbourhoodReport (bound : Nat) : IO Unit :=
  emitFixtureRow "neighbourhood"
    (auditFixture neighbourhoodMachine neighbourhoodDistance bound)

/-- Emit a deterministic, versioned, line-oriented report for the Python
benchmark and mutation harness. -/
def emitCorpusReport (bound : Nat) : IO Unit := do
  emitCorpusHeader bound
  emitControlReport bound
  emitSelfReport bound
  emitNeighbourhoodReport bound

end FPRD.Theorem16.FixtureAudit