keiki 0.6.0.0 → 0.7.0.0
raw patch · 16 files changed
+3893/−1178 lines, 16 files
Files
- CHANGELOG.md +60/−0
- keiki.cabal +7/−2
- src/Keiki/Core.hs +515/−40
- src/Keiki/Internal/ProjectionDomain.hs +174/−0
- src/Keiki/Internal/SymbolicTypes.hs +12/−0
- src/Keiki/ProjectionDomain.hs +33/−0
- src/Keiki/Symbolic.hs +1808/−1121
- test/Keiki/CoreInFlightSpec.hs +61/−2
- test/Keiki/FieldProjSpec.hs +504/−1
- test/Keiki/ProjectionDomainSpec.hs +324/−0
- test/Keiki/ReplayEitherSpec.hs +66/−0
- test/Keiki/ReplayOnlySpec.hs +30/−10
- test/Keiki/RoundTrip.hs +136/−1
- test/Keiki/StepEitherSpec.hs +117/−1
- test/Keiki/SymbolicSpec.hs +44/−0
- test/Spec.hs +2/−0
CHANGELOG.md view
@@ -9,6 +9,66 @@ ## [Unreleased] +## [0.7.0.0] — 2026-08-01++### Added++- `Keiki.ProjectionDomain` provides backend-neutral exact images for nominal+ projections: non-empty finite domains, audited whole-carrier domains, and a+ validated full-string `TextPattern` algebra with literal, character set/range,+ concatenation, alternation, and bounded repetition forms.+- `ExactFieldProjection`, `exactFieldWitness`,+ `checkFieldProjectionOwner`, and `checkFieldProjectionKey` let one coherent+ projection tag declare its complete image and a checked canonical-owner+ inverse without changing existing `fieldWitness` call sites.+- `predicateTranslationReport` explains predicate-wide exactness, including+ conflicting views, direct-plus-projected reads, unsupported operations, and+ unguarded input projections. `verifyPredicateDetailed` returns translation+ strength, full solver status, and typed, checked path-local+ `ProjectionModel` values. Detailed determinism and dead-edge APIs retain the+ one solver result and `EdgeRef` attribution used by compatibility warnings.+- `StepSuccess` and `stepDetailedEither` expose the exact construction-local+ `EdgeRef`, `Live` mode, post-state, registers, and ordered output word selected+ by forward execution. `stepEither` preserves its signature and erases this+ proof-relevant success without changing failures.+- `ReplayEventSpan`, `ReplayAttribution`, `ReplaySuccess`,+ `applyEventsDetailedEither`, and `reconstituteDetailedEither` expose an+ ordered completed-edge factorization of a successful strict replay. Spans+ are zero-based and half-open, multi-event tails complete one attribution,+ live-first mode is reported exactly, and epsilon-output edges remain+ unobservable in replay. Existing replay functions share the evaluator but+ retain a nullary no-trace policy and O(1) auxiliary trace state.++### Changed++- Exact projection domains are constrained once per structured symbolic key.+ Finite domains are accepted only when every literal round-trips through its+ symbolic representation and satisfies backend bounds such as Text's+ U+2FFFF ceiling; unsupported domains emit no partial constraint.+ Satisfying model keys are checked for domain membership, inverse success, and+ getter round-trip before they are exposed. Relation-safe owners may override+ the matching structural path during `symSatExt`, whose final concrete recheck+ remains authoritative.+- `verifyPredicate` is now a compatibility projection of the detailed solver+ result and reports verified SAT/UNSAT only for predicate-global exact+ translations. `symIsBot`, determinism, and dead-edge compatibility paths use+ the same failure-aware solving kernel; only definite UNSAT counts as proof.+- **Semantic correctness fix:** `predicateTranslationExact` no longer treats a+ one-way `fieldWitness` projection as exact merely because its result carrier+ is solver-supported. Existing projection callers now receive+ `UnverifiedOpaque` from `verifyPredicate`; path-stable repeated reads and the+ conservative `symIsBot` emptiness proof remain available. The new+ documented-internals query `fieldWitnessHasExactDomain` reports the private+ evidence used by this classification and returns `False` for every released+ `fieldWitness`.+- `symSatExt` now concretely rechecks every reconstructed candidate, restoring+ the unconditional guarantee that each returned pair satisfies `models`.+ Unrealizable free projection assignments, opaque `TApp1`/`TApp2`+ assignments, and non-`Sym` equality fallbacks now return `Nothing` instead+ of a pair that fails concrete evaluation. `Nothing` remains “no concrete+ witness recovered,” not proof of unsatisfiability.++ ## [0.6.0.0] — 2026-07-31 ### Added
keiki.cabal view
@@ -1,6 +1,6 @@ cabal-version: 3.0 name: keiki-version: 0.6.0.0+version: 0.7.0.0 synopsis: Pure core for symbolic-register transducer event sourcing. description: A Haskell library for the pure core of event sourcing, workflow@@ -72,6 +72,7 @@ Keiki.NoThunks Keiki.Operators Keiki.Profunctor+ Keiki.ProjectionDomain Keiki.Render.Inspector Keiki.Render.Markdown Keiki.Render.Mermaid@@ -80,7 +81,10 @@ Keiki.Shape Keiki.Symbolic - other-modules: Keiki.Internal.SymbolicTypes+ other-modules:+ Keiki.Internal.ProjectionDomain+ Keiki.Internal.SymbolicTypes+ hs-source-dirs: src build-depends: , base ^>=4.21@@ -134,6 +138,7 @@ Keiki.OperatorsQualifiedSpec Keiki.OperatorsSpec Keiki.ProfunctorSpec+ Keiki.ProjectionDomainSpec Keiki.RecomputeVerifySpec Keiki.Render.InspectorSpec Keiki.Render.MarkdownSpec
src/Keiki/Core.hs view
@@ -61,8 +61,13 @@ Term (..), NumOp (..), FieldProjection (..),+ ExactFieldProjection (..), FieldWitness, fieldWitness,+ exactFieldWitness,+ ProjectionLawFailure (..),+ checkFieldProjectionOwner,+ checkFieldProjectionKey, ProjBase (..), -- * Input-side structural constructor (v2)@@ -142,6 +147,8 @@ -- * Pure-layer entry points (effects-boundary note) step, stepEither,+ stepDetailedEither,+ StepSuccess (..), StepFailure (..), EdgeRef (..), RejectedEdgeSummary (..),@@ -149,13 +156,18 @@ ReplayStepFailure (..), ReplayFailureReason (..), ReplayFailure (..),+ ReplayEventSpan (..),+ ReplayAttribution (..),+ ReplaySuccess (..), reconstitute, reconstituteEither,+ reconstituteDetailedEither, applyEvent, applyEventStreaming, applyEventStreamingEither, applyEvents, applyEventsEither,+ applyEventsDetailedEither, replayEvents, -- * Streaming-replay state wrapper (EP-19 M3)@@ -175,6 +187,7 @@ headRecoverabilityWarnings, inversionAmbiguityWarnings, guardImpliesInputReadWarnings,+ predicateImpliesInCtor, stateChangingEpsilonWarnings, opaqueGuardWarnings, DeterminismWarning (..),@@ -195,6 +208,9 @@ MissingInCtorFields (..), fieldProjectionPath, fieldWitnessAgrees,+ fieldWitnessHasExactDomain,+ fieldWitnessDomain,+ fieldWitnessReconstruct, fieldWitnessGet, indexPosition, )@@ -223,6 +239,10 @@ symbolicTypeSupportsNumeric, symbolicTypeSupportsOrdering, )+import Keiki.ProjectionDomain+ ( ProjectionDomain,+ memberProjectionDomain,+ ) import Numeric.Natural (Natural) import Type.Reflection (eqTypeRep, typeRep, type (:~~:) (HRefl)) @@ -351,14 +371,47 @@ projectFieldValue :: Proxy projection -> FieldOwner projection -> FieldResult projection --- | Abstract nominal token for a coherent 'FieldProjection' instance.--- Construct one with 'fieldWitness'. Its nominal role prevents changing the--- projection tag with 'coerce', and the tag's 'TypeRep' supplies symbolic--- cache identity independently of caller-controlled diagnostic strings.+-- | A projection whose declared symbolic domain is exactly the image of its+-- concrete getter and whose inverse returns a canonical owner for every+-- admitted key.+--+-- Instances must satisfy both directions of the contract:+--+-- * every well-formed owner projects to a member of+-- 'fieldProjectionDomain'; and+-- * every domain member is accepted by 'reconstructFieldOwner', whose returned+-- owner projects back to that same key.+--+-- 'checkFieldProjectionOwner' and 'checkFieldProjectionKey' make these laws+-- executable for consumer conformance suites. Keiki also checks every+-- solver-returned model before reporting it as satisfiable. An omitted real+-- owner key can still create false UNSAT, so owner-side conformance testing is+-- required whenever 'exactFieldWitness' is used.+class (FieldProjection projection) => ExactFieldProjection projection where+ fieldProjectionDomain ::+ Proxy projection -> ProjectionDomain (FieldResult projection)+ reconstructFieldOwner ::+ Proxy projection ->+ FieldResult projection ->+ Maybe (FieldOwner projection)++-- | Abstract nominal token for a coherent 'FieldProjection' instance and its+-- private symbolic-domain evidence. Construct one with 'fieldWitness'. Its+-- nominal role prevents changing the projection tag with 'coerce', and the+-- tag's 'TypeRep' supplies symbolic cache identity independently of+-- caller-controlled diagnostic strings. type role FieldWitness nominal -data FieldWitness projection = FieldWitness+data FieldDomainEvidence projection where+ FieldDomainUnconstrained :: FieldDomainEvidence projection+ FieldDomainExact ::+ (Eq (FieldResult projection)) =>+ ProjectionDomain (FieldResult projection) ->+ (FieldResult projection -> Maybe (FieldOwner projection)) ->+ FieldDomainEvidence projection +data FieldWitness projection = FieldWitness (FieldDomainEvidence projection)+ -- | Construct the abstract witness for a projection tag. Normal Haskell -- instance coherence supplies one getter per tag; generators should therefore -- reuse one canonical tag for every occurrence of the same logical field and@@ -372,8 +425,52 @@ Typeable (FieldResult projection) ) => FieldWitness projection-fieldWitness = FieldWitness+fieldWitness = FieldWitness FieldDomainUnconstrained +-- | Construct an exact witness explicitly. Merely defining an+-- 'ExactFieldProjection' instance does not change existing 'fieldWitness' call+-- sites: callers opt into the stronger contract at each use.+exactFieldWitness ::+ forall projection.+ ( ExactFieldProjection projection,+ KnownSymbol (FieldName projection),+ Typeable projection,+ Typeable (FieldOwner projection),+ Typeable (FieldResult projection),+ Eq (FieldResult projection)+ ) =>+ FieldWitness projection+exactFieldWitness =+ FieldWitness+ ( FieldDomainExact+ (fieldProjectionDomain (Proxy @projection))+ (reconstructFieldOwner (Proxy @projection))+ )++-- | Whether a witness carries evidence that the symbolic result domain is+-- exactly the image of its concrete owner getter. The released 'fieldWitness'+-- constructor records only a total one-way getter, so it always returns+-- 'False'. This read-only query does not let callers claim exactness.+fieldWitnessHasExactDomain :: FieldWitness projection -> Bool+fieldWitnessHasExactDomain (FieldWitness FieldDomainUnconstrained) = False+fieldWitnessHasExactDomain (FieldWitness FieldDomainExact {}) = True++-- | Read the declared exact domain without exposing the witness constructor.+fieldWitnessDomain ::+ FieldWitness projection ->+ Maybe (ProjectionDomain (FieldResult projection))+fieldWitnessDomain (FieldWitness FieldDomainUnconstrained) = Nothing+fieldWitnessDomain (FieldWitness (FieldDomainExact domain _)) = Just domain++-- | Apply the declared inverse. An unconstrained witness has no inverse.+fieldWitnessReconstruct ::+ FieldWitness projection ->+ FieldResult projection ->+ Maybe (FieldOwner projection)+fieldWitnessReconstruct (FieldWitness FieldDomainUnconstrained) _ = Nothing+fieldWitnessReconstruct (FieldWitness (FieldDomainExact _ reconstruct)) key =+ reconstruct key+ -- | Eliminate a 'FieldWitness' using its coherent projection instance. fieldWitnessGet :: forall projection.@@ -383,6 +480,48 @@ FieldResult projection fieldWitnessGet _ = projectFieldValue (Proxy @projection) +-- | A failed executable declaration law. No constructor stores the owner or+-- key, so the result is safe to log even when consumer values are sensitive.+data ProjectionLawFailure+ = ProjectionWitnessIsUnconstrained+ | ProjectedKeyOutsideDeclaredDomain+ | ProjectionInverseRejectedDomainKey+ | ProjectionInverseRoundTripMismatch+ deriving stock (Eq, Show)++-- | Check the owner-to-domain direction and the canonical inverse round trip+-- for one consumer-supplied owner value.+checkFieldProjectionOwner ::+ forall projection.+ (FieldProjection projection) =>+ FieldWitness projection ->+ FieldOwner projection ->+ Either ProjectionLawFailure ()+checkFieldProjectionOwner witness owner =+ () <$ checkFieldProjectionKey witness (fieldWitnessGet witness owner)++-- | Check one declared domain key and return its reconstructed owner on+-- success. Finite domains can call this helper for every member; validated+-- infinite text domains should combine it with schema-derived generators.+checkFieldProjectionKey ::+ forall projection.+ (FieldProjection projection) =>+ FieldWitness projection ->+ FieldResult projection ->+ Either ProjectionLawFailure (FieldOwner projection)+checkFieldProjectionKey (FieldWitness FieldDomainUnconstrained) _ =+ Left ProjectionWitnessIsUnconstrained+checkFieldProjectionKey+ witness@(FieldWitness (FieldDomainExact domain reconstruct))+ key+ | not (memberProjectionDomain domain key) =+ Left ProjectedKeyOutsideDeclaredDomain+ | otherwise = case reconstruct key of+ Nothing -> Left ProjectionInverseRejectedDomainKey+ Just owner+ | fieldWitnessGet witness owner == key -> Right owner+ | otherwise -> Left ProjectionInverseRoundTripMismatch+ -- | Where a structural field projection may read its owner value. Restricting -- the base to a register slot or one input-constructor field gives the -- symbolic layer a stable, typed path identity. Arbitrary computed bases are@@ -442,11 +581,14 @@ -- | A single-hop, solver-visible field projection. The coherent nominal tag -- identifies the logical getter; only the projected result needs symbolic -- support, while the consumer-owned base value does not. Concrete- -- evaluation applies the total getter. Symbolic translation creates a free- -- variable for the typed path, so agreement is intentionally one-way: a- -- concrete owner can constrain that variable to its getter result, but a- -- solver model cannot reconstruct the owner. Default validation permits- -- this node in guards and rejects it in updates or outputs.+ -- evaluation applies the total getter. Symbolic translation is /path-exact/:+ -- repeated reads of one typed path share a variable. The released witness is+ -- nevertheless /over-approximate/: that free variable may take values no+ -- concrete owner produces. It is therefore not /translation-exact/, meaning+ -- a satisfying symbolic valuation need not correspond to concrete values.+ -- A concrete owner can constrain the variable to its getter result, but a+ -- solver model cannot reconstruct the owner. Default validation permits this+ -- node in guards and rejects it in updates or outputs. TFieldProj :: ( FieldProjection projection, KnownSymbol (FieldName projection),@@ -1155,14 +1297,38 @@ 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).+-- zero-based position in @'edgesOut' t source@. It is local to one concrete+-- transducer construction, changes when outgoing declaration order changes,+-- and must not be persisted as a stable application identifier. This is the+-- canonical local edge-identity vocabulary shared with build-time diagnostics+-- (EP-56). data EdgeRef s = EdgeRef- { edgeSource :: s,+ { -- | Vertex from which the edge is declared.+ edgeSource :: s,+ -- | Zero-based position in @'edgesOut' t edgeSource@. edgeIndex :: Int } deriving stock (Eq, Show) +-- | Proof-relevant success information for one accepted forward command.+-- The 'EdgeRef' identifies the exact outgoing edge selected in this concrete+-- transducer construction; its zero-based index changes when outgoing edge+-- declaration order changes. Forward stepping considers only 'Live' edges,+-- so 'stepSuccessMode' is always 'Live'.+data StepSuccess (rs :: [Slot]) s co = StepSuccess+ { -- | Exact construction-local edge selected by the evaluator.+ stepSuccessEdge :: EdgeRef s,+ -- | Selected mode; forward success always reports 'Live'.+ stepSuccessMode :: EdgeMode,+ -- | Declared target state of the selected edge.+ stepSuccessState :: s,+ -- | Register file after applying the selected edge update.+ stepSuccessRegs :: RegFile rs,+ -- | Evaluated output word in declaration order, including @[]@ for an+ -- accepted epsilon-output edge.+ stepSuccessOutputs :: [co]+ }+ -- | 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@@ -1199,17 +1365,37 @@ | 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.+-- | Like 'stepDetailedEither', but erases exact edge attribution from a+-- success. Failures pass through unchanged; a successful 'StepSuccess' is+-- projected to the historical @(state, registers, outputs)@ triple. 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 =+stepEither t seed ci =+ case stepDetailedEither t seed ci of+ Left failure -> Left failure+ Right success ->+ Right+ ( stepSuccessState success,+ stepSuccessRegs success,+ stepSuccessOutputs success+ )++-- | Execute one forward command and return the exact selected local edge,+-- its execution mode, and the same post-state, register file, and ordered+-- output word exposed by 'stepEither'. This function is the selection and+-- evaluation authority for both entry points: erasing a success yields the+-- exact historical 'stepEither' result, and failures are identical.+stepDetailedEither ::+ (BoolAlg phi (RegFile rs, ci)) =>+ SymTransducer phi rs s ci co ->+ (s, RegFile rs) ->+ ci ->+ Either (StepFailure s) (StepSuccess rs s co)+stepDetailedEither t (s, regs) ci = case zip [0 ..] (edgesOut t s) of [] -> Left (NoOutgoingEdges s) indexed ->@@ -1231,10 +1417,17 @@ } | (i, e) <- indexed ]- [(_, e)] ->+ [(i, e)] -> let !regs' = applyEdgeUpdate e regs ci outs = [evalOut o regs ci | o <- output e]- in Right (target e, regs', outs)+ in Right+ StepSuccess+ { stepSuccessEdge = EdgeRef {edgeSource = s, edgeIndex = i},+ stepSuccessMode = Live,+ stepSuccessState = target e,+ stepSuccessRegs = regs',+ stepSuccessOutputs = outs+ } _ -> Left $ AmbiguousEdges@@ -1342,6 +1535,66 @@ } deriving stock (Eq, Show) +-- | A zero-based, half-open event interval @[start,end)@. The start is+-- included and the end is excluded, so its length is @end - start@.+data ReplayEventSpan = ReplayEventSpan+ { -- | Inclusive zero-based event index.+ replaySpanStart :: !Int,+ -- | Exclusive zero-based event index.+ replaySpanEnd :: !Int+ }+ deriving stock (Eq, Show)++-- | Attribution for one completed, non-empty edge output word in a strict+-- replay. The local 'EdgeRef', selected 'EdgeMode', state transition, and+-- event span all describe the same concrete edge application.+data ReplayAttribution s = ReplayAttribution+ { -- | Exact construction-local edge selected by replay inversion.+ replayAttributionEdge :: !(EdgeRef s),+ -- | Actual live-first phase that selected the edge.+ replayAttributionMode :: !EdgeMode,+ -- | Settled state before the edge consumed its head event.+ replayAttributionSource :: !s,+ -- | Declared target reached after the complete output word.+ replayAttributionTarget :: !s,+ -- | Half-open interval of observed events consumed by this edge.+ replayAttributionSpan :: !ReplayEventSpan,+ -- | Declared output-word length; equals the span length and is positive.+ replayAttributionEventCount :: !Int+ }+ deriving stock (Eq, Show)++-- | A settled strict-replay result plus its ordered completed-edge trace.+-- The register file deliberately prevents deriving whole-value 'Eq' or+-- 'Show'; callers can inspect the slots relevant to their aggregate.+data ReplaySuccess (rs :: [Slot]) s = ReplaySuccess+ { -- | Final settled state after the complete input log.+ replaySuccessState :: !s,+ -- | Final register file after the complete input log.+ replaySuccessRegs :: RegFile rs,+ -- | Ordered completed-edge factorization of the observed event log.+ replaySuccessTrace :: [ReplayAttribution s]+ }++-- | Private metadata retained from the head event of a multi-event edge+-- until its evaluated tail has been consumed.+data PendingAttribution s = PendingAttribution+ { pendingEdge :: !(EdgeRef s),+ pendingMode :: !EdgeMode,+ pendingSource :: !s,+ pendingTarget :: !s,+ pendingHeadIndex :: !Int,+ pendingEventCount :: !Int+ }++-- | Private cursor used only by opt-in detailed replay. Compatibility replay+-- retains its historical pair-shaped accumulator and cannot construct this+-- value, pending attribution metadata, or completed trace entries.+data ReplayTraceState s+ = ReplayTraceState+ !(Maybe (PendingAttribution s))+ ![ReplayAttribution s]+ -- | Compatibility wrapper around 'applyEventStreamingEither'. Prefer the -- structured 'Either' variant for new code; this function preserves the -- historical @Maybe@ signature and semantics.@@ -1392,10 +1645,37 @@ RegFile rs -> co -> Either (ReplayStepFailure s co) (InFlight s co, RegFile rs)-applyEventStreamingEither t (Settled s) regs co =+applyEventStreamingEither t wrapper regs co =+ applyEventKernel+ t+ wrapper+ regs+ co+ Left+ (\_ _ _ _ nextWrapper nextRegs -> Right (nextWrapper, nextRegs))+ (\_ nextWrapper nextRegs -> Right (nextWrapper, nextRegs))++-- | Apply one observed event through the single semantic replay kernel.+-- Success continuations choose only the result shape: the head continuation+-- receives the selected edge metadata needed by detailed replay, while the+-- tail continuation receives the remaining evaluated queue. This function is+-- the sole authority for inversion, live-first selection, guard checking,+-- update application, tail construction, queue equality, and step failures.+-- Inlining lets compatibility replay recover its historical pair result.+applyEventKernel ::+ (BoolAlg phi (RegFile rs, ci), Eq co) =>+ SymTransducer phi rs s ci co ->+ InFlight s co ->+ RegFile rs ->+ co ->+ (ReplayStepFailure s co -> result) ->+ (s -> Int -> Edge phi rs ci co s -> [co] -> InFlight s co -> RegFile rs -> result) ->+ ([co] -> InFlight s co -> RegFile rs -> result) ->+ result+applyEventKernel t (Settled s) regs co onFailure onHead _onTail = case matched of [] ->- Left $+ onFailure $ ReplayNoInvertingEdge s [ RejectedEdgeSummary@@ -1405,15 +1685,15 @@ } | (i, e) <- indexed ]- [(_, e, ci)] ->+ [(i, 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')+ in onHead s i e evaluatedTail wrapped regs' _ ->- Left $+ onFailure $ ReplayAmbiguousInversions s [ MatchedEdgeSummary@@ -1441,17 +1721,113 @@ Just ci <- [solveOutput o regs co], models (guard e) (regs, ci) ]-applyEventStreamingEither _ (InFlight s queue) regs co = case queue of+applyEventKernel _ (InFlight s queue) regs co onFailure _onHead onTail = case queue of q1 : rest | q1 == co ->- Right+ onTail+ rest ( case rest of [] -> Settled s- _ -> InFlight s rest,- regs+ _ -> InFlight s rest )- _ -> Left (ReplayQueueMismatch s co queue)+ regs+ _ -> onFailure (ReplayQueueMismatch s co queue)+{-# INLINE applyEventKernel #-} +-- | Detailed-result wrapper around 'applyEventKernel'. Trace metadata is+-- created only by these collecting continuations.+applyEventWithTrace ::+ (BoolAlg phi (RegFile rs, ci), Eq co) =>+ SymTransducer phi rs s ci co ->+ Int ->+ ReplayTraceState s ->+ InFlight s co ->+ RegFile rs ->+ co ->+ Either+ (ReplayStepFailure s co)+ (InFlight s co, RegFile rs, ReplayTraceState s)+applyEventWithTrace t eventIndex traceState wrapper regs co =+ applyEventKernel+ t+ wrapper+ regs+ co+ Left+ ( \source edgeNumber edge evaluatedTail nextWrapper nextRegs ->+ Right+ ( nextWrapper,+ nextRegs,+ advanceTraceAtHead+ eventIndex+ source+ edgeNumber+ edge+ (length (output edge))+ evaluatedTail+ traceState+ )+ )+ ( \remaining nextWrapper nextRegs ->+ Right+ ( nextWrapper,+ nextRegs,+ advanceTraceAtTail eventIndex remaining traceState+ )+ )+{-# INLINE applyEventWithTrace #-}++advanceTraceAtHead ::+ Int ->+ s ->+ Int ->+ Edge phi rs ci co s ->+ Int ->+ [co] ->+ ReplayTraceState s ->+ ReplayTraceState s+advanceTraceAtHead eventIndex source edgeNumber edge eventCount evaluatedTail (ReplayTraceState _ reverseTrace) =+ let pending =+ PendingAttribution+ { pendingEdge = EdgeRef {edgeSource = source, edgeIndex = edgeNumber},+ pendingMode = mode edge,+ pendingSource = source,+ pendingTarget = target edge,+ pendingHeadIndex = eventIndex,+ pendingEventCount = eventCount+ }+ in case evaluatedTail of+ [] -> ReplayTraceState Nothing (completeAttribution (eventIndex + 1) pending : reverseTrace)+ _ -> ReplayTraceState (Just pending) reverseTrace+{-# INLINE advanceTraceAtHead #-}++advanceTraceAtTail ::+ Int ->+ [co] ->+ ReplayTraceState s ->+ ReplayTraceState s+advanceTraceAtTail eventIndex remaining (ReplayTraceState pending reverseTrace) =+ case (remaining, pending) of+ ([], Just attribution) ->+ ReplayTraceState Nothing (completeAttribution (eventIndex + 1) attribution : reverseTrace)+ _ -> ReplayTraceState pending reverseTrace+{-# INLINE advanceTraceAtTail #-}++completeAttribution :: Int -> PendingAttribution s -> ReplayAttribution s+completeAttribution end pending =+ ReplayAttribution+ { replayAttributionEdge = pendingEdge pending,+ replayAttributionMode = pendingMode pending,+ replayAttributionSource = pendingSource pending,+ replayAttributionTarget = pendingTarget pending,+ replayAttributionSpan =+ ReplayEventSpan+ { replaySpanStart = pendingHeadIndex pending,+ replaySpanEnd = end+ },+ replayAttributionEventCount = pendingEventCount pending+ }+ -- | 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@@ -1467,15 +1843,36 @@ 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- }+ Left stepFailure -> Left (replayFailureAt eventIndex wrapper stepFailure) Right next -> go (eventIndex + 1) next rest +replayEventsWithTrace ::+ (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, ReplayTraceState s)+replayEventsWithTrace t = go 0 (ReplayTraceState Nothing [])+ where+ go !_ traceState (wrapper, regs) [] = Right (wrapper, regs, traceState)+ go !eventIndex traceState (wrapper, regs) (co : rest) =+ case applyEventWithTrace t eventIndex traceState wrapper regs co of+ Left stepFailure -> Left (replayFailureAt eventIndex wrapper stepFailure)+ Right (nextWrapper, nextRegs, nextTraceState) ->+ go (eventIndex + 1) nextTraceState (nextWrapper, nextRegs) rest+{-# INLINE replayEventsWithTrace #-}++replayFailureAt :: Int -> InFlight s co -> ReplayStepFailure s co -> ReplayFailure s co+replayFailureAt eventIndex wrapper stepFailure =+ ReplayFailure+ { replayFailedIndex = eventIndex,+ replayFailedState = wrapper,+ replayFailureReason = ReplayEventFailed stepFailure+ }+{-# INLINE replayFailureAt #-}+ -- | 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@@ -1496,7 +1893,9 @@ -- | Reconstitute @(state, registers)@ from the transducer's initial -- state, returning the exact event index, wrapper state, and structured--- reason when replay fails.+-- reason when replay fails. This compatibility operation uses the shared+-- event kernel through the pair-shaped replay fold and retains O(1) auxiliary+-- state. reconstituteEither :: (BoolAlg phi (RegFile rs, ci), Eq co) => SymTransducer phi rs s ci co ->@@ -1504,6 +1903,19 @@ Either (ReplayFailure s co) (s, RegFile rs) reconstituteEither t = applyEventsEither t (initial t, initialRegs t) +-- | Detailed 'reconstituteEither' from the transducer's initial seed. On+-- success the returned trace factors the complete observed event list into+-- ordered completed-edge spans; failures are exactly those of compatibility+-- replay and expose no partial trace. Erasing the trace and projecting the+-- state/register file is exactly 'reconstituteEither'.+reconstituteDetailedEither ::+ (BoolAlg phi (RegFile rs, ci), Eq co) =>+ SymTransducer phi rs s ci co ->+ [co] ->+ Either (ReplayFailure s co) (ReplaySuccess rs s)+reconstituteDetailedEither t =+ applyEventsDetailedEither 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@@ -1542,7 +1954,9 @@ -- | 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.+-- multi-event output chain still has pending events. It uses the pair-shaped+-- compatibility fold, so callers retain O(1) auxiliary state and never build+-- detailed entries. applyEventsEither :: (BoolAlg phi (RegFile rs, ci), Eq co) => SymTransducer phi rs s ci co ->@@ -1561,6 +1975,42 @@ replayFailureReason = ReplayLogTruncated pending } +-- | Replay a complete chunk from a caller-supplied settled state and return+-- its ordered completed-edge attribution. Empty input succeeds with an empty+-- trace. For non-empty successful input, spans form a contiguous partition of+-- @[0,length events)@ and adjacent source/target states form a path. A+-- multi-event edge is appended only after its final tail event is consumed;+-- epsilon-output edges are unobservable and never appear. Compatibility+-- 'applyEventsEither' uses the same event kernel through a pair-shaped fold+-- and therefore does not allocate this O(k) trace for @k@ completed edges.+-- Inversion remains live-first: matching 'Live' edges win, and 'ReplayOnly'+-- edges are considered only when the live phase has no match. On any failure,+-- the returned 'Left' is exactly the compatibility failure and exposes no+-- partial trace. Erasing a success trace yields exactly 'applyEventsEither'.+applyEventsDetailedEither ::+ (BoolAlg phi (RegFile rs, ci), Eq co) =>+ SymTransducer phi rs s ci co ->+ (s, RegFile rs) ->+ [co] ->+ Either (ReplayFailure s co) (ReplaySuccess rs s)+applyEventsDetailedEither t (s0, regs0) events =+ case replayEventsWithTrace t (Settled s0, regs0) events of+ Left failure -> Left failure+ Right (Settled s, regs, ReplayTraceState _ reverseTrace) ->+ Right+ ReplaySuccess+ { replaySuccessState = s,+ replaySuccessRegs = regs,+ replaySuccessTrace = reverse reverseTrace+ }+ Right (wrapper@(InFlight _ pending), _regs, ReplayTraceState _ _) ->+ Left+ ReplayFailure+ { replayFailedIndex = length events,+ replayFailedState = wrapper,+ replayFailureReason = ReplayLogTruncated pending+ }+ -- * Build-time analyses ---------------------------------------------------- -- | Recover the input that produced a given output by walking@@ -2474,6 +2924,31 @@ predInCtorReadNames PLeftArm = [] predInCtorReadNames PRightArm = [] predInCtorReadNames (PCmp _ a b) = termInCtorNames a ++ termInCtorNames b++-- | A sound structural implication check for constructor guards. It answers+-- whether every satisfying valuation of the predicate must match the named+-- input constructor. Conjunction needs either side to imply the constructor;+-- disjunction needs both sides. Negation and non-constructor atoms establish+-- nothing.+--+-- Unlike the crash-safety walk in 'guardImpliesInputReadWarnings', this check+-- is deliberately independent of conjunction operand order. Symbolic+-- translation can therefore classify @projection && PInCtor@ the same as+-- @PInCtor && projection@, while concrete evaluation retains its existing+-- left-to-right partiality warning.+predicateImpliesInCtor :: String -> HsPred rs ci -> Bool+predicateImpliesInCtor expected = go+ where+ go PTop = False+ go PBot = True+ go (PAnd p q) = go p || go q+ go (POr p q) = go p && go q+ go (PNot _) = False+ go (PEq _ _) = False+ go (PInCtor ic) = icName ic == expected+ go PLeftArm = False+ go PRightArm = False+ go (PCmp _ _ _) = False updateInCtorNames :: Update rs w ci -> [String] updateInCtorNames UKeep = []
+ src/Keiki/Internal/ProjectionDomain.hs view
@@ -0,0 +1,174 @@+{-# LANGUAGE GADTs #-}++-- | Internal representation shared by the backend-neutral public API and the+-- SBV compiler. The constructors stay hidden from package consumers so every+-- textual pattern is validated before it can be used as exact evidence.+module Keiki.Internal.ProjectionDomain+ ( ProjectionDomain (..),+ TextPattern (..),+ DomainConstructionError (..),+ maximumSmtCodePoint,+ finiteProjectionDomain,+ wholeProjectionDomain,+ textProjectionDomain,+ textLiteral,+ textCharSet,+ textCharRanges,+ textConcat,+ textAlternation,+ textRepeatBetween,+ memberProjectionDomain,+ matchesTextPattern,+ )+where++import Data.Foldable (traverse_)+import Data.List (stripPrefix)+import Data.List.NonEmpty (NonEmpty (..))+import Data.List.NonEmpty qualified as NE+import Data.Text (Text)+import Data.Text qualified as T+import Numeric.Natural (Natural)++-- | The exact image of a field projection. The text constructor is indexed so+-- a text pattern cannot accidentally be attached to another result carrier.+data ProjectionDomain a where+ ProjectionWhole :: ProjectionDomain a+ ProjectionFinite :: (Eq a) => NonEmpty a -> ProjectionDomain a+ ProjectionText :: TextPattern -> ProjectionDomain Text++-- | A deliberately small full-string pattern language. Every constructor has+-- both a pure interpreter and an exact SBV regular-expression translation.+data TextPattern+ = TextLiteral Text+ | TextRanges (NonEmpty (Char, Char))+ | TextConcat (NonEmpty TextPattern)+ | TextAlternation (NonEmpty TextPattern)+ | TextRepeatBetween Natural Natural TextPattern+ deriving stock (Eq, Show)++-- | Why a textual exact-domain declaration could not be constructed.+data DomainConstructionError+ = CodePointAboveSmtMaximum Char+ | ReversedCharacterRange Char Char+ | InvalidRepetitionInterval Natural Natural+ | RepetitionBoundTooLarge Natural+ deriving stock (Eq, Show)++-- | SMT-LIB strings contain code points U+0000 through U+2FFFF.+maximumSmtCodePoint :: Char+maximumSmtCodePoint = '\x2FFFF'++-- | Construct a non-empty finite domain, removing duplicates while retaining+-- the first occurrence of every value. The symbolic compiler separately+-- verifies that each retained literal round-trips through its representation+-- and satisfies backend bounds; failure omits the entire constraint and makes+-- the containing translation conservative.+finiteProjectionDomain :: (Eq a) => NonEmpty a -> ProjectionDomain a+finiteProjectionDomain = ProjectionFinite . stableNub+ where+ stableNub (x :| xs) = x :| go [x] xs+ go _ [] = []+ go seen (x : xs)+ | x `elem` seen = go seen xs+ | otherwise = x : go (x : seen) xs++-- | Declare that every value of the result carrier belongs to the image.+-- Exact witnesses may use this only when Keiki classifies the symbolic+-- representation as a whole-carrier isomorphism.+wholeProjectionDomain :: ProjectionDomain a+wholeProjectionDomain = ProjectionWhole++-- | Lift a validated full-string pattern into a 'Text' projection domain.+textProjectionDomain :: TextPattern -> ProjectionDomain Text+textProjectionDomain = ProjectionText++-- | Match one literal text value. Code points outside SMT-LIB's string domain+-- are rejected instead of making the pure and symbolic meanings disagree.+textLiteral :: Text -> Either DomainConstructionError TextPattern+textLiteral value = TextLiteral value <$ validateCharacters (T.unpack value)++-- | Match exactly one member of a non-empty character set.+textCharSet :: NonEmpty Char -> Either DomainConstructionError TextPattern+textCharSet chars = do+ validateCharacters (NE.toList chars)+ pure (TextRanges ((\c -> (c, c)) <$> stableNub chars))+ where+ stableNub (x :| xs) = x :| go [x] xs+ go _ [] = []+ go seen (x : xs)+ | x `elem` seen = go seen xs+ | otherwise = x : go (x : seen) xs++-- | Match exactly one character from one of the supplied inclusive ranges.+textCharRanges ::+ NonEmpty (Char, Char) ->+ Either DomainConstructionError TextPattern+textCharRanges ranges = do+ traverse_ validateRange ranges+ pure (TextRanges ranges)+ where+ validateRange (lower, upper)+ | lower > upper = Left (ReversedCharacterRange lower upper)+ | otherwise = validateCharacters [lower, upper]++-- | Concatenate a non-empty sequence of full-string patterns.+textConcat :: NonEmpty TextPattern -> TextPattern+textConcat = TextConcat++-- | Match any one of a non-empty sequence of full-string patterns.+textAlternation :: NonEmpty TextPattern -> TextPattern+textAlternation = TextAlternation++-- | Match a pattern between the inclusive lower and upper bounds. SBV's+-- regular-expression node stores machine 'Int' bounds, so larger naturals are+-- rejected at construction rather than truncated.+textRepeatBetween ::+ Natural ->+ Natural ->+ TextPattern ->+ Either DomainConstructionError TextPattern+textRepeatBetween lower upper textPattern+ | lower > upper = Left (InvalidRepetitionInterval lower upper)+ | lower > maxInt = Left (RepetitionBoundTooLarge lower)+ | upper > maxInt = Left (RepetitionBoundTooLarge upper)+ | otherwise = Right (TextRepeatBetween lower upper textPattern)+ where+ maxInt = fromIntegral (maxBound :: Int)++-- | Decide concrete membership in the exact domain.+memberProjectionDomain :: (Eq a) => ProjectionDomain a -> a -> Bool+memberProjectionDomain ProjectionWhole _ = True+memberProjectionDomain (ProjectionFinite values) value = value `elem` values+memberProjectionDomain (ProjectionText textPattern) value =+ matchesTextPattern textPattern value++-- | Interpret a 'TextPattern' as a complete-string matcher.+matchesTextPattern :: TextPattern -> Text -> Bool+matchesTextPattern textPattern value = any null (match textPattern (T.unpack value))+ where+ match :: TextPattern -> String -> [String]+ match (TextLiteral literal) input =+ maybe [] pure (T.unpack literal `stripPrefix` input)+ match (TextRanges ranges) input = case input of+ [] -> []+ c : rest+ | any (\(lower, upper) -> lower <= c && c <= upper) ranges -> [rest]+ | otherwise -> []+ match (TextConcat patterns) input =+ foldl (\remainders next -> remainders >>= match next) [input] patterns+ match (TextAlternation patterns) input =+ concatMap (`match` input) patterns+ match (TextRepeatBetween lower upper repeated) input =+ concatMap (\count -> applyCount count input) [lower .. upper]+ where+ applyCount 0 current = [current]+ applyCount count current =+ match repeated current >>= applyCount (count - 1)++validateCharacters :: [Char] -> Either DomainConstructionError ()+validateCharacters = traverse_ validateCharacter+ where+ validateCharacter c+ | c <= maximumSmtCodePoint = Right ()+ | otherwise = Left (CodePointAboveSmtMaximum c)
src/Keiki/Internal/SymbolicTypes.hs view
@@ -12,6 +12,7 @@ symbolicTypeSupportsEquality, symbolicTypeSupportsOrdering, symbolicTypeSupportsNumeric,+ symbolicTypeWholeCarrierExact, ) where @@ -77,3 +78,14 @@ symbolicTypeSupportsNumeric SymbolicInt64 = True symbolicTypeSupportsNumeric SymbolicInt32 = True symbolicTypeSupportsNumeric _ = False++-- | Whether the symbolic representation is an isomorphism over the complete+-- concrete carrier. This is stricter than supporting equality. In particular,+-- machine 'Int' is represented by unbounded SMT integers, 'Text' contains+-- Haskell code points above SMT-LIB's U+2FFFF maximum, and 'UTCTime' can denote+-- a leap second that POSIX conversion clamps to the following day boundary.+symbolicTypeWholeCarrierExact :: SymbolicType r -> Bool+symbolicTypeWholeCarrierExact SymbolicInt = False+symbolicTypeWholeCarrierExact SymbolicText = False+symbolicTypeWholeCarrierExact SymbolicUTCTime = False+symbolicTypeWholeCarrierExact _ = True
+ src/Keiki/ProjectionDomain.hs view
@@ -0,0 +1,33 @@+-- | Backend-neutral exact domains for nominal field projections.+--+-- A 'ProjectionDomain' is interpreted twice by Keiki: concretely through+-- 'memberProjectionDomain', and symbolically by the SBV translator. Text+-- patterns always match the complete 'Text' value. Their constructors reject+-- code points above U+2FFFF, invalid ranges, and invalid repetition bounds so+-- the two interpretations cannot silently diverge.+--+-- A domain used by 'Keiki.Core.exactFieldWitness' is a consumer-owned proof+-- declaration: every concrete owner must project into it, and every admitted+-- key must reconstruct an owner that projects back to the same key. Keiki's+-- law helpers and satisfying-model checks exercise this contract, but only a+-- consumer or generator can test that no real owner key was omitted.+module Keiki.ProjectionDomain+ ( ProjectionDomain,+ TextPattern,+ DomainConstructionError (..),+ maximumSmtCodePoint,+ finiteProjectionDomain,+ wholeProjectionDomain,+ textProjectionDomain,+ textLiteral,+ textCharSet,+ textCharRanges,+ textConcat,+ textAlternation,+ textRepeatBetween,+ memberProjectionDomain,+ matchesTextPattern,+ )+where++import Keiki.Internal.ProjectionDomain
src/Keiki/Symbolic.hs view
@@ -7,1126 +7,1813 @@ -- @BoolAlg HsPred@ instance pinned by EP-4 of MasterPlan 1's -- Outcomes & Retrospective. After EP-2 of MasterPlan 2, asking -- "are these two edge guards mutually exclusive?" is a mechanical--- question with a precise answer; the synthesis-§7 invariant that--- edge guards form an /effective/ Boolean algebra is honored at v2.------ The module re-exports everything from "Keiki.Core" so a single--- import is sufficient for callers that need both the pure and the--- symbolic surfaces. See @docs/research/sbv-boolalg-design.md@ for--- the design rationale.------ Milestones implemented in this revision (through M5 of EP-2):------ * The 'Sym' typeclass and instances for 'Bool', 'Int', 'Integer',--- 'Natural', 'Text', 'UTCTime', and the fixed-width integers 'Word8' \/--- 'Word16' \/ 'Word32' \/ 'Word64' \/ 'Int32' \/ 'Int64' (the--- last group added by EP-41 so money and count registers are--- solver-visible).--- * 'SymEnv' carrying the shared symbolic input-constructor tag and--- (since EP-42 of MasterPlan 12) an 'IORef' memo cache that shares--- one SBV variable per register slot, input field, or nominal typed field--- projection across repeated reads, so @proj #x .== proj #x@ and repeated--- projected reads are valid, not merely satisfiable.--- * 'translateTermSym' / 'translatePred' walking 'Term' / 'HsPred'--- into SBV expressions.--- * 'discoverSym' — runtime dispatch from 'Typeable' to 'Sym'--- evidence over the curated registry of supported types.--- * 'SymPred' newtype wrapper plus its 'BoolAlg' instance with--- structural 'top' / 'bot' / 'conj' / 'disj' / 'neg', a 'models'--- that re-uses the v1 'evalPred' (concrete evaluation, no solver--- call), and an 'isBot' backed by z3.--- * 'symIsBot' — pure-API wrapper around SBV's solver call (via--- 'unsafePerformIO' + NOINLINE) that 'SymPred''s 'isBot' routes--- through, so the v1 syntactic over-approximation is replaced with a--- precise symbolic answer.--- * 'symSatExt' — full witness extraction. Since EP-44 (MasterPlan 12)--- the 'Keiki.Core.Sat' method 'sat' on 'SymPred' /is/--- 'symSatExt' (via the @Sat (SymPred …)@ instance, which carries the--- 'ExtractRegFile' / 'KnownInCtors' evidence witness reconstruction--- needs); the old crashing placeholder is gone.-module Keiki.Symbolic- ( -- * Symbolic representation- Sym (..),- SymDict (..),- symLit,- symFree,- discoverSym,- SymOrdDict (..),- discoverSymOrd,- SymNumDict (..),- discoverSymNum,-- -- * Translation- SymEnv (..),- mkSymEnv,- translateTermSym,- translatePred,- constrainFieldProjection,- PredicateVerification (..),- predicateTranslationExact,- verifyPredicate,-- -- * Symbolic predicate wrapper- SymPred (..),- SymGuarded,-- -- * Solver-backed analyses- satResultIsProvablyUnsat,- symIsBot,- symSatExt,-- -- * Witness extraction- ExtractRegFile (..),- SomeInCtor (..),- KnownInCtors (..),-- -- * Single-valuedness- isSingleValuedSym,- withSymPred,-- -- * Solver-backed validation diagnostics (EP-56)- checkTransitionDeterminismSym,- checkDeadEdgesSym,-- -- * Re-exports- module Keiki.Core,- )-where--import Control.Monad (when)-import Control.Monad.IO.Class (liftIO)-import Data.Fixed (Fixed (MkFixed))-import Data.IORef (IORef, modifyIORef', newIORef, readIORef)-import Data.Int (Int32, Int64)-import Data.Kind (Type)-import Data.Map.Strict (Map)-import Data.Map.Strict qualified as Map-import Data.Proxy (Proxy (..))-import Data.SBV qualified as SBV-import Data.Text (Text)-import Data.Text qualified as T-import Data.Time (UTCTime, nominalDiffTimeToSeconds, secondsToNominalDiffTime)-import Data.Time.Clock.POSIX (posixSecondsToUTCTime, utcTimeToPOSIXSeconds)-import Data.Typeable (Typeable)-import Data.Word (Word16, Word32, Word64, Word8)-import GHC.TypeLits (KnownSymbol, symbolVal)-import Keiki.Core-import Keiki.Internal.SymbolicTypes- ( SymbolicType (..),- discoverSymbolicType,- )-import Numeric.Natural (Natural)-import System.IO.Unsafe (unsafePerformIO)-import Type.Reflection (SomeTypeRep (..), eqTypeRep, typeRep, type (:~~:) (HRefl))---- * Symbolic representation ----------------------------------------------------- | A type that has a curated representation in the SBV symbolic--- universe. The associated type 'SymRep' pins the SBV-friendly--- representation; the 'toSym' / 'fromSym' round-trip lets us push--- concrete Haskell values into the solver and pull concrete witnesses--- out of a model.------ The 'SBV.SymVal' superclass on 'SymRep' gives us 'SBV.literal',--- 'SBV.free', and 'SBV.unliteral' for free.------ 'symDefault' is consumed by 'symSatExt': when the solver's model--- has no value for a slot or input field that the predicate did not--- reference, the witness extractor falls back to 'symDefault'. Sound--- because such slots are unconstrained — any value satisfies the--- predicate.-class (SBV.SymVal (SymRep a), Typeable a) => Sym a where- type SymRep a :: Type- toSym :: a -> SymRep a- fromSym :: SymRep a -> a- symDefault :: a-- -- | Restrict a symbolic representation to values that denote a real @a@.- -- Most carriers use their whole SBV domain. Refined carriers such as- -- 'Natural' add constraints whenever Keiki allocates a symbolic variable.- constrainSymDomain :: SBV.SBV (SymRep a) -> SBV.Symbolic ()- constrainSymDomain _ = pure ()--instance Sym Bool where- type SymRep Bool = Bool- toSym = id- fromSym = id- symDefault = False--instance Sym Integer where- type SymRep Integer = Integer- toSym = id- fromSym = id- symDefault = 0---- | Arbitrary-precision non-negative integers. The representation stays an--- unbounded SMT integer, while every allocated variable is constrained to the--- actual 'Natural' domain. Numeric arithmetic is deliberately not registered:--- Haskell 'Natural' subtraction throws @Underflow@ when its mathematical result--- would be negative, while ordinary SMT integer subtraction returns that negative--- integer. Treating the operations as identical would not preserve concrete behavior.-instance Sym Natural where- type SymRep Natural = Integer- toSym = fromIntegral- fromSym = fromInteger- symDefault = 0- constrainSymDomain value = SBV.constrain (value SBV..>= 0)---- | Encoded as 'Integer'. SBV does not provide an 'SInt'-of-arbitrary---- size; using 'Integer' means machine-width 'Int' wraparound is not modeled.--- Guards whose truth depends on 'Int' overflow should use an explicit--- fixed-width type instead.-instance Sym Int where- type SymRep Int = Integer- toSym = fromIntegral- fromSym = fromIntegral- symDefault = 0---- The fixed-width instances use SBV's matching bit-vector representations, so--- their arithmetic has exactly the same modular wraparound as Haskell.---- | Money and large counts, modeled as an exact 64-bit unsigned value.-instance Sym Word64 where- type SymRep Word64 = Word64- toSym = id- fromSym = id- symDefault = 0---- | Item counts and similar 32-bit unsigned registers, modeled exactly.-instance Sym Word32 where- type SymRep Word32 = Word32- toSym = id- fromSym = id- symDefault = 0---- | Quantities, basis points, and similar 16-bit unsigned registers, modeled--- exactly.-instance Sym Word16 where- type SymRep Word16 = Word16- toSym = id- fromSym = id- symDefault = 0---- | An exact 8-bit unsigned value.-instance Sym Word8 where- type SymRep Word8 = Word8- toSym = id- fromSym = id- symDefault = 0---- | An exact 64-bit signed value.-instance Sym Int64 where- type SymRep Int64 = Int64- toSym = id- fromSym = id- symDefault = 0---- | An exact 32-bit signed value.-instance Sym Int32 where- type SymRep Int32 = Int32- toSym = id- fromSym = id- symDefault = 0---- | 'Text' is encoded as Haskell 'String' for SBV's 'SString' theory.-instance Sym Text where- type SymRep Text = String- toSym = T.unpack- fromSym = T.pack- symDefault = T.empty---- | 'UTCTime' is encoded as picoseconds since the Unix epoch. The time--- library's 'NominalDiffTime' uses a fixed-point picosecond representation, so--- this 'Integer' encoding is lossless while remaining well supported by z3.-instance Sym UTCTime where- type SymRep UTCTime = Integer- toSym t =- let MkFixed picoseconds =- nominalDiffTimeToSeconds (utcTimeToPOSIXSeconds t)- in picoseconds- fromSym picoseconds =- posixSecondsToUTCTime- (secondsToNominalDiffTime (MkFixed picoseconds))- symDefault = posixSecondsToUTCTime 0---- | Reify a 'Sym' instance so it can be passed around as a--- first-class value. Useful for runtime dispatch on 'Typeable'--- evidence.-data SymDict r where- SymDict :: (Sym r) => SymDict r---- | Try to discover a 'Sym' instance for @r@ at runtime. Returns--- @Just SymDict@ for any of the curated supported types--- ('Bool', 'Int', 'Integer', 'Natural', 'Text', 'UTCTime', and the fixed-width--- integers 'Word8' \/ 'Word16' \/ 'Word32' \/ 'Word64' \/ 'Int32' \/--- 'Int64'); 'Nothing' otherwise. The translator uses this to route--- 'PEq' over arbitrary types: a 'Sym' hit translates to '(.==)' on--- SBV terms; a miss falls back to a fresh 'SBool' (loses precision but--- stays sound).-discoverSym :: forall r. (Typeable r) => Maybe (SymDict r)-discoverSym = case discoverSymbolicType @r of- Just SymbolicBool -> Just SymDict- Just SymbolicInt -> Just SymDict- Just SymbolicInteger -> Just SymDict- Just SymbolicNatural -> Just SymDict- Just SymbolicText -> Just SymDict- Just SymbolicUTCTime -> Just SymDict- Just SymbolicWord64 -> Just SymDict- Just SymbolicWord32 -> Just SymDict- Just SymbolicWord16 -> Just SymDict- Just SymbolicWord8 -> Just SymDict- Just SymbolicInt64 -> Just SymDict- Just SymbolicInt32 -> Just SymDict- Nothing -> Nothing---- | Reify both a 'Sym' instance for @r@ and evidence that its--- 'SymRep' is symbolically orderable (an 'SBV.OrdSymbolic' instance on--- @'SBV.SBV' ('SymRep' r)@). This is exactly what 'PCmp' translation--- needs: 'Sym' to push the operands into SBV, 'OrdSymbolic' to emit a--- real @.<@ \/ @.<=@ \/ @.>@ \/ @.>=@ comparison.-data SymOrdDict r where- SymOrdDict :: (Sym r, SBV.OrdSymbolic (SBV.SBV (SymRep r))) => SymOrdDict r---- | Try to discover ordering evidence for @r@ at runtime, companion to--- 'discoverSym'. Returns @Just SymOrdDict@ for the numeric and time--- types whose 'SymRep' is an 'SBV.OrdSymbolic' 'Integer' ('Int',--- 'Integer', 'Natural', the fixed-width integers 'Word8' \/ 'Word16' \/ 'Word32'--- \/ 'Word64' \/ 'Int32' \/ 'Int64', and 'UTCTime' encoded as epoch--- seconds); 'Nothing' otherwise. 'Bool' and 'Text' are deliberately--- omitted: ordering a 'Bool' guard is not meaningful, and 'SString'--- ordering is out of scope here. A 'Nothing' makes the 'PCmp'--- translator fall back to a fresh opaque 'SBool', exactly as 'goEq'--- does for non-'Sym' operands — sound, just imprecise.-discoverSymOrd :: forall r. (Typeable r) => Maybe (SymOrdDict r)-discoverSymOrd = case discoverSymbolicType @r of- Just SymbolicInt -> Just SymOrdDict- Just SymbolicInteger -> Just SymOrdDict- Just SymbolicNatural -> Just SymOrdDict- Just SymbolicUTCTime -> Just SymOrdDict- Just SymbolicWord64 -> Just SymOrdDict- Just SymbolicWord32 -> Just SymOrdDict- Just SymbolicWord16 -> Just SymOrdDict- Just SymbolicWord8 -> Just SymOrdDict- Just SymbolicInt64 -> Just SymOrdDict- Just SymbolicInt32 -> Just SymOrdDict- Just SymbolicBool -> Nothing- Just SymbolicText -> Nothing- Nothing -> Nothing---- | Reify both a 'Sym' instance for @r@ and evidence that its 'SymRep'--- is symbolically /numeric/ (a 'Num' instance on @'SBV.SBV' ('SymRep'--- r)@). This is what 'TArith' translation needs: 'Sym' to push the--- operands into SBV, 'Num' to emit a real @+@ \/ @-@ \/ @*@ over the--- translated terms. Companion to 'discoverSym' \/ 'discoverSymOrd'--- (EP-43).-data SymNumDict r where- SymNumDict :: (Sym r, Num (SBV.SBV (SymRep r))) => SymNumDict r---- | Try to discover numeric evidence for @r@ at runtime, companion to--- 'discoverSymOrd'. Returns @Just SymNumDict@ for the numeric types--- whose 'SymRep' is the SBV-'Num' 'Integer' ('Int', 'Integer', and the--- fixed-width integers 'Word8' \/ 'Word16' \/ 'Word32' \/ 'Word64' \/--- 'Int32' \/ 'Int64'), plus 'Natural'. Natural subtraction has the explicit--- total monus meaning shared with concrete 'evalTerm'; it is translated as--- @ite (a >= b) (a - b) 0@ rather than ordinary integer subtraction.--- 'Bool', 'Text', and 'UTCTime' are omitted. A 'Nothing'--- makes the 'TArith' translator fall back to a fresh opaque variable,--- exactly as 'goEq' \/ 'goCmp' fall back for non-'Sym' operands —--- sound, just imprecise. (The 'Num' constraint on the 'TArith'--- constructor already prevents arithmetic at non-numeric types, so this--- fallback is only reachable for a numeric type intentionally left out--- of the registry.)-discoverSymNum :: forall r. (Typeable r) => Maybe (SymNumDict r)-discoverSymNum = case discoverSymbolicType @r of- Just SymbolicInt -> Just SymNumDict- Just SymbolicInteger -> Just SymNumDict- Just SymbolicNatural -> Just SymNumDict- Just SymbolicWord64 -> Just SymNumDict- Just SymbolicWord32 -> Just SymNumDict- Just SymbolicWord16 -> Just SymNumDict- Just SymbolicWord8 -> Just SymNumDict- Just SymbolicInt64 -> Just SymNumDict- Just SymbolicInt32 -> Just SymNumDict- Just SymbolicBool -> Nothing- Just SymbolicText -> Nothing- Just SymbolicUTCTime -> Nothing- Nothing -> Nothing---- | Lift a concrete value to an SBV literal of its 'SymRep'.-symLit :: forall a. (Sym a) => a -> SBV.SBV (SymRep a)-symLit = SBV.literal . toSym---- | Allocate a fresh symbolic variable of the carrier's 'SymRep'.-symFree :: forall a. (Sym a) => String -> SBV.Symbolic (SBV.SBV (SymRep a))-symFree label = do- value <- SBV.free label- constrainSymDomain @a value- pure value---- * Translation environment ----------------------------------------------------- | Translation context: shared symbolic state that must be threaded--- through a single predicate's walk so that, for example, two--- 'PInCtor' atoms over distinct constructors agree they cannot both--- be true, and two reads of the same register (or input field) share--- one solver variable.------ Three pieces of state are shared:------ * 'seInputCtor' — the symbolic input-constructor tag, so 'PInCtor'--- atoms over distinct constructors are recognized as mutually--- unsatisfiable.--- * 'seInputArm' — an independent discriminator for 'PLeftArm' and--- 'PRightArm'. It is separate from constructor names so both facts can--- be asserted by the same guard.--- * 'seVarCache' — a per-translation memo cache (EP-42) keyed by a--- structured 'SymVarKey'. Ordinary register and input reads preserve their--- historical labels; field projections use base position and nominal--- 'TypeRep' identity, never caller-controlled diagnostic strings alone.--- The first read allocates one 'SBV.free' variable and stores it; every--- later read of the same key returns the cached variable.--- This makes the solver see two reads of @#x@ as the /same/ value,--- so @proj #x .== proj #x@ is valid (not merely satisfiable). The--- 'TApp1' \/ 'TApp2' escape hatches are deliberately /not/ cached:--- they wrap opaque Haskell functions with no 'Eq', so two--- applications cannot be recognized as equal and each stays a fresh--- per-occurrence variable.-data ProjectionBaseKey- = ProjectionReg String Int- | ProjectionInp String String Int- deriving stock (Eq, Ord, Show)--data SymVarKey- = RegVar String- | InpVar String String- | ProjectionVar- ProjectionBaseKey- SomeTypeRep- SomeTypeRep- SomeTypeRep- deriving stock (Eq, Ord, Show)--data SymEnv = SymEnv- { -- | The shared symbolic input constructor tag. 'PInCtor' atoms- -- assert @seInputCtor .== literal (icName ic)@; the solver- -- recognizes that two such constraints with distinct names are- -- mutually unsatisfiable.- seInputCtor :: SBV.SBV String,- -- | @True@ denotes the outer 'Left' arm; @False@ denotes 'Right'.- seInputArm :: SBV.SBool,- -- | Memo cache: maps a deterministic variable name ("reg/\<slot\>"- -- or "inp/\<ctor\>/\<field\>") to the single SBV variable allocated- -- for it during this predicate translation. Lazily populated on- -- first read so unread slots stay unconstrained (and 'symSatExt'- -- falls back to 'symDefault' for them). Scoped to one- -- 'translatePred' walk (one 'mkSymEnv'), so variables are shared- -- /within/ a query but never leak across independent queries.- seVarCache :: IORef (Map SymVarKey SomeSBV),- -- | Next internal projection label. Projection labels are intentionally- -- generated by Keiki so arbitrary schema names never reach SBV's- -- restricted label namespace.- seProjectionOrdinal :: IORef Int- }---- | An SBV variable of some representation type, packed so the memo--- cache in 'SymEnv' can hold variables of different representation--- types under one map. 'SBV.SymVal' has a 'Typeable' superclass, so--- pattern-matching @SomeSBV (v :: SBV.SBV a)@ brings @Typeable a@ into--- scope — exactly what 'memoFree' needs to check the recovered type--- matches the requested one on a cache hit.-data SomeSBV where- SomeSBV :: (SBV.SymVal a) => SBV.SBV a -> SomeSBV---- | Allocate a fresh 'SymEnv'. Lives in 'SBV.Symbolic' because--- 'seInputCtor' is a free symbolic variable and the memo cache is an--- 'IORef' created in the underlying 'IO' ('SBV.Symbolic' is--- @SymbolicT IO@, hence 'MonadIO').-mkSymEnv :: SBV.Symbolic SymEnv-mkSymEnv = do- ctor <- SBV.free "inputCtor"- arm <- SBV.free "inputArm"- cache <- liftIO (newIORef Map.empty)- projectionOrdinal <- liftIO (newIORef 0)- pure (SymEnv ctor arm cache projectionOrdinal)---- * Translation ----------------------------------------------------------------- | Translate a 'Term rs ci r' to an SBV expression of the carrier's--- representation type. Requires 'Sym' evidence for @r@.------ The translation is /structural/ for 'TLit', 'TReg',--- 'TInpCtorField', and (since EP-43) 'TArith': a 'TArith' over a type--- whose 'SymRep' is SBV-numeric (a 'discoverSymNum' hit) emits a real--- @+@ \/ @-@ \/ @*@ over the translated operands, so a guard over a--- /computed/ value is visible to the solver. 'TApp1' and 'TApp2' wrap--- opaque Haskell functions and translate to fresh SBV variables of the--- result type — sound but imprecise; 'TArith' falls back to the same--- fresh variable only if its (numeric) operand type is absent from the--- 'discoverSymNum' registry.------ Variable naming (consumed by 'symSatExt' for witness extraction):------ * 'TReg' allocates @"reg/<slotName>"@ where @slotName@ is the--- slot's label recovered from the 'Index'\'s 'KnownSymbol'--- evidence on its leaf 'ZIdx'.--- * 'TInpCtorField' allocates--- @"inp/<icName>/<slotName>"@ — the 'InCtor''s name plus the--- field's slot label.--- * 'TFieldProj' uses a structured cache key containing the base position,--- nominal projection tag, owner type, and result type. Its actual SBV--- label is an internal @"proj/<ordinal>"@, so arbitrary schema strings--- cannot collide with or violate SBV's label syntax.--- * 'TApp1' / 'TApp2' keep their anonymous names; their values are--- not extracted as part of the witness.------ Note on repeated reads (EP-42): 'TReg', 'TInpCtorField', and--- 'TFieldProj' reads are memoized through the env's 'seVarCache'. The first--- read of a given structural key allocates one 'SBV.free' variable and caches--- it; every later read of the same key returns the cached variable. So two--- reads of the same slot (e.g.--- @proj #x .== proj #x@) share /one/ SBV variable: the solver knows--- they are equal, @x \/= x@ is unsat, and 'symSatExt''s by-name witness--- extraction is correct for ordinary repeated reads. Projection variables--- are deliberately not extracted: the solver knows the scalar result but not--- how to construct its consumer-owned base value. The 'TApp1' \/ 'TApp2'--- escape hatches stay per-occurrence fresh (their opaque functions--- have no 'Eq', so two applications cannot be recognized as equal);--- their values are not part of the extracted witness.-translateTermSym ::- forall rs ci ifs r.- (Sym r) =>- SymEnv ->- Term rs ci ifs r ->- SBV.Symbolic (SBV.SBV (SymRep r))-translateTermSym _env (TLit r) = pure (symLit r)-translateTermSym env (TReg ix) =- memoFree @r env (RegVar (indexName ix))-translateTermSym env (TInpCtorField ic ix) =- memoFree @r env (InpVar (icName ic) (indexName ix))-translateTermSym _env (TApp1 _f _t) = symFree @r "app1"-translateTermSym _env (TApp2 _f _a _b) = symFree @r "app2"-translateTermSym env (TArith op a b) = case discoverSymNum @r of- Nothing -> symFree @r "arith" -- sound opaque fallback within the carrier domain- Just SymNumDict -> do- sa <- translateTermSym env a- sb <- translateTermSym env b- case (discoverSymbolicType @r, op) of- (Just SymbolicNatural, OpSub) ->- pure (SBV.ite (sa SBV..>= sb) (sa - sb) 0)- _ -> do- let apply = case op of- OpAdd -> (+)- OpSub -> (-)- OpMul -> (*)- pure (apply sa sb)-translateTermSym env (TFieldProj (witness :: FieldWitness projection) base) =- memoFree @r env (projectionVarKey witness base)--projectionVarKey ::- forall projection rs ci ifs.- ( Typeable projection,- Typeable (FieldOwner projection),- Typeable (FieldResult projection)- ) =>- FieldWitness projection ->- ProjBase rs ci ifs (FieldOwner projection) ->- SymVarKey-projectionVarKey _ base =- ProjectionVar- ( case base of- PBReg ix -> ProjectionReg (indexName ix) (indexPosition ix)- PBInp ic ix ->- ProjectionInp (icName ic) (indexName ix) (indexPosition ix)- )- (SomeTypeRep (typeRep @projection))- (SomeTypeRep (typeRep @(FieldOwner projection)))- (SomeTypeRep (typeRep @(FieldResult projection)))---- | Bind one memoized projection variable to the concrete getter result for--- a known owner. Pass @fieldWitnessGet witness owner@ as the concrete result.--- This supplies the concrete-to-symbolic simulation used by agreement--- properties: every concrete evaluation has a matching symbolic valuation.--- The converse is intentionally not claimed. This function is not an inverse--- for 'symSatExt', and projection variables are not extracted into or checked--- for joint realizability as consumer-owned values.-constrainFieldProjection ::- forall projection rs ci ifs.- ( Typeable projection,- Typeable (FieldOwner projection),- Sym (FieldResult projection)- ) =>- SymEnv ->- FieldWitness projection ->- ProjBase rs ci ifs (FieldOwner projection) ->- FieldResult projection ->- SBV.Symbolic ()-constrainFieldProjection env witness base concrete = do- symbolic <- memoFree @(FieldResult projection) env (projectionVarKey witness base)- SBV.constrain (symbolic SBV..== symLit concrete)---- | Memoized symbolic-variable allocator (EP-42). Looks @name@ up in--- the env's 'seVarCache'. On a hit, recover the cached SBV variable —--- checking its representation type matches the requested one, which it--- always does because a deterministic name maps to exactly one type.--- On a miss, allocate a fresh 'SBV.free', store it under @name@, and--- return it. This is what makes repeated reads of the same register or--- input field share a single solver variable.-memoFree ::- forall r.- (Sym r) =>- SymEnv -> SymVarKey -> SBV.Symbolic (SBV.SBV (SymRep r))-memoFree env key = do- m <- liftIO (readIORef (seVarCache env))- case Map.lookup key m of- Just (SomeSBV (v :: SBV.SBV b)) ->- case eqTypeRep (typeRep @(SymRep r)) (typeRep @b) of- Just HRefl -> pure v- Nothing ->- -- Unreachable: a name maps to exactly one representation type.- error ("memoFree: type mismatch for cached variable " <> show key)- Nothing -> do- label <- case key of- RegVar name -> pure ("reg/" <> name)- InpVar ctorName fieldName ->- pure ("inp/" <> ctorName <> "/" <> fieldName)- ProjectionVar {} -> liftIO $ do- ordinal <- readIORef (seProjectionOrdinal env)- modifyIORef' (seProjectionOrdinal env) (+ 1)- pure ("proj/" <> show ordinal)- v <- symFree @r label- liftIO (modifyIORef' (seVarCache env) (Map.insert key (SomeSBV v)))- pure v---- | Recover the slot name an 'Index' points at by walking to the--- leaf 'ZIdx' and reading off the 'KnownSymbol' evidence the--- constructor carries. Used for deterministic SBV variable naming--- in 'translateTermSym'.-indexName :: forall rs r. Index rs r -> String-indexName (ZIdx @s) = symbolVal (Proxy @s)-indexName (SIdx i) = indexName i---- | Translate an 'HsPred' to an SBV 'SBool'. The translation is--- structural for every constructor:------ * 'PTop' / 'PBot' map to @sTrue@ / @sFalse@.--- * 'PAnd' / 'POr' / 'PNot' map to '(SBV..&&)' / '(SBV..||)' /--- 'SBV.sNot' on the recursive translations.--- * 'PEq' tries 'discoverSym' on its operand type; on a hit it--- emits '(.==)' between the two translated terms; on a miss it--- emits a fresh 'SBool' (the equality is opaque to the solver).--- * 'PInCtor' emits @seInputCtor .== literal (icName ic)@; the--- shared 'seInputCtor' makes constructor-mutual-exclusion--- decidable.--- * 'PLeftArm' / 'PRightArm' assert the independent 'seInputArm'--- discriminator.--- * 'PCmp' tries 'discoverSymOrd' on its operand type; on a hit it--- emits the matching SBV comparison ('SBV..<' \/ '.<=' \/ '.>' \/--- '.>=') between the two translated terms; on a miss it emits a--- fresh 'SBool' (the comparison is opaque to the solver).-translatePred ::- forall rs ci. SymEnv -> HsPred rs ci -> SBV.Symbolic SBV.SBool-translatePred env = go- where- go :: HsPred rs ci -> SBV.Symbolic SBV.SBool- go PTop = pure SBV.sTrue- go PBot = pure SBV.sFalse- go (PAnd p q) = (SBV..&&) <$> go p <*> go q- go (POr p q) = (SBV..||) <$> go p <*> go q- go (PNot p) = SBV.sNot <$> go p- go (PEq a b) = goEq a b- go (PInCtor ic) = pure (seInputCtor env SBV..== SBV.literal (icName ic))- go PLeftArm = pure (seInputArm env)- go PRightArm = pure (SBV.sNot (seInputArm env))- go (PCmp op a b) = goCmp op a b-- goEq ::- forall r ifs1 ifs2.- (Typeable r) =>- Term rs ci ifs1 r -> Term rs ci ifs2 r -> SBV.Symbolic SBV.SBool- goEq a b = case discoverSym @r of- Nothing -> SBV.free "neq"- Just SymDict -> do- sa <- translateTermSym env a- sb <- translateTermSym env b- pure (sa SBV..== sb)-- goCmp ::- forall r ifs1 ifs2.- (Typeable r) =>- Cmp -> Term rs ci ifs1 r -> Term rs ci ifs2 r -> SBV.Symbolic SBV.SBool- goCmp op a b = case discoverSymOrd @r of- Nothing -> SBV.free "cmp" -- sound opaque fallback- Just SymOrdDict -> do- sa <- translateTermSym env a- sb <- translateTermSym env b- let apply = case op of- CmpLt -> (SBV..<)- CmpLe -> (SBV..<=)- CmpGt -> (SBV..>)- CmpGe -> (SBV..>=)- pure (apply sa sb)---- | A conservative answer from 'verifyPredicate'. The two @Verified@--- constructors mean every predicate node translated structurally and the--- solver returned a definite result. Opaque Haskell applications, unsupported--- carrier dictionaries, solver timeouts or @Unknown@, and solver failures are--- represented explicitly and must not be treated as successful verification.-data PredicateVerification- = VerifiedSatisfiable- | VerifiedUnsatisfiable- | UnverifiedOpaque- | UnverifiedSolverUnknown String- | UnverifiedSolverFailure String- deriving stock (Eq, Show)---- | Whether every node in a predicate has an exact structural symbolic--- translation. This is stricter than merely being accepted by 'translatePred',--- whose compatibility fallback intentionally replaces unsupported pieces with--- fresh variables.-predicateTranslationExact :: forall rs ci. HsPred rs ci -> Bool-predicateTranslationExact = goPred- where- goPred :: HsPred rs ci -> Bool- goPred PTop = True- goPred PBot = True- goPred (PAnd p q) = goPred p && goPred q- goPred (POr p q) = goPred p && goPred q- goPred (PNot p) = goPred p- goPred (PEq a b) = exactEquality a b- goPred (PInCtor _) = True- goPred PLeftArm = True- goPred PRightArm = True- goPred (PCmp _ a b) = exactOrdering a b-- exactEquality ::- forall r ifs1 ifs2.- (Typeable r) =>- Term rs ci ifs1 r ->- Term rs ci ifs2 r ->- Bool- exactEquality a b = case discoverSym @r of- Nothing -> False- Just SymDict -> exactTerm a && exactTerm b-- exactOrdering ::- forall r ifs1 ifs2.- (Typeable r) =>- Term rs ci ifs1 r ->- Term rs ci ifs2 r ->- Bool- exactOrdering a b = case discoverSymOrd @r of- Nothing -> False- Just SymOrdDict -> exactTerm a && exactTerm b-- exactTerm :: forall ifs r. (Sym r) => Term rs ci ifs r -> Bool- exactTerm (TLit _) = True- exactTerm (TReg _) = True- exactTerm (TInpCtorField _ _) = True- exactTerm (TApp1 _ _) = False- exactTerm (TApp2 _ _ _) = False- exactTerm (TArith _ a b) = case discoverSymNum @r of- Nothing -> False- Just SymNumDict -> exactTerm a && exactTerm b- exactTerm TFieldProj {} = True---- | Translate and solve one predicate without collapsing uncertainty into a--- Boolean. Exact translations produce a verified satisfiable or unsatisfiable--- answer. Any opaque fallback is rejected before invoking the solver, and--- every non-definite solver result remains visibly unverified.-verifyPredicate :: HsPred rs ci -> IO PredicateVerification-verifyPredicate predicate- | not (predicateTranslationExact predicate) = pure UnverifiedOpaque- | otherwise = do- result <- SBV.sat $ do- env <- mkSymEnv- translatePred env predicate- pure $ case result of- SBV.SatResult status -> case status of- SBV.Satisfiable {} -> VerifiedSatisfiable- SBV.Unsatisfiable {} -> VerifiedUnsatisfiable- SBV.Unknown {} -> UnverifiedSolverUnknown "solver returned Unknown"- SBV.ProofError {} -> UnverifiedSolverFailure "solver returned ProofError"- SBV.DeltaSat {} -> UnverifiedSolverUnknown "solver returned DeltaSat"- SBV.SatExtField {} -> UnverifiedSolverUnknown "solver returned SatExtField"---- * Symbolic predicate wrapper -------------------------------------------------- | A newtype wrapper over 'HsPred' that selects the v2 'BoolAlg'--- instance (with SBV-backed analyses) instead of the v1 syntactic--- one. The v1 'BoolAlg HsPred' instance in "Keiki.Core" stays--- unchanged for back-compat; consumers that want symbolic answers--- wrap with 'SymPred'.------ The 'SymPred' constructor is exported so callers can lift--- @userReg@-style transducers via 'fmap'-like adapters; M6 of EP-2--- ships 'withSymPred' which re-tags every edge guard.-newtype SymPred (rs :: [Slot]) (ci :: Type) = SymPred {unSymPred :: HsPred rs ci}---- | A 'SymTransducer' whose guard carrier is the SBV-backed 'SymPred'.--- The symbolic analogue of 'Keiki.Core.Guarded'.-type SymGuarded rs s ci co = SymTransducer (SymPred rs ci) rs s ci co---- | The v2 'BoolAlg' instance. The five structural methods compose--- 'HsPred' constructors. 'models' delegates to the v1 'evalPred'--- (concrete evaluation, no solver call). 'isBot' routes through--- 'symIsBot', which dispatches to an external z3 process via SBV and--- 'unsafePerformIO'. Consequently, evaluating 'isBot' throws an exception from--- otherwise pure code when z3 is not on @PATH@; the repository's nix development--- shell supplies it. Witness extraction--- ('Keiki.Core.sat') lives in the separate 'Sat' instance below, which--- carries the 'ExtractRegFile' / 'KnownInCtors' evidence it needs; this--- instance is deliberately /unconstrained/ so the witness-free analyses--- ('isSingleValuedSym') keep type-checking on register-file-existential--- carriers and on @ci@ types with no 'KnownInCtors'.-instance BoolAlg (SymPred rs ci) (RegFile rs, ci) where- top = SymPred PTop- bot = SymPred PBot- conj (SymPred p) (SymPred q) = SymPred (PAnd p q)- disj (SymPred p) (SymPred q) = SymPred (POr p q)- neg (SymPred p) = SymPred (PNot p)- models (SymPred p) (regs, ci) = evalPred p regs ci- isBot (SymPred p) = symIsBot p---- | Witness extraction for the SBV-backed carrier (EP-44, MasterPlan--- 12). @'sat' (SymPred p)@ returns the same real, forceable witness as--- 'symSatExt' — a concrete @(RegFile rs, ci)@ reconstructed from the--- solver model. The constraints @ExtractRegFile rs@ / @KnownInCtors ci@--- live here (not on 'BoolAlg') so only witness extraction pays for them.-instance- (ExtractRegFile rs, KnownInCtors ci) =>- Sat (SymPred rs ci) (RegFile rs, ci)- where- sat (SymPred p) = symSatExt p---- * Solver-backed analyses ------------------------------------------------------ | Interpret a solver result for emptiness ('Keiki.Core.isBot') purposes.--- Returns 'True' only for a definite 'SBV.Unsatisfiable' result. Every other--- result means "not provably empty": that includes 'SBV.Satisfiable',--- 'SBV.Unknown' (for example, a timeout or an incomplete string-theory query),--- 'SBV.ProofError', 'SBV.DeltaSat', and 'SBV.SatExtField'. This is the--- conservative direction for callers that use emptiness to bless two guards as--- disjoint or to diagnose an edge as dead.-satResultIsProvablyUnsat :: SBV.SatResult -> Bool-satResultIsProvablyUnsat (SBV.SatResult result) = case result of- SBV.Unsatisfiable {} -> True- SBV.Satisfiable {} -> False- SBV.DeltaSat {} -> False- SBV.SatExtField {} -> False- SBV.Unknown {} -> False- SBV.ProofError {} -> False---- | Symbolic emptiness check. Translates the predicate to an SBV expression and--- asks z3 whether it is definitely unsatisfiable. A 'True' result proves the--- predicate is bot; 'False' means either satisfiable or that the solver gave up.--- The latter can occur for 'Text' guards translated through z3's string theory.--- This conservative failure direction may surface an overlap warning but never--- blesses an uncertain pair as disjoint. Requires z3 on @PATH@; because the call--- is wrapped in 'unsafePerformIO', a missing solver throws from pure code. The--- wrapper is justified because each query is deterministic for a given predicate--- and side-effect-free outside the solver process.-{-# NOINLINE symIsBot #-}-symIsBot :: HsPred rs ci -> Bool-symIsBot p = unsafePerformIO $ do- res <- SBV.sat $ do- env <- mkSymEnv- translatePred env p- pure (satResultIsProvablyUnsat res)---- * Single-valuedness ---------------------------------------------------------- | A transducer is /single-valued/ when, at every reachable--- vertex, at most one outgoing edge's guard is satisfied for any--- given input. The check decomposes into "for every vertex @s@, for--- every distinct pair @(e1, e2)@ of outgoing edges, is the--- conjunction of their guards 'isBot'?". The function is--- 'BoolAlg'-polymorphic; precision depends on the chosen 'isBot'--- implementation. With 'SymPred', this is the v2 SBV-backed--- decision; with the v1 'HsPred' instance the answer is the v1--- syntactic over-approximation. A solver 'SBV.Unknown' is conservatively treated--- as a possibly overlapping pair, so this function returns 'False'.-isSingleValuedSym ::- forall phi rs s ci co.- (BoolAlg phi (RegFile rs, ci), Bounded s, Enum s) =>- SymTransducer phi rs s ci co ->- Bool-isSingleValuedSym t = all vertexSV [minBound .. maxBound]- where- vertexSV :: s -> Bool- vertexSV s =- let es = edgesOut t s- ies = zip [(0 :: Int) ..] es- -- Only 'Live' edges compete in forward dispatch; guard- -- overlap with or between 'ReplayOnly' edges cannot cause- -- forward ambiguity.- pairs =- [ (e1, e2)- | (i, e1) <- ies,- (j, e2) <- ies,- i < j,- mode e1 == Live,- mode e2 == Live- ]- in all (\(e1, e2) -> isBot (guard e1 `conj` guard e2)) pairs---- | Lift a transducer's edges from the v1 'HsPred' guard carrier to--- the v2 'SymPred' carrier so 'isSingleValuedSym' (or any other--- 'BoolAlg'-polymorphic analysis) sees the SBV-backed instance.--- The control graph and update / output terms are unchanged.-withSymPred ::- SymTransducer (HsPred rs ci) rs s ci co ->- SymTransducer (SymPred rs ci) rs s ci co-withSymPred t =- SymTransducer- { edgesOut = \s -> map liftEdge (edgesOut t s),- initial = initial t,- initialRegs = initialRegs t,- isFinal = isFinal t- }- where- liftEdge ::- Edge (HsPred rs ci) rs ci co s ->- Edge (SymPred rs ci) rs ci co s- liftEdge e@Edge {update = u} =- Edge- { guard = SymPred (guard e),- update = u,- output = output e,- target = target e,- mode = mode e- }---- * Solver-backed validation diagnostics (EP-56) ------------------------------- | Solver-backed determinism diagnostic. Lifts the transducer with--- 'withSymPred' and runs the 'BoolAlg'-polymorphic 'checkTransitionDeterminism'--- at the 'SymPred' carrier, whose 'isBot' is the exact z3 decision. Unlike the--- pure path in 'validateTransducer', this catches register-value-dependent and--- other non-syntactic overlaps. A solver 'SBV.Unknown' conservatively produces a--- warning rather than blessing the pair as disjoint. Requires z3 on @PATH@.-checkTransitionDeterminismSym ::- (Bounded s, Enum s, Show s) =>- SymTransducer (HsPred rs ci) rs s ci co ->- [DeterminismWarning s]-checkTransitionDeterminismSym = checkTransitionDeterminism . withSymPred---- | Symbolic dead-edge sketch. Flags edges whose guard is unsatisfiable--- /in isolation/ (via 'symIsBot'), which the structural 'checkDeadEdges'--- misses unless the guard is literally 'PBot' (e.g. @amount > 0 && amount < 0@).--- It does NOT compute the register configurations reachable at each vertex, so--- it still cannot catch the FieldResource case (a guard satisfiable in--- isolation but never under the registers reachable there); that needs a full--- reachable-state fixpoint and is left as future work. A solver 'SBV.Unknown'--- does not diagnose an edge as dead, because it is not proof of unsatisfiability.--- Requires z3 on @PATH@.-checkDeadEdgesSym ::- (Bounded s, Enum s) =>- SymTransducer (HsPred rs ci) rs s ci co ->- [DeadEdgeWarning s]-checkDeadEdgesSym t =- [ DeadEdgeWarning- (EdgeRef {edgeSource = s, edgeIndex = i})- "guard is unsatisfiable in isolation (symbolic)"- | s <- [minBound .. maxBound],- (i, e) <- zip [(0 :: Int) ..] (edgesOut t s),- symIsBot (guard e)- ]---- * Witness extraction --------------------------------------------------------- | Materialize a 'RegFile' from a name-keyed reader. The reader's--- input is a slot name (the same string 'translateTermSym' allocates--- under @"reg/" <> slotName@); the reader's output is the slot's--- value, of any 'Sym'-supported type. The reader is total: callers--- (notably 'symSatExt') fall back to 'symDefault' for slots whose--- names the SBV model did not bind.------ Two instances cover the slot list:------ * @ExtractRegFile \'[]@ — return 'RNil' regardless of the reader.--- * @ExtractRegFile (\'(s, t) ': rs)@ — read the head slot's name--- via the reader, recurse on the tail, build an 'RCons'.------ The instance constraints @KnownSymbol s@ and @Sym t@ make this--- automatic for any concrete slot list whose value types are in the--- curated 'Sym' registry ('Bool', 'Int', 'Integer', 'Natural', 'Text',--- 'UTCTime'). User Registration's 'UserRegRegs' shape qualifies--- without further user code.-class ExtractRegFile (rs :: [Slot]) where- extractRegFile :: (forall r. (Sym r) => String -> r) -> RegFile rs--instance ExtractRegFile '[] where- extractRegFile _ = RNil--instance- ( KnownSymbol s,- Sym t,- ExtractRegFile rs- ) =>- ExtractRegFile ('(s, t) ': rs)- where- extractRegFile reader =- RCons- (Proxy @s)- (reader @t (symbolVal (Proxy @s)))- (extractRegFile @rs reader)---- | Existential wrapper around an 'InCtor' that hides the--- input-field slot list. The hidden 'ExtractRegFile' constraint lets--- 'symSatExt' rebuild the input register file once the constructor--- tag is known from the SBV model.-data SomeInCtor (ci :: Type) where- SomeInCtor :: (ExtractRegFile ifs) => InCtor ci ifs -> SomeInCtor ci---- | A 'ci' type whose set of 'InCtor's is statically known. Each--- 'SomeInCtor' bag entry pairs an 'InCtor' value with the--- 'ExtractRegFile' evidence its field-list shape requires.------ For the User Registration aggregate, the instance is a five-line--- list pairing the existing @inCtorStart@ … @inCtorContinue@--- declarations:------ > instance KnownInCtors UserCmd where--- > allInCtors =--- > [ SomeInCtor inCtorStart--- > , SomeInCtor inCtorConfirm--- > , SomeInCtor inCtorResend--- > , SomeInCtor inCtorGdpr--- > , SomeInCtor inCtorContinue--- > ]------ Future work: a Generic-derived default via 'GHasCtor' so users--- get the instance for free with @deriving (Generic)@. Out of scope--- for EP-9 because the explicit list is already one line per--- constructor.-class KnownInCtors ci where- allInCtors :: [SomeInCtor ci]---- | The single zero-field constructor of @()@ — a transducer whose--- command alphabet carries no information. Lets 'symSatExt' (and hence--- 'Keiki.Core.sat') reconstruct a @()@ witness for predicates over--- @SymPred rs ()@.-inCtorUnit :: InCtor () '[]-inCtorUnit =- InCtor- { icName = "()",- icMatch = \() -> Just RNil,- icBuild = \RNil -> ()- }---- | @()@ has one constructor; its 'allInCtors' is the singleton--- 'inCtorUnit'. Added by EP-44 so @sat@ over a no-command carrier--- (@SymPred '[] ()@) yields a real @(RNil, ())@ witness.-instance KnownInCtors () where- allInCtors = [SomeInCtor inCtorUnit]---- * symSatExt ------------------------------------------------------------------- | Symbolic satisfiability with full witness extraction. On a--- satisfiable predicate, returns @Just (regs, cmd)@ where @regs@--- and @cmd@ are concrete values reconstructed from the SBV model.--- @models p (regs, cmd) == True@ holds for the returned witness,--- modulo one known limitation:------ * /Escape-hatch terms/ ('TApp1', 'TApp2', and 'PEq' over a--- non-'Sym' operand type, the @neq@ fallback in 'goEq').--- These translate to fresh anonymous SBV variables; their values--- are not extracted, and two occurrences of the same opaque--- application do not share a variable (opaque functions have no--- 'Eq'). The witness reflects only the slots and input-fields the--- predicate references through 'TReg' and 'TInpCtorField'.------ /Repeated reads/ of the same register or input field are handled--- correctly: since EP-42 'translateTermSym' memoizes 'TReg' \/--- 'TInpCtorField' reads (see 'SymEnv'\'s 'seVarCache'), so two reads of--- @#x@ share one SBV variable and the by-name witness extraction--- satisfies @proj #x .== proj #x@-style structural equality.------ The model's input-constructor tag is confined to the known--- constructor domain (@KnownInCtors ci@), so a predicate without a--- 'PInCtor' atom still reconstructs a real command (the first/only--- constructor) rather than failing to match an arbitrary solver string.------ 'symSatExt' is /pure/ via 'unsafePerformIO' on the SBV solver--- call (deterministic for a given predicate, side-effect-free--- outside the solver process). Since EP-44 it /is/ the implementation--- of the 'Keiki.Core.Sat' method 'sat' on 'SymPred' (via the--- @Sat (SymPred …)@ instance, which carries the 'ExtractRegFile' /--- 'KnownInCtors' evidence the witness-free 'BoolAlg' class cannot). A 'Nothing'--- result means only that no model was found: the predicate may be unsatisfiable,--- or the solver may have returned 'SBV.Unknown'. Callers must not treat--- 'Nothing' as a proof of emptiness; 'symIsBot' returns 'True' only for that proof.-{-# NOINLINE symSatExt #-}-symSatExt ::- forall rs ci.- ( ExtractRegFile rs,- KnownInCtors ci- ) =>- HsPred rs ci -> Maybe (RegFile rs, ci)-symSatExt p = unsafePerformIO $ do- res <- SBV.sat $ do- env <- mkSymEnv- b <- translatePred env p- -- Constrain the shared input-constructor tag to the known- -- constructor domain so the solver cannot pick a string matching no- -- constructor. Predicates without a 'PInCtor' atom leave the tag- -- free, so without this the solver could choose an unknown tag,- -- 'pickCi' would find no match, and a satisfiable predicate would- -- (wrongly) yield no witness. Confining the tag to the real finite- -- domain keeps the reconstructed witness sound (it always satisfies- -- 'models') and improves completeness on @PNot (PInCtor …)@ guards.- let ctorNames = [icName ic | SomeInCtor ic <- allInCtors @ci]- when (not (null ctorNames)) $- SBV.constrain $- SBV.sOr [seInputCtor env SBV..== SBV.literal n | n <- ctorNames]- pure b- pure $- if SBV.modelExists res- then do- ctorTag <- SBV.getModelValue "inputCtor" res- let regReader :: forall r. (Sym r) => String -> r- regReader name = readModel res ("reg/" <> name)- let regs = extractRegFile @rs regReader- ci <-- pickCi @ci- ctorTag- ( \icN fieldName ->- readModel- res- ("inp/" <> icN <> "/" <> fieldName)- )- pure (regs, ci)- else Nothing---- | Look up @name@ in @res@'s SBV model; on a hit return @fromSym@--- of the model value, on a miss return @symDefault@. Used by--- 'symSatExt' to convert SBV's typed model lookups into Haskell--- values for any 'Sym'-supported slot type.-readModel :: forall r. (Sym r) => SBV.SatResult -> String -> r-readModel res name =- case SBV.getModelValue name res :: Maybe (SymRep r) of- Just rep -> fromSym rep- Nothing -> symDefault---- | Walk the 'allInCtors' list, find the entry whose 'icName'--- matches the model's input-constructor tag, then 'extractRegFile'--- over the matched 'InCtor''s field list and call 'icBuild' to--- assemble a @ci@. Returns 'Nothing' when no entry matches the tag--- — this is the case when the predicate over-allocated the--- @"inputCtor"@ slot (the solver picked a string that isn't any--- known constructor name, which can happen if the predicate--- doesn't include any 'PInCtor' atom).-pickCi ::- forall ci.- (KnownInCtors ci) =>- String ->- (forall r. (Sym r) => String -> String -> r) ->- Maybe ci-pickCi tag readField = go (allInCtors @ci)- where- go [] = Nothing- go (SomeInCtor ic@InCtor {} : rest)- | icName ic == tag =- let regs = extractRegFile (readField (icName ic))+-- question with a precise answer for exact translations. Conservative+-- translations remain one-sided and carry explicit strength evidence.+--+-- The module re-exports everything from "Keiki.Core" so a single+-- import is sufficient for callers that need both the pure and the+-- symbolic surfaces. See @docs/research/sbv-boolalg-design.md@ for+-- the design rationale.+--+-- Milestones implemented in this revision (through M5 of EP-2):+--+-- * The 'Sym' typeclass and instances for 'Bool', 'Int', 'Integer',+-- 'Natural', 'Text', 'UTCTime', and the fixed-width integers 'Word8' \/+-- 'Word16' \/ 'Word32' \/ 'Word64' \/ 'Int32' \/ 'Int64' (the+-- last group added by EP-41 so money and count registers are+-- solver-visible).+-- * 'SymEnv' carrying the shared symbolic input-constructor tag and+-- (since EP-42 of MasterPlan 12) an 'IORef' memo cache that shares+-- one SBV variable per register slot, input field, or nominal typed field+-- projection across repeated reads, so @proj #x .== proj #x@ and repeated+-- projected reads are valid, not merely satisfiable.+-- * 'translateTermSym' / 'translatePred' walking 'Term' / 'HsPred'+-- into SBV expressions.+-- * 'discoverSym' — runtime dispatch from 'Typeable' to 'Sym'+-- evidence over the curated registry of supported types.+-- * 'SymPred' newtype wrapper plus its 'BoolAlg' instance with+-- structural 'top' / 'bot' / 'conj' / 'disj' / 'neg', a 'models'+-- that re-uses the v1 'evalPred' (concrete evaluation, no solver+-- call), and an 'isBot' backed by z3.+-- * 'symIsBot' — conservative pure-API wrapper around SBV's solver call+-- (via 'unsafePerformIO' + NOINLINE) that 'SymPred''s 'isBot' routes+-- through. Solver failures and non-UNSAT statuses return 'False'.+-- * 'symSatExt' — full witness extraction. Since EP-44 (MasterPlan 12)+-- the 'Keiki.Core.Sat' method 'sat' on 'SymPred' /is/+-- 'symSatExt' (via the @Sat (SymPred …)@ instance, which carries the+-- 'ExtractRegFile' / 'KnownInCtors' evidence witness reconstruction+-- needs); the old crashing placeholder is gone.+module Keiki.Symbolic+ ( -- * Symbolic representation+ Sym (..),+ SymDict (..),+ symLit,+ symFree,+ discoverSym,+ SymOrdDict (..),+ discoverSymOrd,+ SymNumDict (..),+ discoverSymNum,+ symbolicWholeCarrierExact,++ -- * Translation+ SymEnv (..),+ mkSymEnv,+ translateTermSym,+ translatePred,+ constrainFieldProjection,+ ProjectionBaseKind (..),+ ProjectionBaseDescriptor (..),+ ProjectionDescriptor (..),+ TranslationStrength (..),+ TranslationIssue (..),+ PredicateVerification (..),+ ProjectionModel (..),+ projectionModelKeyAs,+ projectionModelOwnerAs,+ PredicateVerificationDetail (..),+ predicateTranslationReport,+ predicateTranslationExact,+ verifyPredicateDetailed,+ verifyPredicate,++ -- * Symbolic predicate wrapper+ SymPred (..),+ SymGuarded,++ -- * Solver-backed analyses+ satResultIsProvablyUnsat,+ symIsBot,+ symSatExt,++ -- * Witness extraction+ ExtractRegFile (..),+ SomeInCtor (..),+ KnownInCtors (..),++ -- * Single-valuedness+ isSingleValuedSym,+ withSymPred,++ -- * Solver-backed validation diagnostics (EP-56)+ DeterminismAnalysisDetail (..),+ checkTransitionDeterminismSymDetailed,+ checkTransitionDeterminismSym,+ DeadEdgeAnalysisDetail (..),+ checkDeadEdgesSymDetailed,+ checkDeadEdgesSym,++ -- * Re-exports+ module Keiki.Core,+ module Keiki.ProjectionDomain,+ )+where++import Control.Exception (ErrorCall, SomeException, displayException, evaluate, try)+import Control.Monad (forM, when)+import Control.Monad.IO.Class (liftIO)+import Data.Dynamic (Dynamic, fromDynamic, toDyn)+import Data.Fixed (Fixed (MkFixed))+import Data.Foldable (toList)+import Data.IORef (IORef, modifyIORef', newIORef, readIORef, writeIORef)+import Data.Int (Int32, Int64)+import Data.Kind (Type)+import Data.List.NonEmpty (NonEmpty (..))+import Data.Map.Strict (Map)+import Data.Map.Strict qualified as Map+import Data.Maybe (listToMaybe)+import Data.Proxy (Proxy (..))+import Data.SBV qualified as SBV+import Data.SBV.RegExp qualified as SBV.RegExp+import Data.Set (Set)+import Data.Set qualified as Set+import Data.Text (Text)+import Data.Text qualified as T+import Data.Time (UTCTime, nominalDiffTimeToSeconds, secondsToNominalDiffTime)+import Data.Time.Clock.POSIX (posixSecondsToUTCTime, utcTimeToPOSIXSeconds)+import Data.Typeable (Typeable)+import Data.Word (Word16, Word32, Word64, Word8)+import GHC.TypeLits (KnownSymbol, symbolVal)+import Keiki.Core+import Keiki.Internal.ProjectionDomain+ ( ProjectionDomain (..),+ TextPattern (..),+ )+import Keiki.Internal.SymbolicTypes+ ( SymbolicType (..),+ discoverSymbolicType,+ symbolicTypeWholeCarrierExact,+ )+import Keiki.ProjectionDomain+import Numeric.Natural (Natural)+import System.IO.Unsafe (unsafePerformIO)+import Type.Reflection (SomeTypeRep (..), eqTypeRep, typeRep, type (:~~:) (HRefl))++-- * Symbolic representation -------------------------------------------------++-- | A type that has a curated representation in the SBV symbolic+-- universe. The associated type 'SymRep' pins the SBV-friendly+-- representation; the 'toSym' / 'fromSym' round-trip lets us push+-- concrete Haskell values into the solver and pull concrete witnesses+-- out of a model.+--+-- The 'SBV.SymVal' superclass on 'SymRep' gives us 'SBV.literal',+-- 'SBV.free', and 'SBV.unliteral' for free.+--+-- 'symDefault' is consumed by 'symSatExt': when the solver's model+-- has no value for a slot or input field that the predicate did not+-- reference, the witness extractor falls back to 'symDefault'. Sound+-- because such slots are unconstrained — any value satisfies the+-- predicate.+class (SBV.SymVal (SymRep a), Typeable a) => Sym a where+ type SymRep a :: Type+ toSym :: a -> SymRep a+ fromSym :: SymRep a -> a+ symDefault :: a++ -- | Restrict a symbolic representation to values that denote a real @a@.+ -- Most carriers use their whole SBV domain. Refined carriers such as+ -- 'Natural' add constraints whenever Keiki allocates a symbolic variable.+ constrainSymDomain :: SBV.SBV (SymRep a) -> SBV.Symbolic ()+ constrainSymDomain _ = pure ()++instance Sym Bool where+ type SymRep Bool = Bool+ toSym = id+ fromSym = id+ symDefault = False++instance Sym Integer where+ type SymRep Integer = Integer+ toSym = id+ fromSym = id+ symDefault = 0++-- | Arbitrary-precision non-negative integers. The representation stays an+-- unbounded SMT integer, while every allocated variable is constrained to the+-- actual 'Natural' domain. Numeric arithmetic is deliberately not registered:+-- Haskell 'Natural' subtraction throws @Underflow@ when its mathematical result+-- would be negative, while ordinary SMT integer subtraction returns that negative+-- integer. Treating the operations as identical would not preserve concrete behavior.+instance Sym Natural where+ type SymRep Natural = Integer+ toSym = fromIntegral+ fromSym = fromInteger+ symDefault = 0+ constrainSymDomain value = SBV.constrain (value SBV..>= 0)++-- | Encoded as 'Integer'. SBV does not provide an 'SInt'-of-arbitrary-+-- size; using 'Integer' means machine-width 'Int' wraparound is not modeled.+-- Guards whose truth depends on 'Int' overflow should use an explicit+-- fixed-width type instead.+instance Sym Int where+ type SymRep Int = Integer+ toSym = fromIntegral+ fromSym = fromIntegral+ symDefault = 0++-- The fixed-width instances use SBV's matching bit-vector representations, so+-- their arithmetic has exactly the same modular wraparound as Haskell.++-- | Money and large counts, modeled as an exact 64-bit unsigned value.+instance Sym Word64 where+ type SymRep Word64 = Word64+ toSym = id+ fromSym = id+ symDefault = 0++-- | Item counts and similar 32-bit unsigned registers, modeled exactly.+instance Sym Word32 where+ type SymRep Word32 = Word32+ toSym = id+ fromSym = id+ symDefault = 0++-- | Quantities, basis points, and similar 16-bit unsigned registers, modeled+-- exactly.+instance Sym Word16 where+ type SymRep Word16 = Word16+ toSym = id+ fromSym = id+ symDefault = 0++-- | An exact 8-bit unsigned value.+instance Sym Word8 where+ type SymRep Word8 = Word8+ toSym = id+ fromSym = id+ symDefault = 0++-- | An exact 64-bit signed value.+instance Sym Int64 where+ type SymRep Int64 = Int64+ toSym = id+ fromSym = id+ symDefault = 0++-- | An exact 32-bit signed value.+instance Sym Int32 where+ type SymRep Int32 = Int32+ toSym = id+ fromSym = id+ symDefault = 0++-- | 'Text' is encoded as Haskell 'String' for SBV's 'SString' theory.+instance Sym Text where+ type SymRep Text = String+ toSym = T.unpack+ fromSym = T.pack+ symDefault = T.empty++-- | 'UTCTime' is encoded as picoseconds since the Unix epoch. The time+-- library's 'NominalDiffTime' uses a fixed-point picosecond representation, so+-- this 'Integer' encoding is lossless while remaining well supported by z3.+instance Sym UTCTime where+ type SymRep UTCTime = Integer+ toSym t =+ let MkFixed picoseconds =+ nominalDiffTimeToSeconds (utcTimeToPOSIXSeconds t)+ in picoseconds+ fromSym picoseconds =+ posixSecondsToUTCTime+ (secondsToNominalDiffTime (MkFixed picoseconds))+ symDefault = posixSecondsToUTCTime 0++-- | Reify a 'Sym' instance so it can be passed around as a+-- first-class value. Useful for runtime dispatch on 'Typeable'+-- evidence.+data SymDict r where+ SymDict :: (Sym r) => SymDict r++-- | Try to discover a 'Sym' instance for @r@ at runtime. Returns+-- @Just SymDict@ for any of the curated supported types+-- ('Bool', 'Int', 'Integer', 'Natural', 'Text', 'UTCTime', and the fixed-width+-- integers 'Word8' \/ 'Word16' \/ 'Word32' \/ 'Word64' \/ 'Int32' \/+-- 'Int64'); 'Nothing' otherwise. The translator uses this to route+-- 'PEq' over arbitrary types: a 'Sym' hit translates to '(.==)' on+-- SBV terms; a miss falls back to a fresh 'SBool' (loses precision but+-- stays sound).+discoverSym :: forall r. (Typeable r) => Maybe (SymDict r)+discoverSym = case discoverSymbolicType @r of+ Just SymbolicBool -> Just SymDict+ Just SymbolicInt -> Just SymDict+ Just SymbolicInteger -> Just SymDict+ Just SymbolicNatural -> Just SymDict+ Just SymbolicText -> Just SymDict+ Just SymbolicUTCTime -> Just SymDict+ Just SymbolicWord64 -> Just SymDict+ Just SymbolicWord32 -> Just SymDict+ Just SymbolicWord16 -> Just SymDict+ Just SymbolicWord8 -> Just SymDict+ Just SymbolicInt64 -> Just SymDict+ Just SymbolicInt32 -> Just SymDict+ Nothing -> Nothing++-- | Reify both a 'Sym' instance for @r@ and evidence that its+-- 'SymRep' is symbolically orderable (an 'SBV.OrdSymbolic' instance on+-- @'SBV.SBV' ('SymRep' r)@). This is exactly what 'PCmp' translation+-- needs: 'Sym' to push the operands into SBV, 'OrdSymbolic' to emit a+-- real @.<@ \/ @.<=@ \/ @.>@ \/ @.>=@ comparison.+data SymOrdDict r where+ SymOrdDict :: (Sym r, SBV.OrdSymbolic (SBV.SBV (SymRep r))) => SymOrdDict r++-- | Try to discover ordering evidence for @r@ at runtime, companion to+-- 'discoverSym'. Returns @Just SymOrdDict@ for the numeric and time+-- types whose 'SymRep' is an 'SBV.OrdSymbolic' 'Integer' ('Int',+-- 'Integer', 'Natural', the fixed-width integers 'Word8' \/ 'Word16' \/ 'Word32'+-- \/ 'Word64' \/ 'Int32' \/ 'Int64', and 'UTCTime' encoded as epoch+-- seconds); 'Nothing' otherwise. 'Bool' and 'Text' are deliberately+-- omitted: ordering a 'Bool' guard is not meaningful, and 'SString'+-- ordering is out of scope here. A 'Nothing' makes the 'PCmp'+-- translator fall back to a fresh opaque 'SBool', exactly as 'goEq'+-- does for non-'Sym' operands — sound, just imprecise.+discoverSymOrd :: forall r. (Typeable r) => Maybe (SymOrdDict r)+discoverSymOrd = case discoverSymbolicType @r of+ Just SymbolicInt -> Just SymOrdDict+ Just SymbolicInteger -> Just SymOrdDict+ Just SymbolicNatural -> Just SymOrdDict+ Just SymbolicUTCTime -> Just SymOrdDict+ Just SymbolicWord64 -> Just SymOrdDict+ Just SymbolicWord32 -> Just SymOrdDict+ Just SymbolicWord16 -> Just SymOrdDict+ Just SymbolicWord8 -> Just SymOrdDict+ Just SymbolicInt64 -> Just SymOrdDict+ Just SymbolicInt32 -> Just SymOrdDict+ Just SymbolicBool -> Nothing+ Just SymbolicText -> Nothing+ Nothing -> Nothing++-- | Reify both a 'Sym' instance for @r@ and evidence that its 'SymRep'+-- is symbolically /numeric/ (a 'Num' instance on @'SBV.SBV' ('SymRep'+-- r)@). This is what 'TArith' translation needs: 'Sym' to push the+-- operands into SBV, 'Num' to emit a real @+@ \/ @-@ \/ @*@ over the+-- translated terms. Companion to 'discoverSym' \/ 'discoverSymOrd'+-- (EP-43).+data SymNumDict r where+ SymNumDict :: (Sym r, Num (SBV.SBV (SymRep r))) => SymNumDict r++-- | Try to discover numeric evidence for @r@ at runtime, companion to+-- 'discoverSymOrd'. Returns @Just SymNumDict@ for the numeric types+-- whose 'SymRep' is the SBV-'Num' 'Integer' ('Int', 'Integer', and the+-- fixed-width integers 'Word8' \/ 'Word16' \/ 'Word32' \/ 'Word64' \/+-- 'Int32' \/ 'Int64'), plus 'Natural'. Natural subtraction has the explicit+-- total monus meaning shared with concrete 'evalTerm'; it is translated as+-- @ite (a >= b) (a - b) 0@ rather than ordinary integer subtraction.+-- 'Bool', 'Text', and 'UTCTime' are omitted. A 'Nothing'+-- makes the 'TArith' translator fall back to a fresh opaque variable,+-- exactly as 'goEq' \/ 'goCmp' fall back for non-'Sym' operands —+-- sound, just imprecise. (The 'Num' constraint on the 'TArith'+-- constructor already prevents arithmetic at non-numeric types, so this+-- fallback is only reachable for a numeric type intentionally left out+-- of the registry.)+discoverSymNum :: forall r. (Typeable r) => Maybe (SymNumDict r)+discoverSymNum = case discoverSymbolicType @r of+ Just SymbolicInt -> Just SymNumDict+ Just SymbolicInteger -> Just SymNumDict+ Just SymbolicNatural -> Just SymNumDict+ Just SymbolicWord64 -> Just SymNumDict+ Just SymbolicWord32 -> Just SymNumDict+ Just SymbolicWord16 -> Just SymNumDict+ Just SymbolicWord8 -> Just SymNumDict+ Just SymbolicInt64 -> Just SymNumDict+ Just SymbolicInt32 -> Just SymNumDict+ Just SymbolicBool -> Nothing+ Just SymbolicText -> Nothing+ Just SymbolicUTCTime -> Nothing+ Nothing -> Nothing++-- | Whether the curated representation covers the complete concrete carrier+-- bijectively. This is the gate for 'wholeProjectionDomain': supporting+-- symbolic equality alone is not sufficient.+symbolicWholeCarrierExact :: forall (r :: Type). (Typeable r) => Bool+symbolicWholeCarrierExact =+ maybe False symbolicTypeWholeCarrierExact (discoverSymbolicType @r)++-- | Lift a concrete value to an SBV literal of its 'SymRep'.+symLit :: forall a. (Sym a) => a -> SBV.SBV (SymRep a)+symLit = SBV.literal . toSym++-- | Allocate a fresh symbolic variable of the carrier's 'SymRep'.+symFree :: forall a. (Sym a) => String -> SBV.Symbolic (SBV.SBV (SymRep a))+symFree label = do+ value <- SBV.free label+ constrainSymDomain @a value+ pure value++-- * Translation environment -------------------------------------------------++-- | Translation context: shared symbolic state that must be threaded+-- through a single predicate's walk so that, for example, two+-- 'PInCtor' atoms over distinct constructors agree they cannot both+-- be true, and two reads of the same register (or input field) share+-- one solver variable.+--+-- Three pieces of state are shared:+--+-- * 'seInputCtor' — the symbolic input-constructor tag, so 'PInCtor'+-- atoms over distinct constructors are recognized as mutually+-- unsatisfiable.+-- * 'seInputArm' — an independent discriminator for 'PLeftArm' and+-- 'PRightArm'. It is separate from constructor names so both facts can+-- be asserted by the same guard.+-- * 'seVarCache' — a per-translation memo cache (EP-42) keyed by a+-- structured 'SymVarKey'. Ordinary register and input reads preserve their+-- historical labels; field projections use base position and nominal+-- 'TypeRep' identity, never caller-controlled diagnostic strings alone.+-- The first read allocates one 'SBV.free' variable and stores it; every+-- later read of the same key returns the cached variable.+-- This makes the solver see two reads of @#x@ as the /same/ value,+-- so @proj #x .== proj #x@ is valid (not merely satisfiable). The+-- 'TApp1' \/ 'TApp2' escape hatches are deliberately /not/ cached:+-- they wrap opaque Haskell functions with no 'Eq', so two+-- applications cannot be recognized as equal and each stays a fresh+-- per-occurrence variable.+data ProjectionBaseKey+ = ProjectionReg String Int+ | ProjectionInp String String Int+ deriving stock (Eq, Ord, Show)++-- | Which structural carrier owns a projection base.+data ProjectionBaseKind+ = ProjectionRegisterOwner+ | ProjectionInputOwner+ deriving stock (Eq, Ord, Show)++-- | Stable structural identity for the concrete owner read beneath a field+-- projection. Display names are diagnostic; kind, optional input constructor,+-- and zero-based position keep identity structural.+data ProjectionBaseDescriptor = ProjectionBaseDescriptor+ { projectionBaseKind :: ProjectionBaseKind,+ projectionBaseConstructorName :: Maybe String,+ projectionBaseSlotName :: String,+ projectionBasePosition :: Int,+ projectionBaseOwnerType :: SomeTypeRep+ }+ deriving stock (Eq, Ord, Show)++-- | Public, function-free metadata for one nominal projection occurrence.+data ProjectionDescriptor = ProjectionDescriptor+ { projectionDescriptorBase :: ProjectionBaseDescriptor,+ projectionDescriptorPath :: String,+ projectionDescriptorShape :: String,+ projectionDescriptorTagType :: SomeTypeRep,+ projectionDescriptorOwnerType :: SomeTypeRep,+ projectionDescriptorResultType :: SomeTypeRep+ }+ deriving stock (Eq, Ord, Show)++-- | Whether every symbolic valuation of a predicate corresponds to its+-- concrete semantics, or the translation is only a sound over-approximation.+data TranslationStrength+ = ExactTranslation+ | ConservativeOverApproximation (NonEmpty TranslationIssue)+ deriving stock (Eq, Show)++-- | A deterministic explanation for lost translation exactness.+data TranslationIssue+ = OpaqueApplication+ | UnsupportedEquality SomeTypeRep+ | UnsupportedOrdering SomeTypeRep+ | UnsupportedArithmetic SomeTypeRep+ | UnconstrainedProjection ProjectionDescriptor+ | UnsupportedProjectionDomain ProjectionDescriptor String+ | ProjectionUsedOutsideEquality ProjectionDescriptor+ | ConflictingProjectionViews ProjectionBaseDescriptor+ | DirectAndProjectedOwnerRead ProjectionBaseDescriptor+ | UnguardedProjectionInputRead ProjectionDescriptor+ deriving stock (Eq, Show)++data SymVarKey+ = RegVar String+ | InpVar String String+ | ProjectionVar+ ProjectionBaseKey+ SomeTypeRep+ SomeTypeRep+ SomeTypeRep+ deriving stock (Eq, Ord, Show)++data SymEnv = SymEnv+ { -- | The shared symbolic input constructor tag. 'PInCtor' atoms+ -- assert @seInputCtor .== literal (icName ic)@; the solver+ -- recognizes that two such constraints with distinct names are+ -- mutually unsatisfiable.+ seInputCtor :: SBV.SBV String,+ -- | @True@ denotes the outer 'Left' arm; @False@ denotes 'Right'.+ seInputArm :: SBV.SBool,+ -- | Memo cache: maps a deterministic variable name ("reg/\<slot\>"+ -- or "inp/\<ctor\>/\<field\>") to the single SBV variable allocated+ -- for it during this predicate translation. Lazily populated on+ -- first read so unread slots stay unconstrained (and 'symSatExt'+ -- falls back to 'symDefault' for them). Scoped to one+ -- 'translatePred' walk (one 'mkSymEnv'), so variables are shared+ -- /within/ a query but never leak across independent queries.+ seVarCache :: IORef (Map SymVarKey SomeSBV),+ -- | Stable model label for every memoized structural variable.+ seVarLabels :: IORef (Map SymVarKey String),+ -- | Projection keys in allocation/first-occurrence order.+ seProjectionKeyOrder :: IORef [SymVarKey],+ -- | Keys whose complete exact-domain constraint was emitted.+ seConstrainedProjectionKeys :: IORef (Set SymVarKey),+ -- | Exact evidence used to decode and reconstruct satisfiable models.+ seProjectionBindings :: IORef (Map SymVarKey SomeProjectionBinding),+ -- | Next internal projection label. Projection labels are intentionally+ -- generated by Keiki so arbitrary schema names never reach SBV's+ -- restricted label namespace.+ seProjectionOrdinal :: IORef Int+ }++-- | An SBV variable of some representation type, packed so the memo+-- cache in 'SymEnv' can hold variables of different representation+-- types under one map. 'SBV.SymVal' has a 'Typeable' superclass, so+-- pattern-matching @SomeSBV (v :: SBV.SBV a)@ brings @Typeable a@ into+-- scope — exactly what 'memoFree' needs to check the recovered type+-- matches the requested one on a cache hit.+data SomeSBV where+ SomeSBV :: (SBV.SymVal a) => SBV.SBV a -> SomeSBV++data SomeProjectionBinding where+ SomeProjectionBinding ::+ ( FieldProjection projection,+ Typeable projection,+ Typeable (FieldOwner projection),+ Typeable (FieldResult projection),+ Sym (FieldResult projection)+ ) =>+ ProjectionDescriptor ->+ String ->+ FieldWitness projection ->+ SomeProjectionBinding++-- | Allocate a fresh 'SymEnv'. Lives in 'SBV.Symbolic' because+-- 'seInputCtor' is a free symbolic variable and the memo cache is an+-- 'IORef' created in the underlying 'IO' ('SBV.Symbolic' is+-- @SymbolicT IO@, hence 'MonadIO').+mkSymEnv :: SBV.Symbolic SymEnv+mkSymEnv = do+ ctor <- SBV.free "inputCtor"+ arm <- SBV.free "inputArm"+ cache <- liftIO (newIORef Map.empty)+ labels <- liftIO (newIORef Map.empty)+ projectionOrder <- liftIO (newIORef [])+ constrainedProjectionKeys <- liftIO (newIORef Set.empty)+ projectionBindings <- liftIO (newIORef Map.empty)+ projectionOrdinal <- liftIO (newIORef 0)+ pure+ ( SymEnv+ ctor+ arm+ cache+ labels+ projectionOrder+ constrainedProjectionKeys+ projectionBindings+ projectionOrdinal+ )++-- * Translation -------------------------------------------------------------++-- | Translate a 'Term rs ci r' to an SBV expression of the carrier's+-- representation type. Requires 'Sym' evidence for @r@.+--+-- The translation is /structural/ for 'TLit', 'TReg',+-- 'TInpCtorField', and (since EP-43) 'TArith': a 'TArith' over a type+-- whose 'SymRep' is SBV-numeric (a 'discoverSymNum' hit) emits a real+-- @+@ \/ @-@ \/ @*@ over the translated operands, so a guard over a+-- /computed/ value is visible to the solver. 'TApp1' and 'TApp2' wrap+-- opaque Haskell functions and translate to fresh SBV variables of the+-- result type — sound but imprecise; 'TArith' falls back to the same+-- fresh variable only if its (numeric) operand type is absent from the+-- 'discoverSymNum' registry.+--+-- Variable naming (consumed by 'symSatExt' for witness extraction):+--+-- * 'TReg' allocates @"reg/<slotName>"@ where @slotName@ is the+-- slot's label recovered from the 'Index'\'s 'KnownSymbol'+-- evidence on its leaf 'ZIdx'.+-- * 'TInpCtorField' allocates+-- @"inp/<icName>/<slotName>"@ — the 'InCtor''s name plus the+-- field's slot label.+-- * 'TFieldProj' uses a structured cache key containing the base position,+-- nominal projection tag, owner type, and result type. Its actual SBV+-- label is an internal @"proj/<ordinal>"@, so arbitrary schema strings+-- cannot collide with or violate SBV's label syntax.+-- * 'TApp1' / 'TApp2' keep their anonymous names; their values are+-- not extracted as part of the witness.+--+-- Note on repeated reads (EP-42): 'TReg', 'TInpCtorField', and+-- 'TFieldProj' reads are memoized through the env's 'seVarCache'. This is+-- /path-exact/: the first+-- read of a given structural key allocates one 'SBV.free' variable and caches+-- it; every later read of the same key returns the cached variable. So two+-- reads of the same slot (e.g.+-- @proj #x .== proj #x@) share /one/ SBV variable: the solver knows+-- they are equal, @x \/= x@ is unsat, and 'symSatExt''s by-name witness+-- extraction is correct for ordinary repeated reads. Exact projection+-- variables carry a declared image and inverse, so detailed verification can+-- decode model values and reconstruct path-local owner witnesses. Legacy+-- one-way projections remain over-approximate and are not reconstructed. The+-- 'TApp1' \/ 'TApp2'+-- escape hatches stay per-occurrence fresh (their opaque functions+-- have no 'Eq', so two applications cannot be recognized as equal);+-- their values are not part of the extracted witness.+translateTermSym ::+ forall rs ci ifs r.+ (Sym r) =>+ SymEnv ->+ Term rs ci ifs r ->+ SBV.Symbolic (SBV.SBV (SymRep r))+translateTermSym _env (TLit r) = pure (symLit r)+translateTermSym env (TReg ix) =+ memoFree @r env (RegVar (indexName ix))+translateTermSym env (TInpCtorField ic ix) =+ memoFree @r env (InpVar (icName ic) (indexName ix))+translateTermSym _env (TApp1 _f _t) = symFree @r "app1"+translateTermSym _env (TApp2 _f _a _b) = symFree @r "app2"+translateTermSym env (TArith op a b) = case discoverSymNum @r of+ Nothing -> symFree @r "arith" -- sound opaque fallback within the carrier domain+ Just SymNumDict -> do+ sa <- translateTermSym env a+ sb <- translateTermSym env b+ case (discoverSymbolicType @r, op) of+ (Just SymbolicNatural, OpSub) ->+ pure (SBV.ite (sa SBV..>= sb) (sa - sb) 0)+ _ -> do+ let apply = case op of+ OpAdd -> (+)+ OpSub -> (-)+ OpMul -> (*)+ pure (apply sa sb)+translateTermSym env (TFieldProj (witness :: FieldWitness projection) base) =+ do+ let key = projectionVarKey witness base+ symbolic <- memoFree @r env key+ case fieldWitnessDomain witness of+ Nothing -> pure ()+ Just domain -> case compileProjectionDomain @r domain symbolic of+ Left _unsupported -> pure ()+ Right domainConstraint -> do+ constrained <- liftIO (readIORef (seConstrainedProjectionKeys env))+ when (key `Set.notMember` constrained) $ do+ SBV.constrain domainConstraint+ liftIO+ ( modifyIORef'+ (seConstrainedProjectionKeys env)+ (Set.insert key)+ )+ labels <- liftIO (readIORef (seVarLabels env))+ case Map.lookup key labels of+ Nothing -> error "translateTermSym: projection variable has no model label"+ Just label ->+ liftIO+ ( modifyIORef'+ (seProjectionBindings env)+ ( Map.insertWith+ (\_existing original -> original)+ key+ ( SomeProjectionBinding+ (projectionDescriptor witness base)+ label+ witness+ )+ )+ )+ pure symbolic++-- | Why a declared projection domain could not be compiled exactly for its+-- active symbolic carrier. The translator must omit the entire constraint on+-- failure; emitting a stronger subset could manufacture false UNSAT.+data ProjectionDomainCompileError+ = UnsupportedWholeProjectionCarrier SomeTypeRep+ | UnsupportedFiniteProjectionLiteral SomeTypeRep+ deriving stock (Eq, Show)++compileProjectionDomain ::+ forall r.+ (Sym r) =>+ ProjectionDomain r ->+ SBV.SBV (SymRep r) ->+ Either ProjectionDomainCompileError SBV.SBool+compileProjectionDomain ProjectionWhole _symbolic+ | symbolicWholeCarrierExact @r = Right SBV.sTrue+ | otherwise = Left (UnsupportedWholeProjectionCarrier (SomeTypeRep (typeRep @r)))+compileProjectionDomain (ProjectionFinite values) symbolic+ | all projectionLiteralExact values =+ Right (SBV.sOr [symbolic SBV..== symLit value | value <- toList values])+ | otherwise =+ Left (UnsupportedFiniteProjectionLiteral (SomeTypeRep (typeRep @r)))+compileProjectionDomain (ProjectionText textPattern) symbolic =+ Right (symbolic `SBV.RegExp.match` compileTextPattern textPattern)++-- | A finite domain can be exact on a carrier whose whole representation is+-- not: machine 'Int', ordinary 'UTCTime', and bounded 'Text' literals are+-- examples. Each literal must nevertheless round-trip through 'SymRep', and a+-- 'Text' literal must stay within SMT-LIB's code-point ceiling.+projectionLiteralExact :: forall r. (Sym r, Eq r) => r -> Bool+projectionLiteralExact value =+ fromSym (toSym value) == value+ && case discoverSymbolicType @r of+ Just SymbolicText -> T.all (<= maximumSmtCodePoint) value+ _ -> True++compileTextPattern :: TextPattern -> SBV.RegExp.RegExp+compileTextPattern (TextLiteral literal) =+ SBV.RegExp.Literal (T.unpack literal)+compileTextPattern (TextRanges ranges) =+ SBV.RegExp.Union+ [ SBV.RegExp.Range lower upper+ | (lower, upper) <- toList ranges+ ]+compileTextPattern (TextConcat patterns) =+ SBV.RegExp.Conc (compileTextPattern <$> toList patterns)+compileTextPattern (TextAlternation patterns) =+ SBV.RegExp.Union (compileTextPattern <$> toList patterns)+compileTextPattern (TextRepeatBetween lower upper textPattern) =+ SBV.RegExp.Loop+ (fromIntegral lower)+ (fromIntegral upper)+ (compileTextPattern textPattern)++projectionVarKey ::+ forall projection rs ci ifs.+ ( Typeable projection,+ Typeable (FieldOwner projection),+ Typeable (FieldResult projection)+ ) =>+ FieldWitness projection ->+ ProjBase rs ci ifs (FieldOwner projection) ->+ SymVarKey+projectionVarKey _ base =+ ProjectionVar+ ( case base of+ PBReg ix -> ProjectionReg (indexName ix) (indexPosition ix)+ PBInp ic ix ->+ ProjectionInp (icName ic) (indexName ix) (indexPosition ix)+ )+ (SomeTypeRep (typeRep @projection))+ (SomeTypeRep (typeRep @(FieldOwner projection)))+ (SomeTypeRep (typeRep @(FieldResult projection)))++-- | Bind one memoized projection variable to the concrete getter result for+-- a known owner. Pass @fieldWitnessGet witness owner@ as the concrete result.+-- This supplies the concrete-to-symbolic simulation used by agreement+-- properties: every concrete evaluation has a matching symbolic valuation.+-- The converse requires an 'ExactFieldProjection' witness; legacy witnesses+-- remain over-approximate and are not reconstructed by 'symSatExt'.+constrainFieldProjection ::+ forall projection rs ci ifs.+ ( Typeable projection,+ Typeable (FieldOwner projection),+ Sym (FieldResult projection)+ ) =>+ SymEnv ->+ FieldWitness projection ->+ ProjBase rs ci ifs (FieldOwner projection) ->+ FieldResult projection ->+ SBV.Symbolic ()+constrainFieldProjection env witness base concrete = do+ symbolic <- memoFree @(FieldResult projection) env (projectionVarKey witness base)+ SBV.constrain (symbolic SBV..== symLit concrete)++-- | Memoized symbolic-variable allocator (EP-42). Looks @name@ up in+-- the env's 'seVarCache'. On a hit, recover the cached SBV variable —+-- checking its representation type matches the requested one, which it+-- always does because a deterministic name maps to exactly one type.+-- On a miss, allocate a fresh 'SBV.free', store it under @name@, and+-- return it. This is what makes repeated reads of the same register or+-- input field share a single solver variable.+memoFree ::+ forall r.+ (Sym r) =>+ SymEnv -> SymVarKey -> SBV.Symbolic (SBV.SBV (SymRep r))+memoFree env key = do+ m <- liftIO (readIORef (seVarCache env))+ case Map.lookup key m of+ Just (SomeSBV (v :: SBV.SBV b)) ->+ case eqTypeRep (typeRep @(SymRep r)) (typeRep @b) of+ Just HRefl -> pure v+ Nothing ->+ -- Unreachable: a name maps to exactly one representation type.+ error ("memoFree: type mismatch for cached variable " <> show key)+ Nothing -> do+ label <- case key of+ RegVar name -> pure ("reg/" <> name)+ InpVar ctorName fieldName ->+ pure ("inp/" <> ctorName <> "/" <> fieldName)+ ProjectionVar {} -> liftIO $ do+ ordinal <- readIORef (seProjectionOrdinal env)+ modifyIORef' (seProjectionOrdinal env) (+ 1)+ pure ("proj/" <> show ordinal)+ v <- symFree @r label+ liftIO $ do+ modifyIORef' (seVarCache env) (Map.insert key (SomeSBV v))+ modifyIORef' (seVarLabels env) (Map.insert key label)+ case key of+ ProjectionVar {} ->+ modifyIORef' (seProjectionKeyOrder env) (++ [key])+ _ -> pure ()+ pure v++-- | Recover the slot name an 'Index' points at by walking to the+-- leaf 'ZIdx' and reading off the 'KnownSymbol' evidence the+-- constructor carries. Used for deterministic SBV variable naming+-- in 'translateTermSym'.+indexName :: forall rs r. Index rs r -> String+indexName (ZIdx @s) = symbolVal (Proxy @s)+indexName (SIdx i) = indexName i++-- | Translate an 'HsPred' to an SBV 'SBool'. The translation is+-- structural for every constructor:+--+-- * 'PTop' / 'PBot' map to @sTrue@ / @sFalse@.+-- * 'PAnd' / 'POr' / 'PNot' map to '(SBV..&&)' / '(SBV..||)' /+-- 'SBV.sNot' on the recursive translations.+-- * 'PEq' tries 'discoverSym' on its operand type; on a hit it+-- emits '(.==)' between the two translated terms; on a miss it+-- emits a fresh 'SBool' (the equality is opaque to the solver).+-- * 'PInCtor' emits @seInputCtor .== literal (icName ic)@; the+-- shared 'seInputCtor' makes constructor-mutual-exclusion+-- decidable.+-- * 'PLeftArm' / 'PRightArm' assert the independent 'seInputArm'+-- discriminator.+-- * 'PCmp' tries 'discoverSymOrd' on its operand type; on a hit it+-- emits the matching SBV comparison ('SBV..<' \/ '.<=' \/ '.>' \/+-- '.>=') between the two translated terms; on a miss it emits a+-- fresh 'SBool' (the comparison is opaque to the solver).+translatePred ::+ forall rs ci. SymEnv -> HsPred rs ci -> SBV.Symbolic SBV.SBool+translatePred env = go+ where+ go :: HsPred rs ci -> SBV.Symbolic SBV.SBool+ go PTop = pure SBV.sTrue+ go PBot = pure SBV.sFalse+ go (PAnd p q) = (SBV..&&) <$> go p <*> go q+ go (POr p q) = (SBV..||) <$> go p <*> go q+ go (PNot p) = SBV.sNot <$> go p+ go (PEq a b) = goEq a b+ go (PInCtor ic) = pure (seInputCtor env SBV..== SBV.literal (icName ic))+ go PLeftArm = pure (seInputArm env)+ go PRightArm = pure (SBV.sNot (seInputArm env))+ go (PCmp op a b) = goCmp op a b++ goEq ::+ forall r ifs1 ifs2.+ (Typeable r) =>+ Term rs ci ifs1 r -> Term rs ci ifs2 r -> SBV.Symbolic SBV.SBool+ goEq a b = case discoverSym @r of+ Nothing -> SBV.free "neq"+ Just SymDict -> do+ sa <- translateTermSym env a+ sb <- translateTermSym env b+ pure (sa SBV..== sb)++ goCmp ::+ forall r ifs1 ifs2.+ (Typeable r) =>+ Cmp -> Term rs ci ifs1 r -> Term rs ci ifs2 r -> SBV.Symbolic SBV.SBool+ goCmp op a b = case discoverSymOrd @r of+ Nothing -> SBV.free "cmp" -- sound opaque fallback+ Just SymOrdDict -> do+ sa <- translateTermSym env a+ sb <- translateTermSym env b+ let apply = case op of+ CmpLt -> (SBV..<)+ CmpLe -> (SBV..<=)+ CmpGt -> (SBV..>)+ CmpGe -> (SBV..>=)+ pure (apply sa sb)++-- | A conservative answer from 'verifyPredicate'. The two @Verified@+-- constructors mean every predicate node translated structurally and the+-- solver returned a definite result. Opaque Haskell applications, unsupported+-- carrier dictionaries, solver timeouts or @Unknown@, and solver failures are+-- represented explicitly and must not be treated as successful verification.+data PredicateVerification+ = VerifiedSatisfiable+ | VerifiedUnsatisfiable+ | UnverifiedOpaque+ | UnverifiedSolverUnknown String+ | UnverifiedSolverFailure String+ deriving stock (Eq, Show)++-- | One solver-origin projection key and its checked reconstructed owner.+-- Values stay dynamically typed because one predicate can mention unrelated+-- projection carriers. Use the typed eliminators, never display names, to cast.+data ProjectionModel = ProjectionModel+ { projectionModelDescriptor :: ProjectionDescriptor,+ projectionModelKey :: Dynamic,+ projectionModelOwner :: Dynamic+ }+ deriving stock (Show)++-- | Cast a projection model key using its runtime type evidence.+projectionModelKeyAs :: (Typeable a) => ProjectionModel -> Maybe a+projectionModelKeyAs = fromDynamic . projectionModelKey++-- | Cast a reconstructed projection owner using its runtime type evidence.+projectionModelOwnerAs :: (Typeable a) => ProjectionModel -> Maybe a+projectionModelOwnerAs = fromDynamic . projectionModelOwner++-- | Solver status, translation strength, and checked projection-origin models+-- without changing the compatibility 'PredicateVerification' constructor set.+data PredicateVerificationDetail+ = -- | A satisfying symbolic valuation. Projection models are checked,+ -- path-local key/owner pairs, not complete register/input witnesses.+ PredicateSatisfiable TranslationStrength [ProjectionModel]+ | -- | A definite solver proof of emptiness. For exact projections this proof+ -- is conditional on the consumer's owner-to-domain declaration law.+ PredicateUnsatisfiable TranslationStrength+ | -- | The solver returned an inconclusive status.+ PredicateSolverUnknown TranslationStrength String+ | -- | Translation, solver startup, solver execution, or model decoding failed.+ PredicateSolverFailure TranslationStrength String+ | -- | An admitted model key was rejected by the declared inverse or failed+ -- its getter round trip.+ PredicateProjectionContractViolation+ TranslationStrength+ ProjectionDescriptor+ String+ deriving stock (Show)++data ProjectionUseContext+ = ProjectionEqualityOperand+ | ProjectionOutsideEquality++data TranslationReportEvent+ = TranslationIssueEvent TranslationIssue+ | DirectOwnerReadEvent ProjectionBaseDescriptor+ | ProjectionReadEvent ProjectionDescriptor Bool++data ProjectionBaseUsage = ProjectionBaseUsage+ { projectionUsageDirect :: Bool,+ projectionUsageViews :: [(SomeTypeRep, Bool)]+ }++-- | Explain the complete predicate translation. Per-node support is combined+-- with predicate-wide owner-path analysis so individually exact projections+-- are not promoted when the solver lacks their joint relation.+predicateTranslationReport :: forall rs ci. HsPred rs ci -> TranslationStrength+predicateTranslationReport predicate =+ case reportIssues of+ [] -> ExactTranslation+ firstIssue : remainingIssues ->+ ConservativeOverApproximation (firstIssue :| remainingIssues)+ where+ events = predicateReportEvents predicate predicate+ (reportIssues, _) = foldl consumeEvent ([], Map.empty) events++ consumeEvent ::+ ([TranslationIssue], Map ProjectionBaseDescriptor ProjectionBaseUsage) ->+ TranslationReportEvent ->+ ([TranslationIssue], Map ProjectionBaseDescriptor ProjectionBaseUsage)+ consumeEvent (issues, usages) event = case event of+ TranslationIssueEvent issue -> (appendIssue issue issues, usages)+ DirectOwnerReadEvent base ->+ let usage = Map.findWithDefault (ProjectionBaseUsage False []) base usages+ issues' =+ if null (projectionUsageViews usage)+ then issues+ else appendIssue (DirectAndProjectedOwnerRead base) issues+ usage' = usage {projectionUsageDirect = True}+ in (issues', Map.insert base usage' usages)+ ProjectionReadEvent descriptor exactEvidence ->+ let base = projectionDescriptorBase descriptor+ tag = projectionDescriptorTagType descriptor+ usage = Map.findWithDefault (ProjectionBaseUsage False []) base usages+ conflicts =+ any+ (\(seenTag, seenExact) -> seenTag /= tag || seenExact /= exactEvidence)+ (projectionUsageViews usage)+ issuesWithDirect =+ if projectionUsageDirect usage+ then appendIssue (DirectAndProjectedOwnerRead base) issues+ else issues+ issues' =+ if conflicts+ then appendIssue (ConflictingProjectionViews base) issuesWithDirect+ else issuesWithDirect+ views =+ if (tag, exactEvidence) `elem` projectionUsageViews usage+ then projectionUsageViews usage+ else projectionUsageViews usage ++ [(tag, exactEvidence)]+ usage' = usage {projectionUsageViews = views}+ in (issues', Map.insert base usage' usages)++ appendIssue issue issues+ | issue `elem` issues = issues+ | otherwise = issues ++ [issue]++predicateReportEvents ::+ forall rs ci.+ HsPred rs ci ->+ HsPred rs ci ->+ [TranslationReportEvent]+predicateReportEvents root = go+ where+ go PTop = []+ go PBot = []+ go (PAnd p q) = go p ++ go q+ go (POr p q) = go p ++ go q+ go (PNot p) = go p+ go (PEq (a :: Term rs ci ifs1 r) b) =+ equalitySupport @r+ ++ termReportEvents root ProjectionEqualityOperand a+ ++ termReportEvents root ProjectionEqualityOperand b+ go (PInCtor _) = []+ go PLeftArm = []+ go PRightArm = []+ go (PCmp _ (a :: Term rs ci ifs1 r) b) =+ orderingSupport @r+ ++ termReportEvents root ProjectionOutsideEquality a+ ++ termReportEvents root ProjectionOutsideEquality b++ equalitySupport :: forall (r :: Type). (Typeable r) => [TranslationReportEvent]+ equalitySupport = case discoverSym @r of+ Nothing -> [TranslationIssueEvent (UnsupportedEquality (SomeTypeRep (typeRep @r)))]+ Just SymDict -> []++ orderingSupport :: forall (r :: Type). (Typeable r) => [TranslationReportEvent]+ orderingSupport = case discoverSymOrd @r of+ Nothing -> [TranslationIssueEvent (UnsupportedOrdering (SomeTypeRep (typeRep @r)))]+ Just SymOrdDict -> []++termReportEvents ::+ forall rs ci ifs r.+ (Typeable r) =>+ HsPred rs ci ->+ ProjectionUseContext ->+ Term rs ci ifs r ->+ [TranslationReportEvent]+termReportEvents _root _context (TLit _) = []+termReportEvents _root _context (TReg ix) =+ [DirectOwnerReadEvent (registerBaseDescriptor @r ix)]+termReportEvents _root _context (TInpCtorField ic ix) =+ [DirectOwnerReadEvent (inputBaseDescriptor @r ic ix)]+termReportEvents _root _context (TApp1 _ _) =+ [TranslationIssueEvent OpaqueApplication]+termReportEvents _root _context (TApp2 _ _ _) =+ [TranslationIssueEvent OpaqueApplication]+termReportEvents root _context (TArith _ a b) =+ arithmeticSupport @r+ ++ termReportEvents root ProjectionOutsideEquality a+ ++ termReportEvents root ProjectionOutsideEquality b+ where+ arithmeticSupport :: forall (a :: Type). (Typeable a) => [TranslationReportEvent]+ arithmeticSupport = case discoverSymNum @a of+ Nothing -> [TranslationIssueEvent (UnsupportedArithmetic (SomeTypeRep (typeRep @a)))]+ Just SymNumDict -> []+termReportEvents+ root+ context+ (TFieldProj (witness :: FieldWitness projection) base) =+ relationIssue+ ++ evidenceIssues+ ++ inputGuardIssue+ ++ [ProjectionReadEvent descriptor exactEvidence]+ where+ descriptor = projectionDescriptor witness base+ relationIssue = case context of+ ProjectionEqualityOperand -> []+ ProjectionOutsideEquality ->+ [TranslationIssueEvent (ProjectionUsedOutsideEquality descriptor)]+ (evidenceIssues, exactEvidence) = case fieldWitnessDomain witness of+ Nothing ->+ ([TranslationIssueEvent (UnconstrainedProjection descriptor)], False)+ Just domain -> case discoverSym @(FieldResult projection) of+ Nothing -> ([], False)+ Just SymDict -> case projectionDomainSupport domain of+ Nothing -> ([], True)+ Just reason ->+ ( [TranslationIssueEvent (UnsupportedProjectionDomain descriptor reason)],+ False+ )+ inputGuardIssue = case projectionDescriptorBase descriptor of+ ProjectionBaseDescriptor {projectionBaseKind = ProjectionRegisterOwner} -> []+ ProjectionBaseDescriptor+ { projectionBaseKind = ProjectionInputOwner,+ projectionBaseConstructorName = Just ctorName+ }+ | predicateImpliesInCtor ctorName root -> []+ | otherwise ->+ [TranslationIssueEvent (UnguardedProjectionInputRead descriptor)]+ ProjectionBaseDescriptor {projectionBaseKind = ProjectionInputOwner} ->+ [TranslationIssueEvent (UnguardedProjectionInputRead descriptor)]++projectionDomainSupport ::+ forall r.+ (Sym r) =>+ ProjectionDomain r ->+ Maybe String+projectionDomainSupport ProjectionWhole+ | symbolicWholeCarrierExact @r = Nothing+ | otherwise = Just "whole carrier is not representation-exact"+projectionDomainSupport (ProjectionFinite values)+ | all projectionLiteralExact values = Nothing+ | otherwise = Just "finite domain contains a non-representable symbolic literal"+projectionDomainSupport ProjectionText {} = Nothing++registerBaseDescriptor ::+ forall r rs.+ (Typeable r) =>+ Index rs r ->+ ProjectionBaseDescriptor+registerBaseDescriptor ix =+ ProjectionBaseDescriptor+ { projectionBaseKind = ProjectionRegisterOwner,+ projectionBaseConstructorName = Nothing,+ projectionBaseSlotName = indexName ix,+ projectionBasePosition = indexPosition ix,+ projectionBaseOwnerType = SomeTypeRep (typeRep @r)+ }++inputBaseDescriptor ::+ forall r ci ifs.+ (Typeable r) =>+ InCtor ci ifs ->+ Index ifs r ->+ ProjectionBaseDescriptor+inputBaseDescriptor ic ix =+ ProjectionBaseDescriptor+ { projectionBaseKind = ProjectionInputOwner,+ projectionBaseConstructorName = Just (icName ic),+ projectionBaseSlotName = indexName ix,+ projectionBasePosition = indexPosition ix,+ projectionBaseOwnerType = SomeTypeRep (typeRep @r)+ }++projectionDescriptor ::+ forall projection rs ci ifs.+ ( FieldProjection projection,+ KnownSymbol (FieldName projection),+ Typeable projection,+ Typeable (FieldOwner projection),+ Typeable (FieldResult projection)+ ) =>+ FieldWitness projection ->+ ProjBase rs ci ifs (FieldOwner projection) ->+ ProjectionDescriptor+projectionDescriptor witness base =+ ProjectionDescriptor+ { projectionDescriptorBase = case base of+ PBReg ix -> registerBaseDescriptor @(FieldOwner projection) ix+ PBInp ic ix -> inputBaseDescriptor @(FieldOwner projection) ic ix,+ projectionDescriptorPath = fieldProjectionPath witness base,+ projectionDescriptorShape = fieldShapeId (Proxy @projection),+ projectionDescriptorTagType = SomeTypeRep (typeRep @projection),+ projectionDescriptorOwnerType = SomeTypeRep (typeRep @(FieldOwner projection)),+ projectionDescriptorResultType = SomeTypeRep (typeRep @(FieldResult projection))+ }++-- | Whether the predicate-wide report contains no translation issue.+predicateTranslationExact :: HsPred rs ci -> Bool+predicateTranslationExact predicate = case predicateTranslationReport predicate of+ ExactTranslation -> True+ ConservativeOverApproximation _ -> False++data PredicateSolve = PredicateSolve+ { predicateSolveStrength :: TranslationStrength,+ predicateSolveEnvironment :: SymEnv,+ predicateSolveResult :: SBV.SatResult+ }++runPredicateSolver ::+ HsPred rs ci ->+ (SymEnv -> SBV.Symbolic ()) ->+ IO (Either String PredicateSolve)+runPredicateSolver predicate addConstraints = do+ environmentRef <- newIORef Nothing+ attempt <- try @SomeException $ SBV.sat $ do+ environment <- mkSymEnv+ liftIO (writeIORef environmentRef (Just environment))+ translated <- translatePred environment predicate+ addConstraints environment+ pure translated+ case attempt of+ Left failure -> pure (Left (displayException failure))+ Right result -> do+ maybeEnvironment <- readIORef environmentRef+ pure $ case maybeEnvironment of+ Nothing -> Left "solver translation did not publish its environment"+ Just environment ->+ Right+ PredicateSolve+ { predicateSolveStrength = predicateTranslationReport predicate,+ predicateSolveEnvironment = environment,+ predicateSolveResult = result+ }++-- | Solve once and preserve status, predicate-global translation strength,+-- and checked exact projection models. This can report definite results for a+-- conservative translation without promoting them through 'verifyPredicate'.+verifyPredicateDetailed :: HsPred rs ci -> IO PredicateVerificationDetail+verifyPredicateDetailed predicate = do+ solved <- runPredicateSolver predicate (const (pure ()))+ case solved of+ Left failure ->+ pure (PredicateSolverFailure (predicateTranslationReport predicate) failure)+ Right PredicateSolve {predicateSolveStrength = strength, predicateSolveEnvironment = environment, predicateSolveResult = result} ->+ decodeDetailedResult strength environment result++decodeDetailedResult ::+ TranslationStrength ->+ SymEnv ->+ SBV.SatResult ->+ IO PredicateVerificationDetail+decodeDetailedResult strength environment result@(SBV.SatResult status) =+ case status of+ SBV.Satisfiable {} -> do+ extracted <- extractProjectionModels environment result+ pure $ case extracted of+ Left (descriptor, failure) ->+ PredicateProjectionContractViolation strength descriptor failure+ Right projectionModels -> PredicateSatisfiable strength projectionModels+ SBV.Unsatisfiable {} -> pure (PredicateUnsatisfiable strength)+ SBV.Unknown {} -> pure (PredicateSolverUnknown strength "solver returned Unknown")+ SBV.ProofError {} -> pure (PredicateSolverFailure strength "solver returned ProofError")+ SBV.DeltaSat {} -> pure (PredicateSolverUnknown strength "solver returned DeltaSat")+ SBV.SatExtField {} -> pure (PredicateSolverUnknown strength "solver returned SatExtField")++extractProjectionModels ::+ SymEnv ->+ SBV.SatResult ->+ IO (Either (ProjectionDescriptor, String) [ProjectionModel])+extractProjectionModels environment result = do+ orderedKeys <- readIORef (seProjectionKeyOrder environment)+ bindings <- readIORef (seProjectionBindings environment)+ pure $ do+ projectionModels <- forM orderedKeys $ \key -> case Map.lookup key bindings of+ Nothing -> Right Nothing+ Just (SomeProjectionBinding descriptor label witness) ->+ case SBV.getModelValue label result of+ Nothing -> Left (descriptor, "solver model omitted the projection value")+ Just symbolicRepresentation ->+ let concreteKey = fromSym symbolicRepresentation+ in case checkFieldProjectionKey witness concreteKey of+ Left lawFailure -> Left (descriptor, show lawFailure)+ Right owner ->+ Right+ ( Just+ ProjectionModel+ { projectionModelDescriptor = descriptor,+ projectionModelKey = toDyn concreteKey,+ projectionModelOwner = toDyn owner+ }+ )+ pure [model | Just model <- projectionModels]++-- | Conservative compatibility projection of 'verifyPredicateDetailed'.+verifyPredicate :: HsPred rs ci -> IO PredicateVerification+verifyPredicate predicate = do+ detail <- verifyPredicateDetailed predicate+ pure $ case detail of+ PredicateSatisfiable ExactTranslation _ -> VerifiedSatisfiable+ PredicateUnsatisfiable ExactTranslation -> VerifiedUnsatisfiable+ PredicateSatisfiable ConservativeOverApproximation {} _ -> UnverifiedOpaque+ PredicateUnsatisfiable ConservativeOverApproximation {} -> UnverifiedOpaque+ PredicateSolverUnknown _ message -> UnverifiedSolverUnknown message+ PredicateSolverFailure _ message -> UnverifiedSolverFailure message+ PredicateProjectionContractViolation _ _ message ->+ UnverifiedSolverFailure ("projection contract violation: " <> message)++-- * Symbolic predicate wrapper ----------------------------------------------++-- | A newtype wrapper over 'HsPred' that selects the v2 'BoolAlg'+-- instance (with SBV-backed analyses) instead of the v1 syntactic+-- one. The v1 'BoolAlg HsPred' instance in "Keiki.Core" stays+-- unchanged for back-compat; consumers that want symbolic answers+-- wrap with 'SymPred'.+--+-- The 'SymPred' constructor is exported so callers can lift+-- @userReg@-style transducers via 'fmap'-like adapters; M6 of EP-2+-- ships 'withSymPred' which re-tags every edge guard.+newtype SymPred (rs :: [Slot]) (ci :: Type) = SymPred {unSymPred :: HsPred rs ci}++-- | A 'SymTransducer' whose guard carrier is the SBV-backed 'SymPred'.+-- The symbolic analogue of 'Keiki.Core.Guarded'.+type SymGuarded rs s ci co = SymTransducer (SymPred rs ci) rs s ci co++-- | The v2 'BoolAlg' instance. The five structural methods compose+-- 'HsPred' constructors. 'models' delegates to the v1 'evalPred'+-- (concrete evaluation, no solver call). 'isBot' routes through+-- 'symIsBot', which dispatches to an external z3 process via SBV and+-- 'unsafePerformIO'. Solver failures are caught and conservatively mean "not+-- proved empty". Witness extraction+-- ('Keiki.Core.sat') lives in the separate 'Sat' instance below, which+-- carries the 'ExtractRegFile' / 'KnownInCtors' evidence it needs; this+-- instance is deliberately /unconstrained/ so the witness-free analyses+-- ('isSingleValuedSym') keep type-checking on register-file-existential+-- carriers and on @ci@ types with no 'KnownInCtors'.+instance BoolAlg (SymPred rs ci) (RegFile rs, ci) where+ top = SymPred PTop+ bot = SymPred PBot+ conj (SymPred p) (SymPred q) = SymPred (PAnd p q)+ disj (SymPred p) (SymPred q) = SymPred (POr p q)+ neg (SymPred p) = SymPred (PNot p)+ models (SymPred p) (regs, ci) = evalPred p regs ci+ isBot (SymPred p) = symIsBot p++-- | Witness extraction for the SBV-backed carrier (EP-44, MasterPlan+-- 12). @'sat' (SymPred p)@ returns the same real, forceable witness as+-- 'symSatExt' — a concrete @(RegFile rs, ci)@ reconstructed from the+-- solver model. The constraints @ExtractRegFile rs@ / @KnownInCtors ci@+-- live here (not on 'BoolAlg') so only witness extraction pays for them.+instance+ (ExtractRegFile rs, KnownInCtors ci) =>+ Sat (SymPred rs ci) (RegFile rs, ci)+ where+ sat (SymPred p) = symSatExt p++-- * Solver-backed analyses --------------------------------------------------++-- | Interpret a solver result for emptiness ('Keiki.Core.isBot') purposes.+-- Returns 'True' only for a definite 'SBV.Unsatisfiable' result. Every other+-- result means "not provably empty": that includes 'SBV.Satisfiable',+-- 'SBV.Unknown' (for example, a timeout or an incomplete string-theory query),+-- 'SBV.ProofError', 'SBV.DeltaSat', and 'SBV.SatExtField'. This is the+-- conservative direction for callers that use emptiness to bless two guards as+-- disjoint or to diagnose an edge as dead.+satResultIsProvablyUnsat :: SBV.SatResult -> Bool+satResultIsProvablyUnsat (SBV.SatResult result) = case result of+ SBV.Unsatisfiable {} -> True+ SBV.Satisfiable {} -> False+ SBV.DeltaSat {} -> False+ SBV.SatExtField {} -> False+ SBV.Unknown {} -> False+ SBV.ProofError {} -> False++-- | Symbolic emptiness check. Translates the predicate to an SBV expression and+-- asks z3 whether it is definitely unsatisfiable. A 'True' result proves the+-- predicate is bot; 'False' means either satisfiable or that the solver gave up.+-- The latter can occur for 'Text' guards translated through z3's string theory.+-- This conservative failure direction may surface an overlap warning but never+-- blesses an uncertain pair as disjoint. Solver startup and execution failures+-- are caught and conservatively return 'False'. The wrapper is justified+-- because each query is deterministic for a given predicate and side-effect-free+-- outside the solver process. When @p@ contains 'exactFieldWitness', a 'True'+-- result is conditional on the declaration laws documented by+-- 'ExactFieldProjection'; an under-declared image can otherwise create false+-- UNSAT without producing a model that Keiki could check.+{-# NOINLINE symIsBot #-}+symIsBot :: HsPred rs ci -> Bool+symIsBot p = unsafePerformIO $ do+ solved <- runPredicateSolver p (const (pure ()))+ pure $ case solved of+ Left _ -> False+ Right result -> satResultIsProvablyUnsat (predicateSolveResult result)++-- * Single-valuedness ------------------------------------------------------++-- | A transducer is /single-valued/ when, at every reachable+-- vertex, at most one outgoing edge's guard is satisfied for any+-- given input. The check decomposes into "for every vertex @s@, for+-- every distinct pair @(e1, e2)@ of outgoing edges, is the+-- conjunction of their guards 'isBot'?". The function is+-- 'BoolAlg'-polymorphic; precision depends on the chosen 'isBot'+-- implementation. With 'SymPred', this is the v2 SBV-backed+-- decision; with the v1 'HsPred' instance the answer is the v1+-- syntactic over-approximation. A solver 'SBV.Unknown' is conservatively treated+-- as a possibly overlapping pair, so this function returns 'False'.+isSingleValuedSym ::+ forall phi rs s ci co.+ (BoolAlg phi (RegFile rs, ci), Bounded s, Enum s) =>+ SymTransducer phi rs s ci co ->+ Bool+isSingleValuedSym t = all vertexSV [minBound .. maxBound]+ where+ vertexSV :: s -> Bool+ vertexSV s =+ let es = edgesOut t s+ ies = zip [(0 :: Int) ..] es+ -- Only 'Live' edges compete in forward dispatch; guard+ -- overlap with or between 'ReplayOnly' edges cannot cause+ -- forward ambiguity.+ pairs =+ [ (e1, e2)+ | (i, e1) <- ies,+ (j, e2) <- ies,+ i < j,+ mode e1 == Live,+ mode e2 == Live+ ]+ in all (\(e1, e2) -> isBot (guard e1 `conj` guard e2)) pairs++-- | Lift a transducer's edges from the v1 'HsPred' guard carrier to+-- the v2 'SymPred' carrier so 'isSingleValuedSym' (or any other+-- 'BoolAlg'-polymorphic analysis) sees the SBV-backed instance.+-- The control graph and update / output terms are unchanged.+withSymPred ::+ SymTransducer (HsPred rs ci) rs s ci co ->+ SymTransducer (SymPred rs ci) rs s ci co+withSymPred t =+ SymTransducer+ { edgesOut = \s -> map liftEdge (edgesOut t s),+ initial = initial t,+ initialRegs = initialRegs t,+ isFinal = isFinal t+ }+ where+ liftEdge ::+ Edge (HsPred rs ci) rs ci co s ->+ Edge (SymPred rs ci) rs ci co s+ liftEdge e@Edge {update = u} =+ Edge+ { guard = SymPred (guard e),+ update = u,+ output = output e,+ target = target e,+ mode = mode e+ }++-- * Solver-backed validation diagnostics (EP-56) ---------------------------++-- | One live outgoing-edge pair and the single detailed solver result used to+-- decide its compatibility warning.+data DeterminismAnalysisDetail s = DeterminismAnalysisDetail+ { determinismDetailEdgeA :: EdgeRef s,+ determinismDetailEdgeB :: EdgeRef s,+ determinismDetailVerification :: PredicateVerificationDetail+ }++-- | Solve every live pair once, retaining edge attribution and full status.+checkTransitionDeterminismSymDetailed ::+ (Bounded s, Enum s) =>+ SymTransducer (HsPred rs ci) rs s ci co ->+ IO [DeterminismAnalysisDetail s]+checkTransitionDeterminismSymDetailed transducer =+ sequence+ [ DeterminismAnalysisDetail+ (EdgeRef {edgeSource = source, edgeIndex = firstIndex})+ (EdgeRef {edgeSource = source, edgeIndex = secondIndex})+ <$> verifyPredicateDetailed (PAnd (guard firstEdge) (guard secondEdge))+ | source <- [minBound .. maxBound],+ let indexedEdges = zip [(0 :: Int) ..] (edgesOut transducer source),+ (firstIndex, firstEdge) <- indexedEdges,+ (secondIndex, secondEdge) <- indexedEdges,+ firstIndex < secondIndex,+ mode firstEdge == Live,+ mode secondEdge == Live+ ]++-- | Solver-backed determinism diagnostic. Lifts the transducer with+-- 'withSymPred' and runs the 'BoolAlg'-polymorphic 'checkTransitionDeterminism'+-- at the 'SymPred' carrier, whose 'isBot' is the exact z3 decision. Unlike the+-- pure path in 'validateTransducer', this catches register-value-dependent and+-- other non-syntactic overlaps. A solver 'SBV.Unknown' conservatively produces a+-- warning rather than blessing the pair as disjoint. Requires z3 on @PATH@.+checkTransitionDeterminismSym ::+ (Bounded s, Enum s, Show s) =>+ SymTransducer (HsPred rs ci) rs s ci co ->+ [DeterminismWarning s]+checkTransitionDeterminismSym transducer = unsafePerformIO $ do+ details <- checkTransitionDeterminismSymDetailed transducer+ pure+ [ DeterminismWarning+ { dwSource = edgeSource firstRef,+ dwEdgeA = edgeIndex firstRef,+ dwEdgeB = edgeIndex secondRef,+ dwDetail =+ "edges #"+ <> show (edgeIndex firstRef)+ <> " and #"+ <> show (edgeIndex secondRef)+ <> " out of "+ <> show (edgeSource firstRef)+ <> " may overlap (symbolic)"+ }+ | DeterminismAnalysisDetail firstRef secondRef verification <- details,+ not (verificationIsDefinitelyUnsatisfiable verification)+ ]+{-# NOINLINE checkTransitionDeterminismSym #-}++-- | One edge and the detailed result used to decide whether it is dead in+-- isolation.+data DeadEdgeAnalysisDetail s = DeadEdgeAnalysisDetail+ { deadEdgeDetailEdge :: EdgeRef s,+ deadEdgeDetailVerification :: PredicateVerificationDetail+ }++-- | Solve every edge guard once and retain its attribution and full status.+checkDeadEdgesSymDetailed ::+ (Bounded s, Enum s) =>+ SymTransducer (HsPred rs ci) rs s ci co ->+ IO [DeadEdgeAnalysisDetail s]+checkDeadEdgesSymDetailed transducer =+ sequence+ [ DeadEdgeAnalysisDetail+ (EdgeRef {edgeSource = source, edgeIndex = edgeNumber})+ <$> verifyPredicateDetailed (guard edge)+ | source <- [minBound .. maxBound],+ (edgeNumber, edge) <- zip [(0 :: Int) ..] (edgesOut transducer source)+ ]++-- | Symbolic dead-edge sketch. Flags edges whose guard is unsatisfiable+-- /in isolation/ (via 'symIsBot'), which the structural 'checkDeadEdges'+-- misses unless the guard is literally 'PBot' (e.g. @amount > 0 && amount < 0@).+-- It does NOT compute the register configurations reachable at each vertex, so+-- it still cannot catch the FieldResource case (a guard satisfiable in+-- isolation but never under the registers reachable there); that needs a full+-- reachable-state fixpoint and is left as future work. A solver 'SBV.Unknown'+-- does not diagnose an edge as dead, because it is not proof of unsatisfiability.+-- Requires z3 on @PATH@.+checkDeadEdgesSym ::+ (Bounded s, Enum s) =>+ SymTransducer (HsPred rs ci) rs s ci co ->+ [DeadEdgeWarning s]+checkDeadEdgesSym transducer = unsafePerformIO $ do+ details <- checkDeadEdgesSymDetailed transducer+ pure+ [ DeadEdgeWarning+ edgeRef+ "guard is unsatisfiable in isolation (symbolic)"+ | DeadEdgeAnalysisDetail edgeRef verification <- details,+ verificationIsDefinitelyUnsatisfiable verification+ ]+{-# NOINLINE checkDeadEdgesSym #-}++verificationIsDefinitelyUnsatisfiable :: PredicateVerificationDetail -> Bool+verificationIsDefinitelyUnsatisfiable PredicateUnsatisfiable {} = True+verificationIsDefinitelyUnsatisfiable _ = False++-- * Witness extraction -----------------------------------------------------++-- | Materialize a 'RegFile' from a name-keyed reader. The reader's input is a+-- slot name; its output is a value of any 'Sym'-supported type. The reader is+-- total: callers fall back to 'symDefault' for slots absent from the model.+-- 'extractRegFileAt' additionally supplies zero-based structural position so+-- exact projection owners remain distinct even when diagnostic names repeat.+--+-- Two instances cover the slot list:+--+-- * @ExtractRegFile \'[]@ — return 'RNil' regardless of the reader.+-- * @ExtractRegFile (\'(s, t) ': rs)@ — read the head slot's name+-- via the reader, recurse on the tail, build an 'RCons'.+--+-- The instance constraints @KnownSymbol s@ and @Sym t@ make this+-- automatic for any concrete slot list whose value types are in the+-- curated 'Sym' registry ('Bool', 'Int', 'Integer', 'Natural', 'Text',+-- 'UTCTime'). User Registration's 'UserRegRegs' shape qualifies+-- without further user code.+class ExtractRegFile (rs :: [Slot]) where+ extractRegFile :: (forall r. (Sym r) => String -> r) -> RegFile rs++ -- | Position-aware private traversal used to install exact reconstructed+ -- projection owners. The default preserves source compatibility for custom+ -- instances by delegating to their existing name-only implementation.+ extractRegFileAt ::+ Int ->+ (forall r. (Sym r) => Int -> String -> r) ->+ RegFile rs+ extractRegFileAt _ reader = extractRegFile (reader (-1))++instance ExtractRegFile '[] where+ extractRegFile _ = RNil+ extractRegFileAt _ _ = RNil++instance+ ( KnownSymbol s,+ Sym t,+ ExtractRegFile rs+ ) =>+ ExtractRegFile ('(s, t) ': rs)+ where+ extractRegFile reader =+ RCons+ (Proxy @s)+ (reader @t (symbolVal (Proxy @s)))+ (extractRegFile @rs reader)+ extractRegFileAt position reader =+ RCons+ (Proxy @s)+ (reader @t position (symbolVal (Proxy @s)))+ (extractRegFileAt @rs (position + 1) reader)++-- | Existential wrapper around an 'InCtor' that hides the+-- input-field slot list. The hidden 'ExtractRegFile' constraint lets+-- 'symSatExt' rebuild the input register file once the constructor+-- tag is known from the SBV model.+data SomeInCtor (ci :: Type) where+ SomeInCtor :: (ExtractRegFile ifs) => InCtor ci ifs -> SomeInCtor ci++-- | A 'ci' type whose set of 'InCtor's is statically known. Each+-- 'SomeInCtor' bag entry pairs an 'InCtor' value with the+-- 'ExtractRegFile' evidence its field-list shape requires.+--+-- For the User Registration aggregate, the instance is a five-line+-- list pairing the existing @inCtorStart@ … @inCtorContinue@+-- declarations:+--+-- > instance KnownInCtors UserCmd where+-- > allInCtors =+-- > [ SomeInCtor inCtorStart+-- > , SomeInCtor inCtorConfirm+-- > , SomeInCtor inCtorResend+-- > , SomeInCtor inCtorGdpr+-- > , SomeInCtor inCtorContinue+-- > ]+--+-- Future work: a Generic-derived default via 'GHasCtor' so users+-- get the instance for free with @deriving (Generic)@. Out of scope+-- for EP-9 because the explicit list is already one line per+-- constructor.+class KnownInCtors ci where+ allInCtors :: [SomeInCtor ci]++-- | The single zero-field constructor of @()@ — a transducer whose+-- command alphabet carries no information. Lets 'symSatExt' (and hence+-- 'Keiki.Core.sat') reconstruct a @()@ witness for predicates over+-- @SymPred rs ()@.+inCtorUnit :: InCtor () '[]+inCtorUnit =+ InCtor+ { icName = "()",+ icMatch = \() -> Just RNil,+ icBuild = \RNil -> ()+ }++-- | @()@ has one constructor; its 'allInCtors' is the singleton+-- 'inCtorUnit'. Added by EP-44 so @sat@ over a no-command carrier+-- (@SymPred '[] ()@) yields a real @(RNil, ())@ witness.+instance KnownInCtors () where+ allInCtors = [SomeInCtor inCtorUnit]++-- * symSatExt ---------------------------------------------------------------++-- | Symbolic satisfiability with full witness extraction. On a satisfiable+-- translation, reconstructs a candidate @(regs, cmd)@ from the SBV model and+-- returns it only when concrete 'models' evaluation confirms the predicate.+-- Thus @models p (regs, cmd) == True@ holds unconditionally for every returned+-- witness. Escape-hatch terms ('TApp1', 'TApp2', and 'PEq' over a non-'Sym'+-- operand type) and legacy over-approximate field projections can make the+-- solver's assignment impossible for the reconstructed values; such a+-- candidate is discarded. Exact projections contribute checked, path-local+-- owner overrides when their predicate-wide relation is safe. Every decoded+-- key is validated against its domain, inverse, and getter round-trip before+-- any override is installed.+--+-- /Repeated reads/ of the same register or input field are handled+-- correctly: since EP-42 'translateTermSym' memoizes 'TReg' \/+-- 'TInpCtorField' reads (see 'SymEnv'\'s 'seVarCache'), so two reads of+-- @#x@ share one SBV variable and the by-name witness extraction+-- satisfies @proj #x .== proj #x@-style structural equality.+--+-- The model's input-constructor tag is confined to the known+-- constructor domain (@KnownInCtors ci@), so a predicate without a+-- 'PInCtor' atom still reconstructs a real command (the first/only+-- constructor) rather than failing to match an arbitrary solver string.+--+-- 'symSatExt' is /pure/ via 'unsafePerformIO' on the SBV solver+-- call (deterministic for a given predicate, side-effect-free+-- outside the solver process). Since EP-44 it /is/ the implementation+-- of the 'Keiki.Core.Sat' method 'sat' on 'SymPred' (via the+-- @Sat (SymPred …)@ instance, which carries the 'ExtractRegFile' /+-- 'KnownInCtors' evidence the witness-free 'BoolAlg' class cannot). A 'Nothing'+-- result means only that no concrete witness was recovered: the predicate may+-- be unsatisfiable, the solver may have returned 'SBV.Unknown', or a+-- satisfiable over-approximate or opaque assignment may have failed the+-- concrete recheck. An input-field read used without its constructor guard is+-- also discarded if concrete evaluation raises its guard-violation error.+-- Callers must not treat 'Nothing' as a proof of emptiness; 'symIsBot' returns+-- 'True' only for that proof.+{-# NOINLINE symSatExt #-}+symSatExt ::+ forall rs ci.+ ( ExtractRegFile rs,+ KnownInCtors ci+ ) =>+ HsPred rs ci -> Maybe (RegFile rs, ci)+symSatExt p = unsafePerformIO $ do+ solved <- runPredicateSolver p constrainKnownConstructors+ case solved of+ Left _ -> pure Nothing+ Right PredicateSolve {predicateSolveStrength = strength, predicateSolveEnvironment = environment, predicateSolveResult = result}+ | SBV.modelExists result -> do+ extracted <- extractProjectionModels environment result+ case extracted of+ Left _ -> pure Nothing+ Right projectionModels -> do+ let safeProjectionModels =+ filter+ (projectionModelRelationSafe strength)+ projectionModels+ candidate = do+ ctorTag <- SBV.getModelValue "inputCtor" result+ let regReader :: forall r. (Sym r) => Int -> String -> r+ regReader position name =+ maybe+ (readModel result ("reg/" <> name))+ id+ ( projectionOwnerOverride @r+ safeProjectionModels+ ProjectionBaseDescriptor+ { projectionBaseKind = ProjectionRegisterOwner,+ projectionBaseConstructorName = Nothing,+ projectionBaseSlotName = name,+ projectionBasePosition = position,+ projectionBaseOwnerType = SomeTypeRep (typeRep @r)+ }+ )+ registers = extractRegFileAt @rs 0 regReader+ inputReader ::+ forall r.+ (Sym r) =>+ String ->+ Int ->+ String ->+ r+ inputReader ctorName position fieldName =+ maybe+ (readModel result ("inp/" <> ctorName <> "/" <> fieldName))+ id+ ( projectionOwnerOverride @r+ safeProjectionModels+ ProjectionBaseDescriptor+ { projectionBaseKind = ProjectionInputOwner,+ projectionBaseConstructorName = Just ctorName,+ projectionBaseSlotName = fieldName,+ projectionBasePosition = position,+ projectionBaseOwnerType = SomeTypeRep (typeRep @r)+ }+ )+ command <-+ pickCi @ci+ ctorTag+ inputReader+ pure (registers, command)+ case candidate of+ Nothing -> pure Nothing+ Just witness -> do+ checked <- try @ErrorCall (evaluate (models (SymPred p) witness))+ pure $ case checked of+ Right True -> Just witness+ Right False -> Nothing+ Left _ -> Nothing+ | otherwise -> pure Nothing+ where+ constrainKnownConstructors environment = do+ let ctorNames = [icName ic | SomeInCtor ic <- allInCtors @ci]+ when (not (null ctorNames)) $+ SBV.constrain $+ SBV.sOr+ [ seInputCtor environment SBV..== SBV.literal name+ | name <- ctorNames+ ]++projectionOwnerOverride ::+ forall r.+ (Typeable r) =>+ [ProjectionModel] ->+ ProjectionBaseDescriptor ->+ Maybe r+projectionOwnerOverride projectionModels base =+ listToMaybe+ [ owner+ | projectionModel <- projectionModels,+ projectionDescriptorBase (projectionModelDescriptor projectionModel) == base,+ Just owner <- [projectionModelOwnerAs projectionModel]+ ]++projectionModelRelationSafe :: TranslationStrength -> ProjectionModel -> Bool+projectionModelRelationSafe strength projectionModel =+ all (not . invalidates base) (translationIssues strength)+ where+ base = projectionDescriptorBase (projectionModelDescriptor projectionModel)+ invalidates expected (ConflictingProjectionViews actual) = expected == actual+ invalidates expected (DirectAndProjectedOwnerRead actual) = expected == actual+ invalidates _ _ = False++translationIssues :: TranslationStrength -> [TranslationIssue]+translationIssues ExactTranslation = []+translationIssues (ConservativeOverApproximation issues) = toList issues++-- | Look up @name@ in @res@'s SBV model; on a hit return @fromSym@+-- of the model value, on a miss return @symDefault@. Used by+-- 'symSatExt' to convert SBV's typed model lookups into Haskell+-- values for any 'Sym'-supported slot type.+readModel :: forall r. (Sym r) => SBV.SatResult -> String -> r+readModel res name =+ case SBV.getModelValue name res :: Maybe (SymRep r) of+ Just rep -> fromSym rep+ Nothing -> symDefault++-- | Walk the 'allInCtors' list, find the entry whose 'icName'+-- matches the model's input-constructor tag, then 'extractRegFile'+-- over the matched 'InCtor''s field list and call 'icBuild' to+-- assemble a @ci@. Returns 'Nothing' when no entry matches the tag+-- — this is the case when the predicate over-allocated the+-- @"inputCtor"@ slot (the solver picked a string that isn't any+-- known constructor name, which can happen if the predicate+-- doesn't include any 'PInCtor' atom).+pickCi ::+ forall ci.+ (KnownInCtors ci) =>+ String ->+ (forall r. (Sym r) => String -> Int -> String -> r) ->+ Maybe ci+pickCi tag readField = go (allInCtors @ci)+ where+ go [] = Nothing+ go (SomeInCtor ic@InCtor {} : rest)+ | icName ic == tag =+ let regs = extractRegFileAt 0 (readField (icName ic)) in Just (icBuild ic regs) | otherwise = go rest
test/Keiki/CoreInFlightSpec.hs view
@@ -40,9 +40,11 @@ wcBuild = \(n, ()) -> Echoed n } --- | A minimal 2-vertex transducer with one length-2 edge:+-- | A minimal 2-vertex transducer with one length-2 edge followed by a+-- length-1 self-loop: -- -- False --[guard ci=Begin / output [Started n, Echoed n]]--> True+-- True --[guard ci=Begin / output [Started n]]------------> True multi :: SymTransducer (HsPred '[] MultiInput) '[] Bool MultiInput MultiOutput multi = SymTransducer@@ -65,7 +67,20 @@ mode = Live } ]- True -> [],+ True ->+ [ Edge+ { guard = matchInCtor inCtorBegin,+ update = UKeep,+ output =+ [ pack+ inCtorBegin+ wcStarted+ (OFCons (TInpCtorField inCtorBegin (#payload :: Index '[ '("payload", Int)] Int)) OFNil)+ ],+ target = True,+ mode = Live+ }+ ], initial = False, initialRegs = RNil, isFinal = id@@ -138,6 +153,50 @@ _ -> expectationFailure "chunked and streaming replay disagreed on the final state"++ describe "applyEventsDetailedEither" $ do+ it "returns an empty trace and unchanged settled seed for empty input" $+ case applyEventsDetailedEither multi (False, RNil) [] of+ Right success -> do+ replaySuccessState success `shouldBe` False+ replaySuccessTrace success `shouldBe` []+ Left failure -> expectationFailure ("unexpected failure: " <> show failure)++ it "attributes one two-event edge followed by one one-event edge" $+ let events = [Started 42, Echoed 42, Started 7]+ in case ( applyEventsDetailedEither multi (False, RNil) events,+ applyEventsEither multi (False, RNil) events+ ) of+ (Right detailed, Right (compatibilityState, _)) -> do+ replaySuccessState detailed `shouldBe` compatibilityState+ replaySuccessTrace detailed+ `shouldBe` [ ReplayAttribution+ { replayAttributionEdge = EdgeRef False 0,+ replayAttributionMode = Live,+ replayAttributionSource = False,+ replayAttributionTarget = True,+ replayAttributionSpan = ReplayEventSpan 0 2,+ replayAttributionEventCount = 2+ },+ ReplayAttribution+ { replayAttributionEdge = EdgeRef True 0,+ replayAttributionMode = Live,+ replayAttributionSource = True,+ replayAttributionTarget = True,+ replayAttributionSpan = ReplayEventSpan 2 3,+ replayAttributionEventCount = 1+ }+ ]+ (Left failure, _) -> expectationFailure ("detailed replay failed: " <> show failure)+ (_, Left failure) -> expectationFailure ("compatibility replay failed: " <> show failure)++ it "returns exactly the compatibility truncation failure" $+ case ( applyEventsDetailedEither multi (False, RNil) [Started 42],+ applyEventsEither multi (False, RNil) [Started 42]+ ) of+ (Left detailedFailure, Left compatibilityFailure) ->+ detailedFailure `shouldBe` compatibilityFailure+ _ -> expectationFailure "expected paired truncation failures" where show3 :: Maybe (Bool, x, [MultiOutput]) -> String show3 Nothing = "Nothing"
test/Keiki/FieldProjSpec.hs view
@@ -2,17 +2,43 @@ module Keiki.FieldProjSpec where +import Data.Foldable (toList)+import Data.List.NonEmpty (NonEmpty (..))+import Data.Maybe (isNothing) import Data.Proxy (Proxy (..)) import Data.SBV qualified as SBV import Data.Text (Text) import Data.Text qualified as T import Keiki.Core+import Keiki.ProjectionDomain import Keiki.Symbolic- ( SymEnv (..),+ ( DeadEdgeAnalysisDetail (..),+ DeterminismAnalysisDetail (..),+ KnownInCtors (..),+ PredicateVerification (..),+ PredicateVerificationDetail (..),+ ProjectionBaseDescriptor (..),+ ProjectionDescriptor (..),+ ProjectionModel (..),+ SomeInCtor (..),+ SymEnv (..),+ TranslationIssue (..),+ TranslationStrength (..),+ checkDeadEdgesSym,+ checkDeadEdgesSymDetailed,+ checkTransitionDeterminismSym,+ checkTransitionDeterminismSymDetailed, constrainFieldProjection, mkSymEnv,+ predicateTranslationExact,+ predicateTranslationReport,+ projectionModelKeyAs,+ projectionModelOwnerAs, symIsBot,+ symSatExt, translatePred,+ verifyPredicate,+ verifyPredicateDetailed, ) import Test.Hspec import Test.QuickCheck@@ -235,6 +261,187 @@ numberIntegerW :: FieldWitness NumberAsInteger numberIntegerW = fieldWitness @NumberAsInteger +data BoolKey++instance FieldProjection BoolKey where+ type FieldName BoolKey = "key"+ type FieldOwner BoolKey = Bool+ type FieldResult BoolKey = Text+ fieldShapeId _ = "test.bool-key.v1"+ projectFieldValue _ False = "disabled"+ projectFieldValue _ True = "enabled"++instance ExactFieldProjection BoolKey where+ fieldProjectionDomain _ =+ finiteProjectionDomain ("disabled" :| ["enabled"])+ reconstructFieldOwner _ "disabled" = Just False+ reconstructFieldOwner _ "enabled" = Just True+ reconstructFieldOwner _ _ = Nothing++type BoolOwnerRegs = '[ '("owner", Bool)]++boolKeyW :: FieldWitness BoolKey+boolKeyW = fieldWitness @BoolKey++exactBoolKeyW :: FieldWitness BoolKey+exactBoolKeyW = exactFieldWitness @BoolKey++boolOwnerIx :: Index BoolOwnerRegs Bool+boolOwnerIx = #owner++exhaustiveProjectionPredicate :: HsPred BoolOwnerRegs ()+exhaustiveProjectionPredicate =+ PAnd+ (regProj boolKeyW boolOwnerIx ./= TLit "disabled")+ (regProj boolKeyW boolOwnerIx ./= TLit "enabled")++repeatedProjectionContradiction :: HsPred BoolOwnerRegs ()+repeatedProjectionContradiction =+ regProj boolKeyW boolOwnerIx ./= regProj boolKeyW boolOwnerIx++exactExhaustiveProjectionPredicate :: HsPred BoolOwnerRegs ()+exactExhaustiveProjectionPredicate =+ PAnd+ (regProj exactBoolKeyW boolOwnerIx ./= TLit "disabled")+ (regProj exactBoolKeyW boolOwnerIx ./= TLit "enabled")++exactEnabledProjectionPredicate :: HsPred BoolOwnerRegs ()+exactEnabledProjectionPredicate =+ regProj exactBoolKeyW boolOwnerIx .== TLit "enabled"++data BoolAsInt++instance FieldProjection BoolAsInt where+ type FieldName BoolAsInt = "asInt"+ type FieldOwner BoolAsInt = Bool+ type FieldResult BoolAsInt = Int+ fieldShapeId _ = "test.bool-as-int.v1"+ projectFieldValue _ False = 0+ projectFieldValue _ True = 1++instance ExactFieldProjection BoolAsInt where+ fieldProjectionDomain _ = finiteProjectionDomain (0 :| [1])+ reconstructFieldOwner _ 0 = Just False+ reconstructFieldOwner _ 1 = Just True+ reconstructFieldOwner _ _ = Nothing++exactBoolAsIntW :: FieldWitness BoolAsInt+exactBoolAsIntW = exactFieldWitness @BoolAsInt++data RichOwner = RichOwner Bool Bool+ deriving stock (Eq, Show)++data RichFirst++instance FieldProjection RichFirst where+ type FieldName RichFirst = "first"+ type FieldOwner RichFirst = RichOwner+ type FieldResult RichFirst = Bool+ fieldShapeId _ = "test.rich-owner.v1"+ projectFieldValue _ (RichOwner first _) = first++instance ExactFieldProjection RichFirst where+ fieldProjectionDomain _ = wholeProjectionDomain+ reconstructFieldOwner _ first = Just (RichOwner first False)++data RichSecond++instance FieldProjection RichSecond where+ type FieldName RichSecond = "second"+ type FieldOwner RichSecond = RichOwner+ type FieldResult RichSecond = Bool+ fieldShapeId _ = "test.rich-owner.v1"+ projectFieldValue _ (RichOwner _ second) = second++instance ExactFieldProjection RichSecond where+ fieldProjectionDomain _ = wholeProjectionDomain+ reconstructFieldOwner _ second = Just (RichOwner False second)++exactRichFirstW :: FieldWitness RichFirst+exactRichFirstW = exactFieldWitness @RichFirst++exactRichSecondW :: FieldWitness RichSecond+exactRichSecondW = exactFieldWitness @RichSecond++type RichRegs = '[ '("left", RichOwner), '("right", RichOwner)]++richLeftIx :: Index RichRegs RichOwner+richLeftIx = #left++richRightIx :: Index RichRegs RichOwner+richRightIx = #right++data BrokenRejectInverse++instance FieldProjection BrokenRejectInverse where+ type FieldName BrokenRejectInverse = "brokenReject"+ type FieldOwner BrokenRejectInverse = Bool+ type FieldResult BrokenRejectInverse = Text+ fieldShapeId _ = "test.broken-reject.v1"+ projectFieldValue _ False = "disabled"+ projectFieldValue _ True = "enabled"++instance ExactFieldProjection BrokenRejectInverse where+ fieldProjectionDomain _ = finiteProjectionDomain ("enabled" :| [])+ reconstructFieldOwner _ _ = Nothing++data BrokenRoundTripInverse++instance FieldProjection BrokenRoundTripInverse where+ type FieldName BrokenRoundTripInverse = "brokenRoundTrip"+ type FieldOwner BrokenRoundTripInverse = Bool+ type FieldResult BrokenRoundTripInverse = Text+ fieldShapeId _ = "test.broken-round-trip.v1"+ projectFieldValue _ False = "disabled"+ projectFieldValue _ True = "enabled"++instance ExactFieldProjection BrokenRoundTripInverse where+ fieldProjectionDomain _ = finiteProjectionDomain ("enabled" :| [])+ reconstructFieldOwner _ _ = Just False++data UnderDeclaredDomain++instance FieldProjection UnderDeclaredDomain where+ type FieldName UnderDeclaredDomain = "underDeclared"+ type FieldOwner UnderDeclaredDomain = Bool+ type FieldResult UnderDeclaredDomain = Text+ fieldShapeId _ = "test.under-declared.v1"+ projectFieldValue _ False = "disabled"+ projectFieldValue _ True = "enabled"++instance ExactFieldProjection UnderDeclaredDomain where+ fieldProjectionDomain _ = finiteProjectionDomain ("disabled" :| [])+ reconstructFieldOwner _ "disabled" = Just False+ reconstructFieldOwner _ _ = Nothing++data BoolProjectionCmd = WithOwner Bool | WithoutOwner+ deriving stock (Eq, Show)++type WithOwnerFields = '[ '("owner", Bool)]++withOwnerCtor :: InCtor BoolProjectionCmd WithOwnerFields+withOwnerCtor =+ InCtor+ { icName = "WithOwner",+ icMatch = \case+ WithOwner owner -> Just (RCons (Proxy @"owner") owner RNil)+ WithoutOwner -> Nothing,+ icBuild = \(RCons _ owner RNil) -> WithOwner owner+ }++withoutOwnerCtor :: InCtor BoolProjectionCmd '[]+withoutOwnerCtor =+ InCtor+ { icName = "WithoutOwner",+ icMatch = \case+ WithoutOwner -> Just RNil+ WithOwner _ -> Nothing,+ icBuild = \RNil -> WithoutOwner+ }++instance KnownInCtors BoolProjectionCmd where+ allInCtors = [SomeInCtor withOwnerCtor, SomeInCtor withoutOwnerCtor]+ proveConcreteAgreement :: HsPred rs ci -> (SymEnv -> SBV.Symbolic ()) ->@@ -248,6 +455,78 @@ pure (translated SBV..<=> SBV.literal concrete) pure (not (SBV.modelExists result)) +translationIssuesOf :: HsPred rs ci -> [TranslationIssue]+translationIssuesOf predicate = case predicateTranslationReport predicate of+ ExactTranslation -> []+ ConservativeOverApproximation issues -> toList issues++isConflictingViews :: TranslationIssue -> Bool+isConflictingViews ConflictingProjectionViews {} = True+isConflictingViews _ = False++isDirectAndProjected :: TranslationIssue -> Bool+isDirectAndProjected DirectAndProjectedOwnerRead {} = True+isDirectAndProjected _ = False++isUnguardedProjection :: TranslationIssue -> Bool+isUnguardedProjection UnguardedProjectionInputRead {} = True+isUnguardedProjection _ = False++isOutsideEquality :: TranslationIssue -> Bool+isOutsideEquality ProjectionUsedOutsideEquality {} = True+isOutsideEquality _ = False++data ProjectionAnalysisState = ProjectionAnalysisState+ deriving stock (Eq, Show, Enum, Bounded)++projectionAnalysisEdge ::+ HsPred BoolOwnerRegs () ->+ Edge (HsPred BoolOwnerRegs ()) BoolOwnerRegs () () ProjectionAnalysisState+projectionAnalysisEdge edgeGuard =+ Edge+ { guard = edgeGuard,+ update = UKeep,+ output = [],+ target = ProjectionAnalysisState,+ mode = Live+ }++projectionDeterminismTransducer ::+ SymTransducer+ (HsPred BoolOwnerRegs ())+ BoolOwnerRegs+ ProjectionAnalysisState+ ()+ ()+projectionDeterminismTransducer =+ SymTransducer+ { edgesOut = \ProjectionAnalysisState ->+ [ projectionAnalysisEdge+ (regProj exactBoolKeyW boolOwnerIx .== TLit "disabled"),+ projectionAnalysisEdge+ (regProj exactBoolKeyW boolOwnerIx .== TLit "enabled")+ ],+ initial = ProjectionAnalysisState,+ initialRegs = RCons (Proxy @"owner") False RNil,+ isFinal = const True+ }++projectionDeadEdgeTransducer ::+ SymTransducer+ (HsPred BoolOwnerRegs ())+ BoolOwnerRegs+ ProjectionAnalysisState+ ()+ ()+projectionDeadEdgeTransducer =+ SymTransducer+ { edgesOut = \ProjectionAnalysisState ->+ [projectionAnalysisEdge exactExhaustiveProjectionPredicate],+ initial = ProjectionAnalysisState,+ initialRegs = RCons (Proxy @"owner") False RNil,+ isFinal = const True+ }+ spec :: Spec spec = do describe "concrete field projection" $ do@@ -345,6 +624,230 @@ HsPred '[ '("doc/|\\owner", DocInfo)] () ) `shouldBe` True++ describe "projection verification" $ do+ it "checks every owner and key in the finite exact image" $+ mapM_+ ( \(owner, key) -> do+ checkFieldProjectionOwner exactBoolKeyW owner `shouldBe` Right ()+ checkFieldProjectionKey exactBoolKeyW key `shouldBe` Right owner+ )+ [(False, "disabled"), (True, "enabled")]++ it "does not call a supported but unconstrained projection translation-exact" $ do+ -- Before the conservative classifier, z3 could invent a third Text key+ -- outside the getter's two-value image and verify that fabricated model.+ evalPred+ exhaustiveProjectionPredicate+ (RCons (Proxy @"owner") False RNil)+ ()+ `shouldBe` False+ evalPred+ exhaustiveProjectionPredicate+ (RCons (Proxy @"owner") True RNil)+ ()+ `shouldBe` False+ fieldWitnessHasExactDomain boolKeyW `shouldBe` False+ predicateTranslationExact exhaustiveProjectionPredicate `shouldBe` False+ verifyPredicate exhaustiveProjectionPredicate `shouldReturn` UnverifiedOpaque+ isNothing (symSatExt exhaustiveProjectionPredicate) `shouldBe` True++ it "keeps one-sided emptiness proofs for repeated projection reads" $ do+ predicateTranslationExact repeatedProjectionContradiction `shouldBe` False+ verifyPredicate repeatedProjectionContradiction `shouldReturn` UnverifiedOpaque+ symIsBot repeatedProjectionContradiction `shouldBe` True++ it "keeps ordinary register witness extraction" $ do+ let predicate = TReg boolOwnerIx .== TLit True :: HsPred BoolOwnerRegs ()+ case symSatExt predicate of+ Nothing -> expectationFailure "ordinary Bool register predicate lost its witness"+ Just (registers, command) ->+ evalPred predicate registers command `shouldBe` True++ it "returns no witness instead of throwing on an unguarded input projection" $ do+ let predicate =+ PAnd+ (inpProj boolKeyW withOwnerCtor #owner .== TLit "invented")+ (PInCtor withoutOwnerCtor) ::+ HsPred '[] BoolProjectionCmd+ isNothing (symSatExt predicate) `shouldBe` True++ it "proves the excluded third key unsatisfiable for an exact finite image" $ do+ predicateTranslationReport exactExhaustiveProjectionPredicate+ `shouldBe` ExactTranslation+ verifyPredicate exactExhaustiveProjectionPredicate+ `shouldReturn` VerifiedUnsatisfiable+ symIsBot exactExhaustiveProjectionPredicate `shouldBe` True++ it "returns a typed checked projection model" $ do+ detail <- verifyPredicateDetailed exactEnabledProjectionPredicate+ case detail of+ PredicateSatisfiable ExactTranslation [projectionModel] -> do+ projectionModelKeyAs @Text projectionModel `shouldBe` Just "enabled"+ projectionModelOwnerAs @Bool projectionModel `shouldBe` Just True+ other -> expectationFailure ("expected one exact projection model, got " <> show other)+ verifyPredicate exactEnabledProjectionPredicate+ `shouldReturn` VerifiedSatisfiable++ it "uses a relation-safe projection owner in full witness extraction" $+ case symSatExt exactEnabledProjectionPredicate of+ Nothing -> expectationFailure "expected exact projection owner override"+ Just (registers, ()) -> registers ! boolOwnerIx `shouldBe` True++ it "installs a relation-safe owner into the matching input constructor field" $ do+ let predicate =+ PAnd+ (PInCtor withOwnerCtor)+ (inpProj exactBoolKeyW withOwnerCtor #owner .== TLit "enabled") ::+ HsPred '[] BoolProjectionCmd+ case symSatExt predicate of+ Just (RNil, WithOwner True) -> pure ()+ other -> expectationFailure ("expected WithOwner True, got " <> show (snd <$> other))++ it "keeps path-local models distinct from an inconsistent full owner witness" $ do+ let predicate =+ PAnd+ (regProj exactBoolKeyW boolOwnerIx .== TLit "enabled")+ (regProj exactBoolAsIntW boolOwnerIx .== TLit 0) ::+ HsPred BoolOwnerRegs ()+ detail <- verifyPredicateDetailed predicate+ case detail of+ PredicateSatisfiable (ConservativeOverApproximation _) projectionModels ->+ length projectionModels `shouldBe` 2+ other -> expectationFailure ("expected conservative path models, got " <> show other)+ isNothing (symSatExt predicate) `shouldBe` True++ it "keeps equal display names distinct by structural position in models" $ do+ let first = ZIdx :: Index '[ '("owner", Bool), '("owner", Bool)] Bool+ second = SIdx ZIdx :: Index '[ '("owner", Bool), '("owner", Bool)] Bool+ predicate =+ PAnd+ (regProj exactBoolKeyW first .== TLit "disabled")+ (regProj exactBoolKeyW second .== TLit "enabled") ::+ HsPred '[ '("owner", Bool), '("owner", Bool)] ()+ detail <- verifyPredicateDetailed predicate+ case detail of+ PredicateSatisfiable ExactTranslation projectionModels -> do+ length projectionModels `shouldBe` 2+ fmap (projectionBasePosition . projectionDescriptorBase . projectionModelDescriptor) projectionModels+ `shouldBe` [0, 1]+ other -> expectationFailure ("expected two structural models, got " <> show other)++ it "reports an inverse that rejects an admitted model as a contract violation" $ do+ let witness = exactFieldWitness @BrokenRejectInverse+ predicate =+ regProj witness boolOwnerIx .== TLit "enabled" ::+ HsPred BoolOwnerRegs ()+ detail <- verifyPredicateDetailed predicate+ case detail of+ PredicateProjectionContractViolation ExactTranslation _ message ->+ message `shouldContain` show ProjectionInverseRejectedDomainKey+ other -> expectationFailure ("expected inverse rejection, got " <> show other)+ compatibility <- verifyPredicate predicate+ compatibility `shouldSatisfy` \case+ UnverifiedSolverFailure _ -> True+ _ -> False++ it "reports an inverse getter mismatch as a contract violation" $ do+ let witness = exactFieldWitness @BrokenRoundTripInverse+ predicate =+ regProj witness boolOwnerIx .== TLit "enabled" ::+ HsPred BoolOwnerRegs ()+ detail <- verifyPredicateDetailed predicate+ case detail of+ PredicateProjectionContractViolation ExactTranslation _ message ->+ message `shouldContain` show ProjectionInverseRoundTripMismatch+ other -> expectationFailure ("expected round-trip violation, got " <> show other)++ it "catches an under-declared image only through the owner-side law" $ do+ let witness = exactFieldWitness @UnderDeclaredDomain+ checkFieldProjectionOwner witness True+ `shouldBe` Left ProjectedKeyOutsideDeclaredDomain++ describe "predicate-wide projection translation report" $ do+ it "allows repeated exact reads and the same tag on distinct bases" $ do+ let repeated =+ regProj exactBoolKeyW boolOwnerIx+ .== regProj exactBoolKeyW boolOwnerIx+ distinctBases =+ PAnd+ (regProj exactRichFirstW richLeftIx .== TLit True)+ (regProj exactRichFirstW richRightIx .== TLit False)+ predicateTranslationReport repeated `shouldBe` ExactTranslation+ predicateTranslationReport distinctBases `shouldBe` ExactTranslation++ it "allows distinct exact tags only when their bases differ" $ do+ let separate =+ PAnd+ (regProj exactRichFirstW richLeftIx .== TLit True)+ (regProj exactRichSecondW richRightIx .== TLit False)+ correlated =+ PAnd+ (regProj exactRichFirstW richLeftIx .== TLit True)+ (regProj exactRichSecondW richLeftIx .== TLit False)+ predicateTranslationReport separate `shouldBe` ExactTranslation+ translationIssuesOf correlated `shouldSatisfy` any isConflictingViews++ it "rejects a direct owner read combined with its projection" $ do+ let predicate =+ PAnd+ (TReg boolOwnerIx .== TLit True)+ (regProj exactBoolKeyW boolOwnerIx .== TLit "enabled")+ translationIssuesOf predicate `shouldSatisfy` any isDirectAndProjected++ it "constrains mixed exact/unconstrained occurrences in both orders but reports both inexact" $ do+ let unconstrainedFirst =+ PAnd+ (regProj boolKeyW boolOwnerIx ./= TLit "disabled")+ (regProj exactBoolKeyW boolOwnerIx ./= TLit "enabled")+ exactFirst =+ PAnd+ (regProj exactBoolKeyW boolOwnerIx ./= TLit "enabled")+ (regProj boolKeyW boolOwnerIx ./= TLit "disabled")+ symIsBot unconstrainedFirst `shouldBe` True+ symIsBot exactFirst `shouldBe` True+ predicateTranslationExact unconstrainedFirst `shouldBe` False+ predicateTranslationExact exactFirst `shouldBe` False+ translationIssuesOf unconstrainedFirst `shouldSatisfy` any isConflictingViews+ translationIssuesOf exactFirst `shouldSatisfy` any isConflictingViews++ it "uses logical constructor domination independently of conjunction order" $ do+ let projectionAtom =+ inpProj exactBoolKeyW withOwnerCtor #owner .== TLit "enabled"+ guardFirst = PAnd (PInCtor withOwnerCtor) projectionAtom+ projectionFirst = PAnd projectionAtom (PInCtor withOwnerCtor)+ nonDominating = POr (PInCtor withOwnerCtor) projectionAtom+ predicateTranslationReport guardFirst `shouldBe` ExactTranslation+ predicateTranslationReport projectionFirst `shouldBe` ExactTranslation+ translationIssuesOf nonDominating+ `shouldSatisfy` any isUnguardedProjection++ it "keeps projection ordering and arithmetic conservative" $ do+ let ordered =+ PCmp+ CmpLt+ (regProj exactBoolAsIntW boolOwnerIx)+ (TLit 1)+ arithmetic =+ tadd (regProj exactBoolAsIntW boolOwnerIx) (TLit 1)+ .== TLit 2+ translationIssuesOf ordered `shouldSatisfy` any isOutsideEquality+ translationIssuesOf arithmetic `shouldSatisfy` any isOutsideEquality++ describe "detailed projection analyses" $ do+ it "retains one exact UNSAT result for a disjoint live pair" $ do+ details <- checkTransitionDeterminismSymDetailed projectionDeterminismTransducer+ case details of+ [DeterminismAnalysisDetail _ _ (PredicateUnsatisfiable ExactTranslation)] -> pure ()+ _ -> expectationFailure ("unexpected determinism details: " <> show (length details))+ checkTransitionDeterminismSym projectionDeterminismTransducer `shouldBe` []++ it "retains the exact dead-edge result used by the compatibility warning" $ do+ details <- checkDeadEdgesSymDetailed projectionDeadEdgeTransducer+ case details of+ [DeadEdgeAnalysisDetail _ (PredicateUnsatisfiable ExactTranslation)] -> pure ()+ _ -> expectationFailure ("unexpected dead-edge details: " <> show (length details))+ length (checkDeadEdgesSym projectionDeadEdgeTransducer) `shouldBe` 1 describe "concrete-to-symbolic agreement" $ do it "agrees for register projections in both truth directions" $
+ test/Keiki/ProjectionDomainSpec.hs view
@@ -0,0 +1,324 @@+{-# LANGUAGE TypeFamilies #-}++module Keiki.ProjectionDomainSpec where++import Control.Monad (forM_, replicateM)+import Data.Int (Int32, Int64)+import Data.List.NonEmpty (NonEmpty (..))+import Data.Text (Text)+import Data.Text qualified as T+import Data.Time (UTCTime (..), fromGregorian, secondsToDiffTime)+import Data.Word (Word16, Word32, Word64, Word8)+import Keiki.Core+import Keiki.ProjectionDomain+import Keiki.Symbolic+ ( PredicateVerificationDetail (..),+ Sym (..),+ TranslationIssue (..),+ TranslationStrength (..),+ predicateTranslationReport,+ projectionModelKeyAs,+ projectionModelOwnerAs,+ symIsBot,+ symbolicWholeCarrierExact,+ verifyPredicateDetailed,+ )+import Numeric.Natural (Natural)+import Test.Hspec++expectRight :: (HasCallStack, Show e) => Either e a -> IO a+expectRight (Right value) = pure value+expectRight (Left err) = do+ expectationFailure (show err)+ fail "expected Right"++smallPattern :: TextPattern+smallPattern = either (error . show) id $ do+ chars <- textCharSet ('a' :| ['b'])+ textRepeatBetween 1 2 chars++data SmallTextProjection++instance FieldProjection SmallTextProjection where+ type FieldName SmallTextProjection = "key"+ type FieldOwner SmallTextProjection = Text+ type FieldResult SmallTextProjection = Text+ fieldShapeId _ = "test.small-text.v1"+ projectFieldValue _ = id++instance ExactFieldProjection SmallTextProjection where+ fieldProjectionDomain _ = textProjectionDomain smallPattern+ reconstructFieldOwner _ key+ | matchesTextPattern smallPattern key = Just key+ | otherwise = Nothing++smallTextWitness :: FieldWitness SmallTextProjection+smallTextWitness = exactFieldWitness @SmallTextProjection++type SmallTextRegs = '[ '("owner", Text)]++smallTextOwner :: Index SmallTextRegs Text+smallTextOwner = #owner++-- A schema-local TypeID-v7-shaped key. This fixture intentionally derives its+-- accepted language without depending on the consumer's TypeID package:+-- "order_", followed by a 26-character Crockford Base32 UUID encoding whose+-- leading character cannot overflow 128 bits, whose character 10 encodes UUID+-- version 7, and whose character 13 encodes the RFC 4122 variant.+newtype OrderTypeIdOwner = OrderTypeIdOwner Text+ deriving stock (Eq, Show)++data OrderTypeIdText++orderTypeIdPattern :: TextPattern+orderTypeIdPattern = either (error . show) id $ do+ prefix <- textLiteral "order_"+ leading <- textCharSet ('0' :| "1234567")+ crockford <- textCharSet ('0' :| "123456789abcdefghjkmnpqrstvwxyz")+ version <- textCharSet ('e' :| "f")+ variant <- textCharSet ('8' :| "9abrstv")+ beforeVersion <- textRepeatBetween 9 9 crockford+ beforeVariant <- textRepeatBetween 2 2 crockford+ afterVariant <- textRepeatBetween 12 12 crockford+ pure+ ( textConcat+ ( prefix+ :| [ leading,+ beforeVersion,+ version,+ beforeVariant,+ variant,+ afterVariant+ ]+ )+ )++instance FieldProjection OrderTypeIdText where+ type FieldName OrderTypeIdText = "typeId"+ type FieldOwner OrderTypeIdText = OrderTypeIdOwner+ type FieldResult OrderTypeIdText = Text+ fieldShapeId _ = "test.order-type-id.v7"+ projectFieldValue _ (OrderTypeIdOwner value) = value++instance ExactFieldProjection OrderTypeIdText where+ fieldProjectionDomain _ = textProjectionDomain orderTypeIdPattern+ reconstructFieldOwner _ value+ | matchesTextPattern orderTypeIdPattern value = Just (OrderTypeIdOwner value)+ | otherwise = Nothing++orderTypeIdWitness :: FieldWitness OrderTypeIdText+orderTypeIdWitness = exactFieldWitness @OrderTypeIdText++type OrderTypeIdRegs = '[ '("owner", OrderTypeIdOwner)]++orderTypeIdOwner :: Index OrderTypeIdRegs OrderTypeIdOwner+orderTypeIdOwner = #owner++orderTypeIdSuffix :: Text+orderTypeIdSuffix = "01h455vb4pex5vsknk084sn02q"++orderTypeIdSample :: Text+orderTypeIdSample = "order_" <> orderTypeIdSuffix++replaceTextAt :: Int -> Char -> Text -> Text+replaceTextAt position replacement value =+ T.take position value <> T.singleton replacement <> T.drop (position + 1) value++replaceSuffixAt :: Int -> Char -> Text+replaceSuffixAt position replacement =+ replaceTextAt (T.length "order_" + position) replacement orderTypeIdSample++leapSecondValue :: UTCTime+leapSecondValue = UTCTime (fromGregorian 2016 12 31) (secondsToDiffTime 86400)++data FiniteLeapSecond++instance FieldProjection FiniteLeapSecond where+ type FieldName FiniteLeapSecond = "leap"+ type FieldOwner FiniteLeapSecond = UTCTime+ type FieldResult FiniteLeapSecond = UTCTime+ fieldShapeId _ = "test.finite-leap-second.v1"+ projectFieldValue _ = id++instance ExactFieldProjection FiniteLeapSecond where+ fieldProjectionDomain _ = finiteProjectionDomain (leapSecondValue :| [])+ reconstructFieldOwner _ value+ | value == leapSecondValue = Just value+ | otherwise = Nothing++finiteLeapSecondWitness :: FieldWitness FiniteLeapSecond+finiteLeapSecondWitness = exactFieldWitness @FiniteLeapSecond++data FiniteHighText++instance FieldProjection FiniteHighText where+ type FieldName FiniteHighText = "highText"+ type FieldOwner FiniteHighText = Text+ type FieldResult FiniteHighText = Text+ fieldShapeId _ = "test.finite-high-text.v1"+ projectFieldValue _ = id++instance ExactFieldProjection FiniteHighText where+ fieldProjectionDomain _ =+ finiteProjectionDomain (T.singleton '\x30000' :| [])+ reconstructFieldOwner _ value+ | value == T.singleton '\x30000' = Just value+ | otherwise = Nothing++finiteHighTextWitness :: FieldWitness FiniteHighText+finiteHighTextWitness = exactFieldWitness @FiniteHighText++spec :: Spec+spec = describe "projection domain" $ do+ it "deduplicates finite values while preserving membership" $ do+ let domain =+ finiteProjectionDomain ("open" :| ["closed", "open"]) ::+ ProjectionDomain Text+ memberProjectionDomain domain "open" `shouldBe` True+ memberProjectionDomain domain "closed" `shouldBe` True+ memberProjectionDomain domain "invented" `shouldBe` False++ it "matches literals as complete strings" $ do+ textPattern <- expectRight (textLiteral "type_")+ matchesTextPattern textPattern "type_" `shouldBe` True+ matchesTextPattern textPattern "type_value" `shouldBe` False++ it "composes sets, ranges, alternation, and bounded repetition" $ do+ prefix <- expectRight (textLiteral "id_")+ lower <- expectRight (textCharRanges (('a', 'z') :| []))+ digits <- expectRight (textCharSet ('0' :| ['1']))+ suffix <- expectRight (textRepeatBetween 2 3 digits)+ let textPattern = textConcat (prefix :| [textAlternation (lower :| [digits]), suffix])+ matchesTextPattern textPattern "id_a01" `shouldBe` True+ matchesTextPattern textPattern "id_1011" `shouldBe` True+ matchesTextPattern textPattern "id_a0" `shouldBe` False+ matchesTextPattern textPattern "id_A01" `shouldBe` False+ matchesTextPattern textPattern "xid_a01" `shouldBe` False++ it "gives the pure matcher and SBV compiler the same small language" $ do+ let samples = T.pack <$> concatMap (`replicateM` "abx") [0 .. 3]+ forM_ samples $ \sample -> do+ let concrete = matchesTextPattern smallPattern sample+ predicate =+ regProj smallTextWitness smallTextOwner .== TLit sample ::+ HsPred SmallTextRegs ()+ symIsBot predicate `shouldBe` not concrete++ it "checks both directions of an exact witness declaration" $ do+ checkFieldProjectionOwner smallTextWitness "ab" `shouldBe` Right ()+ checkFieldProjectionKey smallTextWitness "ba" `shouldBe` Right "ba"+ checkFieldProjectionOwner smallTextWitness "x"+ `shouldBe` Left ProjectedKeyOutsideDeclaredDomain++ it "classifies every curated whole carrier conservatively" $ do+ symbolicWholeCarrierExact @Bool `shouldBe` True+ symbolicWholeCarrierExact @Int `shouldBe` False+ symbolicWholeCarrierExact @Integer `shouldBe` True+ symbolicWholeCarrierExact @Natural `shouldBe` True+ symbolicWholeCarrierExact @Text `shouldBe` False+ symbolicWholeCarrierExact @UTCTime `shouldBe` False+ symbolicWholeCarrierExact @Word64 `shouldBe` True+ symbolicWholeCarrierExact @Word32 `shouldBe` True+ symbolicWholeCarrierExact @Word16 `shouldBe` True+ symbolicWholeCarrierExact @Word8 `shouldBe` True+ symbolicWholeCarrierExact @Int64 `shouldBe` True+ symbolicWholeCarrierExact @Int32 `shouldBe` True++ it "keeps leap-second UTCTime values out of the whole-carrier claim" $ do+ fromSym (toSym leapSecondValue) `shouldNotBe` leapSecondValue++ it "rejects non-representable literals from otherwise finite domains" $ do+ let leapOwner = ZIdx :: Index '[ '("owner", UTCTime)] UTCTime+ leapPredicate =+ regProj finiteLeapSecondWitness leapOwner+ .== TLit (fromSym (toSym leapSecondValue)) ::+ HsPred '[ '("owner", UTCTime)] ()+ textOwner = ZIdx :: Index '[ '("owner", Text)] Text+ textPredicate =+ regProj finiteHighTextWitness textOwner .== TLit "ordinary" ::+ HsPred '[ '("owner", Text)] ()+ predicateTranslationReport leapPredicate `shouldSatisfy` hasUnsupportedDomain+ predicateTranslationReport textPredicate `shouldSatisfy` hasUnsupportedDomain+ symIsBot leapPredicate `shouldBe` False+ symIsBot textPredicate `shouldBe` False++ it "rejects reversed ranges and repetition intervals" $ do+ textCharRanges (('z', 'a') :| [])+ `shouldBe` Left (ReversedCharacterRange 'z' 'a')+ literal <- expectRight (textLiteral "x")+ textRepeatBetween 2 1 literal+ `shouldBe` Left (InvalidRepetitionInterval 2 1)+ let tooLarge = fromIntegral (maxBound :: Int) + 1+ textRepeatBetween tooLarge tooLarge literal+ `shouldBe` Left (RepetitionBoundTooLarge tooLarge)+ textRepeatBetween 0 tooLarge literal+ `shouldBe` Left (RepetitionBoundTooLarge tooLarge)++ it "accepts U+2FFFF and rejects U+30000 in every character constructor" $ do+ textLiteral (T.singleton maximumSmtCodePoint) `shouldSatisfy` isRight+ textCharSet (maximumSmtCodePoint :| []) `shouldSatisfy` isRight+ textCharRanges ((maximumSmtCodePoint, maximumSmtCodePoint) :| [])+ `shouldSatisfy` isRight+ let firstUnrepresentable = '\x30000'+ textLiteral (T.singleton firstUnrepresentable)+ `shouldBe` Left (CodePointAboveSmtMaximum firstUnrepresentable)+ textCharSet (firstUnrepresentable :| [])+ `shouldBe` Left (CodePointAboveSmtMaximum firstUnrepresentable)+ textCharRanges ((firstUnrepresentable, firstUnrepresentable) :| [])+ `shouldBe` Left (CodePointAboveSmtMaximum firstUnrepresentable)++ describe "TypeID-v7-shaped exact text domain" $ do+ let accepted =+ orderTypeIdSample+ : replaceSuffixAt 0 '7'+ : replaceSuffixAt 10 'f'+ : [replaceSuffixAt 13 variant | variant <- "89abrstv"]+ rejected =+ [ "",+ orderTypeIdSuffix,+ "user_" <> orderTypeIdSuffix,+ "order__" <> orderTypeIdSuffix,+ T.dropEnd 1 orderTypeIdSample,+ orderTypeIdSample <> "0",+ replaceSuffixAt 0 '8',+ replaceSuffixAt 1 'i',+ replaceSuffixAt 1 'l',+ replaceSuffixAt 1 'o',+ replaceSuffixAt 1 'u',+ replaceSuffixAt 1 'H',+ replaceSuffixAt 1 '_',+ replaceSuffixAt 10 'd',+ replaceSuffixAt 10 'g',+ replaceSuffixAt 13 'c'+ ]+ predicate sample =+ regProj orderTypeIdWitness orderTypeIdOwner .== TLit sample ::+ HsPred OrderTypeIdRegs ()++ it "accepts every version/variant boundary and rejects malformed boundaries" $ do+ forM_ accepted $ \sample -> do+ matchesTextPattern orderTypeIdPattern sample `shouldBe` True+ symIsBot (predicate sample) `shouldBe` False+ forM_ rejected $ \sample -> do+ matchesTextPattern orderTypeIdPattern sample `shouldBe` False+ symIsBot (predicate sample) `shouldBe` True++ it "reconstructs and round-trips every accepted boundary model" $+ forM_ accepted $ \sample -> do+ checkFieldProjectionKey orderTypeIdWitness sample+ `shouldBe` Right (OrderTypeIdOwner sample)+ detail <- verifyPredicateDetailed (predicate sample)+ case detail of+ PredicateSatisfiable ExactTranslation [projectionModel] -> do+ projectionModelKeyAs @Text projectionModel `shouldBe` Just sample+ projectionModelOwnerAs @OrderTypeIdOwner projectionModel+ `shouldBe` Just (OrderTypeIdOwner sample)+ other -> expectationFailure ("expected one exact TypeID model, got " <> show other)+ where+ isRight (Right _) = True+ isRight (Left _) = False+ hasUnsupportedDomain (ConservativeOverApproximation issues) =+ any isUnsupportedDomain issues+ hasUnsupportedDomain ExactTranslation = False+ isUnsupportedDomain UnsupportedProjectionDomain {} = True+ isUnsupportedDomain _ = False
test/Keiki/ReplayEitherSpec.hs view
@@ -1,5 +1,6 @@ module Keiki.ReplayEitherSpec (spec) where +import Data.Text qualified as T import Data.Time (UTCTime (..), fromGregorian, secondsToDiffTime) import Keiki.Core import Keiki.Fixtures.UserRegistration@@ -25,6 +26,24 @@ AccountDeleted (AccountDeletedData "alice@x" (t 300)) ] +longLog :: [UserEvent]+longLog =+ RegistrationStarted (RegistrationStartedData "alice@x" "C0000" (t 0))+ : ConfirmationEmailSent (ConfirmationEmailSentData "alice@x")+ : [ ConfirmationResent+ (ConfirmationResentData "alice@x" (T.pack ("C" <> pad4 i)) (t (fromIntegral i)))+ | i <- [1 .. 1020 :: Int]+ ]+ ++ [ AccountConfirmed (AccountConfirmedData "alice@x" "C1020" (t 2000)),+ AccountDeleted (AccountDeletedData "alice@x" (t 3000))+ ]+ where+ pad4 n+ | n < 10 = "000" <> show n+ | n < 100 = "00" <> show n+ | n < 1000 = "0" <> show n+ | otherwise = show n+ type Snapshot = (Email, ConfirmationCode, UTCTime, UTCTime, UTCTime) snapshot :: RegFile UserRegRegs -> Snapshot@@ -135,6 +154,14 @@ Nothing -> pure () Just _ -> expectationFailure "expected Nothing from compatibility wrapper" +shouldReturnSameLeft :: (Eq failure, Show failure) => Either failure detailed -> Either failure compatibility -> Expectation+shouldReturnSameLeft detailed compatibility =+ case (detailed, compatibility) of+ (Left detailedFailure, Left compatibilityFailure) ->+ detailedFailure `shouldBe` compatibilityFailure+ (Right _, _) -> expectationFailure "detailed replay unexpectedly succeeded"+ (_, Right _) -> expectationFailure "compatibility replay unexpectedly succeeded"+ spec :: Spec spec = do singleStepSpec@@ -247,6 +274,45 @@ case applyEventsEither userReg (initial userReg, initialRegs userReg) corrupted of Left _ -> pure () Right _ -> expectationFailure "applyEventsEither accepted corrupted log"++ describe "detailed replay compatibility" $ do+ it "preserves no-inversion failures exactly" $+ let events = [AccountConfirmed (AccountConfirmedData "alice@x" "Z9F4" (t 0))]+ in shouldReturnSameLeft+ (reconstituteDetailedEither userReg events)+ (reconstituteEither userReg events)++ it "preserves ambiguous-inversion failures exactly" $+ shouldReturnSameLeft+ (applyEventsDetailedEither ambiguousUserReg (PotentialCustomer, initialRegs ambiguousUserReg) [headEvent])+ (applyEventsEither ambiguousUserReg (PotentialCustomer, initialRegs ambiguousUserReg) [headEvent])++ it "preserves queue-mismatch failures exactly" $+ let observed = AccountDeleted (AccountDeletedData "alice@x" (t 999))+ corrupted = headEvent : observed : drop 2 canonicalLog+ in shouldReturnSameLeft+ (reconstituteDetailedEither userReg corrupted)+ (reconstituteEither userReg corrupted)++ it "preserves truncation failures exactly" $+ shouldReturnSameLeft+ (reconstituteDetailedEither userReg [headEvent])+ (reconstituteEither userReg [headEvent])++ it "replays 1,024 events through compatibility and detailed paths" $+ case ( applyEventsEither userReg (initial userReg, initialRegs userReg) longLog,+ reconstituteEither userReg longLog,+ reconstituteDetailedEither userReg longLog+ ) of+ (Right (applyState, _), Right (reconstituteState, _), Right detailed) -> do+ (applyState, reconstituteState, replaySuccessState detailed)+ `shouldBe` (Deleted, Deleted, Deleted)+ length (replaySuccessTrace detailed) `shouldBe` 1023+ replayAttributionSpan (last (replaySuccessTrace detailed))+ `shouldBe` ReplayEventSpan 1023 1024+ (Left failure, _, _) -> expectationFailure ("applyEventsEither failed: " <> show failure)+ (_, Left failure, _) -> expectationFailure ("reconstituteEither failed: " <> show failure)+ (_, _, Left failure) -> expectationFailure ("detailed replay failed: " <> show failure) describe "former Decider behavioral coverage" $ do it "replays the complete multi-event output of one forward step" $ do
test/Keiki/ReplayOnlySpec.hs view
@@ -258,21 +258,41 @@ (Left failure, _) -> expectationFailure ("machine A replay failed: " <> show failure) (_, Left failure) -> expectationFailure ("machine B replay failed: " <> show failure) - it "prefers the live edge when a sloppy twin's guard overlaps it" $- case reconstituteEither machineOverlap [ReservationConfirmed False] of- Right (v, regs) -> do- v `shouldBe` Confirmed+ it "prefers and attributes the live edge when a sloppy twin overlaps it" $+ case reconstituteDetailedEither machineOverlap [ReservationConfirmed False] of+ Right success -> do+ replaySuccessState success `shouldBe` Confirmed -- The live edge writes the event's own acuity (False); the -- sloppy twin would have written the constant True. Live wins.- regs ! #wasBlack `shouldBe` False+ replaySuccessRegs success ! #wasBlack `shouldBe` False+ replaySuccessTrace success+ `shouldBe` [ ReplayAttribution+ { replayAttributionEdge = EdgeRef Held 0,+ replayAttributionMode = Live,+ replayAttributionSource = Held,+ replayAttributionTarget = Confirmed,+ replayAttributionSpan = ReplayEventSpan 0 1,+ replayAttributionEventCount = 1+ }+ ] Left failure -> expectationFailure ("expected live-phase attribution: " <> show failure) - it "falls through to the sloppy twin only for unattributable history" $- case reconstituteEither machineOverlap blackHistory of- Right (v, regs) -> do- v `shouldBe` Confirmed- regs ! #wasBlack `shouldBe` True+ it "falls through to and attributes the sloppy twin for historical input" $+ case reconstituteDetailedEither machineOverlap blackHistory of+ Right success -> do+ replaySuccessState success `shouldBe` Confirmed+ replaySuccessRegs success ! #wasBlack `shouldBe` True+ replaySuccessTrace success+ `shouldBe` [ ReplayAttribution+ { replayAttributionEdge = EdgeRef Held 1,+ replayAttributionMode = ReplayOnly,+ replayAttributionSource = Held,+ replayAttributionTarget = Confirmed,+ replayAttributionSpan = ReplayEventSpan 0 1,+ replayAttributionEventCount = 1+ }+ ] Left failure -> expectationFailure ("twin fallthrough failed: " <> show failure) it "still reports ambiguity between two replay-only candidates" $
test/Keiki/RoundTrip.hs view
@@ -20,12 +20,18 @@ import Data.Time (UTCTime) import Data.Time.Clock.POSIX (posixSecondsToUTCTime) import Keiki.Core- ( HsPred,+ ( Edge (..),+ EdgeRef (..),+ HsPred, RegFile,+ ReplayAttribution (..),+ ReplayEventSpan (..), ReplayFailure,+ ReplaySuccess (..), SymTransducer (..), applyEventsEither, defaultValidationOptions,+ reconstituteDetailedEither, reconstituteEither, step, validateTransducer,@@ -98,6 +104,8 @@ wholeLogProperty transducer genCommand observe it "P2: chunked replay agrees at every command boundary" $ chunkedProperty transducer genCommand observe+ it "P3: detailed replay attributes a complete contiguous edge path" $+ attributionProperty transducer genCommand observe mapM_ (tamperSpec transducer genCommand observe) tamperCases -- | Run the replay laws without forcing validation. This is reserved for a@@ -111,6 +119,8 @@ wholeLogProperty transducer genCommand observe it "P2: chunked replay agrees at every command boundary" $ chunkedProperty transducer genCommand observe+ it "P3: detailed replay attributes a complete contiguous edge path" $+ attributionProperty transducer genCommand observe mapM_ (tamperSpec transducer genCommand observe) tamperCases teethSpec :: RoundTripFixture -> Spec@@ -181,6 +191,115 @@ <> renderState actualState (observe actualState actualRegs) ) +attributionProperty ::+ (Eq s, Show s, Show ci, Eq co, Show co) =>+ SymTransducer (HsPred rs ci) rs s ci co ->+ (s -> RegFile rs -> Gen ci) ->+ (s -> RegFile rs -> Text) ->+ Property+attributionProperty transducer genCommand observe =+ forAllCommands transducer genCommand $ \commands ->+ let run = forwardRun transducer observe commands+ compatibility = reconstituteEither transducer run.frEvents+ detailed = reconstituteDetailedEither transducer run.frEvents+ context =+ renderRun run+ <> "\ncompatibility replay: "+ <> renderReplay observe compatibility+ <> "\ndetailed replay: "+ <> renderDetailedReplay observe detailed+ in counterexample context case (compatibility, detailed) of+ (Left _, _) -> property False+ (_, Left _) -> property False+ (Right (compatibilityState, compatibilityRegs), Right success) ->+ case validateDetailedTrace transducer observe run.frEvents success of+ Left message -> counterexample message (property False)+ Right () ->+ ( compatibilityState,+ observe compatibilityState compatibilityRegs,+ replaySuccessState success,+ observe (replaySuccessState success) (replaySuccessRegs success)+ )+ === ( run.frFinalState,+ run.frFinalObservation,+ run.frFinalState,+ run.frFinalObservation+ )++validateDetailedTrace ::+ (Eq s, Show s) =>+ SymTransducer phi rs s ci co ->+ (s -> RegFile rs -> Text) ->+ [co] ->+ ReplaySuccess rs s ->+ Either String ()+validateDetailedTrace transducer observe events success =+ case events of+ [] -> do+ require (null trace) "empty event log produced a non-empty attribution trace"+ require+ ( replaySuccessState success == transducer.initial+ && observe (replaySuccessState success) (replaySuccessRegs success)+ == observe transducer.initial transducer.initialRegs+ )+ "empty event log changed the replay seed"+ _ -> case trace of+ [] -> Left "non-empty event log produced an empty attribution trace"+ firstAttribution : remainingAttributions -> do+ let finalAttribution = foldl (\_ current -> current) firstAttribution remainingAttributions+ require+ (replaySpanStart (replayAttributionSpan firstAttribution) == 0)+ "first attribution span did not start at zero"+ require+ (replaySpanEnd (replayAttributionSpan finalAttribution) == length events)+ "last attribution span did not end at the event-log length"+ mapM_ checkAttribution trace+ mapM_ checkAdjacent (zip trace (drop 1 trace))+ require+ (replayAttributionTarget finalAttribution == replaySuccessState success)+ "last attribution target did not equal the replay result state"+ where+ trace = replaySuccessTrace success++ checkAttribution attribution = do+ let span' = replayAttributionSpan attribution+ count = replayAttributionEventCount attribution+ source = replayAttributionSource attribution+ ref = replayAttributionEdge attribution+ require (count > 0) ("non-positive attribution event count: " <> show attribution)+ require+ (replaySpanEnd span' - replaySpanStart span' == count)+ ("span length disagreed with event count: " <> show attribution)+ require+ (edgeSource ref == source)+ ("edge reference source disagreed with attribution source: " <> show attribution)+ require (edgeIndex ref >= 0) ("negative edge reference index: " <> show attribution)+ case drop (edgeIndex ref) (edgesOut transducer source) of+ [] -> Left ("edge reference did not resolve: " <> show ref)+ edge : _ -> do+ require+ (mode edge == replayAttributionMode attribution)+ ("resolved edge mode disagreed with attribution: " <> show attribution)+ require+ (target edge == replayAttributionTarget attribution)+ ("resolved edge target disagreed with attribution: " <> show attribution)+ require+ (length (output edge) == count)+ ("resolved edge output length disagreed with attribution: " <> show attribution)++ checkAdjacent (left, right) = do+ require+ ( replaySpanEnd (replayAttributionSpan left)+ == replaySpanStart (replayAttributionSpan right)+ )+ ("attribution spans had a gap or overlap: " <> show (left, right))+ require+ (replayAttributionTarget left == replayAttributionSource right)+ ("attribution entries did not form a state path: " <> show (left, right))++ require True _ = Right ()+ require False message = Left message+ tamperSpec :: (Eq s, Show s, Show ci, Eq co, Show co) => SymTransducer (HsPred rs ci) rs s ci co ->@@ -309,6 +428,22 @@ renderReplay observe = \case Left failure -> "Left " <> show failure Right (state, regs) -> "Right (" <> renderState state (observe state regs) <> ")"++renderDetailedReplay ::+ (Show s, Show co) =>+ (s -> RegFile rs -> Text) ->+ Either (ReplayFailure s co) (ReplaySuccess rs s) ->+ String+renderDetailedReplay observe = \case+ Left failure -> "Left " <> show failure+ Right success ->+ "Right ("+ <> renderState+ (replaySuccessState success)+ (observe (replaySuccessState success) (replaySuccessRegs success))+ <> ", trace="+ <> show (replaySuccessTrace success)+ <> ")" renderChunkResult :: (Show s) => Either String (s, RegFile rs) -> String renderChunkResult = \case
test/Keiki/StepEitherSpec.hs view
@@ -6,7 +6,7 @@ -- Vertices: 0 has two always-true edges (ambiguous); 1 has one -- always-false edge (no match); 2 has no edges; 3 has one always-true -- edge (the normal accepting case).-data V = V0 | V1 | V2 | V3 | VEnd+data V = V0 | V1 | V2 | V3 | VReplay | VEnd deriving stock (Eq, Show) -- A no-op output term is awkward to build generically; instead each@@ -24,12 +24,72 @@ V1 -> [Edge {guard = PBot, update = UKeep, output = [], target = VEnd, mode = Live}] V2 -> [] V3 -> [Edge {guard = PTop, update = UKeep, output = [], target = VEnd, mode = Live}]+ VReplay -> [Edge {guard = PTop, update = UKeep, output = [], target = VEnd, mode = ReplayOnly}] VEnd -> [], initial = V0, initialRegs = RNil, isFinal = (== VEnd) } +data IdentityCommand = ChooseFirst | ChooseSecond+ deriving stock (Eq, Show)++data IdentityEvent = Chosen+ deriving stock (Eq, Show)++firstCtor :: InCtor IdentityCommand '[]+firstCtor =+ InCtor+ { icName = "ChooseFirst",+ icMatch = \case ChooseFirst -> Just RNil; _ -> Nothing,+ icBuild = \RNil -> ChooseFirst+ }++secondCtor :: InCtor IdentityCommand '[]+secondCtor =+ InCtor+ { icName = "ChooseSecond",+ icMatch = \case ChooseSecond -> Just RNil; _ -> Nothing,+ icBuild = \RNil -> ChooseSecond+ }++chosenWire :: WireCtor IdentityEvent ()+chosenWire =+ WireCtor+ { wcName = "Chosen",+ wcMatch = \case Chosen -> Just (),+ wcBuild = \() -> Chosen+ }++-- The two live siblings are behaviorally indistinguishable after erasure:+-- they preserve the same registers, reach the same target, and emit equal+-- values. Only their local edge references distinguish them.+identityFixture :: SymTransducer (HsPred '[] IdentityCommand) '[] V IdentityCommand IdentityEvent+identityFixture =+ SymTransducer+ { edgesOut = \case+ V0 ->+ [ Edge+ { guard = matchInCtor firstCtor,+ update = UKeep,+ output = [pack firstCtor chosenWire oNil],+ target = VEnd,+ mode = Live+ },+ Edge+ { guard = matchInCtor secondCtor,+ update = UKeep,+ output = [pack secondCtor chosenWire oNil],+ target = VEnd,+ mode = Live+ }+ ]+ _ -> [],+ initial = V0,+ initialRegs = RNil,+ isFinal = (== VEnd)+ }+ -- NOTE: 'RegFile' has no 'Eq'/'Show' instance (verified 2026-06-06), so we -- cannot 'shouldBe' a whole 'Either (StepFailure V) (V, RegFile '[], [String])'. -- The failure ('Left') values carry no register data and ARE 'Eq'/'Show', so@@ -85,3 +145,59 @@ (Just (s1, _r1, e1), Right (s2, _r2, e2)) -> (s1, e1) `shouldBe` (s2, e2) (Nothing, _) -> expectationFailure "step returned Nothing on the accepting edge" (_, Left f) -> expectationFailure ("stepEither returned Left: " <> show f)++ describe "stepDetailedEither" $ do+ it "distinguishes behaviorally identical guarded siblings by local EdgeRef" $+ case ( stepDetailedEither identityFixture (V0, RNil) ChooseFirst,+ stepDetailedEither identityFixture (V0, RNil) ChooseSecond,+ stepEither identityFixture (V0, RNil) ChooseFirst,+ stepEither identityFixture (V0, RNil) ChooseSecond+ ) of+ (Right first, Right second, Right (firstState, _, firstOut), Right (secondState, _, secondOut)) -> do+ stepSuccessEdge first `shouldBe` EdgeRef V0 0+ stepSuccessEdge second `shouldBe` EdgeRef V0 1+ stepSuccessMode first `shouldBe` Live+ stepSuccessMode second `shouldBe` Live+ (stepSuccessState first, stepSuccessOutputs first)+ `shouldBe` (firstState, firstOut)+ (stepSuccessState second, stepSuccessOutputs second)+ `shouldBe` (secondState, secondOut)+ (firstState, firstOut) `shouldBe` (secondState, secondOut)+ _ -> expectationFailure "expected four successful stepping results"++ it "attributes an accepted epsilon-output edge" $+ case stepDetailedEither fixture (V3, RNil) True of+ Right success -> do+ stepSuccessEdge success `shouldBe` EdgeRef V3 0+ stepSuccessMode success `shouldBe` Live+ (stepSuccessState success, stepSuccessOutputs success) `shouldBe` (VEnd, [])+ Left failure -> expectationFailure ("expected Right, got " <> show failure)++ it "never selects a replay-only edge during forward stepping" $ do+ let expected =+ NoMatchingEdge+ VReplay+ [ RejectedEdgeSummary+ { rejectedEdge = EdgeRef VReplay 0,+ rejectedTarget = VEnd,+ rejectedGuard = False+ }+ ]+ case (stepDetailedEither fixture (VReplay, RNil) True, stepEither fixture (VReplay, RNil) True) of+ (Left detailedFailure, Left compatibilityFailure) -> do+ detailedFailure `shouldBe` expected+ compatibilityFailure `shouldBe` expected+ _ -> expectationFailure "expected replay-only edge rejection"++ it "returns exactly the compatibility failures" $ do+ let cases = [(V0, True), (V1, True), (V2, True)]+ mapM_+ ( \(source, command) ->+ case ( stepDetailedEither fixture (source, RNil) command,+ stepEither fixture (source, RNil) command+ ) of+ (Left detailedFailure, Left compatibilityFailure) ->+ detailedFailure `shouldBe` compatibilityFailure+ _ -> expectationFailure "expected paired failures"+ )+ cases
test/Keiki/SymbolicSpec.hs view
@@ -18,6 +18,8 @@ -- | A two-constructor input symbol for the 'PInCtor' tests. data TinyCmd = TinyFoo Int | TinyBar Int deriving (Eq, Show) +data OpaqueCarrier = OpaqueLeft | OpaqueRight deriving (Eq, Show)+ -- * Numeric-registry fixtures (EP-41 M1) --------------------------------- -- | A single-slot register file whose value type is the money/count@@ -438,6 +440,48 @@ PEq (TApp1 id (lit (1 :: Integer))) (lit 1) :: HsPred '[] AmtCmd predicateTranslationExact opaque `shouldBe` False verifyPredicate opaque `shouldReturn` UnverifiedOpaque++ describe "predicate verification classification" $ do+ it "keeps unsupported projection results unverified" $ do+ let unsupported =+ FieldProj.docNumbersW `regProj` FieldProj.docIx .== TLit [] ::+ HsPred FieldProj.DocRegs ()+ predicateTranslationExact unsupported `shouldBe` False+ verifyPredicate unsupported `shouldReturn` UnverifiedOpaque++ it "keeps supported but unconstrained projection results unverified" $ do+ predicateTranslationExact FieldProj.exhaustiveProjectionPredicate+ `shouldBe` False+ verifyPredicate FieldProj.exhaustiveProjectionPredicate+ `shouldReturn` UnverifiedOpaque++ it "keeps opaque applications unverified and rejects their fabricated witness" $ do+ let opaque =+ PEq (TApp1 (const False) (TLit ())) (TLit True) :: HsPred '[] ()+ predicateTranslationExact opaque `shouldBe` False+ verifyPredicate opaque `shouldReturn` UnverifiedOpaque+ isNothing (symSatExt opaque) `shouldBe` True++ it "rejects a fabricated non-Sym equality witness" $ do+ let fallback =+ PEq (TLit OpaqueLeft) (TLit OpaqueRight) :: HsPred '[] ()+ predicateTranslationExact fallback `shouldBe` False+ verifyPredicate fallback `shouldReturn` UnverifiedOpaque+ isNothing (symSatExt fallback) `shouldBe` True++ it "verifies ordinary exact scalars in both solver directions" $ do+ let satisfiable = PEq (TLit True) (TLit True) :: HsPred '[] ()+ unsatisfiable = PEq (TLit True) (TLit False) :: HsPred '[] ()+ predicateTranslationExact satisfiable `shouldBe` True+ predicateTranslationExact unsatisfiable `shouldBe` True+ verifyPredicate satisfiable `shouldReturn` VerifiedSatisfiable+ verifyPredicate unsatisfiable `shouldReturn` VerifiedUnsatisfiable++ it "verifies supported structural arithmetic" $ do+ let arithmetic =+ PEq (tadd (TLit (2 :: Int)) (TLit 3)) (TLit 5) :: HsPred '[] ()+ predicateTranslationExact arithmetic `shouldBe` True+ verifyPredicate arithmetic `shouldReturn` VerifiedSatisfiable describe "ordering predicate PCmp (EP-41 M2)" $ do it "constant contradiction 5 >= 10 over Word64 is symIsBot" $
test/Spec.hs view
@@ -26,6 +26,7 @@ import Keiki.OperatorsQualifiedSpec qualified import Keiki.OperatorsSpec qualified import Keiki.ProfunctorSpec qualified+import Keiki.ProjectionDomainSpec qualified import Keiki.RecomputeVerifySpec qualified import Keiki.Render.InspectorSpec qualified import Keiki.Render.MarkdownSpec qualified@@ -70,6 +71,7 @@ describe "Keiki.Core operators (EP-45)" Keiki.OperatorsSpec.spec describe "Keiki.Operators (qualified import, EP-58)" Keiki.OperatorsQualifiedSpec.spec describe "Keiki.Profunctor (EP-27)" Keiki.ProfunctorSpec.spec+ describe "Keiki.ProjectionDomain" Keiki.ProjectionDomainSpec.spec describe "Keiki.Profunctor (Strong, EP-29 M2)" Keiki.StrongSpec.spec describe "Keiki.Profunctor (Arrow, EP-29 M3)" Keiki.ArrowSpec.spec describe "Keiki.RecomputeVerify (EP-47)" Keiki.RecomputeVerifySpec.spec