diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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 diff --git a/keiki.cabal b/keiki.cabal --- a/keiki.cabal +++ b/keiki.cabal @@ -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 diff --git a/src/Keiki/Core.hs b/src/Keiki/Core.hs --- a/src/Keiki/Core.hs +++ b/src/Keiki/Core.hs @@ -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 = [] diff --git a/src/Keiki/Internal/ProjectionDomain.hs b/src/Keiki/Internal/ProjectionDomain.hs new file mode 100644 --- /dev/null +++ b/src/Keiki/Internal/ProjectionDomain.hs @@ -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) diff --git a/src/Keiki/Internal/SymbolicTypes.hs b/src/Keiki/Internal/SymbolicTypes.hs --- a/src/Keiki/Internal/SymbolicTypes.hs +++ b/src/Keiki/Internal/SymbolicTypes.hs @@ -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 diff --git a/src/Keiki/ProjectionDomain.hs b/src/Keiki/ProjectionDomain.hs new file mode 100644 --- /dev/null +++ b/src/Keiki/ProjectionDomain.hs @@ -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 diff --git a/src/Keiki/Symbolic.hs b/src/Keiki/Symbolic.hs --- a/src/Keiki/Symbolic.hs +++ b/src/Keiki/Symbolic.hs @@ -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/\" - -- or "inp/\/\") 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/"@ where @slotName@ is the --- slot's label recovered from the 'Index'\'s 'KnownSymbol' --- evidence on its leaf 'ZIdx'. --- * 'TInpCtorField' allocates --- @"inp//"@ — 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/"@, 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/\" + -- or "inp/\/\") 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/"@ where @slotName@ is the +-- slot's label recovered from the 'Index'\'s 'KnownSymbol' +-- evidence on its leaf 'ZIdx'. +-- * 'TInpCtorField' allocates +-- @"inp//"@ — 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/"@, 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 diff --git a/test/Keiki/CoreInFlightSpec.hs b/test/Keiki/CoreInFlightSpec.hs --- a/test/Keiki/CoreInFlightSpec.hs +++ b/test/Keiki/CoreInFlightSpec.hs @@ -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" diff --git a/test/Keiki/FieldProjSpec.hs b/test/Keiki/FieldProjSpec.hs --- a/test/Keiki/FieldProjSpec.hs +++ b/test/Keiki/FieldProjSpec.hs @@ -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" $ diff --git a/test/Keiki/ProjectionDomainSpec.hs b/test/Keiki/ProjectionDomainSpec.hs new file mode 100644 --- /dev/null +++ b/test/Keiki/ProjectionDomainSpec.hs @@ -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 diff --git a/test/Keiki/ReplayEitherSpec.hs b/test/Keiki/ReplayEitherSpec.hs --- a/test/Keiki/ReplayEitherSpec.hs +++ b/test/Keiki/ReplayEitherSpec.hs @@ -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 diff --git a/test/Keiki/ReplayOnlySpec.hs b/test/Keiki/ReplayOnlySpec.hs --- a/test/Keiki/ReplayOnlySpec.hs +++ b/test/Keiki/ReplayOnlySpec.hs @@ -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" $ diff --git a/test/Keiki/RoundTrip.hs b/test/Keiki/RoundTrip.hs --- a/test/Keiki/RoundTrip.hs +++ b/test/Keiki/RoundTrip.hs @@ -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 diff --git a/test/Keiki/StepEitherSpec.hs b/test/Keiki/StepEitherSpec.hs --- a/test/Keiki/StepEitherSpec.hs +++ b/test/Keiki/StepEitherSpec.hs @@ -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 diff --git a/test/Keiki/SymbolicSpec.hs b/test/Keiki/SymbolicSpec.hs --- a/test/Keiki/SymbolicSpec.hs +++ b/test/Keiki/SymbolicSpec.hs @@ -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" $ diff --git a/test/Spec.hs b/test/Spec.hs --- a/test/Spec.hs +++ b/test/Spec.hs @@ -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