keiki-0.2.0.0: src/Keiki/Core.hs
-- 'combine''s 'Disjoint' constraint is the static check itself; GHC
-- sees it as unused (the body is @UCombine@) and would otherwise warn.
-- Same reasoning for any future helpers that re-export the constraint
-- as a typed witness.
{-# LANGUAGE TypeAbstractions #-}
-- Validation diagnostics intentionally expose constructor-specific record
-- selectors. Changing them to total fields would break the public diagnostic
-- API, so keep the partiality explicit and silence the definition-site warning.
{-# OPTIONS_GHC -Wno-partial-fields -Wno-redundant-constraints #-}
-- | The pure core of keiki: the symbolic-register transducer.
--
-- This module is the v1 prototype of the design pinned by
-- @docs/research/dsl-shape-for-symbolic-register.md@ (the DSL note),
-- @docs/research/effects-boundary.md@ (the boundary note), and
-- @docs/research/synthesis-c-foundation-b-presentation-with-worked-examples.md@
-- (the working baseline). See those notes for the rationale behind every
-- shape declared here.
--
-- All v1 escape hatches were retired by MasterPlan 6 (see the
-- Outcomes section of
-- @docs/masterplans/6-retire-remaining-v1-escape-hatches-in-pure-core-ofn-pmatchc-unsafecombine-static-check.md@):
-- @TInpField@ / @OPack@'s hand-written inverse (MP-2 EP-1), 'OFn' /
-- 'mkOut' (MP-6 EP-16), 'PMatchC' / 'matchCmd' (MP-6 EP-17), and
-- 'unsafeCombine' (MP-6 EP-18, replaced by the static 'Disjoint'
-- check on 'combine').
--
-- == Guard-authoring operators (EP-45)
--
-- Predicates and term arithmetic can be written with infix operators
-- that mirror their Prelude counterparts:
--
-- * Relational (build 'HsPred', @infix 4@): '.<' '.<=' '.>' '.>='
-- '.==' './=' — each an alias for 'PCmp'/'PEq' at a fixed relation.
-- * Logical (combine 'HsPred'): '.&&' (@infixr 3@, 'PAnd'),
-- '.||' (@infixr 2@, 'POr'), 'pnot' ('PNot').
-- * Arithmetic (build 'Term', mirror @+@\/@-@\/@*@): '.+' '.-' '.*' —
-- aliases for 'tadd'\/'tsub'\/'tmul'.
--
-- The verbose carrier signatures have synonyms: 'Pred' @rs ci@ for
-- @'HsPred' rs ci@, 'Guarded' @rs s ci co@ for
-- @'SymTransducer' ('HsPred' rs ci) rs s ci co@ (and
-- 'Keiki.Symbolic.SymGuarded' for the SBV-backed carrier).
--
-- Keep spaces around the operators (@lit a .* lit b@); a dot touching an
-- identifier (@x.y@) is OverloadedRecordDot field access. If you import
-- "Data.SBV" alongside this module, import it qualified — SBV exports
-- the same operator names.
module Keiki.Core
( -- * Slots and the register file
Slot,
RegFile (..),
Index (..),
(!),
-- * Index resolution from labels
HasIndex (..),
-- * Term language
Term (..),
NumOp (..),
-- * Input-side structural constructor (v2)
InCtor (..),
AssembleRegFile,
KnownSlotNames (..),
slotNamesOf,
-- * Slot-name machinery (re-exported from "Keiki.Internal.Slots")
IndexN (..),
HasIndexN (..),
Disjoint,
DistinctNames,
Concat,
Names,
-- * Update language
Update (..),
combine,
-- * Output term language
WireCtor (..),
OutFields (..),
(*:),
oNil,
OutTerm (..),
-- * Predicate carrier (v1 first-class AST)
HsPred (..),
Pred,
Cmp (..),
-- * Effective Boolean algebra
BoolAlg (..),
Sat (..),
-- * Edges and the transducer
Edge (..),
SymTransducer (..),
Guarded,
applyEdgeUpdate,
edgeReadsInput,
-- * Helpers (the user-facing DSL surface)
matchInCtor,
proj,
inpCtor,
lit,
tadd,
tsub,
tmul,
(.==),
(.<),
(.<=),
(.>),
(.>=),
(./=),
(.&&),
(.||),
pnot,
(.+),
(.-),
(.*),
pack,
-- * Evaluators
evalTerm,
evalOut,
evalPred,
runUpdate,
delta,
omega,
-- * Pure-layer entry points (effects-boundary note)
step,
stepEither,
StepFailure (..),
EdgeRef (..),
RejectedEdgeSummary (..),
MatchedEdgeSummary (..),
ReplayStepFailure (..),
ReplayFailureReason (..),
ReplayFailure (..),
reconstitute,
reconstituteEither,
applyEvent,
applyEventStreaming,
applyEventStreamingEither,
applyEvents,
applyEventsEither,
replayEvents,
-- * Streaming-replay state wrapper (EP-19 M3)
InFlight (..),
-- * Build-time analyses
solveOutput,
HiddenInputWarning (..),
checkHiddenInputs,
-- * Build-time validation umbrella (EP-56)
TransducerValidationWarning (..),
ValidationOptions (..),
defaultValidationOptions,
validateTransducer,
hiddenInputWarnings,
headRecoverabilityWarnings,
inversionAmbiguityWarnings,
guardImpliesInputReadWarnings,
stateChangingEpsilonWarnings,
opaqueGuardWarnings,
DeterminismWarning (..),
checkTransitionDeterminism,
checkTransitionDeterminismPure,
DeadEdgeOptions (..),
defaultDeadEdgeOptions,
DeadEdgeWarning (..),
checkDeadEdges,
-- * Internals exposed for testing
termReadsInput,
updateReadsInput,
outFieldsHaveInpCtorField,
HiddenInputReason (..),
hiddenInputReasons,
detectMissingInCtorFields,
MissingInCtorFields (..),
)
where
import Data.Int (Int32, Int64)
import Data.Kind (Type)
import Data.List (nub, partition, (\\))
import Data.Proxy (Proxy (..))
import Data.Set qualified as Set
import Data.Typeable (Typeable)
import Data.Word (Word16, Word32, Word64, Word8)
import GHC.OverloadedLabels (IsLabel (..))
import GHC.TypeLits (KnownSymbol, Symbol, symbolVal)
import Keiki.Internal.Slots
( Concat,
Disjoint,
DistinctNames,
HasIndexN (..),
IndexN (..),
Names,
)
import Type.Reflection (eqTypeRep, typeRep, type (:~~:) (HRefl))
-- | A register slot is a label paired with the type of its value.
type Slot = (Symbol, Type)
-- * Register file -----------------------------------------------------------
-- | A typed heterogeneous register tuple indexed by a list of 'Slot's.
--
-- The slot-value field is intentionally lazy: 'Keiki.Generics.emptyRegFile'
-- seeds each slot with a deferred @error "uninit: \<slot\>"@ thunk so
-- that reading an unwritten slot fails loudly with a targeted message
-- instead of returning a silent bottom. Strictness for *written*
-- slots is enforced on the write path ('setSlotN') instead — see
-- EP-23's Surprises entry for the long-running-service rationale.
data RegFile (rs :: [Slot]) where
RNil :: RegFile '[]
RCons ::
(KnownSymbol s) =>
Proxy s -> r -> RegFile rs -> RegFile ('(s, r) ': rs)
-- | A type-safe pointer into a 'RegFile'. 'ZIdx' picks the head;
-- 'SIdx' skips one slot.
data Index (rs :: [Slot]) (r :: Type) where
ZIdx :: (KnownSymbol s) => Index ('(s, r) ': rs) r
SIdx :: Index rs r -> Index ('(s', r') ': rs) r
-- | Runtime register lookup. Matching on 'Index' first lets GHC's GADT
-- pattern checker see that 'RNil' is unreachable — 'ZIdx' and 'SIdx'
-- both refine @rs@ to @'(_,_) ': _@.
(!) :: RegFile rs -> Index rs r -> r
regs ! ZIdx = case regs of RCons _ x _ -> x
regs ! SIdx i = case regs of RCons _ _ rest -> rest ! i
infixl 9 !
-- * IsLabel / HasIndex -----------------------------------------------------
-- | Resolve a label @s@ against a slot list @rs@ to an 'Index' for the
-- value at that slot. The functional dependency @s rs -> r@ ensures that
-- a label uniquely determines the slot's type.
class
HasIndex (s :: Symbol) (rs :: [Slot]) (r :: Type)
| s rs -> r
where
indexOf :: Index rs r
instance
{-# OVERLAPPING #-}
(KnownSymbol s) =>
HasIndex s ('(s, r) ': rs) r
where
indexOf = ZIdx
instance
{-# OVERLAPPABLE #-}
forall s s' r r' rs.
(HasIndex s rs r) =>
HasIndex s ('(s', r') ': rs) r
where
indexOf = SIdx (indexOf @s @rs @r)
instance
forall s rs r.
(HasIndex s rs r) =>
IsLabel s (Index rs r)
where
fromLabel = indexOf @s @rs @r
-- | Resolve a label directly to a 'Term' that reads the named register.
-- This instance lets call sites write @#name@ in any 'Term'-typed
-- context (the arguments of 'requireEq', the elements of 'OutFields',
-- etc.) without the @proj (#name :: Index Regs T)@ annotation that
-- 'IsLabel s (Index rs r)' alone would require.
--
-- The two 'IsLabel' instances ('Index' and 'Term') coexist because GHC
-- dispatches by the expected result type: a context expecting an
-- 'Index' (e.g. 'inpFoo'\'s argument) selects the 'Index' instance; a
-- context expecting a 'Term' (e.g. 'requireEq'\'s arguments) selects
-- this one.
instance
forall s rs ci ifs r.
(HasIndex s rs r) =>
IsLabel s (Term rs ci ifs r)
where
fromLabel = TReg (indexOf @s @rs @r)
-- The @IsLabel s (IndexN s rs r)@ instance lives next to 'IndexN' in
-- "Keiki.Internal.Slots" so the orphan check is satisfied.
-- * Term language ----------------------------------------------------------
-- | A numeric operation carried by 'TArith'. @OpAdd@\/@OpSub@\/@OpMul@
-- are @+@\/@-@\/@*@ respectively. Kept as a single tag (rather than
-- three 'Term' constructors) so each total 'Term' walker switches on
-- one value; the three directions are recovered by the smart
-- constructors 'tadd'\/'tsub'\/'tmul'.
data NumOp = OpAdd | OpSub | OpMul
deriving stock (Eq, Show)
-- | A pure expression over the register file and the input symbol,
-- yielding a value of type @r@.
--
-- The @ifs :: [Slot]@ parameter is the /input field schema/ this term
-- may project from: it is pinned by 'TInpCtorField' (whose 'Index' is
-- into @ifs@) and left free by terms that do not read an input field
-- ('TLit', 'TReg'). Threading @ifs@ through the AST is what lets an
-- 'OutFields' (and hence an 'OPack') guarantee /by construction/ that
-- every top-level input projection reads the same constructor schema as
-- the 'OPack''s 'InCtor' — so 'solveOutput' recovers a command field
-- with no @unsafeCoerce@. Terms that do not appear in an invertible
-- output position ('Update' right-hand sides, 'HsPred' operands)
-- existentially hide @ifs@, so it never leaks into the 'Edge' /
-- 'SymTransducer' surface. See @docs/research/tinpproj-design.md@.
data Term (rs :: [Slot]) (ci :: Type) (ifs :: [Slot]) (r :: Type) where
TLit :: r -> Term rs ci ifs r
TReg :: Index rs r -> Term rs ci ifs r
-- | Structural input projection: read field @ix@ of the input
-- constructor described by @ic@. The 'InCtor' value names the
-- expected constructor and supplies the round-trip
-- ('icMatch'/'icBuild') so that 'solveOutput' can mechanically
-- recover @ci@ from an observed output. Pins the term's @ifs@ to the
-- constructor's field schema. See @docs/research/tinpproj-design.md@.
TInpCtorField :: InCtor ci ifs -> Index ifs r -> Term rs ci ifs r
TApp1 ::
(a -> r) ->
Term rs ci ifs a ->
Term rs ci ifs r
TApp2 ::
(a -> b -> r) ->
Term rs ci ifs a ->
Term rs ci ifs b ->
Term rs ci ifs r
-- | Structural arithmetic over a numeric operand type. Unlike the
-- opaque 'TApp1'\/'TApp2' escape hatches, the SBV translator reads
-- 'TArith' for real (on a 'Keiki.Symbolic.discoverSymNum' hit), so a
-- guard over a /computed/ value — a weighted sum, a derived cap — is
-- visible to the solver. The 'Num' constraint prevents constructing
-- arithmetic at non-numeric operand types; 'Typeable' lets the SBV
-- translator dispatch on @r@. Build with 'tadd'\/'tsub'\/'tmul'.
TArith ::
(Num r, Typeable r) =>
NumOp ->
Term rs ci ifs r ->
Term rs ci ifs r ->
Term rs ci ifs r
-- | Per-constructor input projection. An 'InCtor' value names one
-- constructor of the input symbol type @ci@ and pins the round-trip
-- between that constructor's payload and a typed register file
-- @'RegFile' ifs@. The slot list @ifs@ is the field schema for the
-- constructor; together with 'Index' it lets call sites read fields
-- via 'OverloadedLabels' (for example @inpStart #email@).
--
-- 'icMatch' must return 'Just' iff @ci@ is the named constructor.
-- 'icBuild' is its left inverse: @icMatch (icBuild rf) == Just rf@ for
-- every well-formed @rf@.
--
-- The constraints 'AssembleRegFile' and 'KnownSlotNames' on the data
-- constructor mean that any code holding an 'InCtor' can both
-- mechanically rebuild a 'RegFile' from a bag of '(Index, value)' pairs
-- and recover the slot names of @ifs@ at run time. The instances are
-- automatic for any concrete slot list, so users do not write any
-- additional code.
--
-- See @docs/research/tinpproj-design.md@ for the design rationale and
-- the inversion algorithm that walks 'OutFields' gathering these
-- per-field reads.
data InCtor ci (ifs :: [Slot]) where
InCtor ::
(AssembleRegFile ifs, KnownSlotNames ifs) =>
{ icName :: String,
icMatch :: ci -> Maybe (RegFile ifs),
icBuild :: RegFile ifs -> ci
} ->
InCtor ci ifs
-- * Slot-list helper classes (v2 inversion machinery) ---------------------
-- | Recover the slot names of an @ifs :: [Slot]@ at run time. Used to
-- print precise hidden-input warnings.
class KnownSlotNames (rs :: [Slot]) where
slotNames :: [String]
instance KnownSlotNames '[] where
slotNames = []
instance
(KnownSymbol s, KnownSlotNames rs) =>
KnownSlotNames ('(s, r) ': rs)
where
slotNames = symbolVal (Proxy @s) : slotNames @rs
-- | An (Index, value) pair indexed by an InCtor's slot list. Using a
-- GADT existential lets us bag entries with different element types
-- under one slot list and unpack them safely via pattern matching on
-- the carried 'Index'.
data ByIndex (ifs :: [Slot]) where
ByIndex :: Index ifs r -> r -> ByIndex ifs
-- | Class to assemble a 'RegFile' from a bag of '(Index, value)' pairs.
-- 'assemble' returns 'Just' iff every slot of @ifs@ is covered by
-- exactly one entry of the bag (extra entries beyond what slots
-- demand are ignored as long as the per-slot lookups succeed in
-- order).
class AssembleRegFile (ifs :: [Slot]) where
assemble :: [ByIndex ifs] -> Maybe (RegFile ifs)
instance AssembleRegFile '[] where
assemble _ = Just RNil
instance
(KnownSymbol s, AssembleRegFile rs) =>
AssembleRegFile ('(s, r) ': rs)
where
assemble entries = do
v <- findHead entries
rest <- assemble (popHead entries)
pure (RCons (Proxy @s) v rest)
where
findHead :: [ByIndex ('(s, r) ': rs)] -> Maybe r
findHead [] = Nothing
findHead (ByIndex ZIdx v : _) = Just v
findHead (_ : rest) = findHead rest
popHead :: [ByIndex ('(s, r) ': rs)] -> [ByIndex rs]
popHead [] = []
popHead (ByIndex ZIdx _ : rest) = popHead rest
popHead (ByIndex (SIdx i) v : rest) = ByIndex i v : popHead rest
-- * Update language --------------------------------------------------------
-- | The copyless update language. The @(w :: [Symbol])@ index
-- records the set of slot names this update writes; the smart
-- constructor 'combine' demands @'Disjoint' w1 w2@ to combine two
-- updates, so "each register is written at most once per edge
-- update" becomes a type-level invariant rather than a runtime check.
--
-- The 'UCombine' raw constructor is *not* constrained by 'Disjoint':
-- the invariant is enforced at the smart-constructor introduction
-- point ('combine'). This keeps internal pattern-matches in
-- "Keiki.Composition" (which reconstruct 'UCombine' values during
-- weakening / substitution) cheap. EP-18 M8 retired the v1
-- 'unsafeCombine' escape hatch; aggregate authors use 'combine'
-- exclusively.
data Update (rs :: [Slot]) (w :: [Symbol]) (ci :: Type) where
UKeep :: Update rs '[] ci
-- The right-hand-side 'Term''s input field schema @ifs@ is
-- existentially hidden: updates are never inverted, so @ifs@ need not
-- escape into the 'Update' kind (keeping 'Edge' / 'SymTransducer'
-- unchanged).
USet ::
(KnownSymbol s) =>
IndexN s rs r -> Term rs ci ifs r -> Update rs '[s] ci
UCombine ::
Update rs w1 ci ->
Update rs w2 ci ->
Update rs (Concat w1 w2) ci
-- | Smart constructor for 'UCombine'. The @'Disjoint' w1 w2@
-- constraint statically enforces that the two halves write to
-- disjoint slot-name sets; an aggregate that writes the same slot
-- twice (e.g. @'USet' #email t1 \`combine\` 'USet' #email t2@) is
-- rejected at compile time with a 'GHC.TypeError.TypeError' naming
-- the offending slot.
combine ::
(Disjoint w1 w2) =>
Update rs w1 ci ->
Update rs w2 ci ->
Update rs (Concat w1 w2) ci
combine = UCombine
-- * Output term language ---------------------------------------------------
-- | A wire-type tag for one constructor of the user's output sum @co@.
-- The functions let 'solveOutput' pattern-match an observed @co@ and
-- 'evalOut' rebuild a @co@ from its fields.
data WireCtor co fields = WireCtor
{ wcName :: String,
wcMatch :: co -> Maybe fields,
wcBuild :: fields -> co
}
-- | An HList of 'Term's, one per field of the wire constructor. The
-- field-tuple type @fs@ is built up nested-pair style so that
-- 'solveOutput' can walk the HList structurally.
--
-- The @ifs :: [Slot]@ parameter is the shared input field schema of
-- every 'Term' in the list (see 'Term'). 'OPack' ties it to the
-- 'OPack''s 'InCtor', so a top-level 'TInpCtorField' inside an
-- 'OutFields' is statically an 'Index' into the 'OPack''s constructor
-- schema — 'gatherInpEntries' recovers it with no coercion.
data OutFields rs ci ifs fs where
OFNil :: OutFields rs ci ifs ()
OFCons ::
Term rs ci ifs f ->
OutFields rs ci ifs fs ->
OutFields rs ci ifs (f, fs)
-- | Right-associative HList constructor synonym for 'OFCons'. Lets
-- 'OutFields' literals read top-to-bottom in the wire ctor's field
-- order:
--
-- > d.recipient *: d.subject *: d.at *: oNil
--
-- Identical AST: @t1 *: t2 *: oNil@ produces the same 'OutFields'
-- value as @OFCons t1 (OFCons t2 OFNil)@. Available at the AST
-- layer (here) so authors who skip the builder can use it; also
-- re-exported by "Keiki.Builder" for builder-form call sites.
(*:) :: Term rs ci ifs f -> OutFields rs ci ifs fs -> OutFields rs ci ifs (f, fs)
(*:) = OFCons
infixr 5 *:
-- | The empty 'OutFields' HList. Synonym for 'OFNil'.
oNil :: OutFields rs ci ifs ()
oNil = OFNil
-- | A pure expression yielding an output value @co@.
data OutTerm (rs :: [Slot]) (ci :: Type) (co :: Type) where
-- | Structural pack: tagged by an input constructor (which the edge
-- consumes) and an output wire constructor (which the edge produces),
-- with one 'Term' per field of the wire constructor. 'solveOutput'
-- walks the structural 'OutFields', gathering '(Index, value)' pairs
-- against the named 'InCtor', and reconstructs the input by calling
-- 'icBuild' on the assembled register file. Empty-payload input
-- constructors (the 'InCtor's slot list is @\'[]@) recover trivially
-- as @icBuild ic RNil@.
OPack ::
InCtor ci ifs ->
WireCtor co fields ->
OutFields rs ci ifs fields ->
OutTerm rs ci co
-- * Predicate carrier ------------------------------------------------------
-- | The predicate AST. Carries enough structure to evaluate guards and
-- to translate to SMT through the SBV-backed 'BoolAlg' instance in
-- "Keiki.Symbolic" (added in EP-2 of MasterPlan 2).
data HsPred (rs :: [Slot]) (ci :: Type) where
PTop :: HsPred rs ci
PBot :: HsPred rs ci
PAnd :: HsPred rs ci -> HsPred rs ci -> HsPred rs ci
POr :: HsPred rs ci -> HsPred rs ci -> HsPred rs ci
PNot :: HsPred rs ci -> HsPred rs ci
PEq ::
(Eq r, Typeable r) =>
Term rs ci ifs1 r -> Term rs ci ifs2 r -> HsPred rs ci
-- | Structural input-constructor guard: @True@ iff the input symbol
-- is the constructor named by the carried 'InCtor'. The SBV-backed
-- 'BoolAlg' instance recognises constructor mutual exclusion
-- symbolically through this constructor. See
-- @docs/research/sbv-boolalg-design.md@.
PInCtor :: InCtor ci ifs -> HsPred rs ci
-- | Structural guard for the outer @Left@ arm of an 'Either' input.
-- This discriminator is independent of 'PInCtor', so a guard can
-- constrain both the sum arm and the constructor inside that arm.
PLeftArm :: HsPred rs (Either ci1 ci2)
-- | Structural guard for the outer @Right@ arm of an 'Either' input.
PRightArm :: HsPred rs (Either ci1 ci2)
-- | Ordering guard: compares two 'Term's of the same orderable type
-- with the relation named by 'Cmp'. @PCmp CmpGe a b@ means @a >= b@,
-- and so on. Unlike a threshold written through 'TApp1'\/'TApp2'
-- (which is opaque to the solver), 'PCmp' is /structural/: the
-- SBV-backed translator in "Keiki.Symbolic" emits a real symbolic
-- comparison (@.<@, @.<=@, @.>@, @.>=@) whenever the operand type's
-- 'Keiki.Symbolic.SymRep' is symbolically orderable (see
-- 'Keiki.Symbolic.discoverSymOrd'); otherwise it falls back to a
-- fresh opaque 'SBool', exactly as 'PEq' does for non-'Sym' operands.
-- Equality is intentionally left to 'PEq' — 'Cmp' has no "equal"
-- case. Added by EP-41.
PCmp ::
(Ord r, Typeable r) =>
Cmp -> Term rs ci ifs1 r -> Term rs ci ifs2 r -> HsPred rs ci
-- | A four-way ordering relation carried by 'PCmp'. @Lt@\/@Le@\/@Gt@\/
-- @Ge@ are @<@\/@<=@\/@>@\/@>=@ respectively. Kept as a single tag
-- (rather than four 'HsPred' constructors) so the evaluator and the
-- SBV translator each switch on one value; the four directions are
-- recovered by the builder conveniences
-- 'Keiki.Builder.requireLt'\/'requireLe'\/'requireGt'\/'requireGe'.
data Cmp = CmpLt | CmpLe | CmpGt | CmpGe
deriving stock (Eq, Show)
-- * Effective Boolean algebra ----------------------------------------------
-- | An effective Boolean algebra over @a@-typed witnesses, used as the
-- guard carrier of edges. Witness /extraction/ ('sat') is a separate,
-- stronger capability — see 'Sat'.
class BoolAlg phi a | phi -> a where
top :: phi
bot :: phi
conj :: phi -> phi -> phi
disj :: phi -> phi -> phi
neg :: phi -> phi
models :: phi -> a -> Bool
isBot :: phi -> Bool
-- | A 'BoolAlg' whose witnesses can be /extracted/ from a satisfiable
-- predicate: @'sat' phi@ returns 'Just' a value satisfying @phi@, or
-- 'Nothing' when @phi@ is unsatisfiable.
--
-- Split out of 'BoolAlg' by EP-44 (MasterPlan 12). Witness
-- reconstruction needs carrier-specific evidence — for the SBV-backed
-- 'Keiki.Symbolic.SymPred' carrier, @ExtractRegFile rs@ (to rebuild the
-- register file from the solver model) and @KnownInCtors ci@ (to rebuild
-- the command) — that the algebra's build/decide methods do not. Keeping
-- 'sat' in its own class means the witness-free analyses
-- ('Keiki.Symbolic.isSingleValuedSym', which uses only 'isBot'/'conj')
-- carry no extraction constraints, so they keep type-checking on
-- register-file-existential carriers (e.g. 'Keiki.Profunctor.SomeSymTransducer')
-- and on composition-produced @ci@ types ('Either', tuples) that have no
-- 'KnownInCtors'. See @docs/research/sbv-boolalg-design.md@.
class (BoolAlg phi a) => Sat phi a where
sat :: phi -> Maybe a
instance BoolAlg (HsPred rs ci) (RegFile rs, ci) where
top = PTop
bot = PBot
conj p q = PAnd p q
disj p q = POr p q
neg p = PNot p
models p (regs, ci) = evalPred p regs ci
isBot PBot = True
isBot _ = False
-- | The v1 syntactic carrier has no solver, hence no extractable
-- witness; 'sat' is always 'Nothing'. The precise witnesses come from
-- the SBV-backed @Sat (SymPred …)@ instance in "Keiki.Symbolic".
instance Sat (HsPred rs ci) (RegFile rs, ci) where
sat _ = Nothing
-- * Edges and the transducer -----------------------------------------------
-- | A single transition. The 'output' is a list of 'OutTerm's:
-- @[]@ is the ε-edge (no observable emission), @[o]@ is the letter
-- edge (one event, identical to today's @'Just' o@), @[o1, o2, ...]@
-- is the multi-event edge — one transition emits N events in
-- declaration order. See @docs/research/gsm-widening-design.md@.
--
-- The @(w :: [Symbol])@ index on 'update' (the slot-name set the
-- update writes) is *existentially* quantified at the 'Edge' record
-- — different edges out of the same vertex write different slot
-- sets, but the homogeneous list @[Edge phi rs ci co s]@ in
-- 'edgesOut' demands a single @Edge@ type. The existential preserves
-- the static disjointness check at the *introduction* point of any
-- 'Update' value (via 'combine') without polluting the @Edge@'s
-- public type with a per-edge @w@ parameter.
data Edge phi rs ci co s where
Edge ::
{ guard :: phi,
update :: Update rs w ci,
output :: [OutTerm rs ci co],
target :: s
} ->
Edge phi rs ci co s
-- | The single source of truth: a finite control graph plus a register
-- file evolved by edges' 'update' terms.
data SymTransducer phi rs s ci co = SymTransducer
{ edgesOut :: s -> [Edge phi rs ci co s],
initial :: s,
initialRegs :: RegFile rs,
isFinal :: s -> Bool
}
-- | Readable alias for the v1 predicate carrier:
-- @'Pred' rs ci@ is exactly @'HsPred' rs ci@.
type Pred rs ci = HsPred rs ci
-- | A 'SymTransducer' whose guard carrier is the v1 'HsPred'. Collapses
-- the @'SymTransducer' ('HsPred' rs ci) rs s ci co@ signature — which
-- otherwise repeats @rs@ and @ci@ — into @'Guarded' rs s ci co@.
type Guarded rs s ci co = SymTransducer (HsPred rs ci) rs s ci co
-- | Apply an edge's update to the register file. The 'Edge''s
-- existentially-quantified @w@ index makes @'update' e@ unusable as
-- a function (GHC rejects with "escaped type variables"); this
-- helper hides the existential by pattern-matching internally.
applyEdgeUpdate ::
Edge phi rs ci co s -> RegFile rs -> ci -> RegFile rs
applyEdgeUpdate Edge {update = u} regs ci = runUpdate u regs ci
-- | Does an edge's update read the input symbol via 'TInpCtorField'?
-- Existential-hiding companion to 'updateReadsInput'.
edgeReadsInput :: Edge phi rs ci co s -> Bool
edgeReadsInput Edge {update = u} = updateReadsInput u
-- * Helpers (DSL surface) --------------------------------------------------
-- | Structural input-constructor guard: @True@ iff the input symbol
-- is the constructor named by the supplied 'InCtor'. The SBV-backed
-- 'BoolAlg' instance can decide constructor-mutual-exclusion
-- symbolically through this guard. The semantics is
-- @evalPred (matchInCtor ic) regs ci == isJust (icMatch ic ci)@.
matchInCtor :: InCtor ci ifs -> HsPred rs ci
matchInCtor = PInCtor
-- | Read a register slot into a 'Term'.
proj :: Index rs r -> Term rs ci ifs r
proj = TReg
-- | Structural input projection: read field @ix@ of the input
-- constructor described by @ic@. The result 'Term''s @ifs@ is the
-- constructor's field schema, so an 'OutFields' built from these is
-- statically tied to the 'OPack''s 'InCtor'.
inpCtor :: InCtor ci ifs -> Index ifs r -> Term rs ci ifs r
inpCtor = TInpCtorField
-- | A constant 'Term'.
lit :: r -> Term rs ci ifs r
lit = TLit
-- | Structural arithmetic smart constructors. @tadd@\/@tsub@\/@tmul@
-- build a 'TArith' over @+@\/@-@\/@*@. The operand type must be numeric
-- ('Num') and 'Typeable'; the SBV translator reads them structurally
-- (see 'Keiki.Symbolic.discoverSymNum'), unlike the opaque 'TApp'
-- escape hatches.
tadd,
tsub,
tmul ::
(Num r, Typeable r) =>
Term rs ci ifs r -> Term rs ci ifs r -> Term rs ci ifs r
tadd = TArith OpAdd
tsub = TArith OpSub
tmul = TArith OpMul
-- | Equality predicate sugar.
(.==) :: (Eq r, Typeable r) => Term rs ci ifs1 r -> Term rs ci ifs2 r -> HsPred rs ci
(.==) = PEq
infix 4 .==
-- * Predicate & term operators (readable guard DSL) ----------------------
-- | Ordering-guard operators. Each is an alias for 'PCmp' at a fixed
-- 'Cmp': @a .>= b@ is @'PCmp' 'CmpGe' a b@ (i.e. @a >= b@); @a .< b@ is
-- @'PCmp' 'CmpLt' a b@; and so on. Same fixity as '(.==)' (@infix 4@):
-- relational operators do not chain, sit below the arithmetic operators
-- ('.+'/'.-'/'.*'), and above the logical ones ('.&&'/'.||').
(.<),
(.<=),
(.>),
(.>=) ::
(Ord r, Typeable r) => Term rs ci ifs1 r -> Term rs ci ifs2 r -> HsPred rs ci
(.<) = PCmp CmpLt
(.<=) = PCmp CmpLe
(.>) = PCmp CmpGt
(.>=) = PCmp CmpGe
infix 4 .<, .<=, .>, .>=
-- | Inequality guard. @a ./= b@ is @'pnot' (a '.==' b)@, i.e.
-- @'PNot' ('PEq' a b)@. Mirrors 'Prelude.(/=)' against the existing
-- '(.==)'.
(./=) :: (Eq r, Typeable r) => Term rs ci ifs1 r -> Term rs ci ifs2 r -> HsPred rs ci
a ./= b = PNot (PEq a b)
infix 4 ./=
-- | Conjunction / disjunction of predicates. Aliases for 'PAnd' / 'POr',
-- mirroring 'Prelude.(&&)' / 'Prelude.(||)' in fixity (@infixr 3@ /
-- @infixr 2@), so @p .&& q .|| r@ parses as @(p .&& q) .|| r@.
(.&&), (.||) :: HsPred rs ci -> HsPred rs ci -> HsPred rs ci
(.&&) = PAnd
(.||) = POr
infixr 3 .&&
infixr 2 .||
-- | Predicate negation. Alias for 'PNot'. ('Keiki.Core.BoolAlg' also
-- exposes 'neg', which is this same operation lifted through the class;
-- 'pnot' is the direct AST alias for hand-written guards.)
pnot :: HsPred rs ci -> HsPred rs ci
pnot = PNot
-- | Structural arithmetic operators on 'Term's. Aliases for
-- 'tadd' / 'tsub' / 'tmul', mirroring 'Prelude.(+)' / '(-)' / '(*)' in
-- fixity (@infixl 6@ / @infixl 6@ / @infixl 7@). Because they build the
-- structural 'TArith' node (not an opaque 'TApp'), arithmetic written
-- with them is visible to the SBV translator in "Keiki.Symbolic".
(.+),
(.-),
(.*) ::
(Num r, Typeable r) => Term rs ci ifs r -> Term rs ci ifs r -> Term rs ci ifs r
(.+) = tadd
(.-) = tsub
(.*) = tmul
infixl 6 .+, .-
infixl 7 .*
-- | Structural-output construction. 'solveOutput' inverts the result
-- mechanically by walking 'OutFields' against the named input
-- constructor; users no longer supply an inverse function. The
-- 'InCtor' first argument names the @ci@ constructor the edge expects;
-- it makes recovery work even for edges whose input has no payload
-- (e.g. a singleton 'Continue' command).
pack ::
InCtor ci ifs ->
WireCtor co fields ->
OutFields rs ci ifs fields ->
OutTerm rs ci co
pack = OPack
-- * Evaluators -------------------------------------------------------------
-- | Evaluate a 'Term' against a register file and an input symbol.
evalTerm :: Term rs ci ifs r -> RegFile rs -> ci -> r
evalTerm (TLit r) _ _ = r
evalTerm (TReg ix) regs _ = regs ! ix
evalTerm (TInpCtorField ic ix) _ ci = case icMatch ic ci of
Just rf -> rf ! ix
Nothing -> error ("evalTerm: TInpCtorField guard violation: " ++ icName ic)
evalTerm (TApp1 f t) regs ci = f (evalTerm t regs ci)
evalTerm (TApp2 f a b) regs ci = f (evalTerm a regs ci) (evalTerm b regs ci)
evalTerm (TArith op a b) regs ci =
applyNumOp op (evalTerm a regs ci) (evalTerm b regs ci)
-- | Interpret a 'NumOp' tag as the corresponding numeric operation.
-- The 'Num' evidence is supplied by matching the 'TArith' constructor.
applyNumOp :: (Num r) => NumOp -> r -> r -> r
applyNumOp OpAdd = (+)
applyNumOp OpSub = (-)
applyNumOp OpMul = (*)
-- | Evaluate an 'OutTerm' against a register file and an input symbol.
-- The 'InCtor' on 'OPack' is consulted only by the inverse direction
-- ('solveOutput'); evaluation just runs the wire build over the
-- evaluated 'OutFields'.
evalOut :: OutTerm rs ci co -> RegFile rs -> ci -> co
evalOut (OPack _ic ctor fields) regs ci =
wcBuild ctor (evalOutFields fields regs ci)
evalOutFields :: OutFields rs ci ifs fs -> RegFile rs -> ci -> fs
evalOutFields OFNil _ _ = ()
evalOutFields (OFCons t rest) regs ci =
(evalTerm t regs ci, evalOutFields rest regs ci)
-- | Evaluate a predicate to a 'Bool' on the current state.
evalPred :: HsPred rs ci -> RegFile rs -> ci -> Bool
evalPred PTop _ _ = True
evalPred PBot _ _ = False
evalPred (PAnd p q) r c = evalPred p r c && evalPred q r c
evalPred (POr p q) r c = evalPred p r c || evalPred q r c
evalPred (PNot p) r c = not (evalPred p r c)
evalPred (PEq a b) r c = evalTerm a r c == evalTerm b r c
evalPred (PInCtor ic) _ c = case icMatch ic c of
Just _ -> True
Nothing -> False
evalPred PLeftArm _ input = case input of
Left _ -> True
Right _ -> False
evalPred PRightArm _ input = case input of
Left _ -> False
Right _ -> True
evalPred (PCmp op a b) r c = applyCmp op (evalTerm a r c) (evalTerm b r c)
where
applyCmp :: (Ord x) => Cmp -> x -> x -> Bool
applyCmp CmpLt x y = x < y
applyCmp CmpLe x y = x <= y
applyCmp CmpGt x y = x > y
applyCmp CmpGe x y = x >= y
-- | Apply an 'Update' to the register file. Every right-hand-side term
-- reads the register snapshot from before the whole update began. Writes
-- are then applied left-to-right; the public 'combine' constructor requires
-- disjoint slots, while internal raw 'UCombine' values that repeat a slot
-- therefore keep the rightmost write.
runUpdate :: forall rs w ci. Update rs w ci -> RegFile rs -> ci -> RegFile rs
runUpdate update regs ci = go update regs
where
go :: Update rs w' ci -> RegFile rs -> RegFile rs
go UKeep acc = acc
go (USet ix t) acc = setSlotN ix (evalTerm t regs ci) acc
go (UCombine a b) acc = go b (go a acc)
-- | Pure register-file slot update at a slot-name-tagged 'IndexN'.
--
-- The bang-pattern on @v@ forces the new slot value to WHNF before
-- threading it into the rebuilt 'RCons'. Without this, every
-- 'runUpdate' / 'step' cycle in a long-running embedder accumulates
-- a tower of thunks at the written slot, which is exactly the failure
-- mode the @NoThunks (RegFile rs)@ instance ("Keiki.NoThunks") was
-- introduced to detect (EP-23). Untouched slots retain whatever
-- WHNF status they already had, which preserves
-- 'Keiki.Generics.emptyRegFile'\'s targeted @uninit:@ sentinels for
-- slots that have never been written.
setSlotN :: IndexN s rs r -> r -> RegFile rs -> RegFile rs
setSlotN IZ !v regs = case regs of RCons p _ rest -> RCons p v rest
setSlotN (IS i) !v regs = case regs of
RCons p x rest ->
let !rest' = setSlotN i v rest
in RCons p x rest'
-- | Single-step transition. Returns 'Just (s', regs')' iff exactly one
-- outgoing edge has a satisfied guard.
delta ::
(BoolAlg phi (RegFile rs, ci)) =>
SymTransducer phi rs s ci co ->
s ->
RegFile rs ->
ci ->
Maybe (s, RegFile rs)
delta t s regs ci =
case [ (target e, applyEdgeUpdate e regs ci)
| e <- edgesOut t s,
models (guard e) (regs, ci)
] of
[single] -> Just single
_ -> Nothing
-- | Single-step output. Returns the list of events emitted by the
-- unique active edge: @[]@ for an ε-edge, @[o]@ for a letter edge,
-- @[o1, o2, ...]@ for a multi-event edge. Returns @[]@ if no edge
-- is active or if more than one edge is active. Therefore @[]@ conflates
-- three different outcomes: a rejected command, an ambiguous command,
-- and an accepted ε-edge that emits nothing. Never interpret @[]@ as
-- proof that a command was rejected; use 'stepEither' to distinguish all
-- three outcomes with structured failures.
omega ::
(BoolAlg phi (RegFile rs, ci)) =>
SymTransducer phi rs s ci co ->
s ->
RegFile rs ->
ci ->
[co]
omega t s regs ci =
case [ [evalOut o regs ci | o <- output e]
| e <- edgesOut t s,
models (guard e) (regs, ci)
] of
[evaluatedOuts] -> evaluatedOuts
_ -> []
-- * Pure-layer entry points ------------------------------------------------
-- | One full step of the transducer combining 'delta' and 'omega'.
-- Returns 'Nothing' if no edge from the current vertex has a satisfied
-- guard. The inner @[co]@ is @[]@ for an ε-edge, @[o]@ for a letter
-- edge, @[o1, o2, ...]@ for a multi-event edge.
step ::
(BoolAlg phi (RegFile rs, ci)) =>
SymTransducer phi rs s ci co ->
(s, RegFile rs) ->
ci ->
Maybe (s, RegFile rs, [co])
step t (s, regs) ci = case delta t s regs ci of
Nothing -> Nothing
Just (s', regs') -> Just (s', regs', omega t s regs ci)
-- | A locator for one outgoing edge: the vertex it leaves from and its
-- zero-based position in @'edgesOut' t source@. This is the canonical
-- edge-identity vocabulary shared with build-time diagnostics (EP-56).
data EdgeRef s = EdgeRef
{ edgeSource :: s,
edgeIndex :: Int
}
deriving stock (Eq, Show)
-- | Why one outgoing edge was rejected during a step: its locator, its
-- declared target, and whether its guard matched (always 'False' here;
-- the field keeps the shape uniform with 'MatchedEdgeSummary' and leaves
-- room for richer rejection reasons later). Deliberately carries NO
-- register values — diagnostics summarize, they do not dump state.
data RejectedEdgeSummary s = RejectedEdgeSummary
{ rejectedEdge :: EdgeRef s,
rejectedTarget :: s,
rejectedGuard :: Bool
}
deriving stock (Eq, Show)
-- | One outgoing edge whose guard matched during a step: its locator and
-- its declared target. Carries NO register values.
data MatchedEdgeSummary s = MatchedEdgeSummary
{ matchedEdge :: EdgeRef s,
matchedTarget :: s
}
deriving stock (Eq, Show)
-- | A precise explanation of why a step could not advance.
--
-- * 'NoOutgoingEdges' — the source vertex has no outgoing edges at all.
-- * 'NoMatchingEdge' — there are outgoing edges, but none matched the
-- command; carries one 'RejectedEdgeSummary' per edge, in declaration
-- order.
-- * 'AmbiguousEdges' — two or more guards matched the same command, a
-- runtime witness of a single-valuedness violation (the property
-- EP-56's 'checkTransitionDeterminism' proves statically); carries one
-- 'MatchedEdgeSummary' per matched edge.
data StepFailure s
= NoOutgoingEdges s
| NoMatchingEdge s [RejectedEdgeSummary s]
| AmbiguousEdges s [MatchedEdgeSummary s]
deriving stock (Eq, Show)
-- | Like 'step', but returns a precise 'StepFailure' explanation on the
-- 'Left' instead of collapsing every failure into 'Nothing'. On the
-- 'Right' it returns EXACTLY the triple 'step' returns. 'step' is left
-- unchanged; this is purely additive.
stepEither ::
(BoolAlg phi (RegFile rs, ci)) =>
SymTransducer phi rs s ci co ->
(s, RegFile rs) ->
ci ->
Either (StepFailure s) (s, RegFile rs, [co])
stepEither t (s, regs) ci =
case zip [0 ..] (edgesOut t s) of
[] -> Left (NoOutgoingEdges s)
indexed ->
let matched =
[ (i, e)
| (i, e) <- indexed,
models (guard e) (regs, ci)
]
in case matched of
[] ->
Left $
NoMatchingEdge
s
[ RejectedEdgeSummary
{ rejectedEdge = EdgeRef {edgeSource = s, edgeIndex = i},
rejectedTarget = target e,
rejectedGuard = False
}
| (i, e) <- indexed
]
[(_, e)] ->
let !regs' = applyEdgeUpdate e regs ci
outs = [evalOut o regs ci | o <- output e]
in Right (target e, regs', outs)
_ ->
Left $
AmbiguousEdges
s
[ MatchedEdgeSummary
{ matchedEdge = EdgeRef {edgeSource = s, edgeIndex = i},
matchedTarget = target e
}
| (i, e) <- matched
]
-- | Apply one observed output to the state by walking outgoing edges,
-- inverting each edge's @output@ via 'solveOutput', verifying the
-- guard on the recovered input, and applying the edge's @update@.
-- Exposed for callers that deliberately model letter-only event streams;
-- full-log replay uses the InFlight-aware streaming surface instead.
--
-- == Letter-only semantics
--
-- This function handles ε-edges (@output = []@; skipped because they
-- emit nothing observable) and letter edges (@output = [o]@;
-- inverted via 'solveOutput'). For multi-event edges (@output =
-- [o1, ..., oN]@ with N >= 2), this letter-flavoured 'applyEvent'
-- only inverts against the *head* of the output list, returning the
-- target vertex on a successful match. It is suitable when the
-- caller knows it is replaying letter-only events; for true
-- streaming replay across multi-event edges (where intermediate
-- events in the chain must be matched against the expected tail of
-- a prior edge's output list) use 'applyEventStreaming'.
applyEvent ::
(BoolAlg phi (RegFile rs, ci), Eq co) =>
SymTransducer phi rs s ci co ->
s ->
RegFile rs ->
co ->
Maybe (s, RegFile rs)
applyEvent t s regs co =
case [ (target e, applyEdgeUpdate e regs ci)
| e <- edgesOut t s,
o : _ <- [output e],
Just ci <- [solveOutput o regs co],
models (guard e) (regs, ci)
] of
[single] -> Just single
_ -> Nothing
-- | Streaming-replay state wrapper. Used by 'applyEventStreamingEither'
-- and its 'applyEventStreaming' compatibility wrapper.
--
-- @'Settled' s@ is the state at a stable vertex — the next event
-- must be the first emission of /some/ outgoing edge of @s@.
--
-- @'InFlight' s [e2, ..., eN]@ is the mid-chain state at vertex
-- @s@ (the *target* of the in-flight chain's edge; register updates
-- have already been applied at the transition into 'InFlight'). The
-- queue holds the *evaluated* expected events in order; the next
-- observed event must equal the head, popping it; when the queue
-- empties, the wrapper transitions to @'Settled' s@.
--
-- See @docs/research/gsm-widening-design.md@ §4 for the formal
-- treatment and a worked example on the @StartRegistration@ chain.
data InFlight s co
= Settled !s
| InFlight !s ![co]
deriving (Eq, Show)
-- | Why one observed event could not be replayed. Mirrors 'StepFailure'
-- and deliberately carries NO register values: diagnostics summarize,
-- they do not dump state. Events are carried where they identify the
-- failure because the event log is already observable data.
--
-- 'ReplayNoInvertingEdge' carries one rejected summary per outgoing
-- edge in declaration order, including edges with no output. An empty
-- list means the vertex had no outgoing edges. 'rejectedGuard' is
-- currently always 'False', matching 'NoMatchingEdge'.
data ReplayStepFailure s co
= ReplayNoInvertingEdge s [RejectedEdgeSummary s]
| ReplayAmbiguousInversions s [MatchedEdgeSummary s]
| ReplayQueueMismatch s co [co]
deriving stock (Eq, Show)
-- | Why replaying a list of observed events failed. A step failure
-- identifies an event that could not be consumed; truncation means the
-- input ended while a multi-event output chain still had pending events.
data ReplayFailureReason s co
= ReplayEventFailed (ReplayStepFailure s co)
| ReplayLogTruncated [co]
deriving stock (Eq, Show)
-- | A list-level replay failure with its zero-based input position and
-- wrapper state immediately before the failure. For 'ReplayLogTruncated',
-- 'replayFailedIndex' is the input length: the position where the next
-- expected event was missing.
data ReplayFailure s co = ReplayFailure
{ replayFailedIndex :: Int,
replayFailedState :: InFlight s co,
replayFailureReason :: ReplayFailureReason s co
}
deriving stock (Eq, Show)
-- | Compatibility wrapper around 'applyEventStreamingEither'. Prefer the
-- structured 'Either' variant for new code; this function preserves the
-- historical @Maybe@ signature and semantics.
--
-- Apply one observed output to a streaming-replay state. Two arms:
--
-- 1. @'Settled' s@ — walk outgoing edges of @s@; find the unique
-- edge whose @output@'s *head* inverts to a valid @ci@ via
-- 'solveOutput' satisfying the guard. Commit to that edge, run
-- its update, evaluate the *tail* of the output list against
-- the recovered @(regs, ci)@ snapshot. If the tail is empty
-- (letter edge), return @('Settled' (target e), regs')@. If the
-- tail is non-empty (multi-event edge), return @('InFlight'
-- (target e) tail, regs')@.
--
-- 2. @'InFlight' s (q1 : rest) regs@ — equality-check @q1@
-- against the observed event. On match, advance the queue
-- (returning @'Settled' s@ when @rest == []@, otherwise
-- @'InFlight' s rest@). No register update — registers were
-- updated at the @Settled → InFlight@ transition. On mismatch
-- (out-of-order replay) return 'Nothing'.
--
-- The 'Eq' constraint on @co@ supports the queue equality check.
-- Most aggregate event types derive 'Eq' (a documented expectation
-- of the foundations).
--
-- Inversion is deliberately head-only: 'solveOutput' is applied to the first
-- 'OutTerm' before the tail queue exists, and later events are equality-checked
-- only. Tail events therefore cannot supply command fields missing from the
-- head. 'validateTransducer' reports that authoring error as
-- 'HeadUnrecoverable'.
applyEventStreaming ::
(BoolAlg phi (RegFile rs, ci), Eq co) =>
SymTransducer phi rs s ci co ->
InFlight s co ->
RegFile rs ->
co ->
Maybe (InFlight s co, RegFile rs)
applyEventStreaming t wrapper regs co =
either (const Nothing) Just (applyEventStreamingEither t wrapper regs co)
-- | Apply one observed event to a streaming-replay state, returning a
-- structured explanation when replay cannot advance.
applyEventStreamingEither ::
(BoolAlg phi (RegFile rs, ci), Eq co) =>
SymTransducer phi rs s ci co ->
InFlight s co ->
RegFile rs ->
co ->
Either (ReplayStepFailure s co) (InFlight s co, RegFile rs)
applyEventStreamingEither t (Settled s) regs co =
case matched of
[] ->
Left $
ReplayNoInvertingEdge
s
[ RejectedEdgeSummary
{ rejectedEdge = EdgeRef {edgeSource = s, edgeIndex = i},
rejectedTarget = target e,
rejectedGuard = False
}
| (i, e) <- indexed
]
[(_, e, ci)] ->
let regs' = applyEdgeUpdate e regs ci
evaluatedTail = [evalOut o regs ci | o <- drop 1 (output e)]
wrapped = case evaluatedTail of
[] -> Settled (target e)
xs -> InFlight (target e) xs
in Right (wrapped, regs')
_ ->
Left $
ReplayAmbiguousInversions
s
[ MatchedEdgeSummary
{ matchedEdge = EdgeRef {edgeSource = s, edgeIndex = i},
matchedTarget = target e
}
| (i, e, _) <- matched
]
where
indexed = zip [0 ..] (edgesOut t s)
matched =
[ (i, e, ci)
| (i, e) <- indexed,
o : _ <- [output e],
Just ci <- [solveOutput o regs co],
models (guard e) (regs, ci)
]
applyEventStreamingEither _ (InFlight s queue) regs co = case queue of
q1 : rest
| q1 == co ->
Right
( case rest of
[] -> Settled s
_ -> InFlight s rest,
regs
)
_ -> Left (ReplayQueueMismatch s co queue)
-- | Strictly replay a list of observed events from an arbitrary wrapper
-- state and register-file seed. A list that ends mid-chain succeeds with
-- a final 'InFlight' wrapper so paginated callers can resume with the next
-- page. Use 'applyEventsEither' when ending mid-chain must be an error.
replayEvents ::
(BoolAlg phi (RegFile rs, ci), Eq co) =>
SymTransducer phi rs s ci co ->
(InFlight s co, RegFile rs) ->
[co] ->
Either (ReplayFailure s co) (InFlight s co, RegFile rs)
replayEvents t = go 0
where
go !_ seed [] = Right seed
go !eventIndex (wrapper, regs) (co : rest) =
case applyEventStreamingEither t wrapper regs co of
Left stepFailure ->
Left
ReplayFailure
{ replayFailedIndex = eventIndex,
replayFailedState = wrapper,
replayFailureReason = ReplayEventFailed stepFailure
}
Right next -> go (eventIndex + 1) next rest
-- | Compatibility wrapper around 'reconstituteEither'. Prefer the
-- structured 'Either' variant for new code. This function reconstitutes
-- @(state, registers)@ from a log of outputs while preserving the
-- historical @Maybe@ signature and semantics.
--
-- For letter-only transducers (every edge has @output@ of length 0
-- or 1) the streaming wrapper is always 'Settled' and the result is
-- identical to the pre-EP-19 letter-fold. A log that ends mid-chain
-- through a multi-event edge returns 'Nothing' — there is no valid
-- @(s, regs)@ to surface from an 'InFlight' final state.
reconstitute ::
(BoolAlg phi (RegFile rs, ci), Eq co) =>
SymTransducer phi rs s ci co ->
[co] ->
Maybe (s, RegFile rs)
reconstitute t events =
either (const Nothing) Just (reconstituteEither t events)
-- | Reconstitute @(state, registers)@ from the transducer's initial
-- state, returning the exact event index, wrapper state, and structured
-- reason when replay fails.
reconstituteEither ::
(BoolAlg phi (RegFile rs, ci), Eq co) =>
SymTransducer phi rs s ci co ->
[co] ->
Either (ReplayFailure s co) (s, RegFile rs)
reconstituteEither t = applyEventsEither t (initial t, initialRegs t)
-- | Compatibility wrapper around 'applyEventsEither'. Prefer the
-- structured 'Either' variant for new code. This function replays a
-- chunk of events from a caller-supplied @(state, registers)@ start while
-- preserving the historical @Maybe@ signature and semantics.
--
-- Useful when the runtime preserves command boundaries (event store
-- with command-id tags, transactional batches, deterministic test
-- fixtures): replay one command's events as one atomic step and
-- consume the unwrapped final state.
--
-- == Multi-event edges (EP-19 M3)
--
-- Internally, the implementation lifts the start state to 'Settled'
-- and folds 'applyEventStreaming' over the chunk; the wrapper
-- transitions through 'InFlight' for multi-event edges and unwraps
-- back to 'Settled' when the chunk completes. A chunk that ends
-- mid-flight (the queue is non-empty at the end of the input list)
-- returns 'Nothing'; this signals a truncated chunk relative to the
-- edge's static output length.
--
-- For length-0/1 edges the behaviour is identical to the legacy
-- letter-fold; for length-2+ edges the chunk must contain the full
-- expected sequence of evaluated events in order.
--
-- Returns 'Nothing' if any event in the chunk fails to replay (e.g.
-- a malformed log, an event that does not match any active edge's
-- output at the current vertex, or a chunk that ends mid-flight).
applyEvents ::
(BoolAlg phi (RegFile rs, ci), Eq co) =>
SymTransducer phi rs s ci co ->
(s, RegFile rs) ->
[co] ->
Maybe (s, RegFile rs)
applyEvents t seed events =
either (const Nothing) Just (applyEventsEither t seed events)
-- | Replay a complete chunk from a caller-supplied settled state. Unlike
-- 'replayEvents', this strict facade rejects a chunk that ends while a
-- multi-event output chain still has pending events.
applyEventsEither ::
(BoolAlg phi (RegFile rs, ci), Eq co) =>
SymTransducer phi rs s ci co ->
(s, RegFile rs) ->
[co] ->
Either (ReplayFailure s co) (s, RegFile rs)
applyEventsEither t (s0, regs0) events =
case replayEvents t (Settled s0, regs0) events of
Left failure -> Left failure
Right (Settled s, regs) -> Right (s, regs)
Right (wrapper@(InFlight _ pending), _regs) ->
Left
ReplayFailure
{ replayFailedIndex = length events,
replayFailedState = wrapper,
replayFailureReason = ReplayLogTruncated pending
}
-- * Build-time analyses ----------------------------------------------------
-- | Recover the input that produced a given output by walking
-- 'OutFields' structurally against the input constructor named by the
-- 'OPack'. Gather '(Index, value)' pairs from every top-level
-- 'TInpCtorField' read whose 'InCtor' matches by 'icName'; assemble a
-- 'RegFile' covering every slot of the 'InCtor'; call 'icBuild'.
--
-- == Recompute-and-verify (EP-47)
--
-- The command is recovered from the /invertible/ fields alone
-- (@TLit@\/@TReg@\/@TInpCtorField@); /derived/ fields (@TArith@\/@TApp1@\/
-- @TApp2@) are skipped during recovery by 'gatherInpEntries'. After the
-- command is rebuilt, the observed field tuple is rebuilt with each
-- /derived/ field recomputed forward (via 'recomputeDerivedFields') and
-- the resulting event is required to equal the observed event, so each
-- derived field is /verified/ rather than trusted — a tampered derived
-- value is rejected. Invertible fields are kept at their observed values
-- and are /not/ re-verified (so a @TReg@ audit field still round-trips
-- even when replay starts from a state whose registers are not yet
-- populated). This generalizes, at field granularity, the
-- forward-recompute-and-@Eq@-match that 'applyEventStreaming' already does
-- for multi-event tails (see @docs/research/recompute-and-verify-derived-outputs.md@).
--
-- For an all-invertible edge no field is recomputed, so the rebuilt event
-- equals the observed event by construction (the check is a no-op) and the
-- result is identical to the pre-EP-47 behavior. The build-time net
-- 'checkHiddenInputs' still rejects a schema whose command slot is read
-- only inside a derived field (a hidden input), so the command remains
-- recoverable from invertible fields alone — "the event determines the
-- command" is preserved.
--
-- Streaming replay calls this function only for an edge's head 'OutTerm'. It
-- never combines evidence from later outputs, so every command field needed by
-- replay must be recoverable here; 'HeadUnrecoverable' diagnoses a field found
-- only in the tail.
solveOutput :: (Eq co) => OutTerm rs ci co -> RegFile rs -> co -> Maybe ci
solveOutput (OPack ic@InCtor {} ctor fields) regs co = do
fs_obs <- wcMatch ctor co
entries <- gatherInpEntries fields fs_obs ic
rf <- assemble entries
let ci = icBuild ic rf
-- Rebuild the observed field tuple, recomputing ONLY the derived
-- fields (TApp/TArith) forward; invertible fields keep their observed
-- value. Comparing the rebuilt event to the observed one then verifies
-- exactly the derived fields — never the invertible ones, so a
-- register-read audit field is not re-checked against state and the
-- command thunk is not forced for an all-invertible edge.
rebuilt = wcBuild ctor (recomputeDerivedFields fields fs_obs regs ci)
if rebuilt == co
then Just ci
else Nothing
-- | Rebuild an observed output-field tuple, recomputing each /derived/
-- field ('TApp1'\/'TApp2'\/'TArith') forward via 'evalTerm' against the
-- recovered command and the pre-update registers, while leaving every
-- /invertible/ field ('TLit'\/'TReg'\/'TInpCtorField') at its observed
-- value. Used by 'solveOutput' (EP-47 recompute-and-verify): comparing the
-- rebuilt event to the observed one (via 'Eq' on @co@) then verifies
-- exactly the derived fields. Invertible fields are deliberately /not/
-- recomputed, so (a) a register-read audit field is not re-verified against
-- the current register file — preserving the "@TReg@ round-trips" contract
-- even when replay starts from a state whose registers are not yet
-- populated — and (b) the recovered-command thunk is not forced for an
-- all-invertible edge.
recomputeDerivedFields ::
forall rs ci ifs fs. OutFields rs ci ifs fs -> fs -> RegFile rs -> ci -> fs
recomputeDerivedFields OFNil () _ _ = ()
recomputeDerivedFields (OFCons t rest) (v, vs) regs ci =
(recomputeOne t v, recomputeDerivedFields rest vs regs ci)
where
recomputeOne :: forall f. Term rs ci ifs f -> f -> f
recomputeOne term@(TApp1 _ _) _observed = evalTerm term regs ci
recomputeOne term@(TApp2 _ _ _) _observed = evalTerm term regs ci
recomputeOne term@(TArith _ _ _) _observed = evalTerm term regs ci
recomputeOne _ observed = observed
-- | Walk an 'OutFields' HList in lockstep with an observed-fields
-- tuple, gathering '(Index, value)' pairs for the named 'InCtor' from
-- the /invertible/ fields. 'TLit'\/'TReg' contribute nothing; a
-- 'TInpCtorField' for the matching 'InCtor' contributes its
-- '(Index, value)' pair. Since EP-47 the /derived/ fields
-- ('TArith'\/'TApp1'\/'TApp2') are /skipped/ (they contribute no
-- entries) rather than aborting the walk — 'solveOutput' verifies them
-- forward afterwards. Returns 'Nothing' only on a genuinely malformed
-- edge: a 'TInpCtorField' naming a /different/ 'InCtor' (a runtime
-- diagnostic; soundness no longer depends on it — see below). 'assemble
-- []' for an empty 'ifs' is 'Just RNil', so empty-payload input
-- constructors recover trivially; and if a derived field is the /only/
-- place a command slot is read, the skipped slot leaves 'assemble'
-- short and 'solveOutput' fails — exactly the hidden-input case that
-- 'checkHiddenInputs' flags at build time.
--
-- == Type-safe index recovery (EP-53)
--
-- Because 'OutFields' is indexed by the same input field schema @ifs@ as
-- the 'OPack''s 'InCtor', a top-level 'TInpCtorField' inside this
-- 'OutFields' carries an @'Index' ifs r@ /into the @OPack@'s schema by
-- construction/. So @'ByIndex' ix val@ type-checks directly — no
-- @unsafeCoerce@ — and a constructor whose field schema differs from the
-- 'OPack''s 'InCtor' is rejected at compile time rather than coerced at
-- run time. The @'icName' ic1 == 'icName' ic2@ guard is retained only as
-- a defensive runtime diagnostic for an 'OutFields' that names a
-- different (but same-schema) constructor.
gatherInpEntries ::
forall rs ci ifs fs.
OutFields rs ci ifs fs -> fs -> InCtor ci ifs -> Maybe [ByIndex ifs]
gatherInpEntries OFNil () _ic = Just []
gatherInpEntries (OFCons t rest) (v, fs) ic = do
here <- stepOne t v ic
more <- gatherInpEntries rest fs ic
pure (here ++ more)
where
stepOne :: forall f. Term rs ci ifs f -> f -> InCtor ci ifs -> Maybe [ByIndex ifs]
stepOne (TLit _) _val _ = Just []
stepOne (TReg _) _val _ = Just []
stepOne (TInpCtorField ic2 ix) val ic1
| icName ic1 == icName ic2 = Just [ByIndex ix val]
| otherwise = Nothing
-- Derived fields are skipped here and verified forward by
-- 'solveOutput' (EP-47 recompute-and-verify); they contribute no
-- command information of their own.
stepOne (TApp1 _ _) _val _ = Just []
stepOne (TApp2 _ _ _) _val _ = Just []
stepOne (TArith _ _ _) _val _ = Just []
-- | A diagnostic produced by 'checkHiddenInputs'.
data HiddenInputWarning = HiddenInputWarning
{ -- | Description of the edge's source (typically @show s@).
hiwEdgeSource :: String,
-- | Human-readable description of what's hidden.
hiwReason :: String
}
deriving (Eq, Show)
-- | For every edge in the transducer, check whether the @output@ can
-- mechanically recover the input on replay. Specifically:
--
-- * If @output@ is @[]@ (an ε-edge), and @update@ reads the input
-- symbol, that contribution is silent on the wire and
-- unrecoverable.
-- * If @output@ is non-empty, the per-edge check distinguishes data
-- absent from the entire output union ('HirUnionMiss') from data
-- present only after the head event ('HirHeadUnrecoverable'). Replay
-- cannot use tail-only data because 'applyEventStreaming' inverts only
-- the head and equality-checks the tail.
--
-- For length-1 edges this matches the legacy per-'OPack' check. For
-- length-2+ edges, union coverage is retained only to classify the fix:
-- add absent data to the output, or move tail-only data into the head.
--
-- The check is intentionally conservative: it flags candidates for
-- the author to inspect, not theorems.
checkHiddenInputs ::
forall phi rs s ci co.
(Bounded s, Enum s, Show s) =>
SymTransducer phi rs s ci co ->
[HiddenInputWarning]
checkHiddenInputs t =
[ HiddenInputWarning
{ hiwEdgeSource = show s,
hiwReason = formatHiddenInputReason n r
}
| s <- [minBound .. maxBound],
(n, e) <- zip [(0 :: Int) ..] (edgesOut t s),
r <- hiddenInputReasons e
]
-- | A structured reason an edge's output cannot mechanically recover its
-- input on replay. This is the single source of truth behind both
-- 'checkHiddenInputs' (which formats these into the legacy 'HiddenInputWarning'
-- strings via 'formatHiddenInputReason') and 'hiddenInputWarnings' (which lifts
-- each into a structured 'TransducerValidationWarning' carrying the typed source
-- vertex, the input-constructor name, and the missing slot names).
data HiddenInputReason
= -- | An ε-edge (empty @output@) whose @update@ reads the input symbol,
-- so the read information is silent on the wire.
HirEpsilonReadsInput
| -- | The named input constructor has declared slots the edge's output
-- never recovers (after unioning every same-constructor 'OPack').
-- Carries the constructor name and the missing slot names.
HirUnionMiss String [String]
| -- | The named input constructor's slots appear in the output union but
-- not in the head event, so replay cannot reach them. Carries the
-- constructor name and the tail-only slot names.
HirHeadUnrecoverable String [String]
deriving (Eq, Show)
-- | The per-edge hidden-input analysis, factored out of 'checkHiddenInputs'
-- so the legacy string warnings and the structured 'hiddenInputWarnings' share
-- one implementation. For an ε-edge it reports 'HirEpsilonReadsInput' iff the
-- update reads the input; for a non-empty output it groups 'OPack's by input
-- constructor name, unions the recovered slots, and classifies misses as absent
-- from the union or present only after the head event (first-seen order,
-- deterministic).
hiddenInputReasons ::
forall phi rs ci co s. Edge phi rs ci co s -> [HiddenInputReason]
hiddenInputReasons e = case output e of
[]
| edgeReadsInput e -> [HirEpsilonReadsInput]
| otherwise -> []
outs@(headOut : _) -> concatMap (reasonsFor headOut) (groupByInCtorName outs)
where
reasonsFor ::
OutTerm rs ci co ->
(String, [String], [String]) ->
[HiddenInputReason]
reasonsFor headOut (icN, allSlots, visitedUnion) =
[HirUnionMiss icN missingFromUnion | not (null missingFromUnion)]
++ [HirHeadUnrecoverable icN tailOnly | not (null tailOnly)]
where
missingFromUnion = allSlots \\ nub visitedUnion
missingFromHead = case headOut of
OPack headIc _ headFields
| icName headIc == icN ->
maybe [] mifMissing (detectMissingInCtorFields headIc headFields)
| otherwise -> allSlots
tailOnly = missingFromHead \\ missingFromUnion
-- Walk the output list, accumulating per-InCtor (slot list, visited
-- slots). First seen wins on the slot list; subsequent OPacks with the
-- same InCtor name extend the visited list.
groupByInCtorName ::
[OutTerm rs ci co] -> [(String, [String], [String])]
groupByInCtorName = foldl add []
where
add acc (OPack ic _ fields) =
let icN = icName ic
allSl = slotNamesOf ic
visited = visitedSlotsOf ic fields
in extend acc icN allSl visited
extend [] icN allSl visited = [(icN, allSl, visited)]
extend ((n, sl, v) : rest) icN allSl visited
| n == icN = (n, sl, v ++ visited) : rest
| otherwise = (n, sl, v) : extend rest icN allSl visited
-- Slots of an OPack's named 'InCtor' that the supplied 'OutFields' walk
-- recovers via a /top-level/ 'TInpCtorField'. Since EP-47 this does NOT
-- descend into derived ('TApp1'\/'TApp2'\/'TArith') terms: a slot read
-- only inside a derived field is a /hidden input/, so it is reported
-- missing rather than counted as covered.
visitedSlotsOf ::
forall ifs fs.
InCtor ci ifs -> OutFields rs ci ifs fs -> [String]
visitedSlotsOf ic@InCtor {} fields = goFields fields
where
allSlots = slotNamesOf ic
goFields :: forall fs'. OutFields rs ci ifs fs' -> [String]
goFields OFNil = []
goFields (OFCons tt rest) = goTerm tt ++ goFields rest
goTerm :: forall r. Term rs ci ifs r -> [String]
goTerm (TInpCtorField ic2 ix)
| icName ic2 == icName ic =
[allSlots !! indexPos ix]
| otherwise = []
goTerm _ = [] -- do not descend into derived terms
indexPos :: forall rs' r. Index rs' r -> Int
indexPos ZIdx = 0
indexPos (SIdx i) = 1 + indexPos i
-- | Format a 'HiddenInputReason' into the legacy 'HiddenInputWarning' reason
-- string. The output is byte-identical to the pre-refactor 'checkHiddenInputs'
-- text so existing consumers and tests are unaffected.
formatHiddenInputReason :: Int -> HiddenInputReason -> String
formatHiddenInputReason n HirEpsilonReadsInput =
"edge #" <> show n <> ": ε-edge with input read in update"
formatHiddenInputReason n (HirUnionMiss icN missing) =
"edge #"
<> show n
<> ": OPack walk for InCtor \""
<> icN
<> "\" leaves field"
<> (if length missing == 1 then " " else "s ")
<> "{"
<> showMissing missing
<> "} unrecovered"
where
showMissing :: [String] -> String
showMissing [] = ""
showMissing [x] = "\"" <> x <> "\""
showMissing (x : xs) = "\"" <> x <> "\", " <> showMissing xs
formatHiddenInputReason n (HirHeadUnrecoverable icN missing) =
"edge #"
<> show n
<> ": head event does not recover InCtor \""
<> icN
<> "\" field"
<> (if length missing == 1 then " " else "s ")
<> "{"
<> showMissing missing
<> "}; the data appears only in later events of this edge, which replay cannot invert - move the field(s) into the FIRST emitted event"
where
showMissing :: [String] -> String
showMissing [] = ""
showMissing [x] = "\"" <> x <> "\""
showMissing (x : xs) = "\"" <> x <> "\", " <> showMissing xs
-- | Does the 'Update' read the input symbol via 'TInpCtorField'?
updateReadsInput :: Update rs w ci -> Bool
updateReadsInput UKeep = False
updateReadsInput (USet _ t) = termReadsInput t
updateReadsInput (UCombine a b) = updateReadsInput a || updateReadsInput b
-- | Does the 'Term' read the input symbol via 'TInpCtorField'?
termReadsInput :: Term rs ci ifs r -> Bool
termReadsInput (TLit _) = False
termReadsInput (TReg _) = False
termReadsInput (TInpCtorField _ _) = True
termReadsInput (TApp1 _ t) = termReadsInput t
termReadsInput (TApp2 _ a b) = termReadsInput a || termReadsInput b
termReadsInput (TArith _ a b) = termReadsInput a || termReadsInput b
-- | Do the 'OutFields' contain a 'TInpCtorField' read anywhere?
outFieldsHaveInpCtorField :: OutFields rs ci ifs fs -> Bool
outFieldsHaveInpCtorField OFNil = False
outFieldsHaveInpCtorField (OFCons t rest) =
termHasInpCtorField t || outFieldsHaveInpCtorField rest
where
termHasInpCtorField :: Term rs ci ifs r -> Bool
termHasInpCtorField (TLit _) = False
termHasInpCtorField (TReg _) = False
termHasInpCtorField (TInpCtorField _ _) = True
termHasInpCtorField (TApp1 _ t') = termHasInpCtorField t'
termHasInpCtorField (TApp2 _ a b) = termHasInpCtorField a || termHasInpCtorField b
termHasInpCtorField (TArith _ a b) = termHasInpCtorField a || termHasInpCtorField b
-- | The result of 'detectMissingInCtorFields': the offending 'InCtor'
-- name plus the names of slots its 'OutFields' walk does not visit.
data MissingInCtorFields = MissingInCtorFields
{ mifIcName :: String,
mifMissing :: [String]
}
deriving (Eq, Show)
-- | Given the 'InCtor' an 'OPack' is tagged with and that 'OPack'\'s
-- 'OutFields', return the field names of the 'InCtor' that the
-- 'OutFields' walk does not visit. 'Nothing' means every slot of the
-- 'InCtor' is visited. The slot list comes from the 'InCtor' itself
-- (via 'KnownSlotNames'), not from any 'TInpCtorField' inside the
-- 'OutFields' — this lets us flag empty 'OutFields' against a non-
-- empty 'InCtor' as well.
detectMissingInCtorFields ::
forall rs ci ifs fs.
InCtor ci ifs ->
OutFields rs ci ifs fs ->
Maybe MissingInCtorFields
detectMissingInCtorFields ic@InCtor {} fields =
case allSlots \\ nub visited of
[] -> Nothing
missing -> Just (MissingInCtorFields (icName ic) missing)
where
allSlots = slotNamesOf ic
visited = goFields fields
goFields :: forall fs'. OutFields rs ci ifs fs' -> [String]
goFields OFNil = []
goFields (OFCons t rest) = goTerm t ++ goFields rest
goTerm :: forall r. Term rs ci ifs r -> [String]
goTerm (TInpCtorField ic2 ix)
| icName ic2 == icName ic =
[allSlots !! indexPos ix]
| otherwise = []
goTerm _ = [] -- EP-47: top-level reads only; derived
-- (TApp/TArith) terms are not descended
-- into, so a slot read only inside one is
-- reported missing (a hidden input).
indexPos :: forall rs' r. Index rs' r -> Int
indexPos ZIdx = 0
indexPos (SIdx i) = 1 + indexPos i
-- | Read the slot-name list out of an 'InCtor' (uses the
-- 'KnownSlotNames' instance carried by the data constructor).
slotNamesOf :: forall ci ifs. InCtor ci ifs -> [String]
slotNamesOf InCtor {} = slotNames @ifs
-- * Build-time validation umbrella (EP-56) --------------------------------
-- | A structured build-time validation warning, parameterized over the
-- vertex type @s@ so it carries the real source vertex rather than a
-- pre-stringified one. It reuses the canonical 'EdgeRef' locator owned by EP-55
-- (the runtime explainer 'stepEither'), so the runtime and build-time
-- diagnostics speak one vocabulary.
--
-- Produced by 'validateTransducer'. The warning constructors cover replay
-- recoverability, safe input reads, deterministic inversion, and structural
-- reachability.
data TransducerValidationWarning s
= -- | An edge consumes command information that its output does not
-- emit, so the command cannot be reconstructed on replay.
HiddenInput
{ tvwEdge :: EdgeRef s,
-- | input constructor name, when known
tvwInCtor :: Maybe String,
-- | slot/field names left off the wire
tvwMissingSlots :: [String],
-- | human-readable summary
tvwDetail :: String
}
| -- | A multi-event edge whose first event cannot recover all command
-- fields even though later events carry the missing data. Streaming
-- replay inverts only the first event, so the edge produces a log it
-- cannot replay.
HeadUnrecoverable
{ tvwEdge :: EdgeRef s,
tvwInCtor :: Maybe String,
tvwTailOnlySlots :: [String],
tvwDetail :: String
}
| -- | Two outgoing edges use the same wire constructor for their first
-- event. Replay requires a unique inverting edge, so the observed
-- event may reconstruct commands for both edges and become ambiguous.
InversionAmbiguity
{ tvwSource :: s,
tvwEdgeA :: Int,
tvwEdgeB :: Int,
tvwWireCtor :: String,
tvwDetail :: String
}
| -- | An edge reads a field of an input constructor without first
-- establishing the matching top-level 'PInCtor' guard. A different
-- command can reach the read and make 'evalTerm' throw.
UnguardedInputRead
{ tvwEdge :: EdgeRef s,
tvwInCtor :: Maybe String,
tvwDetail :: String
}
| -- | An output-free edge changes control state or can write registers.
-- Persisting only emitted events loses that transition, so replay of
-- the resulting log cannot reproduce the forward state.
StateChangingEpsilon
{ tvwEdge :: EdgeRef s,
tvwChangesVertex :: Bool,
tvwWritesRegisters :: Bool,
tvwDetail :: String
}
| -- | Two outgoing edges of the same vertex whose guards can both hold
-- for one command — a runtime nondeterminism / single-valuedness
-- violation (its dynamic witness is EP-55's @AmbiguousEdges@).
NondeterministicPair
{ tvwSource :: s,
tvwEdgeA :: Int,
tvwEdgeB :: Int,
tvwInCtor :: Maybe String,
tvwDetail :: String
}
| -- | An edge that can never fire: its source vertex is unreachable
-- from 'initial', or its guard is statically unsatisfiable. Labelled
-- "possibly" because the structural pass is conservative.
PossiblyDeadEdge
{ tvwEdge :: EdgeRef s,
tvwDetail :: String
}
| -- | An edge whose guard contains an opaque 'TApp' term. The symbolic
-- single-valuedness and dead-edge analyses translate such a term to an
-- unconstrained free variable ('Keiki.Symbolic.translateTermSym' emits
-- @SBV.free "app1"@), so they cannot see through the guard and silently
-- under-verify it. Most often this is a collection-content condition
-- (membership, "all resolved", size) lifted through a closure because the
-- structural predicate language has no node for it; see the user guide and
-- @docs\/plans\/60-first-class-collection-registers-design-gated.md@ for the
-- options. Advisory, not a soundness error: opt in via 'warnOpaqueGuards'.
OpaqueGuard
{ tvwEdge :: EdgeRef s,
tvwDetail :: String
}
deriving stock (Eq, Show)
-- | Which checks 'validateTransducer' runs. Construct options by updating
-- 'defaultValidationOptions'; new fields are added as new checks land.
data ValidationOptions = ValidationOptions
{ -- | run the hidden-input check
failOnEpsilonReadsInput :: Bool,
-- | run the (pure, structural) determinism check
checkDeterminism :: Bool,
-- | run the (structural) dead-edge check
checkReachability :: Bool,
-- | run the opaque-guard audit (opt-in; default off). Flags edges whose
-- guard branches on an opaque 'TApp' term the symbolic analyses cannot
-- see through. Off by default so 'defaultValidationOptions' keeps its
-- meaning for existing consumers.
warnOpaqueGuards :: Bool,
-- | require the first emitted event to recover every command field used
-- by replay
checkHeadRecoverability :: Bool,
-- | conservatively flag outgoing edge pairs with the same head wire
-- constructor
checkInversionAmbiguity :: Bool,
-- | require every input-field read to be protected by an earlier matching
-- constructor guard
checkGuardImpliesInputRead :: Bool,
-- | reject output-free edges that change vertex or can write registers.
-- Never disable this for a transducer whose events are persisted:
-- downstream durable boundaries must force-enable it rather than let
-- callers opt out.
checkStateChangingEpsilon :: Bool
}
deriving stock (Eq, Show)
-- | Replay-safety checks enabled; the advisory opaque-guard audit off.
defaultValidationOptions :: ValidationOptions
defaultValidationOptions =
ValidationOptions
{ failOnEpsilonReadsInput = True,
checkDeterminism = True,
checkReachability = True,
warnOpaqueGuards = False,
checkHeadRecoverability = True,
checkInversionAmbiguity = True,
checkGuardImpliesInputRead = True,
checkStateChangingEpsilon = True
}
-- | The build-time validation umbrella. Runs the enabled checks over the
-- 'HsPred' (syntactic, /no solver/) carrier and concatenates their structured
-- warnings, so a project can put @validateTransducer defaultValidationOptions t
-- == []@ directly in a unit test and have it pass or fail in microseconds with
-- no external z3 process.
--
-- Subject to honest 'InCtor' and 'WireCtor' implementations, a transducer for
-- which this returns @[]@ under 'defaultValidationOptions' can replay every log
-- it produces via 'reconstitute'. 'HeadUnrecoverable',
-- 'InversionAmbiguity', 'UnguardedInputRead', and
-- 'StateChangingEpsilon' exist to align build-time acceptance with the
-- head-first semantics of 'applyEventStreaming'. Disabling those checks weakens
-- that replay guarantee.
--
-- The default path is deliberately specialised to the 'HsPred' carrier and is
-- /cheap and pure/: the determinism component flags only structurally-provable
-- overlaps in conjunction spines containing constructor tests and
-- variable-versus-literal comparisons. It uses exact interval reasoning for
-- integral variables and concrete literal witnesses for other types. Disjunction,
-- negation, arithmetic, opaque terms, variable-versus-variable comparisons, and
-- non-integral strict-bound density remain unknown and produce no pure warning.
-- The pass therefore has no false positives but can miss overlaps outside that
-- fragment. The dead-edge component is structural reachability plus a literal-
-- 'PBot' check. For the exact, solver-backed answers use
-- 'Keiki.Symbolic.checkTransitionDeterminismSym' and
-- 'Keiki.Symbolic.checkDeadEdgesSym' directly.
validateTransducer ::
(Bounded s, Enum s, Ord s, Show s) =>
ValidationOptions ->
SymTransducer (HsPred rs ci) rs s ci co ->
[TransducerValidationWarning s]
validateTransducer opts t =
concat
[ if failOnEpsilonReadsInput opts then hiddenInputWarnings t else [],
if checkHeadRecoverability opts then headRecoverabilityWarnings t else [],
if checkInversionAmbiguity opts then inversionAmbiguityWarnings t else [],
if checkGuardImpliesInputRead opts then guardImpliesInputReadWarnings t else [],
if checkStateChangingEpsilon opts then stateChangingEpsilonWarnings t else [],
if checkDeterminism opts then determinismWarnings t else [],
if checkReachability opts
then
[ PossiblyDeadEdge (dewEdge w) (dewReason w)
| w <- checkDeadEdges defaultDeadEdgeOptions t
]
else [],
if warnOpaqueGuards opts then opaqueGuardWarnings t else []
]
-- | Structured form of the hidden-input check, additive over
-- 'checkHiddenInputs'. Reuses the same per-edge analysis ('hiddenInputReasons')
-- and lifts each result into a 'TransducerValidationWarning' carrying the typed
-- source vertex (via 'EdgeRef'), the input-constructor name, and the missing
-- slot names — data a downstream project can pattern-match on rather than parse
-- out of a string.
hiddenInputWarnings ::
(Bounded s, Enum s) =>
SymTransducer phi rs s ci co ->
[TransducerValidationWarning s]
hiddenInputWarnings t =
[ HiddenInput
{ tvwEdge = EdgeRef {edgeSource = s, edgeIndex = n},
tvwInCtor = inCtorOf r,
tvwMissingSlots = missingSlotsOf r,
tvwDetail = formatHiddenInputReason n r
}
| s <- [minBound .. maxBound],
(n, e) <- zip [(0 :: Int) ..] (edgesOut t s),
r <- hiddenInputReasons e,
isHiddenReason r
]
where
inCtorOf (HirUnionMiss icN _) = Just icN
inCtorOf HirEpsilonReadsInput = Nothing
inCtorOf (HirHeadUnrecoverable _ _) = Nothing
missingSlotsOf (HirUnionMiss _ ms) = ms
missingSlotsOf HirEpsilonReadsInput = []
missingSlotsOf (HirHeadUnrecoverable _ _) = []
isHiddenReason HirEpsilonReadsInput = True
isHiddenReason (HirUnionMiss _ _) = True
isHiddenReason (HirHeadUnrecoverable _ _) = False
-- | Warn when a multi-event edge's head event cannot alone recover command
-- fields that appear later in the same output chain. 'applyEventStreaming'
-- inverts only the head output; tail events are equality-checked after the edge
-- has already been selected.
headRecoverabilityWarnings ::
(Bounded s, Enum s) =>
SymTransducer phi rs s ci co ->
[TransducerValidationWarning s]
headRecoverabilityWarnings t =
[ HeadUnrecoverable
{ tvwEdge = EdgeRef {edgeSource = s, edgeIndex = n},
tvwInCtor = Just icN,
tvwTailOnlySlots = missing,
tvwDetail = formatHiddenInputReason n reason
}
| s <- [minBound .. maxBound],
(n, e) <- zip [(0 :: Int) ..] (edgesOut t s),
reason@(HirHeadUnrecoverable icN missing) <- hiddenInputReasons e
]
-- ** Opaque-guard diagnostics
-- | Does the term contain an opaque 'TApp1'\/'TApp2' anywhere? Mirrors the
-- structural recursion of 'termReadsInput'; 'TArith' is transparent, so it
-- recurses into its operands rather than counting as opaque.
termHasOpaqueApp :: Term rs ci ifs r -> Bool
termHasOpaqueApp (TLit _) = False
termHasOpaqueApp (TReg _) = False
termHasOpaqueApp (TInpCtorField _ _) = False
termHasOpaqueApp (TApp1 _ _) = True
termHasOpaqueApp (TApp2 _ _ _) = True
termHasOpaqueApp (TArith _ a b) = termHasOpaqueApp a || termHasOpaqueApp b
-- | Does the guard predicate branch on an opaque term anywhere? The symbolic
-- analyses cannot see through such a guard (it becomes a free SBV variable),
-- so they silently under-verify the edge.
predHasOpaqueTerm :: HsPred rs ci -> Bool
predHasOpaqueTerm PTop = False
predHasOpaqueTerm PBot = False
predHasOpaqueTerm (PAnd p q) = predHasOpaqueTerm p || predHasOpaqueTerm q
predHasOpaqueTerm (POr p q) = predHasOpaqueTerm p || predHasOpaqueTerm q
predHasOpaqueTerm (PNot p) = predHasOpaqueTerm p
predHasOpaqueTerm (PEq a b) = termHasOpaqueApp a || termHasOpaqueApp b
predHasOpaqueTerm (PInCtor _) = False
predHasOpaqueTerm PLeftArm = False
predHasOpaqueTerm PRightArm = False
predHasOpaqueTerm (PCmp _ a b) = termHasOpaqueApp a || termHasOpaqueApp b
-- | The opt-in opaque-guard audit (run by 'validateTransducer' only when
-- 'warnOpaqueGuards' is set). For every edge whose guard contains an opaque
-- 'TApp' term, emit an 'OpaqueGuard' warning locating the edge by its typed
-- 'EdgeRef'. Specialised to the 'HsPred' carrier because it walks the predicate
-- AST, exactly as 'validateTransducer' is.
opaqueGuardWarnings ::
(Bounded s, Enum s) =>
SymTransducer (HsPred rs ci) rs s ci co ->
[TransducerValidationWarning s]
opaqueGuardWarnings t =
[ OpaqueGuard
{ tvwEdge = EdgeRef {edgeSource = s, edgeIndex = n},
tvwDetail =
"guard contains an opaque TApp term the symbolic analyses cannot "
++ "see through; its single-valuedness was not verified"
}
| s <- [minBound .. maxBound],
(n, e) <- zip [(0 :: Int) ..] (edgesOut t s),
predHasOpaqueTerm (guard e)
]
-- ** Guarded input-read diagnostics
termInCtorNames :: Term rs ci ifs r -> [String]
termInCtorNames (TLit _) = []
termInCtorNames (TReg _) = []
termInCtorNames (TInpCtorField ic _) = [icName ic]
termInCtorNames (TApp1 _ t) = termInCtorNames t
termInCtorNames (TApp2 _ a b) = termInCtorNames a ++ termInCtorNames b
termInCtorNames (TArith _ a b) = termInCtorNames a ++ termInCtorNames b
predInCtorReadNames :: HsPred rs ci -> [String]
predInCtorReadNames PTop = []
predInCtorReadNames PBot = []
predInCtorReadNames (PAnd p q) = predInCtorReadNames p ++ predInCtorReadNames q
predInCtorReadNames (POr p q) = predInCtorReadNames p ++ predInCtorReadNames q
predInCtorReadNames (PNot p) = predInCtorReadNames p
predInCtorReadNames (PEq a b) = termInCtorNames a ++ termInCtorNames b
predInCtorReadNames (PInCtor _) = []
predInCtorReadNames PLeftArm = []
predInCtorReadNames PRightArm = []
predInCtorReadNames (PCmp _ a b) = termInCtorNames a ++ termInCtorNames b
updateInCtorNames :: Update rs w ci -> [String]
updateInCtorNames UKeep = []
updateInCtorNames (USet _ term) = termInCtorNames term
updateInCtorNames (UCombine a b) = updateInCtorNames a ++ updateInCtorNames b
outFieldsInCtorNames :: OutFields rs ci ifs fs -> [String]
outFieldsInCtorNames OFNil = []
outFieldsInCtorNames (OFCons term rest) =
termInCtorNames term ++ outFieldsInCtorNames rest
outTermInCtorNames :: OutTerm rs ci co -> [String]
outTermInCtorNames (OPack _ _ fields) = outFieldsInCtorNames fields
-- | Check that every 'TInpCtorField' read is protected by a matching
-- top-level 'PInCtor' conjunct. Guard reads are order-sensitive: the guard is
-- walked along its top-level 'PAnd' spine from left to right, matching Haskell's
-- lazy @(&&)@ evaluation. A constructor established to the right of a read is
-- too late. Reads in updates and outputs run after the complete guard succeeds,
-- so any constructor established on the spine protects them.
--
-- 'POr', 'PNot', comparisons, and nested boolean forms establish nothing; a
-- constructor atom inside them does not imply that the whole guard matched that
-- constructor. Builder 'onCmd' edges are safe by construction because their
-- guard starts with the appropriate 'PInCtor'. An unsatisfiable conjunction of
-- different constructors may pass this crash-safety check and is left to the
-- dead-edge analyses.
guardImpliesInputReadWarnings ::
forall rs s ci co.
(Bounded s, Enum s, Show s) =>
SymTransducer (HsPred rs ci) rs s ci co ->
[TransducerValidationWarning s]
guardImpliesInputReadWarnings t =
[ UnguardedInputRead
{ tvwEdge = EdgeRef {edgeSource = s, edgeIndex = n},
tvwInCtor = Just icN,
tvwDetail =
location
<> " reads InCtor \""
<> icN
<> "\" but edge #"
<> show n
<> " out of "
<> show s
<> " does not establish PInCtor \""
<> icN
<> "\" before it; a non-\""
<> icN
<> "\" command reaching this edge crashes instead of being rejected"
}
| s <- [minBound .. maxBound],
(n, edge) <- zip [(0 :: Int) ..] (edgesOut t s),
(icN, location) <- edgeViolations edge
]
where
edgeViolations :: Edge (HsPred rs ci) rs ci co s -> [(String, String)]
edgeViolations Edge {guard = edgeGuard, update = edgeUpdate, output = edgeOutput} =
nub (guardViolations ++ updateViolations ++ outputViolations)
where
(guardViolations, established) = checkGuard [] edgeGuard
updateViolations =
[ (icN, "update")
| icN <- nub (updateInCtorNames edgeUpdate),
icN `notElem` established
]
outputViolations =
[ (icN, "output")
| icN <- nub (concatMap outTermInCtorNames edgeOutput),
icN `notElem` established
]
checkGuard :: [String] -> HsPred rs ci -> ([(String, String)], [String])
checkGuard established (PAnd p q) =
let (leftViolations, afterLeft) = checkGuard established p
(rightViolations, afterRight) = checkGuard afterLeft q
in (leftViolations ++ rightViolations, afterRight)
checkGuard established (PInCtor ic) =
([], nub (established ++ [icName ic]))
checkGuard established predicate =
( [ (icN, "guard")
| icN <- nub (predInCtorReadNames predicate),
icN `notElem` established
],
established
)
-- ** State-changing epsilon diagnostics
updateWritesRegisters :: Update rs w ci -> Bool
updateWritesRegisters UKeep = False
updateWritesRegisters USet {} = True
updateWritesRegisters (UCombine a b) =
updateWritesRegisters a || updateWritesRegisters b
-- | Flag output-free edges that change control state or are structurally
-- capable of writing registers. Such an edge can be meaningful when a
-- transducer is used only as an in-memory state machine, but it is not durable:
-- persisting the empty output loses the transition and replay cannot reproduce
-- its result.
--
-- Control-state detection is exact. Register detection is conservative:
-- 'USet', or any 'UCombine' containing one, warns even when a particular write
-- happens to store the value already present. A self-loop with 'UKeep' remains
-- clean.
stateChangingEpsilonWarnings ::
forall rs s ci co.
(Bounded s, Enum s, Eq s, Show s) =>
SymTransducer (HsPred rs ci) rs s ci co ->
[TransducerValidationWarning s]
stateChangingEpsilonWarnings t =
[ StateChangingEpsilon
{ tvwEdge = EdgeRef {edgeSource = source, edgeIndex = edgeNumber},
tvwChangesVertex = changesVertex,
tvwWritesRegisters = writesRegisters,
tvwDetail =
"output-free edge #"
<> show edgeNumber
<> " out of "
<> show source
<> changeSummary changesVertex writesRegisters
<> "; persisted replay cannot reproduce that transition without an emitted event"
}
| source <- [minBound .. maxBound],
(edgeNumber, Edge {update = edgeUpdate, output = edgeOutput, target = edgeTarget}) <-
zip [(0 :: Int) ..] (edgesOut t source),
null edgeOutput,
let changesVertex = edgeTarget /= source,
let writesRegisters = updateWritesRegisters edgeUpdate,
changesVertex || writesRegisters
]
where
changeSummary True True = " changes vertex and can write registers"
changeSummary True False = " changes vertex"
changeSummary False True = " can write registers"
changeSummary False False = ""
-- ** Replay inversion diagnostics
-- | Conservatively flag pairs of outgoing edges whose first emitted events
-- use the same 'WireCtor' name. Replay selects an edge by inverting one observed
-- head event, so both edges may reconstruct their own commands and satisfy their
-- own guards even when forward command dispatch is deterministic.
--
-- This structural check intentionally over-approximates ambiguity. It cannot
-- prove semantic guard disjointness over recovered values or registers; it
-- cannot compare differing 'TLit' values because 'TLit' carries no 'Eq' or
-- 'Typeable' evidence; and it does not predict derived-field verification in
-- 'solveOutput'. It ignores tail events because replay equality-checks rather
-- than inverts them. Different head constructor names are safe under the
-- documented honesty law of 'wcMatch'. Literal-'PBot' guards are exempt because
-- such an edge cannot participate in a successful inversion.
inversionAmbiguityWarnings ::
forall rs s ci co.
(Bounded s, Enum s, Show s) =>
SymTransducer (HsPred rs ci) rs s ci co ->
[TransducerValidationWarning s]
inversionAmbiguityWarnings t =
[ InversionAmbiguity
{ tvwSource = s,
tvwEdgeA = i,
tvwEdgeB = j,
tvwWireCtor = wireName,
tvwDetail =
"edges #"
<> show i
<> " and #"
<> show j
<> " out of "
<> show s
<> " both emit \""
<> wireName
<> "\" as their first event; replay may not be able to attribute an observed \""
<> wireName
<> "\" to a unique edge"
}
| s <- [minBound .. maxBound],
let indexedEdges = zip [(0 :: Int) ..] (edgesOut t s),
(i, e1) <- indexedEdges,
(j, e2) <- indexedEdges,
i < j,
not (isBot (guard e1) || isBot (guard e2)),
Just wireName <- [headWireName e1],
Just otherWireName <- [headWireName e2],
wireName == otherWireName
]
where
headWireName :: Edge (HsPred rs ci) rs ci co s -> Maybe String
headWireName Edge {output = OPack _ wire _ : _} = Just (wcName wire)
headWireName _ = Nothing
-- ** Determinism diagnostics
-- | A determinism warning: two outgoing edges of the same vertex whose guards
-- can both hold. Carries both edge indices and the (typed) source vertex.
data DeterminismWarning s = DeterminismWarning
{ dwSource :: s,
-- | first overlapping edge index
dwEdgeA :: Int,
-- | second overlapping edge index
dwEdgeB :: Int,
dwDetail :: String
}
deriving stock (Eq, Show)
-- | Per-vertex, per-pair determinism diagnostic. Reuses the exact pairing
-- structure of 'Keiki.Symbolic.isSingleValuedSym': for every vertex, for every
-- pair @(i,e1),(j,e2)@ with @i<j@, the pair is ambiguous when
-- @guard e1 \`conj\` guard e2@ is /not/ 'isBot'. So
-- @checkTransitionDeterminism t == []@ iff @isSingleValuedSym t@ under the same
-- carrier.
--
-- Soundness direction: with the pure 'HsPred' carrier, 'isBot' only recognises
-- the literal 'PBot', so @not (isBot (a \`conj\` b))@ holds for /every/ non-'PBot'
-- pair — i.e. this polymorphic check over-approximates overlap on the 'HsPred'
-- carrier (it would flag almost every multi-edge vertex). It is intended to be
-- run over the /symbolic/ 'SymPred' carrier (via
-- 'Keiki.Symbolic.checkTransitionDeterminismSym'), whose 'isBot' is exact. For
-- the pure path 'validateTransducer' uses the under-approximating
-- 'checkTransitionDeterminismPure' instead, which flags only true positives.
checkTransitionDeterminism ::
forall phi rs s ci co.
(BoolAlg phi (RegFile rs, ci), Bounded s, Enum s, Show s) =>
SymTransducer phi rs s ci co ->
[DeterminismWarning s]
checkTransitionDeterminism t =
[ DeterminismWarning
{ dwSource = s,
dwEdgeA = i,
dwEdgeB = j,
dwDetail = overlapDetail i j s
}
| s <- [minBound .. maxBound],
let ies = zip [(0 :: Int) ..] (edgesOut t s),
(i, e1) <- ies,
(j, e2) <- ies,
i < j,
not (isBot (guard e1 `conj` guard e2))
]
-- | Over-approximation-free determinism check for the pure 'HsPred' carrier.
-- It proves overlap through conjunction spines containing 'PTop', compatible
-- 'PInCtor' atoms, and variable-versus-literal equality or ordering atoms.
-- Integral variables ('Int', 'Integer', fixed-width words and signed integers)
-- use exact interval intersection; other types require one of the mentioned
-- literals to be a concrete witness. Disjunction, negation, structural
-- arithmetic, opaque terms, variable-versus-variable comparisons, and strict
-- non-integral bounds are outside the fragment and produce no warning. Used by
-- 'validateTransducer' so every warning is a true positive. Absence does not
-- prove determinism; run 'Keiki.Symbolic.checkTransitionDeterminismSym' for the
-- exact solver-backed answer.
checkTransitionDeterminismPure ::
forall rs s ci co.
(Bounded s, Enum s, Show s) =>
SymTransducer (HsPred rs ci) rs s ci co ->
[DeterminismWarning s]
checkTransitionDeterminismPure t =
[ DeterminismWarning
{ dwSource = s,
dwEdgeA = i,
dwEdgeB = j,
dwDetail = overlapDetail i j s
}
| s <- [minBound .. maxBound],
let ies = zip [(0 :: Int) ..] (edgesOut t s),
(i, e1) <- ies,
(j, e2) <- ies,
i < j,
provablyOverlap (guard e1) (guard e2)
]
overlapDetail :: (Show s) => Int -> Int -> s -> String
overlapDetail i j s =
"edges #"
<> show i
<> " and #"
<> show j
<> " out of "
<> show s
<> " have overlapping guards"
-- | A named variable in the pure overlap fragment. Register and input-field
-- namespaces are distinct. Input fields retain their constructor name so a
-- witness is accepted only when a matching 'PInCtor' atom is present.
data PureVariable = PureVariable
{ pureVariableName :: String,
pureVariableInputCtor :: Maybe String
}
deriving stock (Eq, Show)
data PureRelation = PureEq | PureLt | PureLe | PureGt | PureGe
deriving stock (Eq, Show)
-- | One normalized @variable relation literal@ atom. The predicate closure
-- captures the source constructor's real 'Eq' or 'Ord' dictionary for concrete
-- literal-witness probing.
data PureComparison where
PureComparison ::
(Typeable r) =>
PureVariable ->
PureRelation ->
r ->
(r -> Bool) ->
PureComparison
data PureGuard = PureGuard
{ pureGuardConstructors :: [String],
pureGuardComparisons :: [PureComparison]
}
data PureFragment
= PureUnknown
| PureUnsatisfiable
| PureKnown PureGuard
emptyPureGuard :: PureGuard
emptyPureGuard = PureGuard [] []
-- | Parse the exact, deliberately small fragment accepted by
-- 'provablyOverlap'.
pureFragment :: HsPred rs ci -> PureFragment
pureFragment PTop = PureKnown emptyPureGuard
pureFragment PBot = PureUnsatisfiable
pureFragment (PAnd a b) = mergePureFragments (pureFragment a) (pureFragment b)
pureFragment (PInCtor ic) =
PureKnown emptyPureGuard {pureGuardConstructors = [icName ic]}
pureFragment (PEq a b) = pureEquality a b
pureFragment (PCmp relation a b) = pureOrdering relation a b
pureFragment PLeftArm = PureUnknown
pureFragment PRightArm = PureUnknown
pureFragment (POr _ _) = PureUnknown
pureFragment (PNot _) = PureUnknown
mergePureFragments :: PureFragment -> PureFragment -> PureFragment
mergePureFragments PureUnsatisfiable _ = PureUnsatisfiable
mergePureFragments _ PureUnsatisfiable = PureUnsatisfiable
mergePureFragments PureUnknown _ = PureUnknown
mergePureFragments _ PureUnknown = PureUnknown
mergePureFragments (PureKnown a) (PureKnown b) =
PureKnown
PureGuard
{ pureGuardConstructors =
pureGuardConstructors a <> pureGuardConstructors b,
pureGuardComparisons =
pureGuardComparisons a <> pureGuardComparisons b
}
pureEquality ::
forall rs ci ifs1 ifs2 r.
(Eq r, Typeable r) =>
Term rs ci ifs1 r ->
Term rs ci ifs2 r ->
PureFragment
pureEquality (TLit a) (TLit b)
| a == b = PureKnown emptyPureGuard
| otherwise = PureUnsatisfiable
pureEquality variable (TLit literalValue)
| Just name <- pureVariable variable =
knownComparison name PureEq literalValue (== literalValue)
pureEquality (TLit literalValue) variable
| Just name <- pureVariable variable =
knownComparison name PureEq literalValue (== literalValue)
pureEquality _ _ = PureUnknown
pureOrdering ::
forall rs ci ifs1 ifs2 r.
(Ord r, Typeable r) =>
Cmp ->
Term rs ci ifs1 r ->
Term rs ci ifs2 r ->
PureFragment
pureOrdering relation (TLit a) (TLit b)
| applyPureCmp relation a b = PureKnown emptyPureGuard
| otherwise = PureUnsatisfiable
pureOrdering relation variable (TLit literalValue)
| Just name <- pureVariable variable =
let normalized = pureRelation relation
in knownComparison
name
normalized
literalValue
(\value -> applyPureRelation normalized value literalValue)
pureOrdering relation (TLit literalValue) variable
| Just name <- pureVariable variable =
let normalized = flipPureRelation (pureRelation relation)
in knownComparison
name
normalized
literalValue
(\value -> applyPureRelation normalized value literalValue)
pureOrdering _ _ _ = PureUnknown
knownComparison ::
(Typeable r) =>
PureVariable ->
PureRelation ->
r ->
(r -> Bool) ->
PureFragment
knownComparison variable relation literalValue accepts =
PureKnown
emptyPureGuard
{ pureGuardComparisons =
[PureComparison variable relation literalValue accepts]
}
pureVariable :: Term rs ci ifs r -> Maybe PureVariable
pureVariable (TReg index) =
Just (PureVariable ("reg/" <> pureIndexName index) Nothing)
pureVariable (TInpCtorField ic index) =
Just
( PureVariable
("inp/" <> icName ic <> "/" <> pureIndexName index)
(Just (icName ic))
)
pureVariable _ = Nothing
pureIndexName :: forall rs r. Index rs r -> String
pureIndexName (ZIdx @name) = symbolVal (Proxy @name)
pureIndexName (SIdx index) = pureIndexName index
pureRelation :: Cmp -> PureRelation
pureRelation CmpLt = PureLt
pureRelation CmpLe = PureLe
pureRelation CmpGt = PureGt
pureRelation CmpGe = PureGe
flipPureRelation :: PureRelation -> PureRelation
flipPureRelation PureEq = PureEq
flipPureRelation PureLt = PureGt
flipPureRelation PureLe = PureGe
flipPureRelation PureGt = PureLt
flipPureRelation PureGe = PureLe
applyPureCmp :: (Ord r) => Cmp -> r -> r -> Bool
applyPureCmp CmpLt = (<)
applyPureCmp CmpLe = (<=)
applyPureCmp CmpGt = (>)
applyPureCmp CmpGe = (>=)
applyPureRelation :: (Ord r) => PureRelation -> r -> r -> Bool
applyPureRelation PureEq = (==)
applyPureRelation PureLt = (<)
applyPureRelation PureLe = (<=)
applyPureRelation PureGt = (>)
applyPureRelation PureGe = (>=)
-- | Structurally prove that a concrete witness exists for both guards. The
-- accepted fragment is described on 'checkTransitionDeterminismPure'. Returning
-- 'False' means either disjoint or unknown. Like the historical @PTop@ and
-- @PInCtor@ cases, this proof assumes the register and command schemas are
-- inhabited.
provablyOverlap :: HsPred rs ci -> HsPred rs ci -> Bool
provablyOverlap PLeftArm PLeftArm = True
provablyOverlap PRightArm PRightArm = True
provablyOverlap a b = case (pureFragment a, pureFragment b) of
(PureKnown leftGuard, PureKnown rightGuard) ->
pureGuardsOverlap leftGuard rightGuard
_ -> False
pureGuardsOverlap :: PureGuard -> PureGuard -> Bool
pureGuardsOverlap leftGuard rightGuard = case commonPureConstructor of
Nothing -> False
Just constructorName ->
all (comparisonMatchesConstructor constructorName) comparisons
&& all pureComparisonGroupSatisfiable (groupPureComparisons comparisons)
where
comparisons =
pureGuardComparisons leftGuard <> pureGuardComparisons rightGuard
commonPureConstructor = do
leftConstructor <- singlePureConstructor (pureGuardConstructors leftGuard)
rightConstructor <- singlePureConstructor (pureGuardConstructors rightGuard)
compatiblePureConstructors leftConstructor rightConstructor
singlePureConstructor :: [String] -> Maybe (Maybe String)
singlePureConstructor names = case nub names of
[] -> Just Nothing
[name] -> Just (Just name)
_ -> Nothing
compatiblePureConstructors ::
Maybe String -> Maybe String -> Maybe (Maybe String)
compatiblePureConstructors Nothing Nothing = Just Nothing
compatiblePureConstructors (Just name) Nothing = Just (Just name)
compatiblePureConstructors Nothing (Just name) = Just (Just name)
compatiblePureConstructors (Just leftName) (Just rightName)
| leftName == rightName = Just (Just leftName)
| otherwise = Nothing
comparisonMatchesConstructor :: Maybe String -> PureComparison -> Bool
comparisonMatchesConstructor constructorName (PureComparison variable _ _ _) =
case pureVariableInputCtor variable of
Nothing -> True
Just inputConstructor -> constructorName == Just inputConstructor
groupPureComparisons :: [PureComparison] -> [[PureComparison]]
groupPureComparisons [] = []
groupPureComparisons (comparison : rest) =
(comparison : sameVariable) : groupPureComparisons otherVariables
where
variable = pureComparisonVariable comparison
(sameVariable, otherVariables) =
partition ((== variable) . pureComparisonVariable) rest
pureComparisonVariable :: PureComparison -> PureVariable
pureComparisonVariable (PureComparison variable _ _ _) = variable
data TypedPureComparison r = TypedPureComparison
{ typedPureRelation :: PureRelation,
typedPureLiteral :: r,
typedPureAccepts :: r -> Bool
}
alignPureComparison ::
forall r. (Typeable r) => PureComparison -> Maybe (TypedPureComparison r)
alignPureComparison (PureComparison @other _ relation literalValue accepts) =
case eqTypeRep (typeRep @r) (typeRep @other) of
Just HRefl -> Just (TypedPureComparison relation literalValue accepts)
Nothing -> Nothing
pureComparisonGroupSatisfiable :: [PureComparison] -> Bool
pureComparisonGroupSatisfiable [] = True
pureComparisonGroupSatisfiable
(PureComparison @r _ relation literalValue accepts : rest) =
case traverse (alignPureComparison @r) rest of
Nothing -> False
Just alignedRest ->
let comparisons =
TypedPureComparison relation literalValue accepts : alignedRest
in case discoverIntegralDomain @r of
Just domain -> integralComparisonsSatisfiable domain comparisons
Nothing -> literalWitnessSatisfies comparisons
data IntegralDomain r = IntegralDomain
{ integralValue :: r -> Integer,
integralMinimum :: Maybe Integer,
integralMaximum :: Maybe Integer
}
discoverIntegralDomain :: forall r. (Typeable r) => Maybe (IntegralDomain r)
discoverIntegralDomain
| Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Integer) =
Just (IntegralDomain id Nothing Nothing)
| Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Int) =
Just (boundedIntegralDomain @Int)
| Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Word8) =
Just (boundedIntegralDomain @Word8)
| Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Word16) =
Just (boundedIntegralDomain @Word16)
| Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Word32) =
Just (boundedIntegralDomain @Word32)
| Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Word64) =
Just (boundedIntegralDomain @Word64)
| Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Int32) =
Just (boundedIntegralDomain @Int32)
| Just HRefl <- eqTypeRep (typeRep @r) (typeRep @Int64) =
Just (boundedIntegralDomain @Int64)
| otherwise = Nothing
boundedIntegralDomain ::
forall r. (Integral r, Bounded r) => IntegralDomain r
boundedIntegralDomain =
IntegralDomain
{ integralValue = toInteger,
integralMinimum = Just (toInteger (minBound @r)),
integralMaximum = Just (toInteger (maxBound @r))
}
integralComparisonsSatisfiable ::
IntegralDomain r -> [TypedPureComparison r] -> Bool
integralComparisonsSatisfiable domain comparisons =
intervalIsNonempty finalMinimum finalMaximum
where
(finalMinimum, finalMaximum) =
foldl' refine (integralMinimum domain, integralMaximum domain) comparisons
refine (minimumValue, maximumValue) comparison =
let literalValue = integralValue domain (typedPureLiteral comparison)
in case typedPureRelation comparison of
PureEq ->
( maximumMaybe minimumValue (Just literalValue),
minimumMaybe maximumValue (Just literalValue)
)
PureLt ->
(minimumValue, minimumMaybe maximumValue (Just (literalValue - 1)))
PureLe ->
(minimumValue, minimumMaybe maximumValue (Just literalValue))
PureGt ->
(maximumMaybe minimumValue (Just (literalValue + 1)), maximumValue)
PureGe ->
(maximumMaybe minimumValue (Just literalValue), maximumValue)
maximumMaybe :: Maybe Integer -> Maybe Integer -> Maybe Integer
maximumMaybe Nothing b = b
maximumMaybe a Nothing = a
maximumMaybe (Just a) (Just b) = Just (max a b)
minimumMaybe :: Maybe Integer -> Maybe Integer -> Maybe Integer
minimumMaybe Nothing b = b
minimumMaybe a Nothing = a
minimumMaybe (Just a) (Just b) = Just (min a b)
intervalIsNonempty :: Maybe Integer -> Maybe Integer -> Bool
intervalIsNonempty (Just minimumValue) (Just maximumValue) =
minimumValue <= maximumValue
intervalIsNonempty _ _ = True
literalWitnessSatisfies :: [TypedPureComparison r] -> Bool
literalWitnessSatisfies comparisons =
any satisfiesEveryComparison (map typedPureLiteral comparisons)
where
satisfiesEveryComparison candidate =
all (\comparison -> typedPureAccepts comparison candidate) comparisons
overlapConstructor :: HsPred rs ci -> HsPred rs ci -> Maybe String
overlapConstructor leftGuard rightGuard = do
PureKnown left <- Just (pureFragment leftGuard)
PureKnown right <- Just (pureFragment rightGuard)
leftConstructor <- singlePureConstructor (pureGuardConstructors left)
rightConstructor <- singlePureConstructor (pureGuardConstructors right)
compatible <- compatiblePureConstructors leftConstructor rightConstructor
compatible
-- | Internal: the determinism component of 'validateTransducer'. Like
-- 'checkTransitionDeterminismPure' but emits the richer 'NondeterministicPair'
-- directly, populating 'tvwInCtor' with the common command constructor found
-- anywhere in either conjunction spine (and 'Nothing' when neither names one).
determinismWarnings ::
(Bounded s, Enum s, Show s) =>
SymTransducer (HsPred rs ci) rs s ci co ->
[TransducerValidationWarning s]
determinismWarnings t =
[ NondeterministicPair
{ tvwSource = s,
tvwEdgeA = i,
tvwEdgeB = j,
tvwInCtor = overlapConstructor (guard e1) (guard e2),
tvwDetail = overlapDetail i j s
}
| s <- [minBound .. maxBound],
let ies = zip [(0 :: Int) ..] (edgesOut t s),
(i, e1) <- ies,
(j, e2) <- ies,
i < j,
provablyOverlap (guard e1) (guard e2)
]
-- ** Dead-edge diagnostics
-- | Options for 'checkDeadEdges'. 'deoFlagBotGuards' additionally flags edges
-- whose guard is literally 'PBot' (statically unsatisfiable), beyond edges
-- leaving unreachable vertices.
data DeadEdgeOptions = DeadEdgeOptions
{ deoFlagBotGuards :: Bool
}
deriving stock (Eq, Show)
-- | Flag both unreachable-source edges and literal-'PBot' guards.
defaultDeadEdgeOptions :: DeadEdgeOptions
defaultDeadEdgeOptions = DeadEdgeOptions {deoFlagBotGuards = True}
-- | A dead-edge warning: an edge locator and a human-readable reason it is
-- /possibly/ (never certainly) dead.
data DeadEdgeWarning s = DeadEdgeWarning
{ dewEdge :: EdgeRef s,
dewReason :: String
}
deriving stock (Eq, Show)
-- | The set of vertices reachable from 'initial' by following 'target'
-- pointers. A finite fixpoint over the 'Bounded'\/'Enum' vertex set.
reachableVertices ::
(Bounded s, Enum s, Ord s) =>
SymTransducer (HsPred rs ci) rs s ci co ->
Set.Set s
reachableVertices t = go (Set.singleton (initial t)) [initial t]
where
go seen [] = seen
go seen (s : rest) =
let succs = [target e | e <- edgesOut t s]
new = filter (`Set.notMember` seen) succs
in go (foldr Set.insert seen new) (new ++ rest)
-- | Structural, conservative dead-edge analysis. Flags an edge as possibly
-- dead when its source vertex is unreachable from 'initial' (so the edge can
-- never fire) or, optionally, when its guard is the literal 'PBot' (statically
-- unsatisfiable).
--
-- This is purely structural: it follows 'target' pointers and inspects guards
-- syntactically. It CANNOT reason about register values. A self-loop guarded
-- @available == True@ whose @available@ is set 'False' on entry is NOT catchable
-- here (its guard is not literal 'PBot' and its source vertex is reachable) —
-- only 'Keiki.Symbolic.checkDeadEdgesSym' (or a future full reachable-state
-- analysis) could. Therefore every result is labelled "possibly dead".
checkDeadEdges ::
(Bounded s, Enum s, Ord s, Show s) =>
DeadEdgeOptions ->
SymTransducer (HsPred rs ci) rs s ci co ->
[DeadEdgeWarning s]
checkDeadEdges opts t =
let reach = reachableVertices t
in [ DeadEdgeWarning (EdgeRef {edgeSource = s, edgeIndex = i}) reason
| s <- [minBound .. maxBound],
(i, e) <- zip [(0 :: Int) ..] (edgesOut t s),
reason <- deadReasons reach s e
]
where
deadReasons reach s e
| s `Set.notMember` reach =
["source vertex " <> show s <> " is unreachable from initial"]
| deoFlagBotGuards opts && isBotGuard (guard e) =
["guard is statically unsatisfiable (PBot)"]
| otherwise = []
isBotGuard PBot = True
isBotGuard _ = False