-- SPDX-FileCopyrightText: This work was generated by Claude Opus 4.8 in 2026.
--
-- SPDX-License-Identifier: LicenseRef-No-Human-Authorship

module Language.Burro.TCProof.Bisimulator (BisimResult(..), runBisim) where

import qualified Language.Burro.Definition as B

import Language.Turmac.Model (TMRule, Configuration(..), initConfiguration, isHalted)
import Language.Turmac.Simulator (step)
import Language.Turmac.Renderer (renderConfig)
import Language.Burro.TCProof.Configuration (decodeConfiguration)

--
-- Bounded, step-by-step bisimulation checking
-- ===========================================
--
-- Unlike run-and-compare-turmac (which runs both the Turmac simulator and
-- the compiled Burro program to completion and compares only the final
-- configuration -- useless on a non-halting machine, since both sides
-- would simply hang), this compares the TM's configuration against the
-- decoded Burro configuration after *every* step, up to a bound, stopping
-- early if either side halts. This is the executable companion to the
-- Step Simulation Lemma / Bisimulation Theorem in
-- doc/Turing-completeness-of-Burro.md: it can be run on deliberately
-- non-halting machines to give direct evidence for the theorem's
-- non-halting-preservation corollary.
--

data BisimResult
    = BisimMatch Integer Bool
        -- ^ number of steps successfully compared in lockstep; whether
        -- both sides had halted by then (True) or the bound was reached
        -- with neither halting (False)
    | BisimMismatch Integer Configuration Configuration
        -- ^ first step at which the two sides' decoded configurations
        -- disagree, and each side's configuration at that step
    deriving (Eq, Show)

runBisim :: [TMRule] -> B.Burro -> Integer -> BisimResult
runBisim tmRules burroProg n =
    let
        burroCfg0 = decodeConfiguration tmRules False B.newstate
    in
        if renderConfig 0 initConfiguration /= renderConfig 0 burroCfg0
        then BisimMismatch 0 initConfiguration burroCfg0
        else go 0 initConfiguration B.newstate
  where
    go k tmCfg burroState
        | isHalted tmCfg = BisimMatch k True
        | k >= n = BisimMatch k False
        | otherwise =
            let
                tmCfg' = step tmRules tmCfg
                freshState = burroState{ B.stackTape=(B.tape [0]), B.haltFlag=True }
                burroState' = B.exec burroProg freshState
                burroHalted' = B.haltFlag burroState'
                burroCfg' = decodeConfiguration tmRules burroHalted' burroState'
            in
                if renderConfig (k + 1) tmCfg' /= renderConfig (k + 1) burroCfg'
                then BisimMismatch (k + 1) tmCfg' burroCfg'
                else go (k + 1) tmCfg' burroState'