keiki 0.8.0.0 → 0.9.0.0

raw patch · 37 files changed

+7000/−2673 lines, 37 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +90/−0
• README.md +4/−2
• keiki.cabal +6/−1
• src/Keiki/Composition.hs +258/−117
• src/Keiki/Core.hs +635/−42
• src/Keiki/Generics.hs +406/−45
• src/Keiki/Generics/TH.hs +13/−16
• src/Keiki/Internal/ConstructorEvidence.hs +13/−0
• src/Keiki/Internal/WireSchema.hs +652/−0
• src/Keiki/Profunctor.hs +70/−67
• src/Keiki/Symbolic.hs +2725/−1797
• test/Keiki/BuilderSpec.hs +14/−0
• test/Keiki/CompositionAlignmentSpec.hs +203/−31
• test/Keiki/CompositionMultiEventSpec.hs +41/−84
• test/Keiki/CompositionNarySpec.hs +13/−1
• test/Keiki/CoreInFlightSpec.hs +16/−18
• test/Keiki/CoreSpec.hs +35/−43
• test/Keiki/FieldProjSpec.hs +16/−35
• test/Keiki/Fixtures/BrokenTailCoverage.hs +19/−18
• test/Keiki/Fixtures/ComposeStateful.hs +48/−85
• test/Keiki/Fixtures/CounterPipeline.hs +14/−28
• test/Keiki/Fixtures/RegisterEmission.hs +25/−35
• test/Keiki/Fixtures/SplitCoverage.hs +22/−26
• test/Keiki/FullSymbolicReplayInversionSpec.hs +491/−0
• test/Keiki/Generics/THSpec.hs +18/−0
• test/Keiki/InputSchemaSpec.hs +150/−0
• test/Keiki/ProfunctorSpec.hs +22/−0
• test/Keiki/Render/MermaidSpec.hs +12/−50
• test/Keiki/Render/PrettySpec.hs +5/−5
• test/Keiki/ReplayOnlySpec.hs +64/−14
• test/Keiki/StepEitherSpec.hs +12/−15
• test/Keiki/StrongSpec.hs +12/−0
• test/Keiki/SymbolicSpec.hs +121/−37
• test/Keiki/ValidationReplayAlignmentSpec.hs +556/−21
• test/Keiki/ValidationSpec.hs +24/−40
• test/Keiki/WireSchemaSpec.hs +169/−0
• test/Spec.hs +6/−0

@@ -9,6 +9,96 @@ ## [Unreleased]  +## [0.9.0.0] — 2026-08-04++### Added++- `WireCtor` values can carry abstract, Generic-derived structural schemas for+  their constructor path and ordered field types. `classifyWireHeads` exposes a+  proof-safe equal/different/unwitnessed classification without using diagnostic+  names.+- `InCtor` values now carry the input-side counterpart: an abstract constructor+  path and typed slot spine. `classifyInputHeads` exposes structural+  equal/different/unwitnessed classification, and `mkInCtorRecordVia` /+  `mkWireCtorRecordVia` safely derive schemas for constructors whose fields are+  declared directly with record syntax.+- `unavailableWireCtor` / `unavailableInCtor` are the explicit manual-behavior+  constructors, and `renameWireCtor` / `renameInCtor` change diagnostic names+  while preserving behavior and trusted evidence.+- `classifyInputWireHeads` exposes the proof-safe aligned/different/unwitnessed+  relation between an input constructor and an output wire constructor at the+  same carrier — the observer form of the checked alignment that authorizes+  sequential-composition substitution. The documented trust model+  ("Keiki.Generics" Haddocks and the replay-verification foundations page) now+  states explicitly that trusted evidence roots in lawful `Generic` instances;+  a deliberately unlawful hand-written instance is outside the threat model,+  exactly as `unsafeCoerce` is.+- `checkInversionAmbiguitySymDetailed` and+  `checkInversionAmbiguitySym` provide an opt-in SBV analysis of two replay+  candidates against shared registers and a structurally aligned observed head.+  Only definite `Unsatisfiable` results remove compatibility warnings.++### Changed++- Default `inversionAmbiguityWarnings` now uses structural head classification+  and suppresses a same-mode warning only when exact integral+  register-versus-literal conjuncts prove the two replay candidates disjoint.+  Unsupported and opaque guards remain conservative warnings, and their+  `tvwDetail` identifies the construct that blocked the cheap proof. Runtime+  replay and the opt-in symbolic checker are unchanged.+- The symbolic inversion compatibility projection now joins detailed solver+  verdicts to warnings by source vertex and both edge indices. A warning is+  removed only by one uniquely matching definitely-UNSAT, proved-disjoint+  detail; missing, duplicate, or reordered details fail closed.+- **Breaking:** `WireCtor` construction and record update are sealed behind a+  read-only `WireCtor` record pattern. Manual behavior uses+  `unavailableWireCtor`; Generic `mkWireCtorVia` and TH-derived wires provide+  trusted evidence. Schema-preserving composition retains evidence, while+  meaning-changing profunctor transformations drop it.+- **Breaking:** nullary TH-derived wires now use structural Generic matching via+  `mkWireCtor0Via`. Matching therefore requires `Generic co` instead of using+  `Eq co`; `solveOutput` still requires `Eq co`. A quotienting custom `Eq`+  instance no longer changes `wcMatch` behavior.+- `mkWireCtor` and `mkWireCtor0` are deprecated because their closure-taking+  interfaces cannot establish trusted evidence. Use their `Via` counterparts or+  `unavailableWireCtor`.+- **Breaking:** `InCtor` construction and record update are sealed behind a+  read-only `InCtor` record pattern. Manual behavior uses `unavailableInCtor`;+  Generic `mkInCtorVia`, direct-record Via producers, and TH-derived constructors+  provide trusted evidence. `mkInCtor` and `mkInCtor0` are deprecated because+  closure-taking APIs cannot establish it.+- Trusted `WireCtor` / `InCtor` construction requires a strict capability from+  a hidden library module. Public callers cannot import that capability and+  receive only read-only patterns, evidence-unavailable manual constructors,+  and evidence-preserving rename helpers.+- Sequential composition now substitutes mid-side fields and discharges+  constructor guards only through typed input-to-wire alignment. Structural+  mismatch and unavailable evidence produce `StructurallyDifferentInputWire` or+  `UnwitnessedInputWireAlignment` diagnostics instead of authorizing a+  result-type coercion from equal names.+- Composition-only identity alignment now carries a typed `Either` prefix+  spine and derives field equality by lockstep GADT refinement. Schema+  alignment no longer contains an `unsafeCoerce`.+- Symbolic `PInCtor` translation now uses shared structural constructor-path+  decisions. Same-named trusted constructors remain distinct; unwitnessed equal+  names share a conservative fallback atom, while unequal names remain+  independent and therefore cannot manufacture mutual exclusion. Witness+  reconstruction uses a separate stable `KnownInCtors` ordinal.++### Migration++- Replace intentional manual `WireCtor` records with+  `unavailableWireCtor name match build`, or move honest Generic bindings to+  `mkWireCtorVia` / `mkWireCtor0Via`. Use `renameWireCtor` instead of record+  update when only the diagnostic name changes.+- Replace intentional manual `InCtor` records with+  `unavailableInCtor name match build`. Prefer `mkInCtorVia` for constructors+  wrapping record payloads, `mkInCtorRecordVia` for direct record constructors,+  and TH derivation where applicable. Use `renameInCtor` for diagnostic relabels+  and trusted producers on every boundary passed to `composeChecked` or relied+  on for symbolic constructor exclusion.++ ## [0.8.0.0] — 2026-08-02  ### Added

@@ -58,8 +58,10 @@ - profunctor / `Category` / `Strong` / `Choice` / `Arrow` instances, - behavior-readable Mermaid and Markdown renderers, with explicit compact   topology output,-- eager builder validation, default-on replay-safety checks, and optional-  single-valuedness checks via SBV + z3.+- eager builder validation and default-on replay-safety checks, plus opt-in+  SBV + z3 checks for single-valuedness and output-dependent replay inversion,+- trusted Generic/TH wire schemas that align event fields structurally for+  replay proofs without treating diagnostic constructor names as evidence.  `delta` / `omega` / `applyEvent` use concrete predicate evaluation — no solver in the per-event hot path. Solver dispatch is reserved for

@@ -1,6 +1,6 @@ cabal-version:   3.0 name:            keiki-version:         0.8.0.0+version:         0.9.0.0 synopsis:        Pure core for symbolic-register transducer event sourcing. description:   A Haskell library for the pure core of event sourcing, workflow@@ -82,8 +82,10 @@     Keiki.Symbolic    other-modules:+    Keiki.Internal.ConstructorEvidence     Keiki.Internal.ProjectionDomain     Keiki.Internal.SymbolicTypes+    Keiki.Internal.WireSchema    hs-source-dirs:  src   build-depends:@@ -132,7 +134,9 @@     Keiki.Fixtures.RegisterEmission     Keiki.Fixtures.SplitCoverage     Keiki.Fixtures.UserRegistration+    Keiki.FullSymbolicReplayInversionSpec     Keiki.Generics.THSpec+    Keiki.InputSchemaSpec     Keiki.LawHelpers     Keiki.NoThunksSpec     Keiki.OperatorsQualifiedSpec@@ -155,6 +159,7 @@     Keiki.SymbolicSpec     Keiki.ValidationReplayAlignmentSpec     Keiki.ValidationSpec+    Keiki.WireSchemaSpec    build-depends:     , base         ^>=4.21

@@ -114,6 +114,16 @@ import GHC.TypeLits (KnownSymbol) import Keiki.Core import Keiki.Generics (Append, appendRegFile)+import Keiki.Internal.ConstructorEvidence (constructorEvidence)+import Keiki.Internal.WireSchema+  ( InWireFieldAlignment (..),+    InWireSchemaComparison (..),+    compareInCtorWireSchemas,+    prefixInCtorSchemaLeft,+    prefixInCtorSchemaRight,+    prefixWireSchemaLeft,+    prefixWireSchemaRight,+  ) import NoThunks.Class (NoThunks (..), allNoThunks) import Unsafe.Coerce (unsafeCoerce) @@ -448,21 +458,17 @@ indexInt ZIdx = 0 indexInt (SIdx i) = 1 + indexInt i --- | Existential wrapper around a 'Term' so 'nthTerm' can return one--- without exposing the field's type at the call site.-data SomeTerm rs ci where-  SomeTerm :: Term rs ci ifs r -> SomeTerm rs ci---- | Walk an 'OutFields' chain to position @n@. Returns @Nothing@--- when @n@ overshoots the chain (a bug in the caller; the design's--- structural-alignment assumption guarantees @n@ is in range when--- the constructor names match).-nthTerm :: Int -> OutFields rs ci ifs fs -> Maybe (SomeTerm rs ci)-nthTerm _ OFNil = Nothing-nthTerm 0 (OFCons t _) = Just (SomeTerm t)-nthTerm n (OFCons _ rest)-  | n > 0 = nthTerm (n - 1) rest-  | otherwise = Nothing+-- | Select the output term corresponding to one input slot. The alignment+-- witness proves both arity and result type, so no result-type cast is needed.+alignedInputField ::+  InWireFieldAlignment inputFields wireFields ->+  Index inputFields result ->+  OutFields rs ci sourceInputFields wireFields ->+  Term rs ci sourceInputFields result+alignedInputField InWireFieldsAlignedNil index OFNil = case index of {}+alignedInputField (InWireFieldsAlignedCons _) ZIdx (OFCons term _) = term+alignedInputField (InWireFieldsAlignedCons rest) (SIdx index) (OFCons _ fields) =+  alignedInputField rest index fields  -- | A structurally inert term whose value raises only when demanded. -- Structural walkers see an opaque 'TApp1' over a harmless literal, so a@@ -470,25 +476,34 @@ poisonTerm :: String -> Term rs ci ifs r poisonTerm message = TApp1 (\() -> error message) (TOpaqueLit ()) --- | Detect a field read for a constructor other than the mid constructor--- produced by the t1 output currently being substituted.-termHasCtorMismatch :: String -> Term rs ci ifs r -> Bool+-- | Detect a field read that lacks definite structural alignment with the+-- mid constructor produced by the upstream output.+termHasCtorMismatch :: WireCtor mid fields -> Term rs mid ifs r -> Bool termHasCtorMismatch _ (TLit _) = False termHasCtorMismatch _ (TOpaqueLit _) = False termHasCtorMismatch _ (TReg _) = False-termHasCtorMismatch expected (TInpCtorField ic _) = icName ic /= expected+termHasCtorMismatch expected (TInpCtorField inputCtor _) =+  not (inputCtorAlignsWire inputCtor expected) termHasCtorMismatch expected (TApp1 _ term) = termHasCtorMismatch expected term termHasCtorMismatch expected (TArith _ a b) =   termHasCtorMismatch expected a || termHasCtorMismatch expected b termHasCtorMismatch expected (TApp2 _ a b) =   termHasCtorMismatch expected a || termHasCtorMismatch expected b termHasCtorMismatch _ (TFieldProj _ (PBReg _)) = False-termHasCtorMismatch expected (TFieldProj _ (PBInp ic _)) =-  icName ic /= expected+termHasCtorMismatch expected (TFieldProj _ (PBInp inputCtor _)) =+  not (inputCtorAlignsWire inputCtor expected) -outCtorName :: OutTerm rs ci co -> String-outCtorName (OPack _ wc _) = wcName wc+inputCtorAlignsWire :: InCtor carrier inputFields -> WireCtor carrier wireFields -> Bool+inputCtorAlignsWire inputCtor wireCtor =+  case compareInCtorWireSchemas inputCtor.icSchema wireCtor.wcSchema of+    InWireSchemasEqual _ -> True+    InWireSchemasDifferent -> False+    InWireSchemasUnwitnessed -> False +inputCtorAlignsOutTerm :: InCtor carrier inputFields -> OutTerm rs ci carrier -> Bool+inputCtorAlignsOutTerm inputCtor (OPack _ wireCtor _) =+  inputCtorAlignsWire inputCtor wireCtor+ -- | Substitute a t2-side 'Term' against t1's edge output. See the -- design note's "Substituting a Term" section for the rules. --@@ -529,40 +544,29 @@   Term (Append rs1 rs2) ci1 ifsR r substInputField ic2 ix2 o1 =   case o1 of-    OPack _ic1 wc1 of1-      | icName ic2 == wcName wc1 ->-          let n = indexInt ix2-           in case nthTerm n of1 of-                Just (SomeTerm tm) ->-                  -- tm :: Term rs1 ci1 ifsTm r' (r' ~ r and ifsTm ~ ifsR-                  -- structurally; the slot list of ic2 mirrors of1's tuple-                  -- shape via the GRecord/GTuple Generic derivations, and-                  -- of1's elements all read t1's input at the OPack's-                  -- schema). 'unsafeCoerceTerm' realigns both the result-                  -- type and the input field schema.-                  weakenLTerm @rs1 @rs2 (unsafeCoerceTerm tm)-                Nothing ->-                  poisonTerm-                    ( "Keiki.Composition.compose: nthTerm overflow at\-                      \ position "-                        <> show n-                        <> " for InCtor "-                        <> icName ic2-                        <> " — t2 reads a field t1's OutFields doesn't expose.\-                           \ This indicates a structural mismatch between\-                           \ t1's wireCtor and t2's InCtor for the shared\-                           \ mid type."-                    )-      | otherwise ->+    OPack _ic1 wc1 of1 ->+      case compareInCtorWireSchemas ic2.icSchema wc1.wcSchema of+        InWireSchemasEqual alignment ->+          weakenLTerm @rs1 @rs2+            ( unsafeReindexTermInput+                (alignedInputField alignment ix2 of1)+            )+        InWireSchemasDifferent ->           poisonTerm-            ( "Keiki.Composition.compose: t2-side guard, update, or output reads "+            ( "Keiki.Composition.compose: structurally different input and wire constructors: t2 reads "                 <> icName ic2                 <> " while t1's edge carries "                 <> wcName wc1-                <> ". This composite edge cannot supply that constructor field;\-                   \ its mismatched guard leaf should be unsatisfiable before\-                   \ the value is demanded."+                <> ". Diagnostic-name equality cannot authorize substitution."             )+        InWireSchemasUnwitnessed ->+          poisonTerm+            ( "Keiki.Composition.compose: structural input/wire alignment is unavailable for t2 input "+                <> icName ic2+                <> " and t1 wire "+                <> wcName wc1+                <> ". Use Generic-derived trusted constructors before composing field reads."+            )  projectThroughTerm ::   ( FieldProjection projection,@@ -603,14 +607,18 @@ projectThroughTermWithStatus witness ownerTerm =   (TApp1 (fieldWitnessGet witness) ownerTerm, ProjectionLowered) --- | Existentially-coerce a 'Term''s result type /and/ input field--- schema. Unsound in general; justified here by the structural---- alignment invariant the design note documents: when--- @icName ic2 == wcName wc1@, the slot list of @ic2@ and the field--- tuple of @wc1@ are derived from the same 'Generic' representation, so--- positional reads agree on type; and the substituted term reads t1's--- input at t1's 'OPack' schema, which is the schema the composite--- 'OPack' is rebuilt at (see 'substOut').+-- | Re-index only a term's existential input schema after checked+-- input-to-wire alignment has fixed its result type. The term comes from the+-- upstream 'OPack', and 'substOut' rebuilds the composite at that same+-- upstream input schema; this cast cannot alter a value type.+unsafeReindexTermInput ::+  forall rs ci inputFields inputFields' result.+  Term rs ci inputFields' result ->+  Term rs ci inputFields result+unsafeReindexTermInput = unsafeCoerce++-- | Existentially realign a pending term after a separately checked+-- 'TypeRep' equality. This helper is not used by input/wire substitution. unsafeCoerceTerm ::   forall rs ci ifs ifs' r r'. Term rs ci ifs' r' -> Term rs ci ifs r unsafeCoerceTerm = unsafeCoerce@@ -635,26 +643,30 @@     (substPred @rs1 @rs2 q o1) substPred (PNot p) o1 = PNot (substPred @rs1 @rs2 p o1) substPred (PEq a b) o1 =-  if termHasCtorMismatch (outCtorName o1) a-    || termHasCtorMismatch (outCtorName o1) b-    then PBot-    else-      PEq-        (substTerm @rs1 @rs2 a o1)-        (substTerm @rs1 @rs2 b o1)+  case o1 of+    OPack _ wireCtor _ ->+      if termHasCtorMismatch wireCtor a+        || termHasCtorMismatch wireCtor b+        then PBot+        else+          PEq+            (substTerm @rs1 @rs2 a o1)+            (substTerm @rs1 @rs2 b o1) substPred (PCmp op a b) o1 =-  if termHasCtorMismatch (outCtorName o1) a-    || termHasCtorMismatch (outCtorName o1) b-    then PBot-    else-      PCmp-        op-        (substTerm @rs1 @rs2 a o1)-        (substTerm @rs1 @rs2 b o1)+  case o1 of+    OPack _ wireCtor _ ->+      if termHasCtorMismatch wireCtor a+        || termHasCtorMismatch wireCtor b+        then PBot+        else+          PCmp+            op+            (substTerm @rs1 @rs2 a o1)+            (substTerm @rs1 @rs2 b o1) substPred (PInCtor ic2) o1 =   case o1 of     OPack _ wc1 _-      | icName ic2 == wcName wc1 -> PTop+      | inputCtorAlignsWire ic2 wc1 -> PTop       | otherwise -> PBot substPred PLeftArm o1 = substLeftArmPred @rs1 @rs2 o1 substPred PRightArm o1 = substRightArmPred @rs1 @rs2 o1@@ -763,51 +775,61 @@ -- 'icBuild' wraps the rebuilt @ci1@ in 'Left' so the lifted -- transducer's 'solveOutput' walks back to the original input form. leftInCtor :: InCtor ci1 ifs -> InCtor (Either ci1 ci2) ifs-leftInCtor InCtor {icName = n, icMatch = m, icBuild = b} =-  InCtor-    { icName = n,-      icMatch = \case+leftInCtor InCtor {icName = n, icSchema = schema, icMatch = m, icBuild = b} =+  trustedInCtorInternal+    constructorEvidence+    n+    (prefixInCtorSchemaLeft schema)+    ( \case         Left c1 -> m c1-        Right _ -> Nothing,-      icBuild = Left . b-    }+        Right _ -> Nothing+    )+    (Left . b)  -- | Lift an 'InCtor' from the right arm of an 'Either' input -- alphabet. Symmetric to 'leftInCtor'. rightInCtor :: InCtor ci2 ifs -> InCtor (Either ci1 ci2) ifs-rightInCtor InCtor {icName = n, icMatch = m, icBuild = b} =-  InCtor-    { icName = n,-      icMatch = \case+rightInCtor InCtor {icName = n, icSchema = schema, icMatch = m, icBuild = b} =+  trustedInCtorInternal+    constructorEvidence+    n+    (prefixInCtorSchemaRight schema)+    ( \case         Left _ -> Nothing-        Right c2 -> m c2,-      icBuild = Right . b-    }+        Right c2 -> m c2+    )+    (Right . b)  -- | Lift a 'WireCtor' from the left arm of an 'Either' output -- alphabet. Matches only on @Left _@ outputs; rebuilds via--- @Left . wcBuild@.+-- @Left . wcBuild@. Trusted schemas retain their field spine and receive a+-- structural left-arm path prefix; unavailable evidence stays unavailable. leftWireCtor :: WireCtor co1 fs -> WireCtor (Either co1 co2) fs-leftWireCtor WireCtor {wcName = n, wcMatch = m, wcBuild = b} =-  WireCtor-    { wcName = n,-      wcMatch = \case+leftWireCtor WireCtor {wcName = n, wcSchema = schema, wcMatch = m, wcBuild = b} =+  trustedWireCtorInternal+    constructorEvidence+    n+    (prefixWireSchemaLeft schema)+    ( \case         Left c1 -> m c1-        Right _ -> Nothing,-      wcBuild = Left . b-    }+        Right _ -> Nothing+    )+    (Left . b)  -- | Lift a 'WireCtor' from the right arm of an 'Either' output--- alphabet. Symmetric to 'leftWireCtor'.+-- alphabet. Symmetric to 'leftWireCtor', including its preserve-or-drop schema+-- rule. rightWireCtor :: WireCtor co2 fs -> WireCtor (Either co1 co2) fs-rightWireCtor WireCtor {wcName = n, wcMatch = m, wcBuild = b} =-  WireCtor-    { wcName = n,-      wcMatch = \case+rightWireCtor WireCtor {wcName = n, wcSchema = schema, wcMatch = m, wcBuild = b} =+  trustedWireCtorInternal+    constructorEvidence+    n+    (prefixWireSchemaRight schema)+    ( \case         Left _ -> Nothing-        Right c2 -> m c2,-      wcBuild = Right . b-    }+        Right c2 -> m c2+    )+    (Right . b)  -- | Lift a 'Term' from the left side's input alphabet to -- @Either ci1 ci2@. Walks the AST and adjusts every 'TInpCtorField'@@ -914,14 +936,14 @@   Bool ->   InCtor outer '[] liftedArmInCtor outerName project wantLeft =-  InCtor-    { icName = "keiki#" <> outerName <> "#" <> (if wantLeft then "leftArm#lmapped" else "rightArm#lmapped"),-      icMatch = \outer -> case project outer of+  unavailableInCtor+    ("keiki#" <> outerName <> "#" <> (if wantLeft then "leftArm#lmapped" else "rightArm#lmapped"))+    ( \outer -> case project outer of         Just (Left _) | wantLeft -> Just RNil         Just (Right _) | not wantLeft -> Just RNil-        _ -> Nothing,-      icBuild = \_ -> error "Keiki.Composition: nested lifted arm predicates cannot rebuild inputs"-    }+        _ -> Nothing+    )+    (\_ -> error "Keiki.Composition: nested lifted arm predicates cannot rebuild inputs")  -- | Lift an 'Update' from the left side's input alphabet to -- @Either ci1 ci2@. The slot-name index @w@ is preserved; only the@@ -1196,7 +1218,8 @@ -- * compose ----------------------------------------------------------------  -- | A conservative structural fact discovered at a composition boundary.--- The checker reports concrete name/position mismatches. Its reachability scan+-- Constructor names in these warnings are diagnostic only: substitution and+-- guard discharge require typed input-to-wire schema alignment. Its reachability scan -- is conservative, so exotic Boolean guards can produce warnings on a -- semantically unreachable path or hide an expectation the structural walker -- cannot expose. Every warning is a reviewable structural fact, but an empty@@ -1219,6 +1242,18 @@         cawReadPosition :: Int,         cawAvailableFields :: Int       }+  | StructurallyDifferentInputWire+      { cawStructuralT1Edge :: EdgeRef s1,+        cawStructuralT2Edge :: EdgeRef s2,+        cawStructuralWireName :: String,+        cawStructuralInCtorName :: String+      }+  | UnwitnessedInputWireAlignment+      { cawUnwitnessedT1Edge :: EdgeRef s1,+        cawUnwitnessedT2Edge :: EdgeRef s2,+        cawUnwitnessedWireName :: String,+        cawUnwitnessedInCtorName :: String+      }   | PoisonedNameInComposition       { cawName :: String,         cawSide :: String@@ -1244,6 +1279,12 @@     expectedPosition :: Maybe Int   } +data EmittedConstructor carrier s where+  EmittedConstructor :: EdgeRef s -> WireCtor carrier fields -> EmittedConstructor carrier s++data ExpectedConstructor carrier s where+  ExpectedConstructor :: EdgeRef s -> InCtor carrier fields -> ExpectedConstructor carrier s+ outFieldsLength :: OutFields rs ci ifs fs -> Int outFieldsLength OFNil = 0 outFieldsLength (OFCons _ rest) = 1 + outFieldsLength rest@@ -1258,6 +1299,16 @@   | OPack _ wc fields <- output edge   ] +edgeEmittedConstructors ::+  s ->+  Int ->+  Edge p rs ci carrier s ->+  [EmittedConstructor carrier s]+edgeEmittedConstructors source edgeIx edge =+  [ EmittedConstructor (EdgeRef source edgeIx) wireCtor+  | OPack _ wireCtor _ <- output edge+  ]+ termExpectedReads :: Term rs ci ifs r -> [(String, Int)] termExpectedReads (TLit _) = [] termExpectedReads (TOpaqueLit _) = []@@ -1270,6 +1321,22 @@ termExpectedReads (TFieldProj _ (PBInp ic ix)) =   [(icName ic, indexPosition ix)] +termExpectedConstructors :: Term rs ci ifs result -> [SomeInCtor ci]+termExpectedConstructors (TLit _) = []+termExpectedConstructors (TOpaqueLit _) = []+termExpectedConstructors (TReg _) = []+termExpectedConstructors (TInpCtorField inputCtor _) = [SomeInCtor inputCtor]+termExpectedConstructors (TApp1 _ term) = termExpectedConstructors term+termExpectedConstructors (TApp2 _ left right) =+  termExpectedConstructors left ++ termExpectedConstructors right+termExpectedConstructors (TArith _ left right) =+  termExpectedConstructors left ++ termExpectedConstructors right+termExpectedConstructors (TFieldProj _ (PBReg _)) = []+termExpectedConstructors (TFieldProj _ (PBInp inputCtor _)) = [SomeInCtor inputCtor]++data SomeInCtor ci where+  SomeInCtor :: InCtor ci fields -> SomeInCtor ci+ predCtorAtoms :: HsPred rs ci -> [String] predCtorAtoms PTop = [] predCtorAtoms PBot = []@@ -1294,16 +1361,46 @@ predExpectedReads PRightArm = [] predExpectedReads (PCmp _ a b) = termExpectedReads a ++ termExpectedReads b +predExpectedConstructors :: HsPred rs ci -> [SomeInCtor ci]+predExpectedConstructors PTop = []+predExpectedConstructors PBot = []+predExpectedConstructors (PAnd left right) =+  predExpectedConstructors left ++ predExpectedConstructors right+predExpectedConstructors (POr left right) =+  predExpectedConstructors left ++ predExpectedConstructors right+predExpectedConstructors (PNot predicate) = predExpectedConstructors predicate+predExpectedConstructors (PEq left right) =+  termExpectedConstructors left ++ termExpectedConstructors right+predExpectedConstructors (PInCtor inputCtor) = [SomeInCtor inputCtor]+predExpectedConstructors PLeftArm = []+predExpectedConstructors PRightArm = []+predExpectedConstructors (PCmp _ left right) =+  termExpectedConstructors left ++ termExpectedConstructors right+ updateExpectedReads :: Update rs w ci -> [(String, Int)] updateExpectedReads UKeep = [] updateExpectedReads (USet _ term) = termExpectedReads term updateExpectedReads (UCombine a b) = updateExpectedReads a ++ updateExpectedReads b +updateExpectedConstructors :: Update rs writes ci -> [SomeInCtor ci]+updateExpectedConstructors UKeep = []+updateExpectedConstructors (USet _ term) = termExpectedConstructors term+updateExpectedConstructors (UCombine left right) =+  updateExpectedConstructors left ++ updateExpectedConstructors right+ outFieldsExpectedReads :: OutFields rs ci ifs fs -> [(String, Int)] outFieldsExpectedReads OFNil = [] outFieldsExpectedReads (OFCons term rest) =   termExpectedReads term ++ outFieldsExpectedReads rest +outFieldsExpectedConstructors :: OutFields rs ci ifs fields -> [SomeInCtor ci]+outFieldsExpectedConstructors OFNil = []+outFieldsExpectedConstructors (OFCons term rest) =+  termExpectedConstructors term ++ outFieldsExpectedConstructors rest++outTermExpectedConstructors :: OutTerm rs ci co -> [SomeInCtor ci]+outTermExpectedConstructors (OPack _ _ fields) = outFieldsExpectedConstructors fields+ edgeExpectedNames :: s -> Int -> Edge (HsPred rs ci) rs ci co s -> [ExpectedName s] edgeExpectedNames source edgeIx Edge {guard = edgeGuard, update = edgeUpdate, output = edgeOutput} =   [ ExpectedName (EdgeRef source edgeIx) name Nothing@@ -1316,6 +1413,19 @@              ++ concatMap (\(OPack _ _ fields) -> outFieldsExpectedReads fields) edgeOutput        ] +edgeExpectedConstructors ::+  s ->+  Int ->+  Edge (HsPred rs ci) rs ci co s ->+  [ExpectedConstructor ci s]+edgeExpectedConstructors source edgeIx Edge {guard = edgeGuard, update = edgeUpdate, output = edgeOutput} =+  [ ExpectedConstructor (EdgeRef source edgeIx) inputCtor+  | SomeInCtor inputCtor <-+      predExpectedConstructors edgeGuard+        ++ updateExpectedConstructors edgeUpdate+        ++ concatMap outTermExpectedConstructors edgeOutput+  ]+ edgeConsumesName :: String -> Edge (HsPred rs ci) rs ci co s -> Bool edgeConsumesName name edge =   null atoms || name `elem` atoms@@ -1360,7 +1470,7 @@     goTerm (TFieldProj _ (PBReg _)) = []     goTerm       (TFieldProj (witness :: FieldWitness projection) base@(PBInp ic ix))-        | icName ic /= outCtorName midOutput = []+        | not (inputCtorAlignsOutTerm ic midOutput) = []         | otherwise =             let ownerTerm ::                   Term@@ -1473,12 +1583,16 @@       ]      warningsAt (v1, v2) =-      unconsumed ++ unmatched ++ arity ++ poison ++ projection+      unconsumed ++ unmatched ++ arity ++ structural ++ poison ++ projection       where         t1Edges = zip [0 ..] (edgesOut t1 v1)         t2Edges = zip [0 ..] (edgesOut t2 v2)         emissions = concatMap (uncurry (edgeEmittedNames v1)) t1Edges         expectations = concatMap (uncurry (edgeExpectedNames v2)) t2Edges+        emittedConstructors =+          concatMap (uncurry (edgeEmittedConstructors v1)) t1Edges+        expectedConstructors =+          concatMap (uncurry (edgeExpectedConstructors v2)) t2Edges         emittedNames = map emittedName emissions         expectedNames = map expectedName expectations @@ -1510,6 +1624,29 @@             position >= emittedArity emission           ] +        structural =+          concat+            [ case compareInCtorWireSchemas inputCtor.icSchema wireCtor.wcSchema of+                InWireSchemasEqual _ -> []+                InWireSchemasDifferent ->+                  [ StructurallyDifferentInputWire+                      emittedRef+                      expectedRef+                      (wcName wireCtor)+                      (icName inputCtor)+                  ]+                InWireSchemasUnwitnessed ->+                  [ UnwitnessedInputWireAlignment+                      emittedRef+                      expectedRef+                      (wcName wireCtor)+                      (icName inputCtor)+                  ]+            | EmittedConstructor emittedRef wireCtor <- emittedConstructors,+              ExpectedConstructor expectedRef inputCtor <- expectedConstructors,+              wcName wireCtor == icName inputCtor+            ]+         poison =           [ PoisonedNameInComposition name side           | (name, side) <-@@ -1562,8 +1699,12 @@             | (edge2Ix, edge2) <- zip [0 ..] (edgesOut t2 vertex)             ] --- | Checked entry point for validated aggregate pipelines. The unchecked--- 'compose' primitive remains available for internal/experimental use.+-- | Checked entry point for validated aggregate pipelines. In addition to+-- name/arity and projection diagnostics, this requires every reachable mid-side+-- constructor use to have trusted, equal input-to-wire schemas. A diagnostic+-- name collision cannot authorize substitution. The unchecked 'compose'+-- primitive remains available for internal/experimental use, but a mismatched+-- or unwitnessed field read becomes a loud poison term if demanded. composeChecked ::   forall rs1 rs2 s1 s2 ci1 mid co.   ( WeakenR rs1,

@@ -1,3 +1,4 @@+{-# LANGUAGE PatternSynonyms #-} -- 'combine''s 'Disjoint' constraint is the static check itself; GHC -- sees it as unused (the body is @UCombine@) and would otherwise warn. -- Same reasoning for any future helpers that re-export the constraint@@ -71,7 +72,14 @@     ProjBase (..),      -- * Input-side structural constructor (v2)-    InCtor (..),+    InCtor (InCtor, icName, icSchema, icMatch, icBuild),+    unavailableInCtor,+    renameInCtor,+    trustedInCtorInternal,+    InCtorSchema,+    InCtorSchemaAvailability (..),+    inCtorSchemaUnavailable,+    inCtorSchemaAvailability,     AssembleRegFile,     KnownSlotNames (..),     slotNamesOf,@@ -89,7 +97,15 @@     combine,      -- * Output term language-    WireCtor (..),+    WireCtor (WireCtor, wcName, wcSchema, wcMatch, wcBuild),+    unavailableWireCtor,+    renameWireCtor,+    trustedWireCtorInternal,+    WireSchema,+    WireFieldSchema,+    WireSchemaAvailability (..),+    wireSchemaUnavailable,+    wireSchemaAvailability,     OutFields (..),     (*:),     oNil,@@ -187,6 +203,14 @@     hiddenInputWarnings,     headRecoverabilityWarnings,     inversionAmbiguityWarnings,+    InputHeadRelation (..),+    classifyInputHeads,+    WireHeadRelation (..),+    classifyWireHeads,+    InputWireHeadRelation (..),+    classifyInputWireHeads,+    inputWireSpineRelationsForTesting,+    wireHeadsMayAliasForDefault,     guardImpliesInputReadWarnings,     predicateImpliesInCtor,     stateChangingEpsilonWarnings,@@ -214,6 +238,8 @@     fieldWitnessReconstruct,     fieldWitnessGet,     indexPosition,+    inCtorSchemaPrefixRelationForTesting,+    wireSchemaPrefixRelationForTesting,   ) where @@ -225,7 +251,9 @@ import Data.Typeable (Typeable) import Data.Word (Word16, Word32, Word64, Word8) import GHC.OverloadedLabels (IsLabel (..))+import GHC.Records (HasField (..)) import GHC.TypeLits (KnownSymbol, Symbol, symbolVal)+import Keiki.Internal.ConstructorEvidence (ConstructorEvidence (..)) import Keiki.Internal.Slots   ( Concat,     Disjoint,@@ -240,12 +268,34 @@     symbolicTypeSupportsNumeric,     symbolicTypeSupportsOrdering,   )+import Keiki.Internal.WireSchema+  ( InCtorSchema,+    InCtorSchemaAvailability (..),+    InCtorSchemaComparison (..),+    InputHeadRelation (..),+    InputWireHeadRelation (..),+    WireFieldSchema,+    WireHeadRelation (..),+    WireSchema,+    WireSchemaAvailability (..),+    WireSchemaComparison (..),+    classifyInputWireSchemas,+    compareInCtorSchemas,+    compareWireSchemas,+    inCtorSchemaAvailability,+    inCtorSchemaPrefixRelationForTesting,+    inCtorSchemaUnavailable,+    inputWireSpineRelationsForTesting,+    wireSchemaAvailability,+    wireSchemaPrefixRelationForTesting,+    wireSchemaUnavailable,+  ) import Keiki.ProjectionDomain   ( ProjectionDomain,     memberProjectionDomain,   ) import Numeric.Natural (Natural)-import Type.Reflection (eqTypeRep, typeRep, type (:~~:) (HRefl))+import Type.Reflection (SomeTypeRep (..), eqTypeRep, typeRep, type (:~~:) (HRefl))  -- | A register slot is a label paired with the type of its value. type Slot = (Symbol, Type)@@ -612,6 +662,10 @@ -- @'RegFile' ifs@. The slot list @ifs@ is the field schema for the -- constructor; together with 'Index' it lets call sites read fields -- via 'OverloadedLabels' (for example @inpStart #email@).+-- 'icSchema' separately carries abstract structural proof evidence. Generic+-- and TH producers populate it; deliberate manual or meaning-changing+-- constructors use 'unavailableInCtor'. Diagnostic 'icName' text never+-- substitutes for that evidence in composition or symbolic proof. -- -- 'icMatch' must return 'Just' iff @ci@ is the named constructor. -- 'icBuild' is its left inverse: @icMatch (icBuild rf) == Just rf@ for@@ -628,14 +682,98 @@ -- the inversion algorithm that walks 'OutFields' gathering these -- per-field reads. data InCtor ci (ifs :: [Slot]) where-  InCtor ::+  MkInCtor ::     (AssembleRegFile ifs, KnownSlotNames ifs) =>-    { icName :: String,-      icMatch :: ci -> Maybe (RegFile ifs),-      icBuild :: RegFile ifs -> ci-    } ->+    String ->+    InCtorSchema ci ifs ->+    (ci -> Maybe (RegFile ifs)) ->+    (RegFile ifs -> ci) ->     InCtor ci ifs +-- | Read-only record view of an input constructor. Matching and field+-- selection remain available, but construction and record update do not:+-- manual behavior must enter through 'unavailableInCtor', while trusted Keiki+-- producers use the package-private construction capability.+pattern InCtor ::+  () =>+  (AssembleRegFile ifs, KnownSlotNames ifs) =>+  String ->+  InCtorSchema ci ifs ->+  (ci -> Maybe (RegFile ifs)) ->+  (RegFile ifs -> ci) ->+  InCtor ci ifs+pattern InCtor {icName, icSchema, icMatch, icBuild} <-+  MkInCtor icName icSchema icMatch icBuild++{-# COMPLETE InCtor #-}++instance HasField "icName" (InCtor ci ifs) String where+  getField = icName++instance HasField "icSchema" (InCtor ci ifs) (InCtorSchema ci ifs) where+  getField = icSchema++instance HasField "icMatch" (InCtor ci ifs) (ci -> Maybe (RegFile ifs)) where+  getField = icMatch++instance HasField "icBuild" (InCtor ci ifs) (RegFile ifs -> ci) where+  getField = icBuild++-- | Construct a manual input constructor. Its behavior is usable for forward+-- and replay execution, but it carries no trusted structural evidence.+unavailableInCtor ::+  (AssembleRegFile ifs, KnownSlotNames ifs) =>+  String ->+  (ci -> Maybe (RegFile ifs)) ->+  (RegFile ifs -> ci) ->+  InCtor ci ifs+unavailableInCtor name match build =+  MkInCtor name inCtorSchemaUnavailable match build++-- | Change only the diagnostic name while preserving behavior and structural+-- evidence.+renameInCtor :: String -> InCtor ci ifs -> InCtor ci ifs+renameInCtor name (MkInCtor _ schema match build) =+  MkInCtor name schema match build++-- | Internal trusted construction hook. The capability's constructor lives in+-- an unexposed module, and is matched strictly here so downstream code cannot+-- use bottom to manufacture a schema-bearing constructor.+--+-- The strict constructor match is load-bearing: this function is exported (so+-- the exposed producer modules can reach it), and a consumer who cannot name+-- the hidden capability type can still apply it to bottom. The pattern match+-- forces that bottom before any constructor is produced. Never refactor it+-- into a lazy or wildcard match; the bottom-capability regression tests in+-- @test/Keiki/InputSchemaSpec.hs@ and @test/Keiki/WireSchemaSpec.hs@ pin this.+trustedInCtorInternal ::+  (AssembleRegFile ifs, KnownSlotNames ifs) =>+  ConstructorEvidence ->+  String ->+  InCtorSchema ci ifs ->+  (ci -> Maybe (RegFile ifs)) ->+  (RegFile ifs -> ci) ->+  InCtor ci ifs+trustedInCtorInternal ConstructorEvidence = MkInCtor++-- | Compare two input constructors using trusted structural evidence only.+-- Diagnostic names never participate in this proof.+classifyInputHeads :: InCtor ci left -> InCtor ci right -> InputHeadRelation+classifyInputHeads left right =+  case compareInCtorSchemas left.icSchema right.icSchema of+    InCtorSchemasEqual _ -> InputHeadsStructurallyEqual+    InCtorSchemasDifferent -> InputHeadsStructurallyDifferent+    InCtorSchemasUnwitnessed -> InputHeadsUnwitnessed++-- | Compare an input constructor's evidence against an output wire+-- constructor's evidence at the same carrier, using structural evidence+-- only — the observer form of the checked alignment that authorizes+-- sequential-composition substitution. Diagnostic names never participate.+classifyInputWireHeads ::+  InCtor mid ifs -> WireCtor mid fields -> InputWireHeadRelation+classifyInputWireHeads inputCtor wireCtor =+  classifyInputWireSchemas inputCtor.icSchema wireCtor.wcSchema+ -- * Slot-list helper classes (v2 inversion machinery) ---------------------  -- | Recover the slot names of an @ifs :: [Slot]@ at run time. Used to@@ -735,13 +873,88 @@  -- | A wire-type tag for one constructor of the user's output sum @co@. -- The functions let 'solveOutput' pattern-match an observed @co@ and--- 'evalOut' rebuild a @co@ from its fields.-data WireCtor co fields = WireCtor-  { wcName :: String,-    wcMatch :: co -> Maybe fields,-    wcBuild :: fields -> co-  }+-- 'evalOut' rebuild a @co@ from its fields. 'wcSchema' is structural proof+-- evidence, not a persisted identity: Generic/TH producers supply a trusted+-- constructor path and typed field spine, while manual or meaning-changing+-- construction must use 'unavailableWireCtor'. 'wcName' remains diagnostic.+data WireCtor co fields+  = MkWireCtor+      String+      (WireSchema co fields)+      (co -> Maybe fields)+      (fields -> co) +-- | Read-only record view of an output constructor. Matching and field+-- selection remain available, but construction and record update do not.+pattern WireCtor ::+  String ->+  WireSchema co fields ->+  (co -> Maybe fields) ->+  (fields -> co) ->+  WireCtor co fields+pattern WireCtor {wcName, wcSchema, wcMatch, wcBuild} <-+  MkWireCtor wcName wcSchema wcMatch wcBuild++{-# COMPLETE WireCtor #-}++instance HasField "wcName" (WireCtor co fields) String where+  getField = wcName++instance HasField "wcSchema" (WireCtor co fields) (WireSchema co fields) where+  getField = wcSchema++instance HasField "wcMatch" (WireCtor co fields) (co -> Maybe fields) where+  getField = wcMatch++instance HasField "wcBuild" (WireCtor co fields) (fields -> co) where+  getField = wcBuild++-- | Construct a manual output constructor with explicitly unavailable+-- structural evidence.+unavailableWireCtor ::+  String ->+  (co -> Maybe fields) ->+  (fields -> co) ->+  WireCtor co fields+unavailableWireCtor name match build =+  MkWireCtor name wireSchemaUnavailable match build++-- | Change only the diagnostic name while preserving behavior and structural+-- evidence.+renameWireCtor :: String -> WireCtor co fields -> WireCtor co fields+renameWireCtor name (MkWireCtor _ schema match build) =+  MkWireCtor name schema match build++-- | Internal trusted construction hook; see 'trustedInCtorInternal'.+trustedWireCtorInternal ::+  ConstructorEvidence ->+  String ->+  WireSchema co fields ->+  (co -> Maybe fields) ->+  (fields -> co) ->+  WireCtor co fields+trustedWireCtorInternal ConstructorEvidence = MkWireCtor++-- | Compare two output heads using only trusted structural evidence.+-- Constructor names are diagnostics and never participate in this proof.+classifyWireHeads :: WireCtor co left -> WireCtor co right -> WireHeadRelation+classifyWireHeads left right =+  case compareWireSchemas left.wcSchema right.wcSchema of+    WireSchemasEqual _ -> WireHeadsStructurallyEqual+    WireSchemasDifferent -> WireHeadsStructurallyDifferent+    WireSchemasUnwitnessed -> WireHeadsUnwitnessed++-- | Conservative may-alias policy for the future default replay check.+-- Trusted prefix-related or field-misaligned paths stay may-alias. The+-- legacy diagnostic-name fallback is used only when either schema is+-- unavailable.+wireHeadsMayAliasForDefault :: WireCtor co left -> WireCtor co right -> Bool+wireHeadsMayAliasForDefault left right =+  case (wireSchemaAvailability left.wcSchema, wireSchemaAvailability right.wcSchema) of+    (WireSchemaTrusted, WireSchemaTrusted) ->+      classifyWireHeads left right /= WireHeadsStructurallyDifferent+    _ -> left.wcName == right.wcName+ -- | An HList of 'Term's, one per field of the wire constructor. The -- field-tuple type @fs@ is built up nested-pair style so that -- 'solveOutput' can walk the HList structurally.@@ -2485,9 +2698,12 @@         tvwTailOnlySlots :: [String],         tvwDetail :: String       }-  | -- | Two outgoing edges use the same wire constructor for their first-    --       event. Replay requires a unique inverting edge, so the observed-    --       event may reconstruct commands for both edges and become ambiguous.+  | -- | Two same-mode outgoing edges have first-event wire heads that may+    --       alias, and Keiki could not prove their replay candidates disjoint.+    --       Replay requires one unique inverting edge, so the observed event+    --       may reconstruct commands for both edges and become ambiguous. The+    --       human-readable detail names the construct that blocked the cheap+    --       shared-register proof when one is known.     InversionAmbiguity       { tvwSource :: s,         tvwEdgeA :: Int,@@ -2589,8 +2805,9 @@     -- | require the first emitted event to recover every command field used     --     by replay     checkHeadRecoverability :: Bool,-    -- | conservatively flag outgoing edge pairs with the same head wire-    --     constructor+    -- | conservatively flag outgoing same-mode edge pairs whose head wires may+    --     alias, except when exact shared-register conditions prove the replay+    --     candidates disjoint     checkInversionAmbiguity :: Bool,     -- | require every input-field read to be protected by an earlier matching     --     constructor guard@@ -2639,10 +2856,18 @@ -- negation, arithmetic, opaque terms, variable-versus-variable comparisons, and -- non-integral strict-bound density remain unknown and produce no pure warning. -- The pass therefore has no false positives but can miss overlaps outside that--- fragment. The dead-edge component is structural reachability plus a literal---- 'PBot' check. For the exact, solver-backed answers use+-- fragment. The inversion component classifies head wires through trusted+-- structural schemas (with the legacy name fallback for unavailable schemas),+-- then suppresses a same-mode warning only when exact integral+-- register-versus-literal conjuncts are jointly unsatisfiable. Opaque or+-- unsupported conjuncts are dropped as weakening and can never supply proof;+-- retained warnings name the first precision blocker in 'tvwDetail'. The+-- dead-edge component is structural reachability plus a literal-'PBot' check.+-- For the exact, solver-backed answers use -- 'Keiki.Symbolic.checkTransitionDeterminismSym' and--- 'Keiki.Symbolic.checkDeadEdgesSym' directly.+-- 'Keiki.Symbolic.checkDeadEdgesSym' directly, and use+-- @Keiki.Symbolic.checkInversionAmbiguitySymDetailed@ for output-dependent+-- replay-inversion pairs. validateTransducer ::   (Bounded s, Enum s, Ord s, Show s) =>   ValidationOptions ->@@ -3107,20 +3332,32 @@  -- ** Replay inversion diagnostics --- | Conservatively flag pairs of outgoing edges whose first emitted events--- use the same 'WireCtor' name. Replay selects an edge by inverting one observed--- head event, so both edges may reconstruct their own commands and satisfy their--- own guards even when forward command dispatch is deterministic.+-- | Conservatively flag same-mode outgoing edge pairs whose first emitted+-- events may alias and whose replay candidates are not proved disjoint. Replay+-- selects an edge by inverting one observed head event, so both edges may+-- reconstruct their own commands and satisfy their own guards even when+-- forward command dispatch is deterministic. ----- This structural check intentionally over-approximates ambiguity. It cannot--- prove semantic guard disjointness over recovered values or registers; it--- cannot compare differing literal values without the 'Eq' or 'Typeable'--- evidence supplied by a predicate constructor; and it does not predict--- derived-field verification in--- 'solveOutput'. It ignores tail events because replay equality-checks rather--- than inverts them. Different head constructor names are safe under the--- documented honesty law of 'wcMatch'. Literal-'PBot' guards are exempt because--- such an edge cannot participate in a successful inversion.+-- Head aliasing uses 'wireHeadsMayAliasForDefault': trusted structural schemas+-- can prove constructor paths different, while unavailable evidence retains+-- the legacy equal-'wcName' fallback. For a pair that may alias, the cheap pure+-- proof recursively extracts exact integral @TReg relation literal@ conjuncts+-- through 'PAnd'. Register variables are keyed by zero-based position and+-- runtime type; labels are diagnostic only. Unsupported sibling conjuncts are+-- dropped as weakening, so they cannot manufacture disjointness and a supported+-- contradiction may still prove the full candidates disjoint. The warning is+-- suppressed only when the combined necessary register conditions are+-- definitely unsatisfiable. Satisfiable, unsupported, type-inconsistent, and+-- otherwise unknown cases retain the warning, whose 'tvwDetail' names the first+-- precision blocker.+--+-- The proof intentionally does not enter 'POr' or 'PNot', model output fields,+-- or infer disjointness from different reconstructed command constructors. It+-- ignores tail events because replay equality-checks rather than inverts them.+-- Literal-'PBot' guards remain exempt. Call+-- @Keiki.Symbolic.checkInversionAmbiguitySymDetailed@ explicitly for the+-- optional output-dependent solver analysis. Default validation starts no+-- solver, and neither analysis changes runtime replay. inversionAmbiguityWarnings ::   forall rs s ci co.   (Bounded s, Enum s, Show s) =>@@ -3143,7 +3380,8 @@             <> wireName             <> "\" as their first event; replay may not be able to attribute an observed \""             <> wireName-            <> "\" to a unique edge"+            <> "\" to a unique edge; "+            <> candidateRegisterDetail registerAnalysis       }   | s <- [minBound .. maxBound],     let indexedEdges = zip [(0 :: Int) ..] (edgesOut t s),@@ -3155,15 +3393,21 @@     -- so only same-mode pairs can be runtime-ambiguous.     mode e1 == mode e2,     not (isBot (guard e1) || isBot (guard e2)),-    Just wireName <- [headWireName e1],-    Just otherWireName <- [headWireName e2],-    wireName == otherWireName+    Just (SomeWireCtor wire) <- [headWireCtor e1],+    Just (SomeWireCtor otherWire) <- [headWireCtor e2],+    wireHeadsMayAliasForDefault wire otherWire,+    let wireName = wcName wire,+    let registerAnalysis = analyzeCandidateRegisterConstraints (guard e1) (guard e2),+    candidateRegisterDisjointness registerAnalysis == CandidateDisjointnessNotProven   ]   where-    headWireName :: Edge (HsPred rs ci) rs ci co s -> Maybe String-    headWireName Edge {output = OPack _ wire _ : _} = Just (wcName wire)-    headWireName _ = Nothing+    headWireCtor :: Edge (HsPred rs ci) rs ci co s -> Maybe (SomeWireCtor co)+    headWireCtor Edge {output = OPack _ wire _ : _} = Just (SomeWireCtor wire)+    headWireCtor _ = Nothing +data SomeWireCtor co where+  SomeWireCtor :: WireCtor co fields -> SomeWireCtor co+ -- ** Determinism diagnostics  -- | A determinism warning: two outgoing edges of the same vertex whose guards@@ -3271,6 +3515,355 @@  data PureRelation = PureEq | PureLt | PureLe | PureGt | PureGe   deriving stock (Eq, Show)++-- | Result of checking the conjunction of the register-only necessary+-- conditions extracted from two replay guards. Unsatisfiable is the only+-- verdict that may suppress an inversion warning. Satisfiable means the+-- complete supported fragment overlaps; unknown means an unsupported or+-- malformed construct prevented a complete answer.+data RegisterConstraintVerdict+  = RegisterConstraintsUnsatisfiable+  | RegisterConstraintsSatisfiable+  | RegisterConstraintsUnknown+  deriving stock (Eq, Show)++data CandidateDisjointness+  = ProvenCandidateDisjoint+  | CandidateDisjointnessNotProven+  deriving stock (Eq, Show)++-- | Structural register identity. Labels are retained only for diagnostics;+-- proof identity is the zero-based position paired with the value type.+data RegisterVariable = RegisterVariable+  { registerVariablePosition :: Int,+    registerVariableType :: SomeTypeRep,+    registerVariableLabel :: String+  }+  deriving stock (Show)++data RegisterComparison where+  RegisterComparison ::+    (Typeable r) =>+    RegisterVariable ->+    PureRelation ->+    r ->+    (r -> Bool) ->+    RegisterComparison++data RegisterConstraintExtraction = RegisterConstraintExtraction+  { registerExtractionIsBottom :: Bool,+    registerExtractionComparisons :: [RegisterComparison],+    registerExtractionBlockers :: [String]+  }++data CandidateRegisterAnalysis = CandidateRegisterAnalysis+  { candidateRegisterDisjointness :: CandidateDisjointness,+    candidateRegisterDetail :: String+  }++emptyRegisterConstraintExtraction :: RegisterConstraintExtraction+emptyRegisterConstraintExtraction = RegisterConstraintExtraction False [] []++blockedRegisterConstraintExtraction :: String -> RegisterConstraintExtraction+blockedRegisterConstraintExtraction blocker =+  emptyRegisterConstraintExtraction+    { registerExtractionBlockers = [blocker]+    }++mergeRegisterConstraintExtractions ::+  RegisterConstraintExtraction ->+  RegisterConstraintExtraction ->+  RegisterConstraintExtraction+mergeRegisterConstraintExtractions left right =+  RegisterConstraintExtraction+    { registerExtractionIsBottom =+        registerExtractionIsBottom left || registerExtractionIsBottom right,+      registerExtractionComparisons =+        registerExtractionComparisons left <> registerExtractionComparisons right,+      registerExtractionBlockers =+        registerExtractionBlockers left <> registerExtractionBlockers right+    }++-- | Extract a weakened condition that every successful replay candidate must+-- satisfy on the shared pre-event register file. Recursing through 'PAnd' and+-- dropping unsupported sibling conjuncts is sound because a true conjunction+-- implies each retained conjunct. We deliberately do not descend through+-- 'POr' or 'PNot'. Therefore, if the conjunction of two extracted conditions+-- is unsatisfiable, the full replay candidates are disjoint without modeling+-- either reconstructed command or any output field.+extractRegisterConstraints :: HsPred rs ci -> RegisterConstraintExtraction+extractRegisterConstraints PTop = emptyRegisterConstraintExtraction+extractRegisterConstraints PBot =+  emptyRegisterConstraintExtraction {registerExtractionIsBottom = True}+extractRegisterConstraints (PAnd left right) =+  mergeRegisterConstraintExtractions+    (extractRegisterConstraints left)+    (extractRegisterConstraints right)+extractRegisterConstraints (PEq left right) =+  extractRegisterEquality left right+extractRegisterConstraints (PCmp relation left right) =+  extractRegisterOrdering relation left right+-- Input-constructor tests constrain independently reconstructed commands, not+-- the register file shared by the two replay candidates. Dropping them is an+-- intentional weakening and not a precision blocker for this proof.+extractRegisterConstraints (PInCtor _) = emptyRegisterConstraintExtraction+extractRegisterConstraints PLeftArm =+  blockedRegisterConstraintExtraction "unsupported input-arm conjunct (PLeftArm)"+extractRegisterConstraints PRightArm =+  blockedRegisterConstraintExtraction "unsupported input-arm conjunct (PRightArm)"+extractRegisterConstraints (POr _ _) =+  blockedRegisterConstraintExtraction "unsupported disjunction conjunct (POr)"+extractRegisterConstraints (PNot _) =+  blockedRegisterConstraintExtraction "unsupported negation conjunct (PNot)"++extractRegisterEquality ::+  forall rs ci ifs1 ifs2 r.+  (Eq r, Typeable r) =>+  Term rs ci ifs1 r ->+  Term rs ci ifs2 r ->+  RegisterConstraintExtraction+extractRegisterEquality left right+  | Just variable <- registerVariable left,+    Just literalValue <- termLiteralValue right =+      knownRegisterComparison variable PureEq literalValue (== literalValue)+  | Just literalValue <- termLiteralValue left,+    Just variable <- registerVariable right =+      knownRegisterComparison variable PureEq literalValue (== literalValue)+  | otherwise = unsupportedRegisterAtom "equality" left right++extractRegisterOrdering ::+  forall rs ci ifs1 ifs2 r.+  (Ord r, Typeable r) =>+  Cmp ->+  Term rs ci ifs1 r ->+  Term rs ci ifs2 r ->+  RegisterConstraintExtraction+extractRegisterOrdering relation left right+  | Just variable <- registerVariable left,+    Just literalValue <- termLiteralValue right =+      let normalized = pureRelation relation+       in knownRegisterComparison+            variable+            normalized+            literalValue+            (\value -> applyPureRelation normalized value literalValue)+  | Just literalValue <- termLiteralValue left,+    Just variable <- registerVariable right =+      let normalized = flipPureRelation (pureRelation relation)+       in knownRegisterComparison+            variable+            normalized+            literalValue+            (\value -> applyPureRelation normalized value literalValue)+  | otherwise = unsupportedRegisterAtom "ordering" left right++registerVariable ::+  forall rs ci ifs r.+  (Typeable r) =>+  Term rs ci ifs r ->+  Maybe RegisterVariable+registerVariable (TReg index) =+  Just+    RegisterVariable+      { registerVariablePosition = indexPosition index,+        registerVariableType = SomeTypeRep (typeRep @r),+        registerVariableLabel = pureIndexName index+      }+registerVariable _ = Nothing++knownRegisterComparison ::+  forall r.+  (Typeable r) =>+  RegisterVariable ->+  PureRelation ->+  r ->+  (r -> Bool) ->+  RegisterConstraintExtraction+knownRegisterComparison variable relation literalValue accepts =+  case discoverIntegralDomain @r of+    Nothing ->+      blockedRegisterConstraintExtraction+        ( "unsupported register carrier "+            <> show (typeRep @r)+            <> " at position "+            <> show variable.registerVariablePosition+        )+    Just _ ->+      emptyRegisterConstraintExtraction+        { registerExtractionComparisons =+            [RegisterComparison variable relation literalValue accepts]+        }++unsupportedRegisterAtom ::+  String ->+  Term rs ci ifs1 r ->+  Term rs ci ifs2 r ->+  RegisterConstraintExtraction+unsupportedRegisterAtom relation left right =+  blockedRegisterConstraintExtraction+    ( "unsupported "+        <> relation+        <> " conjunct: "+        <> registerAtomObstacle left right+    )++registerAtomObstacle :: Term rs ci ifs1 r -> Term rs ci ifs2 r -> String+registerAtomObstacle left right =+  case termRegisterObstacle left of+    Just obstacle -> obstacle+    Nothing -> case termRegisterObstacle right of+      Just obstacle -> obstacle+      Nothing -> case (left, right) of+        (TReg _, TReg _) -> "register-to-register comparison"+        (TLit _, TLit _) -> "literal-only comparison"+        (TLit _, TOpaqueLit _) -> "literal-only comparison"+        (TOpaqueLit _, TLit _) -> "literal-only comparison"+        (TOpaqueLit _, TOpaqueLit _) -> "literal-only comparison"+        _ -> "unknown term relationship"++termRegisterObstacle :: Term rs ci ifs r -> Maybe String+termRegisterObstacle (TInpCtorField _ _) = Just "input-field read (TInpCtorField)"+termRegisterObstacle (TApp1 _ _) = Just "opaque unary application (TApp1)"+termRegisterObstacle (TApp2 _ _ _) = Just "opaque binary application (TApp2)"+termRegisterObstacle (TArith _ _ _) = Just "structural arithmetic (TArith)"+termRegisterObstacle TFieldProj {} = Just "field projection (TFieldProj)"+termRegisterObstacle _ = Nothing++sameRegisterVariable :: RegisterVariable -> RegisterVariable -> Bool+sameRegisterVariable left right =+  left.registerVariablePosition == right.registerVariablePosition+    && left.registerVariableType == right.registerVariableType++registerComparisonVariable :: RegisterComparison -> RegisterVariable+registerComparisonVariable (RegisterComparison variable _ _ _) = variable++groupRegisterComparisons :: [RegisterComparison] -> [[RegisterComparison]]+groupRegisterComparisons [] = []+groupRegisterComparisons (comparison : rest) =+  (comparison : sameVariable) : groupRegisterComparisons otherVariables+  where+    variable = registerComparisonVariable comparison+    (sameVariable, otherVariables) =+      partition+        (sameRegisterVariable variable . registerComparisonVariable)+        rest++alignRegisterComparison ::+  forall r. (Typeable r) => RegisterComparison -> Maybe (TypedPureComparison r)+alignRegisterComparison+  (RegisterComparison @other _ relation literalValue accepts) =+    case eqTypeRep (typeRep @r) (typeRep @other) of+      Just HRefl -> Just (TypedPureComparison relation literalValue accepts)+      Nothing -> Nothing++registerComparisonGroupVerdict :: [RegisterComparison] -> RegisterConstraintVerdict+registerComparisonGroupVerdict [] = RegisterConstraintsSatisfiable+registerComparisonGroupVerdict+  (RegisterComparison @r _ relation literalValue accepts : rest) =+    case traverse (alignRegisterComparison @r) rest of+      Nothing -> RegisterConstraintsUnknown+      Just alignedRest ->+        let comparisons =+              TypedPureComparison relation literalValue accepts : alignedRest+         in case discoverIntegralDomain @r of+              Nothing -> RegisterConstraintsUnknown+              Just domain+                | integralComparisonsSatisfiable domain comparisons ->+                    RegisterConstraintsSatisfiable+                | otherwise -> RegisterConstraintsUnsatisfiable++registerPositionTypeMismatch :: [RegisterComparison] -> Maybe String+registerPositionTypeMismatch comparisons =+  case [ (leftVariable, rightVariable)+       | left <- comparisons,+         right <- comparisons,+         let leftVariable = registerComparisonVariable left,+         let rightVariable = registerComparisonVariable right,+         leftVariable.registerVariablePosition == rightVariable.registerVariablePosition,+         leftVariable.registerVariableType /= rightVariable.registerVariableType+       ] of+    (leftVariable, rightVariable) : _ ->+      Just+        ( "register type alignment failed at position "+            <> show leftVariable.registerVariablePosition+            <> ": "+            <> show leftVariable.registerVariableType+            <> " versus "+            <> show rightVariable.registerVariableType+        )+    [] -> Nothing++duplicateRegisterLabelDetail :: [RegisterComparison] -> Maybe String+duplicateRegisterLabelDetail comparisons =+  case [ (label, positions)+       | label <- nub (map registerVariableLabel variables),+         let positions =+               nub+                 [ variable.registerVariablePosition+                 | variable <- variables,+                   variable.registerVariableLabel == label+                 ],+         length positions > 1+       ] of+    (label, positions) : _ ->+      Just+        ( "shared-register conditions are satisfiable across distinct positions "+            <> show positions+            <> " carrying duplicate label \""+            <> label+            <> "\""+        )+    [] -> Nothing+  where+    variables = map registerComparisonVariable comparisons++analyzeCandidateRegisterConstraints ::+  HsPred rs ci ->+  HsPred rs ci ->+  CandidateRegisterAnalysis+analyzeCandidateRegisterConstraints leftGuard rightGuard =+  case verdict of+    RegisterConstraintsUnsatisfiable ->+      CandidateRegisterAnalysis+        { candidateRegisterDisjointness = ProvenCandidateDisjoint,+          candidateRegisterDetail =+            "shared-register necessary conditions are unsatisfiable"+        }+    RegisterConstraintsSatisfiable ->+      CandidateRegisterAnalysis+        { candidateRegisterDisjointness = CandidateDisjointnessNotProven,+          candidateRegisterDetail =+            case duplicateRegisterLabelDetail comparisons of+              Just detail -> detail+              Nothing -> "shared-register necessary conditions are satisfiable"+        }+    RegisterConstraintsUnknown ->+      CandidateRegisterAnalysis+        { candidateRegisterDisjointness = CandidateDisjointnessNotProven,+          candidateRegisterDetail =+            case registerPositionTypeMismatch comparisons of+              Just detail -> detail+              Nothing -> case registerExtractionBlockers extraction of+                blocker : _ -> "register proof blocked by " <> blocker+                [] -> "register constraint verdict is unknown"+        }+  where+    extraction =+      mergeRegisterConstraintExtractions+        (extractRegisterConstraints leftGuard)+        (extractRegisterConstraints rightGuard)+    comparisons = registerExtractionComparisons extraction+    groupVerdicts =+      map registerComparisonGroupVerdict (groupRegisterComparisons comparisons)+    verdict+      | registerExtractionIsBottom extraction = RegisterConstraintsUnsatisfiable+      | RegisterConstraintsUnsatisfiable `elem` groupVerdicts =+          RegisterConstraintsUnsatisfiable+      | registerPositionTypeMismatch comparisons /= Nothing =+          RegisterConstraintsUnknown+      | RegisterConstraintsUnknown `elem` groupVerdicts = RegisterConstraintsUnknown+      | not (null (registerExtractionBlockers extraction)) = RegisterConstraintsUnknown+      | otherwise = RegisterConstraintsSatisfiable  -- | One normalized @variable relation literal@ atom. The predicate closure -- captures the source constructor's real 'Eq' or 'Ord' dictionary for concrete

@@ -5,16 +5,33 @@ -- without hand-rolling RCons-towers. -- -- Status: experimental. See the EP-2 retrospective for context.+--+-- == Trust model+--+-- Trusted structural schemas minted by the @Via@ producers are rooted in the+-- lawfulness of the consumer type's 'GHC.Generics.Generic' instance: the+-- constructor path, field spine, and the match\/build closures are all read+-- from the same @Rep@. A derived instance is always lawful, so+-- @deriving stock Generic@ types get honest evidence by construction. A+-- hand-written, deliberately unlawful 'GHC.Generics.Generic' instance can+-- pair trusted evidence with behavior it does not describe; that path is+-- outside the threat model in exactly the way 'Unsafe.Coerce.unsafeCoerce'+-- is. Keiki's sealed boundaries defend against /accidental/ decoupling —+-- record updates, closure-taking helpers, forged capabilities — not against a+-- consumer determined to lie to the compiler. module Keiki.Generics   ( -- * Generic-derived InCtor     mkInCtor,     mkInCtor0,     mkInCtorVia,+    mkInCtorRecordVia,      -- * Generic-derived WireCtor     mkWireCtor,     mkWireCtor0,     mkWireCtorVia,+    mkWireCtor0Via,+    mkWireCtorRecordVia,     FieldsOf,     FieldsOfRep, @@ -25,11 +42,6 @@     -- * Empty register file     EmptyRegFile (..), -    -- * Sum-walking machinery-    GHasCtor (..),-    GHasCtorIf (..),-    NameInRep,-     -- * Internals     GRecord (..),     GTuple (..),@@ -44,9 +56,28 @@ import Data.Kind (Type) import Data.Proxy (Proxy (..)) import Data.Type.Bool (type (||))+import Data.Typeable (Typeable) import GHC.Generics import GHC.TypeLits (KnownSymbol, Symbol, symbolVal) import Keiki.Core+import Keiki.Internal.ConstructorEvidence (constructorEvidence)+import Keiki.Internal.WireSchema+  ( AppendInCtorFields,+    AppendWireFields,+    InCtorFieldSchema,+    WireCtorPath,+    appendInCtorFieldSchema,+    appendWireFieldSchema,+    genericPrefixWireCtorPathLeft,+    genericPrefixWireCtorPathRight,+    inCtorFieldsCons,+    inCtorFieldsNil,+    trustedInCtorSchema,+    trustedWireSchema,+    wireCtorPathRoot,+    wireFieldsCons,+    wireFieldsNil,+  )  -- | Walk a 'GHC.Generics' record representation to/from a 'RegFile'. -- Slot lists are derived from the record's field metadata: every@@ -144,14 +175,15 @@   (ci -> Maybe d) ->   (d -> ci) ->   InCtor ci ifs+{-# DEPRECATED mkInCtor "Use mkInCtorVia for Generic constructors, or unavailableInCtor for manual behavior." #-} mkInCtor name match wrap =-  InCtor-    { icName = name,-      icMatch = \ci -> case match ci of+  unavailableInCtor+    name+    ( \ci -> case match ci of         Just d -> Just (gToRegFile (from d))-        Nothing -> Nothing,-      icBuild = \rf -> wrap (to (gFromRegFile rf))-    }+        Nothing -> Nothing+    )+    (\rf -> wrap (to (gFromRegFile rf)))  -- | Build an 'InCtor' for a no-payload (singleton) constructor. The -- 'icMatch' compares against the named singleton via 'Eq'; 'icBuild'@@ -162,12 +194,12 @@ -- > inCtorContinue :: InCtor UserCmd '[] -- > inCtorContinue = mkInCtor0 "Continue" Continue mkInCtor0 :: forall ci. (Eq ci) => String -> ci -> InCtor ci '[]+{-# DEPRECATED mkInCtor0 "Use mkInCtorVia for Generic nullary constructors, or unavailableInCtor for manual behavior." #-} mkInCtor0 name singleton =-  InCtor-    { icName = name,-      icMatch = \ci -> if ci == singleton then Just RNil else Nothing,-      icBuild = \RNil -> singleton-    }+  unavailableInCtor+    name+    (\ci -> if ci == singleton then Just RNil else Nothing)+    (\RNil -> singleton)  -- * Generic-derived WireCtor ---------------------------------------------- @@ -207,9 +239,7 @@     (lt, rt) -> gFromTuple lt :*: gFromTuple rt  -- | Type-level concat for nested-pair tuples. @ConcatT (f1, (f2, ())) (f3, ()) ~ (f1, (f2, (f3, ())))@.-type family ConcatT (a :: Type) (b :: Type) :: Type where-  ConcatT () b = b-  ConcatT (x, xs) b = (x, ConcatT xs b)+type ConcatT (a :: Type) (b :: Type) = AppendWireFields a b  -- | Split a concatenated nested-pair tuple back into its halves; also -- the inverse direction (append).@@ -271,6 +301,7 @@ -- > wireRegistrationStarted = mkWireCtor "RegistrationStarted" -- >   (\case RegistrationStarted d -> Just d; _ -> Nothing) -- >   RegistrationStarted+{-# DEPRECATED mkWireCtor "Use mkWireCtorVia for Generic constructors, or unavailableWireCtor for manual behavior." #-} mkWireCtor ::   forall co d fs.   ( Generic d,@@ -281,13 +312,13 @@   (d -> co) ->   WireCtor co fs mkWireCtor name match wrap =-  WireCtor-    { wcName = name,-      wcMatch = \co -> case match co of+  unavailableWireCtor+    name+    ( \co -> case match co of         Just d -> Just (gToTuple (from d))-        Nothing -> Nothing,-      wcBuild = \fs -> wrap (to (gFromTuple fs))-    }+        Nothing -> Nothing+    )+    (\fs -> wrap (to (gFromTuple fs)))  -- | Build a 'WireCtor' for a no-payload (singleton) event constructor — -- the event-side twin of 'mkInCtor0'. Its field tuple is @()@ (a@@ -301,13 +332,13 @@ -- -- > wireOpened :: WireCtor DoorEvent () -- > wireOpened = mkWireCtor0 "Opened" Opened+{-# DEPRECATED mkWireCtor0 "Use mkWireCtor0Via for Generic nullary constructors, or unavailableWireCtor for manual behavior." #-} mkWireCtor0 :: forall co. (Eq co) => String -> co -> WireCtor co () mkWireCtor0 name singleton =-  WireCtor-    { wcName = name,-      wcMatch = \co -> if co == singleton then Just () else Nothing,-      wcBuild = \() -> singleton-    }+  unavailableWireCtor+    name+    (\co -> if co == singleton then Just () else Nothing)+    (\() -> singleton)  -- * Empty register file --------------------------------------------------- @@ -366,6 +397,130 @@   gMatchCtor :: rep a -> Maybe d   gBuildCtor :: d -> rep a +-- | Derive the ordinal sum path of a named constructor. This class is kept+-- private so consumers cannot supply a dishonest path instance.+class GWireCtorPath (name :: Symbol) (rep :: Type -> Type) where+  gWireCtorPath :: WireCtorPath carrier++instance (GWireCtorPath name inner) => GWireCtorPath name (M1 D meta inner) where+  gWireCtorPath = gWireCtorPath @name @inner++instance GWireCtorPath name (M1 C ('MetaCons name fix lazy) payload) where+  gWireCtorPath = wireCtorPathRoot++instance+  ( hasLeft ~ NameInRep name left,+    GWireCtorPathIf hasLeft name left right+  ) =>+  GWireCtorPath name (left :+: right)+  where+  gWireCtorPath = gWireCtorPathIf @hasLeft @name @left @right++class+  GWireCtorPathIf+    (hasLeft :: Bool)+    (name :: Symbol)+    (left :: Type -> Type)+    (right :: Type -> Type)+  where+  gWireCtorPathIf :: WireCtorPath carrier++instance (GWireCtorPath name left) => GWireCtorPathIf 'True name left right where+  gWireCtorPathIf =+    genericPrefixWireCtorPathLeft (gWireCtorPath @name @left)++instance (GWireCtorPath name right) => GWireCtorPathIf 'False name left right where+  gWireCtorPathIf =+    genericPrefixWireCtorPathRight (gWireCtorPath @name @right)++-- | Derive a typed, source-ordered field spine from a payload's Generic+-- representation. Like 'GWireCtorPath', this class is private so only the+-- library's Generic instances can mint trusted evidence.+class GWireFieldSchema (rep :: Type -> Type) (fields :: Type) | rep -> fields where+  gWireFieldSchema :: WireFieldSchema fields++instance (GWireFieldSchema inner fields) => GWireFieldSchema (M1 D meta inner) fields where+  gWireFieldSchema = gWireFieldSchema @inner++instance (GWireFieldSchema inner fields) => GWireFieldSchema (M1 C meta inner) fields where+  gWireFieldSchema = gWireFieldSchema @inner++instance+  (Typeable field, Selector meta) =>+  GWireFieldSchema (M1 S meta (K1 r field)) (field, ())+  where+  gWireFieldSchema =+    wireFieldsCons selectorLabel wireFieldsNil+    where+      selectorText = selName (undefined :: M1 S meta (K1 r field) ())+      selectorLabel+        | null selectorText = Nothing+        | otherwise = Just selectorText++instance GWireFieldSchema U1 () where+  gWireFieldSchema = wireFieldsNil++instance+  ( GWireFieldSchema left leftFields,+    GWireFieldSchema right rightFields,+    ConcatT leftFields rightFields ~ fields+  ) =>+  GWireFieldSchema (left :*: right) fields+  where+  gWireFieldSchema =+    appendWireFieldSchema+      (gWireFieldSchema @left)+      (gWireFieldSchema @right)++-- | Derive a typed, source-ordered slot spine from an input payload's+-- Generic representation. This class is private so only Keiki's Generic+-- implementation can mint trusted input-constructor evidence.+class+  GInCtorFieldSchema+    (rep :: Type -> Type)+    (fields :: [Slot])+    | rep -> fields+  where+  gInCtorFieldSchema :: InCtorFieldSchema fields++instance+  (GInCtorFieldSchema inner fields) =>+  GInCtorFieldSchema (M1 D meta inner) fields+  where+  gInCtorFieldSchema = gInCtorFieldSchema @inner++instance+  (GInCtorFieldSchema inner fields) =>+  GInCtorFieldSchema (M1 C meta inner) fields+  where+  gInCtorFieldSchema = gInCtorFieldSchema @inner++instance+  (KnownSymbol name, Typeable field) =>+  GInCtorFieldSchema+    (M1 S ('MetaSel ('Just name) su ss ds) (K1 r field))+    '[ '(name, field)]+  where+  gInCtorFieldSchema =+    inCtorFieldsCons+      (Just (symbolVal (Proxy @name)))+      inCtorFieldsNil++instance GInCtorFieldSchema U1 '[] where+  gInCtorFieldSchema = inCtorFieldsNil++instance+  ( GInCtorFieldSchema left leftFields,+    GInCtorFieldSchema right rightFields,+    AppendInCtorFields leftFields rightFields ~ fields+  ) =>+  GInCtorFieldSchema (left :*: right) fields+  where+  gInCtorFieldSchema =+    appendInCtorFieldSchema+      (gInCtorFieldSchema @left)+      (gInCtorFieldSchema @right)+ -- Pass through the data-type wrapper. instance (GHasCtor n inner d) => GHasCtor n (M1 D meta inner) d where   gMatchCtor (M1 r) = gMatchCtor @n r@@ -415,6 +570,138 @@   gMatchCtorIf (R1 x) = gMatchCtor @n x   gBuildCtorIf d = R1 (gBuildCtor @n d) +-- | Direct-record counterpart of 'GHasCtor'. Instead of resolving one+-- wrapped payload value, this class derives a 'RegFile' directly from the+-- named constructor's own record fields.+class+  GRecordCtor+    (name :: Symbol)+    (rep :: Type -> Type)+    (fields :: [Slot])+    | name rep -> fields+  where+  gMatchRecordCtor :: rep a -> Maybe (RegFile fields)+  gBuildRecordCtor :: RegFile fields -> rep a+  gRecordCtorSchema :: InCtorFieldSchema fields++instance+  (GRecordCtor name inner fields) =>+  GRecordCtor name (M1 D meta inner) fields+  where+  gMatchRecordCtor (M1 representation) = gMatchRecordCtor @name representation+  gBuildRecordCtor fields = M1 (gBuildRecordCtor @name fields)+  gRecordCtorSchema = gRecordCtorSchema @name @inner++instance+  ( GRecord inner fields,+    GInCtorFieldSchema inner fields+  ) =>+  GRecordCtor name (M1 C ('MetaCons name fix lazy) inner) fields+  where+  gMatchRecordCtor (M1 representation) = Just (gToRegFile representation)+  gBuildRecordCtor fields = M1 (gFromRegFile fields)+  gRecordCtorSchema = gInCtorFieldSchema @inner++instance+  ( hasLeft ~ NameInRep name left,+    GRecordCtorIf hasLeft name left right fields+  ) =>+  GRecordCtor name (left :+: right) fields+  where+  gMatchRecordCtor = gMatchRecordCtorIf @hasLeft @name+  gBuildRecordCtor = gBuildRecordCtorIf @hasLeft @name+  gRecordCtorSchema = gRecordCtorSchemaIf @hasLeft @name @left @right++class+  GRecordCtorIf+    (hasLeft :: Bool)+    (name :: Symbol)+    (left :: Type -> Type)+    (right :: Type -> Type)+    (fields :: [Slot])+    | hasLeft name left right -> fields+  where+  gMatchRecordCtorIf :: (left :+: right) a -> Maybe (RegFile fields)+  gBuildRecordCtorIf :: RegFile fields -> (left :+: right) a+  gRecordCtorSchemaIf :: InCtorFieldSchema fields++instance (GRecordCtor name left fields) => GRecordCtorIf 'True name left right fields where+  gMatchRecordCtorIf (L1 representation) = gMatchRecordCtor @name representation+  gMatchRecordCtorIf (R1 _) = Nothing+  gBuildRecordCtorIf fields = L1 (gBuildRecordCtor @name fields)+  gRecordCtorSchemaIf = gRecordCtorSchema @name @left++instance (GRecordCtor name right fields) => GRecordCtorIf 'False name left right fields where+  gMatchRecordCtorIf (L1 _) = Nothing+  gMatchRecordCtorIf (R1 representation) = gMatchRecordCtor @name representation+  gBuildRecordCtorIf fields = R1 (gBuildRecordCtor @name fields)+  gRecordCtorSchemaIf = gRecordCtorSchema @name @right++-- | Direct-record wire counterpart of 'GRecordCtor'.+class+  GTupleCtor+    (name :: Symbol)+    (rep :: Type -> Type)+    (fields :: Type)+    | name rep -> fields+  where+  gMatchTupleCtor :: rep a -> Maybe fields+  gBuildTupleCtor :: fields -> rep a+  gTupleCtorSchema :: WireFieldSchema fields++instance+  (GTupleCtor name inner fields) =>+  GTupleCtor name (M1 D meta inner) fields+  where+  gMatchTupleCtor (M1 representation) = gMatchTupleCtor @name representation+  gBuildTupleCtor fields = M1 (gBuildTupleCtor @name fields)+  gTupleCtorSchema = gTupleCtorSchema @name @inner++instance+  ( GTuple inner fields,+    GWireFieldSchema inner fields+  ) =>+  GTupleCtor name (M1 C ('MetaCons name fix lazy) inner) fields+  where+  gMatchTupleCtor (M1 representation) = Just (gToTuple representation)+  gBuildTupleCtor fields = M1 (gFromTuple fields)+  gTupleCtorSchema = gWireFieldSchema @inner++instance+  ( hasLeft ~ NameInRep name left,+    GTupleCtorIf hasLeft name left right fields+  ) =>+  GTupleCtor name (left :+: right) fields+  where+  gMatchTupleCtor = gMatchTupleCtorIf @hasLeft @name+  gBuildTupleCtor = gBuildTupleCtorIf @hasLeft @name+  gTupleCtorSchema = gTupleCtorSchemaIf @hasLeft @name @left @right++class+  GTupleCtorIf+    (hasLeft :: Bool)+    (name :: Symbol)+    (left :: Type -> Type)+    (right :: Type -> Type)+    (fields :: Type)+    | hasLeft name left right -> fields+  where+  gMatchTupleCtorIf :: (left :+: right) a -> Maybe fields+  gBuildTupleCtorIf :: fields -> (left :+: right) a+  gTupleCtorSchemaIf :: WireFieldSchema fields++instance (GTupleCtor name left fields) => GTupleCtorIf 'True name left right fields where+  gMatchTupleCtorIf (L1 representation) = gMatchTupleCtor @name representation+  gMatchTupleCtorIf (R1 _) = Nothing+  gBuildTupleCtorIf fields = L1 (gBuildTupleCtor @name fields)+  gTupleCtorSchemaIf = gTupleCtorSchema @name @left++instance (GTupleCtor name right fields) => GTupleCtorIf 'False name left right fields where+  gMatchTupleCtorIf (L1 _) = Nothing+  gMatchTupleCtorIf (R1 representation) = gMatchTupleCtor @name representation+  gBuildTupleCtorIf fields = R1 (gBuildTupleCtor @name fields)+  gTupleCtorSchemaIf = gTupleCtorSchema @name @right+ -- * Generic-derived InCtor / WireCtor (Via builders) ----------------------  -- | Build an 'InCtor' from a constructor name alone. The sum-side@@ -435,24 +722,56 @@   ( KnownSymbol name,     Generic ci,     GHasCtor name (Rep ci) d,+    GWireCtorPath name (Rep ci),     Generic d,     GRecord (Rep d) ifs,+    GInCtorFieldSchema (Rep d) ifs,     AssembleRegFile ifs,     KnownSlotNames ifs   ) =>   InCtor ci ifs mkInCtorVia =-  InCtor-    { icName = symbolVal (Proxy @name),-      icMatch = \ci -> case gMatchCtor @name (from ci) of+  trustedInCtorInternal+    constructorEvidence+    (symbolVal (Proxy @name))+    ( trustedInCtorSchema+        (gWireCtorPath @name @(Rep ci))+        (gInCtorFieldSchema @(Rep d))+    )+    ( \ci -> case gMatchCtor @name (from ci) of         Just d -> Just (gToRegFile (from d))-        Nothing -> Nothing,-      icBuild = \rf -> to (gBuildCtor @name (to (gFromRegFile rf) :: d))-    }+        Nothing -> Nothing+    )+    (\rf -> to (gBuildCtor @name (to (gFromRegFile rf) :: d))) --- | Build a 'WireCtor' from a constructor name alone. Mirrors+-- | Build a trusted 'InCtor' for a constructor whose payload fields are+-- declared directly with record syntax. Use 'mkInCtorVia' when the sum+-- constructor instead wraps a separate record value.+mkInCtorRecordVia ::+  forall (name :: Symbol) ci ifs.+  ( KnownSymbol name,+    Generic ci,+    GRecordCtor name (Rep ci) ifs,+    GWireCtorPath name (Rep ci),+    AssembleRegFile ifs,+    KnownSlotNames ifs+  ) =>+  InCtor ci ifs+mkInCtorRecordVia =+  trustedInCtorInternal+    constructorEvidence+    (symbolVal (Proxy @name))+    ( trustedInCtorSchema+        (gWireCtorPath @name @(Rep ci))+        (gRecordCtorSchema @name @(Rep ci))+    )+    (gMatchRecordCtor @name . from)+    (to . gBuildRecordCtor @name)++-- | Build a trusted 'WireCtor' from a constructor name alone. Mirrors -- 'mkInCtorVia' on the wire side: the nested-pair field tuple comes--- from the inferred payload's 'Generic' field metadata.+-- from the inferred payload's 'Generic' field metadata, while the carrier's+-- Generic sum path and ordered field types become its structural schema. -- -- Example: --@@ -464,15 +783,57 @@   ( KnownSymbol name,     Generic co,     GHasCtor name (Rep co) d,+    GWireCtorPath name (Rep co),     Generic d,-    GTuple (Rep d) fs+    GTuple (Rep d) fs,+    GWireFieldSchema (Rep d) fs   ) =>   WireCtor co fs mkWireCtorVia =-  WireCtor-    { wcName = symbolVal (Proxy @name),-      wcMatch = \co -> case gMatchCtor @name (from co) of+  trustedWireCtorInternal+    constructorEvidence+    (symbolVal (Proxy @name))+    ( trustedWireSchema+        (gWireCtorPath @name @(Rep co))+        (gWireFieldSchema @(Rep d))+    )+    ( \co -> case gMatchCtor @name (from co) of         Just d -> Just (gToTuple (from d))-        Nothing -> Nothing,-      wcBuild = \fs -> to (gBuildCtor @name (to (gFromTuple fs) :: d))-    }+        Nothing -> Nothing+    )+    (\fs -> to (gBuildCtor @name (to (gFromTuple fs) :: d)))++-- | Build a trusted 'WireCtor' for a named no-payload constructor using+-- structural Generic matching. Unlike 'mkWireCtor0', matching is not+-- mediated by the carrier's 'Eq' instance.+mkWireCtor0Via ::+  forall (name :: Symbol) co.+  ( KnownSymbol name,+    Generic co,+    GHasCtor name (Rep co) (),+    GWireCtorPath name (Rep co)+  ) =>+  WireCtor co ()+mkWireCtor0Via = mkWireCtorVia @name @co @() @()++-- | Build a trusted 'WireCtor' for a constructor whose fields are declared+-- directly with record syntax. Use 'mkWireCtorVia' for a constructor that+-- wraps a separate record value.+mkWireCtorRecordVia ::+  forall (name :: Symbol) co fields.+  ( KnownSymbol name,+    Generic co,+    GTupleCtor name (Rep co) fields,+    GWireCtorPath name (Rep co)+  ) =>+  WireCtor co fields+mkWireCtorRecordVia =+  trustedWireCtorInternal+    constructorEvidence+    (symbolVal (Proxy @name))+    ( trustedWireSchema+        (gWireCtorPath @name @(Rep co))+        (gTupleCtorSchema @name @(Rep co))+    )+    (gMatchTupleCtor @name . from)+    (to . gBuildTupleCtor @name)

@@ -115,9 +115,8 @@ import Keiki.Generics   ( FieldsOf,     RegFieldsOf,-    mkInCtor0,     mkInCtorVia,-    mkWireCtor0,+    mkWireCtor0Via,     mkWireCtorVia,   ) import Language.Haskell.TH@@ -696,7 +695,7 @@  singletonDecls ::   Name -> Name -> String -> String -> Name -> Q [Dec]-singletonDecls cmdName regsName ctorStr shortStr ctorN = do+singletonDecls cmdName regsName ctorStr shortStr _ctorN = do   let inCtorN = mkName ("inCtor" <> shortStr)       isN = mkName ("is" <> shortStr)   inCtorSig <-@@ -709,11 +708,10 @@       [ clause           []           ( normalB-              [|-                mkInCtor0-                  $(litE (stringL ctorStr))-                  $(conE ctorN)-                |]+              ( appTypeE+                  [|mkInCtorVia|]+                  (litT (strTyLit ctorStr))+              )           )           []       ]@@ -841,10 +839,10 @@         pure ([wireSig, wireDef] ++ termRecDecs)       Just Nothing ->         -- Zero-arg (singleton) event: emit only the wire<Short> binding-        -- via mkWireCtor0 (no payload, so no <Short>TermFields record).-        -- Mirrors the command side's singletonDecls/mkInCtor0.+        -- via structural Generic matching (no payload, so no+        -- <Short>TermFields record).         case conNames con of-          (cn : _) -> do+          (_ : _) -> do             let wireN = mkName ("wire" <> shortStr)             wireSig <-               sigD@@ -856,11 +854,10 @@                 [ clause                     []                     ( normalB-                        [|-                          mkWireCtor0-                            $(litE (stringL ctorStr))-                            $(conE cn)-                          |]+                        ( appTypeE+                            [|mkWireCtor0Via|]+                            (litT (strTyLit ctorStr))+                        )                     )                     []                 ]

@@ -0,0 +1,13 @@+-- | Package-private capability for constructing schema-bearing input and wire+-- constructors. The module is listed under @other-modules@, so downstream+-- packages cannot obtain the constructor needed by Keiki's trusted producers.+module Keiki.Internal.ConstructorEvidence+  ( ConstructorEvidence (..),+    constructorEvidence,+  )+where++data ConstructorEvidence = ConstructorEvidence++constructorEvidence :: ConstructorEvidence+constructorEvidence = ConstructorEvidence

@@ -0,0 +1,652 @@+{-# LANGUAGE GADTs #-}+{-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE TypeAbstractions #-}+{-# LANGUAGE TypeFamilies #-}++-- | Internal constructors and operations for structural wire schemas.+--+-- The public surface is re-exported abstractly from "Keiki.Core". Keeping+-- these constructors in a hidden module prevents consumers from turning+-- names or casts into trusted replay evidence.+module Keiki.Internal.WireSchema+  ( WireSchema,+    WireFieldSchema,+    InCtorSchema,+    InCtorFieldSchema,+    WireCtorPath,+    AppendWireFields,+    AppendInCtorFields,+    WireSchemaAvailability (..),+    InCtorSchemaAvailability (..),+    WireHeadRelation (..),+    InputHeadRelation (..),+    InputWireHeadRelation (..),+    WireFieldAlignment (..),+    WireSchemaComparison (..),+    InCtorFieldAlignment (..),+    InCtorSchemaComparison (..),+    InWireFieldAlignment (..),+    InWireSchemaComparison (..),+    wireSchemaUnavailable,+    wireSchemaAvailability,+    inCtorSchemaUnavailable,+    inCtorSchemaAvailability,+    trustedWireSchema,+    trustedInCtorSchema,+    compositionOnlyWireSchema,+    compositionOnlyInCtorSchema,+    wireFieldsNil,+    wireFieldsCons,+    inCtorFieldsNil,+    inCtorFieldsCons,+    appendWireFieldSchema,+    appendInCtorFieldSchema,+    wireCtorPathRoot,+    prefixWireCtorPathLeft,+    prefixWireCtorPathRight,+    genericPrefixWireCtorPathLeft,+    genericPrefixWireCtorPathRight,+    prefixWireSchemaLeft,+    prefixWireSchemaRight,+    prefixInCtorSchemaLeft,+    prefixInCtorSchemaRight,+    compareWireSchemas,+    compareInCtorSchemas,+    compareInCtorWireSchemas,+    classifyInputWireSchemas,+    inputWireSpineRelationsForTesting,+    inCtorSchemaPath,+    wireSchemaPrefixRelationForTesting,+    inCtorSchemaPrefixRelationForTesting,+  )+where++import Data.Kind (Type)+import Data.Typeable (Typeable)+import GHC.TypeLits (Symbol)+import Type.Reflection (eqTypeRep, typeRep, type (:~~:) (HRefl))++-- | One structural step through either a Generic sum or an explicitly+-- checked 'Either' composition boundary.+data WireCtorPathStep+  = WireCtorPathLeft+  | WireCtorPathRight+  deriving stock (Eq, Show)++-- | A constructor's ordinal path through its carrier's sum tree.+--+-- The carrier is phantom because the type itself supplies the boundary;+-- callers cannot inspect or construct paths outside this hidden module.+newtype WireCtorPath co = WireCtorPath [WireCtorPathStep]++type role WireCtorPath nominal++-- | A typed, ordered description of a constructor's fields. Selector text+-- is diagnostic only; the spine position and 'Typeable' dictionary are the+-- proof evidence.+data WireFieldSchema fields where+  WireFieldsNil :: WireFieldSchema ()+  WireFieldsCons ::+    (Typeable field) =>+    Maybe String ->+    WireFieldSchema rest ->+    WireFieldSchema (field, rest)++type role WireFieldSchema nominal++-- | A typed, ordered description of an input constructor's slots. Slot+-- labels remain diagnostic; the spine position and 'Typeable' dictionary+-- are the proof evidence used to align an input read with an output field.+data InCtorFieldSchema (fields :: [(Symbol, Type)]) where+  InCtorFieldsNil :: InCtorFieldSchema '[]+  InCtorFieldsCons ::+    (Typeable field) =>+    Maybe String ->+    InCtorFieldSchema rest ->+    InCtorFieldSchema ('(name, field) ': rest)++type role InCtorFieldSchema nominal++-- | Typed path from an outer composition carrier back to the one payload type+-- introduced by the polymorphic identity boundary. The root pins payload and+-- carrier to the same type; each prefix records which 'Either' arm preserved+-- that payload. Lockstep comparison can therefore recover payload equality+-- from equal spines without a cast or a 'Typeable' dictionary.+data CompositionOnlySpine carrier payload where+  CompositionOnlyRoot :: CompositionOnlySpine carrier carrier+  CompositionOnlyLeft ::+    CompositionOnlySpine carrier payload ->+    CompositionOnlySpine (Either carrier other) payload+  CompositionOnlyRight ::+    CompositionOnlySpine carrier payload ->+    CompositionOnlySpine (Either other carrier) payload++type role CompositionOnlySpine nominal nominal++-- | Type-level append for the nested-pair field encoding.+type family AppendWireFields (left :: Type) (right :: Type) :: Type where+  AppendWireFields () right = right+  AppendWireFields (field, rest) right =+    (field, AppendWireFields rest right)++-- | Type-level append for input slot lists. Kept private so the schema+-- builder can combine Generic product spines without depending on+-- "Keiki.Core" and creating an import cycle.+type family+  AppendInCtorFields+    (left :: [(Symbol, Type)])+    (right :: [(Symbol, Type)]) ::+    [(Symbol, Type)]+  where+  AppendInCtorFields '[] right = right+  AppendInCtorFields (field ': rest) right =+    field ': AppendInCtorFields rest right++-- | Structural evidence carried by one output wire constructor.+data WireSchema co fields where+  UnavailableWireSchema :: WireSchema co fields+  CompositionOnlyWireSchema ::+    CompositionOnlySpine co field ->+    WireSchema co (field, ())+  TrustedWireSchema ::+    WireCtorPath co ->+    WireFieldSchema fields ->+    WireSchema co fields++type role WireSchema nominal nominal++-- | Structural evidence carried by one input constructor.+data InCtorSchema ci (fields :: [(Symbol, Type)]) where+  UnavailableInCtorSchema :: InCtorSchema ci fields+  CompositionOnlyInCtorSchema ::+    CompositionOnlySpine ci field ->+    InCtorSchema ci '[ '("payload", field)]+  TrustedInCtorSchema ::+    WireCtorPath ci ->+    InCtorFieldSchema fields ->+    InCtorSchema ci fields++type role InCtorSchema nominal nominal++-- | Public observation of whether structural proof evidence is present.+data WireSchemaAvailability+  = WireSchemaTrusted+  | WireSchemaUnavailable+  deriving stock (Eq, Show)++-- | Public observation of whether input-constructor proof evidence exists.+data InCtorSchemaAvailability+  = InCtorSchemaTrusted+  | InCtorSchemaUnavailable+  deriving stock (Eq, Show)++-- | Public, proof-safe classification of two output heads.+data WireHeadRelation+  = WireHeadsStructurallyEqual+  | WireHeadsStructurallyDifferent+  | WireHeadsUnwitnessed+  deriving stock (Eq, Show)++-- | Public, proof-safe classification of two input constructors.+data InputHeadRelation+  = InputHeadsStructurallyEqual+  | InputHeadsStructurallyDifferent+  | InputHeadsUnwitnessed+  deriving stock (Eq, Show)++-- | Public, proof-safe classification of one input constructor against one+-- output wire constructor at the same carrier — the observer form of the+-- checked composition alignment. The typed alignment witness stays internal.+data InputWireHeadRelation+  = InputWireHeadsAligned+  | InputWireHeadsStructurallyDifferent+  | InputWireHeadsUnwitnessed+  deriving stock (Eq, Show)++-- | A position-by-position type alignment between two field spines.+data WireFieldAlignment left right where+  WireFieldsAlignedNil :: WireFieldAlignment () ()+  WireFieldsAlignedCons ::+    (Typeable field) =>+    WireFieldAlignment left right ->+    WireFieldAlignment (field, left) (field, right)++-- | Internal comparison retaining the typed alignment needed by symbolic+-- translation. The public classifier projects this to 'WireHeadRelation'.+data WireSchemaComparison left right where+  WireSchemasEqual ::+    WireFieldAlignment left right ->+    WireSchemaComparison left right+  WireSchemasDifferent :: WireSchemaComparison left right+  WireSchemasUnwitnessed :: WireSchemaComparison left right++-- | Position-by-position alignment between two input slot spines.+data InCtorFieldAlignment left right where+  InCtorFieldsAlignedNil :: InCtorFieldAlignment '[] '[]+  InCtorFieldsAlignedCons ::+    (Typeable field) =>+    InCtorFieldAlignment left right ->+    InCtorFieldAlignment ('(leftName, field) ': left) ('(rightName, field) ': right)++-- | Internal comparison retaining the input-field alignment witness.+data InCtorSchemaComparison left right where+  InCtorSchemasEqual ::+    InCtorFieldAlignment left right ->+    InCtorSchemaComparison left right+  InCtorSchemasDifferent :: InCtorSchemaComparison left right+  InCtorSchemasUnwitnessed :: InCtorSchemaComparison left right++-- | Position-by-position alignment from input slots to an output wire's+-- nested-pair fields. This is the typed bridge used by composition.+data InWireFieldAlignment inputFields wireFields where+  InWireFieldsAlignedNil :: InWireFieldAlignment '[] ()+  InWireFieldsAlignedCons ::+    InWireFieldAlignment inputRest wireRest ->+    InWireFieldAlignment ('(name, field) ': inputRest) (field, wireRest)++-- | Checked structural relationship between an input constructor and an+-- output wire constructor over the same carrier.+data InWireSchemaComparison inputFields wireFields where+  InWireSchemasEqual ::+    InWireFieldAlignment inputFields wireFields ->+    InWireSchemaComparison inputFields wireFields+  InWireSchemasDifferent :: InWireSchemaComparison inputFields wireFields+  InWireSchemasUnwitnessed :: InWireSchemaComparison inputFields wireFields++-- | Explicitly mark a wire as lacking structural proof evidence.+wireSchemaUnavailable :: WireSchema co fields+wireSchemaUnavailable = UnavailableWireSchema++-- | Observe whether a schema is trusted without exposing its evidence.+wireSchemaAvailability :: WireSchema co fields -> WireSchemaAvailability+wireSchemaAvailability UnavailableWireSchema = WireSchemaUnavailable+wireSchemaAvailability CompositionOnlyWireSchema {} = WireSchemaUnavailable+wireSchemaAvailability TrustedWireSchema {} = WireSchemaTrusted++-- | Explicitly mark an input constructor as lacking structural evidence.+inCtorSchemaUnavailable :: InCtorSchema ci fields+inCtorSchemaUnavailable = UnavailableInCtorSchema++-- | Observe whether an input schema is trusted without exposing evidence.+inCtorSchemaAvailability ::+  InCtorSchema ci fields ->+  InCtorSchemaAvailability+inCtorSchemaAvailability UnavailableInCtorSchema = InCtorSchemaUnavailable+inCtorSchemaAvailability CompositionOnlyInCtorSchema {} = InCtorSchemaUnavailable+inCtorSchemaAvailability TrustedInCtorSchema {} = InCtorSchemaTrusted++-- | Internal trusted-schema constructor used only by Generic derivation.+trustedWireSchema ::+  WireCtorPath co ->+  WireFieldSchema fields ->+  WireSchema co fields+trustedWireSchema = TrustedWireSchema++-- | Internal trusted input-schema constructor used only by Generic+-- derivation and checked sum lifting.+trustedInCtorSchema ::+  WireCtorPath ci ->+  InCtorFieldSchema fields ->+  InCtorSchema ci fields+trustedInCtorSchema = TrustedInCtorSchema++-- | Hidden composition-only evidence for the polymorphic identity boundary.+-- It aligns the one payload slot with the one wire field but deliberately+-- remains unavailable to symbolic constructor-identity proofs.+compositionOnlyInCtorSchema ::+  InCtorSchema carrier '[ '("payload", carrier)]+compositionOnlyInCtorSchema = CompositionOnlyInCtorSchema CompositionOnlyRoot++-- | Output-side half of 'compositionOnlyInCtorSchema'.+compositionOnlyWireSchema :: WireSchema carrier (carrier, ())+compositionOnlyWireSchema = CompositionOnlyWireSchema CompositionOnlyRoot++wireFieldsNil :: WireFieldSchema ()+wireFieldsNil = WireFieldsNil++wireFieldsCons ::+  (Typeable field) =>+  Maybe String ->+  WireFieldSchema rest ->+  WireFieldSchema (field, rest)+wireFieldsCons = WireFieldsCons++inCtorFieldsNil :: InCtorFieldSchema '[]+inCtorFieldsNil = InCtorFieldsNil++inCtorFieldsCons ::+  (Typeable field) =>+  Maybe String ->+  InCtorFieldSchema rest ->+  InCtorFieldSchema ('(name, field) ': rest)+inCtorFieldsCons = InCtorFieldsCons++appendWireFieldSchema ::+  WireFieldSchema left ->+  WireFieldSchema right ->+  WireFieldSchema (AppendWireFields left right)+appendWireFieldSchema WireFieldsNil right = right+appendWireFieldSchema (WireFieldsCons label rest) right =+  WireFieldsCons label (appendWireFieldSchema rest right)++appendInCtorFieldSchema ::+  InCtorFieldSchema left ->+  InCtorFieldSchema right ->+  InCtorFieldSchema (AppendInCtorFields left right)+appendInCtorFieldSchema InCtorFieldsNil right = right+appendInCtorFieldSchema (InCtorFieldsCons label rest) right =+  InCtorFieldsCons label (appendInCtorFieldSchema rest right)++-- | The path of a constructor in a carrier with no enclosing sum node.+wireCtorPathRoot :: WireCtorPath co+wireCtorPathRoot = WireCtorPath []++prefixWireCtorPathLeft ::+  WireCtorPath co1 ->+  WireCtorPath (Either co1 co2)+prefixWireCtorPathLeft (WireCtorPath path) =+  WireCtorPath (WireCtorPathLeft : path)++prefixWireCtorPathRight ::+  WireCtorPath co2 ->+  WireCtorPath (Either co1 co2)+prefixWireCtorPathRight (WireCtorPath path) =+  WireCtorPath (WireCtorPathRight : path)++-- | Prefix a path while walking a 'GHC.Generics' sum. The result carrier is+-- supplied by the enclosing trusted schema; this less constrained operation+-- stays hidden with the Generic implementation.+genericPrefixWireCtorPathLeft :: WireCtorPath from -> WireCtorPath to+genericPrefixWireCtorPathLeft (WireCtorPath path) =+  WireCtorPath (WireCtorPathLeft : path)++-- | Right-arm counterpart of 'genericPrefixWireCtorPathLeft'.+genericPrefixWireCtorPathRight :: WireCtorPath from -> WireCtorPath to+genericPrefixWireCtorPathRight (WireCtorPath path) =+  WireCtorPath (WireCtorPathRight : path)++-- | Preserve a trusted schema while crossing a checked sum boundary.+prefixWireSchemaLeft ::+  WireSchema co1 fields ->+  WireSchema (Either co1 co2) fields+prefixWireSchemaLeft UnavailableWireSchema = UnavailableWireSchema+prefixWireSchemaLeft (CompositionOnlyWireSchema spine) =+  CompositionOnlyWireSchema (CompositionOnlyLeft spine)+prefixWireSchemaLeft (TrustedWireSchema path fields) =+  TrustedWireSchema (prefixWireCtorPathLeft path) fields++-- | Preserve a trusted schema while crossing a checked sum boundary.+prefixWireSchemaRight ::+  WireSchema co2 fields ->+  WireSchema (Either co1 co2) fields+prefixWireSchemaRight UnavailableWireSchema = UnavailableWireSchema+prefixWireSchemaRight (CompositionOnlyWireSchema spine) =+  CompositionOnlyWireSchema (CompositionOnlyRight spine)+prefixWireSchemaRight (TrustedWireSchema path fields) =+  TrustedWireSchema (prefixWireCtorPathRight path) fields++-- | Preserve trusted input evidence through a checked left sum boundary.+prefixInCtorSchemaLeft ::+  InCtorSchema ci1 fields ->+  InCtorSchema (Either ci1 ci2) fields+prefixInCtorSchemaLeft UnavailableInCtorSchema = UnavailableInCtorSchema+prefixInCtorSchemaLeft (CompositionOnlyInCtorSchema spine) =+  CompositionOnlyInCtorSchema (CompositionOnlyLeft spine)+prefixInCtorSchemaLeft (TrustedInCtorSchema path fields) =+  TrustedInCtorSchema (prefixWireCtorPathLeft path) fields++-- | Preserve trusted input evidence through a checked right sum boundary.+prefixInCtorSchemaRight ::+  InCtorSchema ci2 fields ->+  InCtorSchema (Either ci1 ci2) fields+prefixInCtorSchemaRight UnavailableInCtorSchema = UnavailableInCtorSchema+prefixInCtorSchemaRight (CompositionOnlyInCtorSchema spine) =+  CompositionOnlyInCtorSchema (CompositionOnlyRight spine)+prefixInCtorSchemaRight (TrustedInCtorSchema path fields) =+  TrustedInCtorSchema (prefixWireCtorPathRight path) fields++-- | Compare two trusted schemas. Paths count as different only when they+-- diverge at a common position. A proper-prefix relation remains+-- unwitnessed because the corresponding match sets can overlap.+compareWireSchemas ::+  WireSchema co left ->+  WireSchema co right ->+  WireSchemaComparison left right+compareWireSchemas UnavailableWireSchema _ = WireSchemasUnwitnessed+compareWireSchemas _ UnavailableWireSchema = WireSchemasUnwitnessed+compareWireSchemas CompositionOnlyWireSchema {} _ = WireSchemasUnwitnessed+compareWireSchemas _ CompositionOnlyWireSchema {} = WireSchemasUnwitnessed+compareWireSchemas+  (TrustedWireSchema (WireCtorPath leftPath) leftFields)+  (TrustedWireSchema (WireCtorPath rightPath) rightFields) =+    case comparePaths leftPath rightPath of+      PathsEqual ->+        maybe+          WireSchemasUnwitnessed+          WireSchemasEqual+          (alignWireFields leftFields rightFields)+      PathsDiverge -> WireSchemasDifferent+      PathsPrefixRelated -> WireSchemasUnwitnessed++-- | Compare two input constructors using path and slot-type evidence.+compareInCtorSchemas ::+  InCtorSchema ci left ->+  InCtorSchema ci right ->+  InCtorSchemaComparison left right+compareInCtorSchemas UnavailableInCtorSchema _ = InCtorSchemasUnwitnessed+compareInCtorSchemas _ UnavailableInCtorSchema = InCtorSchemasUnwitnessed+compareInCtorSchemas CompositionOnlyInCtorSchema {} _ = InCtorSchemasUnwitnessed+compareInCtorSchemas _ CompositionOnlyInCtorSchema {} = InCtorSchemasUnwitnessed+compareInCtorSchemas+  (TrustedInCtorSchema (WireCtorPath leftPath) leftFields)+  (TrustedInCtorSchema (WireCtorPath rightPath) rightFields) =+    case comparePaths leftPath rightPath of+      PathsEqual ->+        maybe+          InCtorSchemasUnwitnessed+          InCtorSchemasEqual+          (alignInCtorFields leftFields rightFields)+      PathsDiverge -> InCtorSchemasDifferent+      PathsPrefixRelated -> InCtorSchemasUnwitnessed++-- | Compare one input constructor with one output wire constructor.+compareInCtorWireSchemas ::+  InCtorSchema carrier inputFields ->+  WireSchema carrier wireFields ->+  InWireSchemaComparison inputFields wireFields+compareInCtorWireSchemas UnavailableInCtorSchema _ = InWireSchemasUnwitnessed+compareInCtorWireSchemas _ UnavailableWireSchema = InWireSchemasUnwitnessed+compareInCtorWireSchemas+  (CompositionOnlyInCtorSchema inputSpine)+  (CompositionOnlyWireSchema wireSpine) =+    compareCompositionOnlySpines inputSpine wireSpine+compareInCtorWireSchemas CompositionOnlyInCtorSchema {} _ = InWireSchemasUnwitnessed+compareInCtorWireSchemas _ CompositionOnlyWireSchema {} = InWireSchemasUnwitnessed+compareInCtorWireSchemas+  (TrustedInCtorSchema (WireCtorPath inputPath) inputFields)+  (TrustedWireSchema (WireCtorPath wirePath) wireFields) =+    case comparePaths inputPath wirePath of+      PathsEqual ->+        maybe+          InWireSchemasUnwitnessed+          InWireSchemasEqual+          (alignInWireFields inputFields wireFields)+      PathsDiverge -> InWireSchemasDifferent+      PathsPrefixRelated -> InWireSchemasUnwitnessed++-- | Regression observers pinning every 'compareInCtorWireSchemas' arm that+-- involves a composition-only spine. Composition-only evidence has no public+-- producer, so the scenarios are constructed here, where the constructors are+-- in scope, and specs assert the full labelled list. Construction-free: the+-- observer returns only proof-safe relations.+inputWireSpineRelationsForTesting :: [(String, InputWireHeadRelation)]+inputWireSpineRelationsForTesting =+  [ ("root/root", classifyInputWireSchemas rootInput rootWire),+    ( "left/left",+      classifyInputWireSchemas+        (prefixInCtorSchemaLeft rootInput :: InCtorSchema (Either Int Bool) '[ '("payload", Int)])+        (prefixWireSchemaLeft rootWire)+    ),+    ( "right/right",+      classifyInputWireSchemas+        (prefixInCtorSchemaRight rootInput :: InCtorSchema (Either Bool Int) '[ '("payload", Int)])+        (prefixWireSchemaRight rootWire)+    ),+    ( "left/right",+      classifyInputWireSchemas+        (prefixInCtorSchemaLeft rootInput :: InCtorSchema (Either Int Int) '[ '("payload", Int)])+        (prefixWireSchemaRight rootWire)+    ),+    ( "root/left-prefixed",+      classifyInputWireSchemas+        (compositionOnlyInCtorSchema :: InCtorSchema (Either Int Bool) '[ '("payload", Either Int Bool)])+        (prefixWireSchemaLeft rootWire)+    ),+    ("composition-only/trusted", classifyInputWireSchemas rootInput trustedRootWire),+    ("trusted/composition-only", classifyInputWireSchemas trustedRootInput rootWire),+    ("unavailable/composition-only", classifyInputWireSchemas inCtorSchemaUnavailable rootWire)+  ]+  where+    rootInput = compositionOnlyInCtorSchema :: InCtorSchema Int '[ '("payload", Int)]+    rootWire = compositionOnlyWireSchema :: WireSchema Int (Int, ())+    trustedRootWire = trustedWireSchema wireCtorPathRoot wireFieldsNil :: WireSchema Int ()+    trustedRootInput = trustedInCtorSchema wireCtorPathRoot inCtorFieldsNil :: InCtorSchema Int '[]++-- | Project 'compareInCtorWireSchemas' to its proof-safe relation, dropping+-- the typed alignment witness. Exists so specs can pin each comparison arm+-- directly without access to internal witnesses.+classifyInputWireSchemas ::+  InCtorSchema carrier inputFields ->+  WireSchema carrier wireFields ->+  InputWireHeadRelation+classifyInputWireSchemas inputSchema wireSchema =+  case compareInCtorWireSchemas inputSchema wireSchema of+    InWireSchemasEqual _ -> InputWireHeadsAligned+    InWireSchemasDifferent -> InputWireHeadsStructurallyDifferent+    InWireSchemasUnwitnessed -> InputWireHeadsUnwitnessed++compareCompositionOnlySpines ::+  CompositionOnlySpine carrier inputField ->+  CompositionOnlySpine carrier wireField ->+  InWireSchemaComparison '[ '("payload", inputField)] (wireField, ())+compareCompositionOnlySpines CompositionOnlyRoot CompositionOnlyRoot =+  InWireSchemasEqual (InWireFieldsAlignedCons InWireFieldsAlignedNil)+compareCompositionOnlySpines CompositionOnlyRoot CompositionOnlyLeft {} =+  InWireSchemasUnwitnessed+compareCompositionOnlySpines CompositionOnlyRoot CompositionOnlyRight {} =+  InWireSchemasUnwitnessed+compareCompositionOnlySpines CompositionOnlyLeft {} CompositionOnlyRoot =+  InWireSchemasUnwitnessed+compareCompositionOnlySpines CompositionOnlyRight {} CompositionOnlyRoot =+  InWireSchemasUnwitnessed+compareCompositionOnlySpines+  (CompositionOnlyLeft inputRest)+  (CompositionOnlyLeft wireRest) =+    compareCompositionOnlySpines inputRest wireRest+compareCompositionOnlySpines CompositionOnlyLeft {} CompositionOnlyRight {} =+  InWireSchemasDifferent+compareCompositionOnlySpines CompositionOnlyRight {} CompositionOnlyLeft {} =+  InWireSchemasDifferent+compareCompositionOnlySpines+  (CompositionOnlyRight inputRest)+  (CompositionOnlyRight wireRest) =+    compareCompositionOnlySpines inputRest wireRest++-- | Hidden symbolic identity: trusted paths become prefix constraints;+-- unavailable evidence remains on the conservative fallback path.+inCtorSchemaPath :: InCtorSchema ci fields -> Maybe [Bool]+inCtorSchemaPath UnavailableInCtorSchema = Nothing+inCtorSchemaPath CompositionOnlyInCtorSchema {} = Nothing+inCtorSchemaPath (TrustedInCtorSchema (WireCtorPath path) _) =+  Just (map stepIsLeft path)+  where+    stepIsLeft WireCtorPathLeft = True+    stepIsLeft WireCtorPathRight = False++-- | Regression observer for the otherwise-unforgeable proper-prefix case.+-- Exported through the testing internals of "Keiki.Core"; it grants no+-- ability to construct trusted evidence.+wireSchemaPrefixRelationForTesting :: WireHeadRelation+wireSchemaPrefixRelationForTesting =+  let root =+        TrustedWireSchema wireCtorPathRoot WireFieldsNil :: WireSchema () ()+      prefixed =+        TrustedWireSchema+          (genericPrefixWireCtorPathLeft wireCtorPathRoot)+          WireFieldsNil ::+          WireSchema () ()+   in case compareWireSchemas root prefixed of+        WireSchemasEqual _ -> WireHeadsStructurallyEqual+        WireSchemasDifferent -> WireHeadsStructurallyDifferent+        WireSchemasUnwitnessed -> WireHeadsUnwitnessed++-- | Regression observer for the input-side proper-prefix rule.+inCtorSchemaPrefixRelationForTesting :: InputHeadRelation+inCtorSchemaPrefixRelationForTesting =+  let root =+        TrustedInCtorSchema wireCtorPathRoot InCtorFieldsNil ::+          InCtorSchema () '[]+      prefixed =+        TrustedInCtorSchema+          (genericPrefixWireCtorPathLeft wireCtorPathRoot)+          InCtorFieldsNil ::+          InCtorSchema () '[]+   in case compareInCtorSchemas root prefixed of+        InCtorSchemasEqual _ -> InputHeadsStructurallyEqual+        InCtorSchemasDifferent -> InputHeadsStructurallyDifferent+        InCtorSchemasUnwitnessed -> InputHeadsUnwitnessed++data PathComparison+  = PathsEqual+  | PathsDiverge+  | PathsPrefixRelated++comparePaths :: [WireCtorPathStep] -> [WireCtorPathStep] -> PathComparison+comparePaths [] [] = PathsEqual+comparePaths [] (_ : _) = PathsPrefixRelated+comparePaths (_ : _) [] = PathsPrefixRelated+comparePaths (left : leftRest) (right : rightRest)+  | left /= right = PathsDiverge+  | otherwise = comparePaths leftRest rightRest++alignWireFields ::+  WireFieldSchema left ->+  WireFieldSchema right ->+  Maybe (WireFieldAlignment left right)+alignWireFields WireFieldsNil WireFieldsNil = Just WireFieldsAlignedNil+alignWireFields WireFieldsNil WireFieldsCons {} = Nothing+alignWireFields WireFieldsCons {} WireFieldsNil = Nothing+alignWireFields+  (WireFieldsCons @fieldLeft _ leftRest)+  (WireFieldsCons @fieldRight _ rightRest) =+    case eqTypeRep (typeRep @fieldLeft) (typeRep @fieldRight) of+      Just HRefl -> WireFieldsAlignedCons <$> alignWireFields leftRest rightRest+      Nothing -> Nothing++alignInCtorFields ::+  InCtorFieldSchema left ->+  InCtorFieldSchema right ->+  Maybe (InCtorFieldAlignment left right)+alignInCtorFields InCtorFieldsNil InCtorFieldsNil = Just InCtorFieldsAlignedNil+alignInCtorFields InCtorFieldsNil InCtorFieldsCons {} = Nothing+alignInCtorFields InCtorFieldsCons {} InCtorFieldsNil = Nothing+alignInCtorFields+  (InCtorFieldsCons @fieldLeft _ leftRest)+  (InCtorFieldsCons @fieldRight _ rightRest) =+    case eqTypeRep (typeRep @fieldLeft) (typeRep @fieldRight) of+      Just HRefl -> InCtorFieldsAlignedCons <$> alignInCtorFields leftRest rightRest+      Nothing -> Nothing++alignInWireFields ::+  InCtorFieldSchema inputFields ->+  WireFieldSchema wireFields ->+  Maybe (InWireFieldAlignment inputFields wireFields)+alignInWireFields InCtorFieldsNil WireFieldsNil = Just InWireFieldsAlignedNil+alignInWireFields InCtorFieldsNil WireFieldsCons {} = Nothing+alignInWireFields InCtorFieldsCons {} WireFieldsNil = Nothing+alignInWireFields+  (InCtorFieldsCons @inputField _ inputRest)+  (WireFieldsCons @wireField _ wireRest) =+    case eqTypeRep (typeRep @inputField) (typeRep @wireField) of+      Just HRefl -> InWireFieldsAlignedCons <$> alignInWireFields inputRest wireRest+      Nothing -> Nothing

@@ -118,6 +118,11 @@     withKnownSlots,   ) import Keiki.Core+import Keiki.Internal.ConstructorEvidence (constructorEvidence)+import Keiki.Internal.WireSchema+  ( compositionOnlyInCtorSchema,+    compositionOnlyWireSchema,+  ) import Unsafe.Coerce (unsafeCoerce)  -- | Existential wrapper hiding @rs@ (register-file slot list) and@@ -147,11 +152,11 @@ --     @ci ~ co@ comes from the constructor's GADT signature. -- -- The sentinel exists because 'Keiki.Composition.compose' substitutes--- t2's 'TInpCtorField'-on-@ic2@ against t1's 'WireCtor'-named--- emission, requiring @icName ic2 == wcName wc1@ for the substitution--- to be sound. A *generic* identity transducer (one whose 'InCtor' is--- the same regardless of @ci@) cannot satisfy this for arbitrary--- upstream wire names. The sentinel sidesteps this by short-circuiting+-- t2's 'TInpCtorField' reads only when their typed input schema is proven+-- equal to t1's emitted wire schema. A *generic* identity transducer (one+-- whose 'InCtor' is the same regardless of @ci@) cannot carry evidence+-- equal to every possible upstream or downstream constructor schema.+-- The sentinel sidesteps this by short-circuiting -- @id . t@ and @t . id@ in 'Cat..' rather than running them through -- 'compose'. See 'identityTransducer' for the concrete-identity -- transducer that some non-Category code paths still want.@@ -351,11 +356,12 @@ -- register is allocated. identityInCtor :: forall a. InCtor a '[ '("payload", a)] identityInCtor =-  InCtor-    { icName = "Identity",-      icMatch = \a -> Just (RCons (Proxy @"payload") a RNil),-      icBuild = \(RCons _ a RNil) -> a-    }+  trustedInCtorInternal+    constructorEvidence+    "Identity"+    compositionOnlyInCtorSchema+    (\a -> Just (RCons (Proxy @"payload") a RNil))+    (\(RCons _ a RNil) -> a)  -- | A 'WireCtor' for an arbitrary alphabet @a@. Uses the field-tuple -- @(a, ())@ that 'OutFields' produces for a single-element list: one@@ -364,11 +370,12 @@ -- payload; inversion via 'wcMatch' wraps an @a@ back up. identityWireCtor :: forall a. WireCtor a (a, ()) identityWireCtor =-  WireCtor-    { wcName = "Identity",-      wcMatch = \a -> Just (a, ()),-      wcBuild = \(a, ()) -> a-    }+  trustedWireCtorInternal+    constructorEvidence+    "Identity"+    compositionOnlyWireSchema+    (\a -> Just (a, ()))+    (\(a, ()) -> a)  -- | The identity transducer for an arbitrary alphabet @a@. One vertex -- ('IdVertex'); one edge whose guard is @'PInCtor' 'identityInCtor'@@@ -502,12 +509,12 @@ -- -- /Why a sentinel rather than a real identity transducer:/ -- 'Keiki.Composition.compose' substitutes t2's @TInpCtorField ic2@--- against t1's emitted 'WireCtor' @wc1@ and demands--- @icName ic2 == wcName wc1@; otherwise it raises a "structural--- mismatch" runtime error. A *generic* identity transducer (one--- 'InCtor' that serves every alphabet) cannot satisfy this for--- arbitrary upstream wire names, so feeding it through 'compose'--- would always fail. The sentinel sidesteps this by short-circuiting.+-- against t1's emitted 'WireCtor' @wc1@ only when their typed schemas+-- carry a definite equality witness. A *generic* identity transducer+-- (one 'InCtor' that serves every alphabet) cannot carry evidence equal+-- to every possible constructor schema, so feeding it through 'compose'+-- would fail closed at many otherwise lawful identity boundaries. The+-- sentinel sidesteps this by short-circuiting. -- -- See @test/Keiki/CategorySpec.hs@ for the law tests (behavioural -- equality on @id . t@, @t . id@, and associativity, plus the@@ -718,11 +725,10 @@      firstWireCtor :: forall fs. WireCtor co fs -> WireCtor (co, c) (c, fs)     firstWireCtor WireCtor {wcName = n, wcBuild = b} =-      WireCtor-        { wcName = n <> "_first",-          wcMatch = \_ -> Nothing,-          wcBuild = \(cv, fs) -> (b fs, cv)-        }+      unavailableWireCtor+        (n <> "_first")+        (\_ -> Nothing)+        (\(cv, fs) -> (b fs, cv))      -- \| Combine an @(ci)@ input constructor with the threaded @c@ into a     -- @(ci, c)@ constructor whose field schema is @"snd"@ (for @c@)@@ -730,13 +736,13 @@     firstInCtor ::       forall ifs. InCtor ci ifs -> InCtor (ci, c) ('("snd", c) ': ifs)     firstInCtor ic@InCtor {} =-      InCtor-        { icName = icName ic,-          icMatch = \(civ, cv) -> case icMatch ic civ of+      unavailableInCtor+        (icName ic)+        ( \(civ, cv) -> case icMatch ic civ of             Just rf -> Just (RCons (Proxy @"snd") cv rf)-            Nothing -> Nothing,-          icBuild = \(RCons _ cv rf) -> (icBuild ic rf, cv)-        }+            Nothing -> Nothing+        )+        (\(RCons _ cv rf) -> (icBuild ic rf, cv))      firstOutFields ::       forall ifs fs.@@ -830,13 +836,14 @@ -- unaffected. -- -- /Composition limitation (see "Law status" above):/ 'Keiki.Composition.compose' substitutes--- t2's 'TInpCtorField' against t1's 'WireCtor'-emitted output and--- demands 'icName ic2 == wcName wc1'. An 'arrTransducer'-produced--- transducer's 'WireCtor' is named @"arr"@ but the next stage's--- 'TInpCtorField' uses 'identityInCtor' (named @"Identity"@), so+-- t2's 'TInpCtorField' against t1's 'WireCtor'-emitted output only with+-- definite typed input-to-wire schema alignment. An+-- 'arrTransducer'-produced wire has unavailable evidence because an+-- arbitrary Haskell function supplies no structural inverse, so -- 'arr f >>> arr g' will not produce 'arr (g . f)' through 'Cat..' -- — substitution turns the composed guard into 'PBot' and the--- composite never fires. This is documented rather than worked+-- composite never fires. Diagnostic names play no role. This is+-- documented rather than worked -- around because the symbolic 'Term' AST has no -- 'TPure'-style constructor for arbitrary function application -- (intentional; see 'Keiki.Symbolic.translateTermSym' for why@@ -872,11 +879,10 @@      arrWc :: WireCtor b (a, ())     arrWc =-      WireCtor-        { wcName = "arr",-          wcMatch = \_ -> Nothing,-          wcBuild = \(a, ()) -> f a-        }+      unavailableWireCtor+        "arr"+        (\_ -> Nothing)+        (\(a, ()) -> f a)  -- | Standard 'Control.Arrow.Arrow' instance. --@@ -889,10 +895,10 @@ -- -- The default @'***'@ and @'&&&'@ methods of 'Arr.Arrow' use -- 'Arr.arr', 'Arr.first', and 'Arr.>>>' under the hood; they--- typecheck and produce composite transducers. The same--- @icName == wcName@ alignment limitation that affects--- 'arr f >>> arr g' applies — see 'arrTransducer' for the full--- caveat.+-- typecheck and produce composite transducers. The same unavailable+-- typed-schema evidence that prevents @arr f >>> arr g@ from crossing+-- a checked composition boundary applies — see 'arrTransducer' for+-- the full caveat. instance Arr.Arrow SomeSymTransducer where   arr f =     SomeSymTransducerWith@@ -913,22 +919,20 @@ -- 'Keiki.Core.solveOutput' on edges built from this 'InCtor'. contraInCtor :: (ci' -> ci) -> InCtor ci ifs -> InCtor ci' ifs contraInCtor f InCtor {icName = n, icMatch = m} =-  InCtor-    { icName = n <> "#lmapped",-      icMatch = m . f,-      icBuild = poisonedIcBuild n-    }+  unavailableInCtor+    (n <> "#lmapped")+    (m . f)+    (poisonedIcBuild n)  -- | Partial-contramap an 'InCtor'. The 'icMatch' becomes -- @\ci' -> f ci' >>= m@; 'icBuild' is poisoned (same caveat as -- 'contraInCtor'). contraMaybeInCtor :: (ci' -> Maybe ci) -> InCtor ci ifs -> InCtor ci' ifs contraMaybeInCtor f InCtor {icName = n, icMatch = m} =-  InCtor-    { icName = n <> "#lmapped",-      icMatch = \ci' -> f ci' >>= m,-      icBuild = poisonedIcBuild n-    }+  unavailableInCtor+    (n <> "#lmapped")+    (\ci' -> f ci' >>= m)+    (poisonedIcBuild n)  poisonedIcBuild :: String -> a -> b poisonedIcBuild icN = \_ ->@@ -944,11 +948,10 @@ -- 'WireCtor's 'wcMatch' is set to @const Nothing@. mapWireCtor :: (co -> co') -> WireCtor co fs -> WireCtor co' fs mapWireCtor g WireCtor {wcName = n, wcBuild = b} =-  WireCtor-    { wcName = n <> "#rmapped",-      wcMatch = \_co' -> Nothing,-      wcBuild = g . b-    }+  unavailableWireCtor+    (n <> "#rmapped")+    (\_co' -> Nothing)+    (g . b)  -- ** Term --------------------------------------------------------------- @@ -1021,14 +1024,14 @@   Bool ->   InCtor ci' '[] mappedArmInCtor f wantLeft =-  InCtor-    { icName = if wantLeft then "keiki#leftArm#lmapped" else "keiki#rightArm#lmapped",-      icMatch = \ci' -> case f ci' of+  unavailableInCtor+    (if wantLeft then "keiki#leftArm#lmapped" else "keiki#rightArm#lmapped")+    ( \ci' -> case f ci' of         Just (Left _) | wantLeft -> Just RNil         Just (Right _) | not wantLeft -> Just RNil-        _ -> Nothing,-      icBuild = poisonedIcBuild (if wantLeft then "keiki#leftArm#lmapped" else "keiki#rightArm#lmapped")-    }+        _ -> Nothing+    )+    (poisonedIcBuild (if wantLeft then "keiki#leftArm#lmapped" else "keiki#rightArm#lmapped"))  -- ** Update ------------------------------------------------------------- 

@@ -22,1800 +22,2728 @@ --     'Word16' \/ 'Word32' \/ 'Word64' \/ 'Int32' \/ 'Int64' (the --     last group added by EP-41 so money and count registers are --     solver-visible).---   * 'SymEnv' carrying the shared symbolic input-constructor tag and---     (since EP-42 of MasterPlan 12) an 'IORef' memo cache that shares---     one SBV variable per register slot, input field, or nominal typed field---     projection across repeated reads, so @proj #x .== proj #x@ and repeated---     projected reads are valid, not merely satisfiable.---   * 'translateTermSym' / 'translatePred' walking 'Term' / 'HsPred'---     into SBV expressions.---   * 'discoverSym' — runtime dispatch from 'Typeable' to 'Sym'---     evidence over the curated registry of supported types.---   * 'SymPred' newtype wrapper plus its 'BoolAlg' instance with---     structural 'top' / 'bot' / 'conj' / 'disj' / 'neg', a 'models'---     that re-uses the v1 'evalPred' (concrete evaluation, no solver---     call), and an 'isBot' backed by z3.---   * 'symIsBot' — conservative pure-API wrapper around SBV's solver call---     (via 'unsafePerformIO' + NOINLINE) that 'SymPred''s 'isBot' routes---     through. Solver failures and non-UNSAT statuses return 'False'.---   * 'symSatExt' — full witness extraction. Since EP-44 (MasterPlan 12)---     the 'Keiki.Core.Sat' method 'sat' on 'SymPred' /is/---     'symSatExt' (via the @Sat (SymPred …)@ instance, which carries the---     'ExtractRegFile' / 'KnownInCtors' evidence witness reconstruction---     needs); the old crashing placeholder is gone.-module Keiki.Symbolic-  ( -- * Symbolic representation-    Sym (..),-    SymDict (..),-    symLit,-    symFree,-    discoverSym,-    SymOrdDict (..),-    discoverSymOrd,-    SymNumDict (..),-    discoverSymNum,-    symbolicWholeCarrierExact,--    -- * Translation-    SymEnv (..),-    mkSymEnv,-    translateTermSym,-    translatePred,-    constrainFieldProjection,-    ProjectionBaseKind (..),-    ProjectionBaseDescriptor (..),-    ProjectionDescriptor (..),-    TranslationStrength (..),-    TranslationIssue (..),-    PredicateVerification (..),-    ProjectionModel (..),-    projectionModelKeyAs,-    projectionModelOwnerAs,-    PredicateVerificationDetail (..),-    predicateTranslationReport,-    predicateTranslationExact,-    verifyPredicateDetailed,-    verifyPredicate,--    -- * Symbolic predicate wrapper-    SymPred (..),-    SymGuarded,--    -- * Solver-backed analyses-    satResultIsProvablyUnsat,-    symIsBot,-    symSatExt,--    -- * Witness extraction-    ExtractRegFile (..),-    SomeInCtor (..),-    KnownInCtors (..),--    -- * Single-valuedness-    isSingleValuedSym,-    withSymPred,--    -- * Solver-backed validation diagnostics (EP-56)-    DeterminismAnalysisDetail (..),-    checkTransitionDeterminismSymDetailed,-    checkTransitionDeterminismSym,-    DeadEdgeAnalysisDetail (..),-    checkDeadEdgesSymDetailed,-    checkDeadEdgesSym,--    -- * Re-exports-    module Keiki.Core,-    module Keiki.ProjectionDomain,-  )-where--import Control.Exception (ErrorCall, SomeException, displayException, evaluate, try)-import Control.Monad (forM, when)-import Control.Monad.IO.Class (liftIO)-import Data.Dynamic (Dynamic, fromDynamic, toDyn)-import Data.Fixed (Fixed (MkFixed))-import Data.Foldable (toList)-import Data.IORef (IORef, modifyIORef', newIORef, readIORef, writeIORef)-import Data.Int (Int32, Int64)-import Data.Kind (Type)-import Data.List.NonEmpty (NonEmpty (..))-import Data.Map.Strict (Map)-import Data.Map.Strict qualified as Map-import Data.Maybe (listToMaybe)-import Data.Proxy (Proxy (..))-import Data.SBV qualified as SBV-import Data.SBV.RegExp qualified as SBV.RegExp-import Data.Set (Set)-import Data.Set qualified as Set-import Data.Text (Text)-import Data.Text qualified as T-import Data.Time (UTCTime, nominalDiffTimeToSeconds, secondsToNominalDiffTime)-import Data.Time.Clock.POSIX (posixSecondsToUTCTime, utcTimeToPOSIXSeconds)-import Data.Typeable (Typeable)-import Data.Word (Word16, Word32, Word64, Word8)-import GHC.TypeLits (KnownSymbol, symbolVal)-import Keiki.Core-import Keiki.Internal.ProjectionDomain-  ( ProjectionDomain (..),-    TextPattern (..),-  )-import Keiki.Internal.SymbolicTypes-  ( SymbolicType (..),-    discoverSymbolicType,-    symbolicTypeWholeCarrierExact,-  )-import Keiki.ProjectionDomain-import Numeric.Natural (Natural)-import System.IO.Unsafe (unsafePerformIO)-import Type.Reflection (SomeTypeRep (..), eqTypeRep, typeRep, type (:~~:) (HRefl))---- * Symbolic representation ----------------------------------------------------- | A type that has a curated representation in the SBV symbolic--- universe. The associated type 'SymRep' pins the SBV-friendly--- representation; the 'toSym' / 'fromSym' round-trip lets us push--- concrete Haskell values into the solver and pull concrete witnesses--- out of a model.------ The 'SBV.SymVal' superclass on 'SymRep' gives us 'SBV.literal',--- 'SBV.free', and 'SBV.unliteral' for free.------ 'symDefault' is consumed by 'symSatExt': when the solver's model--- has no value for a slot or input field that the predicate did not--- reference, the witness extractor falls back to 'symDefault'. Sound--- because such slots are unconstrained — any value satisfies the--- predicate.-class (SBV.SymVal (SymRep a), Typeable a) => Sym a where-  type SymRep a :: Type-  toSym :: a -> SymRep a-  fromSym :: SymRep a -> a-  symDefault :: a--  -- | Restrict a symbolic representation to values that denote a real @a@.-  -- Most carriers use their whole SBV domain. Refined carriers such as-  -- 'Natural' add constraints whenever Keiki allocates a symbolic variable.-  constrainSymDomain :: SBV.SBV (SymRep a) -> SBV.Symbolic ()-  constrainSymDomain _ = pure ()--instance Sym Bool where-  type SymRep Bool = Bool-  toSym = id-  fromSym = id-  symDefault = False--instance Sym Integer where-  type SymRep Integer = Integer-  toSym = id-  fromSym = id-  symDefault = 0---- | Arbitrary-precision non-negative integers. The representation stays an--- unbounded SMT integer, while every allocated variable is constrained to the--- actual 'Natural' domain. Numeric arithmetic is deliberately not registered:--- Haskell 'Natural' subtraction throws @Underflow@ when its mathematical result--- would be negative, while ordinary SMT integer subtraction returns that negative--- integer. Treating the operations as identical would not preserve concrete behavior.-instance Sym Natural where-  type SymRep Natural = Integer-  toSym = fromIntegral-  fromSym = fromInteger-  symDefault = 0-  constrainSymDomain value = SBV.constrain (value SBV..>= 0)---- | Encoded as 'Integer'. SBV does not provide an 'SInt'-of-arbitrary---- size; using 'Integer' means machine-width 'Int' wraparound is not modeled.--- Guards whose truth depends on 'Int' overflow should use an explicit--- fixed-width type instead.-instance Sym Int where-  type SymRep Int = Integer-  toSym = fromIntegral-  fromSym = fromIntegral-  symDefault = 0---- The fixed-width instances use SBV's matching bit-vector representations, so--- their arithmetic has exactly the same modular wraparound as Haskell.---- | Money and large counts, modeled as an exact 64-bit unsigned value.-instance Sym Word64 where-  type SymRep Word64 = Word64-  toSym = id-  fromSym = id-  symDefault = 0---- | Item counts and similar 32-bit unsigned registers, modeled exactly.-instance Sym Word32 where-  type SymRep Word32 = Word32-  toSym = id-  fromSym = id-  symDefault = 0---- | Quantities, basis points, and similar 16-bit unsigned registers, modeled--- exactly.-instance Sym Word16 where-  type SymRep Word16 = Word16-  toSym = id-  fromSym = id-  symDefault = 0---- | An exact 8-bit unsigned value.-instance Sym Word8 where-  type SymRep Word8 = Word8-  toSym = id-  fromSym = id-  symDefault = 0---- | An exact 64-bit signed value.-instance Sym Int64 where-  type SymRep Int64 = Int64-  toSym = id-  fromSym = id-  symDefault = 0---- | An exact 32-bit signed value.-instance Sym Int32 where-  type SymRep Int32 = Int32-  toSym = id-  fromSym = id-  symDefault = 0---- | 'Text' is encoded as Haskell 'String' for SBV's 'SString' theory.-instance Sym Text where-  type SymRep Text = String-  toSym = T.unpack-  fromSym = T.pack-  symDefault = T.empty---- | 'UTCTime' is encoded as picoseconds since the Unix epoch. The time--- library's 'NominalDiffTime' uses a fixed-point picosecond representation, so--- this 'Integer' encoding is lossless while remaining well supported by z3.-instance Sym UTCTime where-  type SymRep UTCTime = Integer-  toSym t =-    let MkFixed picoseconds =-          nominalDiffTimeToSeconds (utcTimeToPOSIXSeconds t)-     in picoseconds-  fromSym picoseconds =-    posixSecondsToUTCTime-      (secondsToNominalDiffTime (MkFixed picoseconds))-  symDefault = posixSecondsToUTCTime 0---- | Reify a 'Sym' instance so it can be passed around as a--- first-class value. Useful for runtime dispatch on 'Typeable'--- evidence.-data SymDict r where-  SymDict :: (Sym r) => SymDict r---- | Try to discover a 'Sym' instance for @r@ at runtime. Returns--- @Just SymDict@ for any of the curated supported types--- ('Bool', 'Int', 'Integer', 'Natural', 'Text', 'UTCTime', and the fixed-width--- integers 'Word8' \/ 'Word16' \/ 'Word32' \/ 'Word64' \/ 'Int32' \/--- 'Int64'); 'Nothing' otherwise. The translator uses this to route--- 'PEq' over arbitrary types: a 'Sym' hit translates to '(.==)' on--- SBV terms; a miss falls back to a fresh 'SBool' (loses precision but--- stays sound).-discoverSym :: forall r. (Typeable r) => Maybe (SymDict r)-discoverSym = case discoverSymbolicType @r of-  Just SymbolicBool -> Just SymDict-  Just SymbolicInt -> Just SymDict-  Just SymbolicInteger -> Just SymDict-  Just SymbolicNatural -> Just SymDict-  Just SymbolicText -> Just SymDict-  Just SymbolicUTCTime -> Just SymDict-  Just SymbolicWord64 -> Just SymDict-  Just SymbolicWord32 -> Just SymDict-  Just SymbolicWord16 -> Just SymDict-  Just SymbolicWord8 -> Just SymDict-  Just SymbolicInt64 -> Just SymDict-  Just SymbolicInt32 -> Just SymDict-  Nothing -> Nothing---- | Reify both a 'Sym' instance for @r@ and evidence that its--- 'SymRep' is symbolically orderable (an 'SBV.OrdSymbolic' instance on--- @'SBV.SBV' ('SymRep' r)@). This is exactly what 'PCmp' translation--- needs: 'Sym' to push the operands into SBV, 'OrdSymbolic' to emit a--- real @.<@ \/ @.<=@ \/ @.>@ \/ @.>=@ comparison.-data SymOrdDict r where-  SymOrdDict :: (Sym r, SBV.OrdSymbolic (SBV.SBV (SymRep r))) => SymOrdDict r---- | Try to discover ordering evidence for @r@ at runtime, companion to--- 'discoverSym'. Returns @Just SymOrdDict@ for the numeric and time--- types whose 'SymRep' is an 'SBV.OrdSymbolic' 'Integer' ('Int',--- 'Integer', 'Natural', the fixed-width integers 'Word8' \/ 'Word16' \/ 'Word32'--- \/ 'Word64' \/ 'Int32' \/ 'Int64', and 'UTCTime' encoded as epoch--- seconds); 'Nothing' otherwise. 'Bool' and 'Text' are deliberately--- omitted: ordering a 'Bool' guard is not meaningful, and 'SString'--- ordering is out of scope here. A 'Nothing' makes the 'PCmp'--- translator fall back to a fresh opaque 'SBool', exactly as 'goEq'--- does for non-'Sym' operands — sound, just imprecise.-discoverSymOrd :: forall r. (Typeable r) => Maybe (SymOrdDict r)-discoverSymOrd = case discoverSymbolicType @r of-  Just SymbolicInt -> Just SymOrdDict-  Just SymbolicInteger -> Just SymOrdDict-  Just SymbolicNatural -> Just SymOrdDict-  Just SymbolicUTCTime -> Just SymOrdDict-  Just SymbolicWord64 -> Just SymOrdDict-  Just SymbolicWord32 -> Just SymOrdDict-  Just SymbolicWord16 -> Just SymOrdDict-  Just SymbolicWord8 -> Just SymOrdDict-  Just SymbolicInt64 -> Just SymOrdDict-  Just SymbolicInt32 -> Just SymOrdDict-  Just SymbolicBool -> Nothing-  Just SymbolicText -> Nothing-  Nothing -> Nothing---- | Reify both a 'Sym' instance for @r@ and evidence that its 'SymRep'--- is symbolically /numeric/ (a 'Num' instance on @'SBV.SBV' ('SymRep'--- r)@). This is what 'TArith' translation needs: 'Sym' to push the--- operands into SBV, 'Num' to emit a real @+@ \/ @-@ \/ @*@ over the--- translated terms. Companion to 'discoverSym' \/ 'discoverSymOrd'--- (EP-43).-data SymNumDict r where-  SymNumDict :: (Sym r, Num (SBV.SBV (SymRep r))) => SymNumDict r---- | Try to discover numeric evidence for @r@ at runtime, companion to--- 'discoverSymOrd'. Returns @Just SymNumDict@ for the numeric types--- whose 'SymRep' is the SBV-'Num' 'Integer' ('Int', 'Integer', and the--- fixed-width integers 'Word8' \/ 'Word16' \/ 'Word32' \/ 'Word64' \/--- 'Int32' \/ 'Int64'), plus 'Natural'. Natural subtraction has the explicit--- total monus meaning shared with concrete 'evalTerm'; it is translated as--- @ite (a >= b) (a - b) 0@ rather than ordinary integer subtraction.--- 'Bool', 'Text', and 'UTCTime' are omitted. A 'Nothing'--- makes the 'TArith' translator fall back to a fresh opaque variable,--- exactly as 'goEq' \/ 'goCmp' fall back for non-'Sym' operands —--- sound, just imprecise. (The 'Num' constraint on the 'TArith'--- constructor already prevents arithmetic at non-numeric types, so this--- fallback is only reachable for a numeric type intentionally left out--- of the registry.)-discoverSymNum :: forall r. (Typeable r) => Maybe (SymNumDict r)-discoverSymNum = case discoverSymbolicType @r of-  Just SymbolicInt -> Just SymNumDict-  Just SymbolicInteger -> Just SymNumDict-  Just SymbolicNatural -> Just SymNumDict-  Just SymbolicWord64 -> Just SymNumDict-  Just SymbolicWord32 -> Just SymNumDict-  Just SymbolicWord16 -> Just SymNumDict-  Just SymbolicWord8 -> Just SymNumDict-  Just SymbolicInt64 -> Just SymNumDict-  Just SymbolicInt32 -> Just SymNumDict-  Just SymbolicBool -> Nothing-  Just SymbolicText -> Nothing-  Just SymbolicUTCTime -> Nothing-  Nothing -> Nothing---- | Whether the curated representation covers the complete concrete carrier--- bijectively. This is the gate for 'wholeProjectionDomain': supporting--- symbolic equality alone is not sufficient.-symbolicWholeCarrierExact :: forall (r :: Type). (Typeable r) => Bool-symbolicWholeCarrierExact =-  maybe False symbolicTypeWholeCarrierExact (discoverSymbolicType @r)---- | Lift a concrete value to an SBV literal of its 'SymRep'.-symLit :: forall a. (Sym a) => a -> SBV.SBV (SymRep a)-symLit = SBV.literal . toSym---- | Allocate a fresh symbolic variable of the carrier's 'SymRep'.-symFree :: forall a. (Sym a) => String -> SBV.Symbolic (SBV.SBV (SymRep a))-symFree label = do-  value <- SBV.free label-  constrainSymDomain @a value-  pure value---- * Translation environment ----------------------------------------------------- | Translation context: shared symbolic state that must be threaded--- through a single predicate's walk so that, for example, two--- 'PInCtor' atoms over distinct constructors agree they cannot both--- be true, and two reads of the same register (or input field) share--- one solver variable.------ Three pieces of state are shared:------   * 'seInputCtor' — the symbolic input-constructor tag, so 'PInCtor'---     atoms over distinct constructors are recognized as mutually---     unsatisfiable.---   * 'seInputArm' — an independent discriminator for 'PLeftArm' and---     'PRightArm'. It is separate from constructor names so both facts can---     be asserted by the same guard.---   * 'seVarCache' — a per-translation memo cache (EP-42) keyed by a---     structured 'SymVarKey'. Ordinary register and input reads preserve their---     historical labels; field projections use base position and nominal---     'TypeRep' identity, never caller-controlled diagnostic strings alone.---     The first read allocates one 'SBV.free' variable and stores it; every---     later read of the same key returns the cached variable.---     This makes the solver see two reads of @#x@ as the /same/ value,---     so @proj #x .== proj #x@ is valid (not merely satisfiable). The---     'TApp1' \/ 'TApp2' escape hatches are deliberately /not/ cached:---     they wrap opaque Haskell functions with no 'Eq', so two---     applications cannot be recognized as equal and each stays a fresh---     per-occurrence variable.-data ProjectionBaseKey-  = ProjectionReg String Int-  | ProjectionInp String String Int-  deriving stock (Eq, Ord, Show)---- | Which structural carrier owns a projection base.-data ProjectionBaseKind-  = ProjectionRegisterOwner-  | ProjectionInputOwner-  deriving stock (Eq, Ord, Show)---- | Stable structural identity for the concrete owner read beneath a field--- projection. Display names are diagnostic; kind, optional input constructor,--- and zero-based position keep identity structural.-data ProjectionBaseDescriptor = ProjectionBaseDescriptor-  { projectionBaseKind :: ProjectionBaseKind,-    projectionBaseConstructorName :: Maybe String,-    projectionBaseSlotName :: String,-    projectionBasePosition :: Int,-    projectionBaseOwnerType :: SomeTypeRep-  }-  deriving stock (Eq, Ord, Show)---- | Public, function-free metadata for one nominal projection occurrence.-data ProjectionDescriptor = ProjectionDescriptor-  { projectionDescriptorBase :: ProjectionBaseDescriptor,-    projectionDescriptorPath :: String,-    projectionDescriptorShape :: String,-    projectionDescriptorTagType :: SomeTypeRep,-    projectionDescriptorOwnerType :: SomeTypeRep,-    projectionDescriptorResultType :: SomeTypeRep-  }-  deriving stock (Eq, Ord, Show)---- | Whether every symbolic valuation of a predicate corresponds to its--- concrete semantics, or the translation is only a sound over-approximation.-data TranslationStrength-  = ExactTranslation-  | ConservativeOverApproximation (NonEmpty TranslationIssue)-  deriving stock (Eq, Show)---- | A deterministic explanation for lost translation exactness.-data TranslationIssue-  = OpaqueApplication-  | UnsupportedEquality SomeTypeRep-  | UnsupportedOrdering SomeTypeRep-  | UnsupportedArithmetic SomeTypeRep-  | UnconstrainedProjection ProjectionDescriptor-  | UnsupportedProjectionDomain ProjectionDescriptor String-  | ProjectionUsedOutsideEquality ProjectionDescriptor-  | ConflictingProjectionViews ProjectionBaseDescriptor-  | DirectAndProjectedOwnerRead ProjectionBaseDescriptor-  | UnguardedProjectionInputRead ProjectionDescriptor-  deriving stock (Eq, Show)--data SymVarKey-  = RegVar String-  | InpVar String String-  | ProjectionVar-      ProjectionBaseKey-      SomeTypeRep-      SomeTypeRep-      SomeTypeRep-  deriving stock (Eq, Ord, Show)--data SymEnv = SymEnv-  { -- | The shared symbolic input constructor tag. 'PInCtor' atoms-    --     assert @seInputCtor .== literal (icName ic)@; the solver-    --     recognizes that two such constraints with distinct names are-    --     mutually unsatisfiable.-    seInputCtor :: SBV.SBV String,-    -- | @True@ denotes the outer 'Left' arm; @False@ denotes 'Right'.-    seInputArm :: SBV.SBool,-    -- | Memo cache: maps a deterministic variable name ("reg/\<slot\>"-    --     or "inp/\<ctor\>/\<field\>") to the single SBV variable allocated-    --     for it during this predicate translation. Lazily populated on-    --     first read so unread slots stay unconstrained (and 'symSatExt'-    --     falls back to 'symDefault' for them). Scoped to one-    --     'translatePred' walk (one 'mkSymEnv'), so variables are shared-    --     /within/ a query but never leak across independent queries.-    seVarCache :: IORef (Map SymVarKey SomeSBV),-    -- | Stable model label for every memoized structural variable.-    seVarLabels :: IORef (Map SymVarKey String),-    -- | Projection keys in allocation/first-occurrence order.-    seProjectionKeyOrder :: IORef [SymVarKey],-    -- | Keys whose complete exact-domain constraint was emitted.-    seConstrainedProjectionKeys :: IORef (Set SymVarKey),-    -- | Exact evidence used to decode and reconstruct satisfiable models.-    seProjectionBindings :: IORef (Map SymVarKey SomeProjectionBinding),-    -- | Next internal projection label. Projection labels are intentionally-    --     generated by Keiki so arbitrary schema names never reach SBV's-    --     restricted label namespace.-    seProjectionOrdinal :: IORef Int-  }---- | An SBV variable of some representation type, packed so the memo--- cache in 'SymEnv' can hold variables of different representation--- types under one map. 'SBV.SymVal' has a 'Typeable' superclass, so--- pattern-matching @SomeSBV (v :: SBV.SBV a)@ brings @Typeable a@ into--- scope — exactly what 'memoFree' needs to check the recovered type--- matches the requested one on a cache hit.-data SomeSBV where-  SomeSBV :: (SBV.SymVal a) => SBV.SBV a -> SomeSBV--data SomeProjectionBinding where-  SomeProjectionBinding ::-    ( FieldProjection projection,-      Typeable projection,-      Typeable (FieldOwner projection),-      Typeable (FieldResult projection),-      Sym (FieldResult projection)-    ) =>-    ProjectionDescriptor ->-    String ->-    FieldWitness projection ->-    SomeProjectionBinding---- | Allocate a fresh 'SymEnv'. Lives in 'SBV.Symbolic' because--- 'seInputCtor' is a free symbolic variable and the memo cache is an--- 'IORef' created in the underlying 'IO' ('SBV.Symbolic' is--- @SymbolicT IO@, hence 'MonadIO').-mkSymEnv :: SBV.Symbolic SymEnv-mkSymEnv = do-  ctor <- SBV.free "inputCtor"-  arm <- SBV.free "inputArm"-  cache <- liftIO (newIORef Map.empty)-  labels <- liftIO (newIORef Map.empty)-  projectionOrder <- liftIO (newIORef [])-  constrainedProjectionKeys <- liftIO (newIORef Set.empty)-  projectionBindings <- liftIO (newIORef Map.empty)-  projectionOrdinal <- liftIO (newIORef 0)-  pure-    ( SymEnv-        ctor-        arm-        cache-        labels-        projectionOrder-        constrainedProjectionKeys-        projectionBindings-        projectionOrdinal-    )---- * Translation ----------------------------------------------------------------- | Translate a 'Term rs ci r' to an SBV expression of the carrier's--- representation type. Requires 'Sym' evidence for @r@.------ The translation is /structural/ for 'TLit', 'TOpaqueLit', 'TReg',--- 'TInpCtorField', and (since EP-43) 'TArith': a 'TArith' over a type--- whose 'SymRep' is SBV-numeric (a 'discoverSymNum' hit) emits a real--- @+@ \/ @-@ \/ @*@ over the translated operands, so a guard over a--- /computed/ value is visible to the solver. 'TApp1' and 'TApp2' wrap--- opaque Haskell functions and translate to fresh SBV variables of the--- result type — sound but imprecise; 'TArith' falls back to the same--- fresh variable only if its (numeric) operand type is absent from the--- 'discoverSymNum' registry.------ Variable naming (consumed by 'symSatExt' for witness extraction):------   * 'TReg' allocates @"reg/<slotName>"@ where @slotName@ is the---     slot's label recovered from the 'Index'\'s 'KnownSymbol'---     evidence on its leaf 'ZIdx'.---   * 'TInpCtorField' allocates---     @"inp/<icName>/<slotName>"@ — the 'InCtor''s name plus the---     field's slot label.---   * 'TFieldProj' uses a structured cache key containing the base position,---     nominal projection tag, owner type, and result type. Its actual SBV---     label is an internal @"proj/<ordinal>"@, so arbitrary schema strings---     cannot collide with or violate SBV's label syntax.---   * 'TApp1' / 'TApp2' keep their anonymous names; their values are---     not extracted as part of the witness.------ Note on repeated reads (EP-42): 'TReg', 'TInpCtorField', and--- 'TFieldProj' reads are memoized through the env's 'seVarCache'. This is--- /path-exact/: the first--- read of a given structural key allocates one 'SBV.free' variable and caches--- it; every later read of the same key returns the cached variable. So two--- reads of the same slot (e.g.--- @proj #x .== proj #x@) share /one/ SBV variable: the solver knows--- they are equal, @x \/= x@ is unsat, and 'symSatExt''s by-name witness--- extraction is correct for ordinary repeated reads. Exact projection--- variables carry a declared image and inverse, so detailed verification can--- decode model values and reconstruct path-local owner witnesses. Legacy--- one-way projections remain over-approximate and are not reconstructed. The--- 'TApp1' \/ 'TApp2'--- escape hatches stay per-occurrence fresh (their opaque functions--- have no 'Eq', so two applications cannot be recognized as equal);--- their values are not part of the extracted witness.-translateTermSym ::-  forall rs ci ifs r.-  (Sym r) =>-  SymEnv ->-  Term rs ci ifs r ->-  SBV.Symbolic (SBV.SBV (SymRep r))-translateTermSym _env (TLit r) = pure (symLit r)-translateTermSym _env (TOpaqueLit 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 (TOpaqueLit _) = []-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+--   * 'SymEnv' carrying shared structural input-constructor path decisions and+--     conservative fallback atoms, plus+--     (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,+    InversionCandidate (..),+    InversionProofVerdict (..),+    InversionSolverStatus (..),+    InversionTranslationIssue (..),+    InversionAnalysisDetail (..),+    checkInversionAmbiguitySymDetailed,+    checkInversionAmbiguitySym,++    -- * 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.Internal.WireSchema+  ( InCtorSchemaComparison (..),+    WireFieldAlignment (..),+    WireSchemaComparison (..),+    compareInCtorSchemas,+    compareWireSchemas,+    inCtorSchemaPath,+  )+import Keiki.ProjectionDomain+import Numeric.Natural (Natural)+import System.IO.Unsafe (unsafePerformIO)+import System.Timeout (timeout)+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 trusted+-- 'PInCtor' atoms with divergent structural paths cannot both be true, and two+-- reads of the same register (or input field) share one solver variable.+--+-- The principal pieces of state are:+--+--   * 'seInputPathCache' and 'seInputFallbackCache' — trusted constructors+--     constrain shared Generic path decisions; unwitnessed constructors use+--     name-keyed atoms whose unequal names remain independent.+--   * 'seInputCtor' — a separate ordinal selector used only for concrete model+--     reconstruction by 'symSatExt'.+--   * '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+  | UnwitnessedInputConstructorIdentity String+  deriving stock (Eq, Show)++data SymVarKey+  = RegVar String+  | InpVar String String+  | ProjectionVar+      ProjectionBaseKey+      SomeTypeRep+      SomeTypeRep+      SomeTypeRep+  deriving stock (Eq, Ord, Show)++data SymEnv = SymEnv+  { -- | Model-only selector used by 'symSatExt' to reconstruct one known+    --     constructor. Predicate identity is encoded independently from+    --     trusted structural paths or conservative fallback atoms.+    seInputCtor :: SBV.SBV String,+    -- | @True@ denotes the outer 'Left' arm; @False@ denotes 'Right'.+    seInputArm :: SBV.SBool,+    -- | One shared Boolean decision per Generic constructor-path position.+    --     @True@ is left and @False@ is right. Equal paths share the same+    --     constraint, divergent paths contradict, and proper prefixes overlap.+    seInputPathCache :: IORef (Map Int SBV.SBool),+    -- | Name-keyed fallback atoms for constructors without trusted evidence.+    --     Different names remain independent, so name inequality cannot prove+    --     mutual exclusion; equal names retain the legacy conflation.+    seInputFallbackCache :: IORef (Map String SBV.SBool),+    -- | Internal label source for fallback atoms. Diagnostic constructor names+    --     never become SBV identifiers.+    seInputFallbackOrdinal :: IORef Int,+    -- | Memo cache: maps a deterministic variable name ("reg/\<slot\>"+    --     or "inp/\<ctor\>/\<field\>") to the single SBV variable allocated+    --     for it during this predicate translation. Lazily populated on+    --     first read so unread slots stay unconstrained (and 'symSatExt'+    --     falls back to 'symDefault' for them). Scoped to one+    --     'translatePred' walk (one 'mkSymEnv'), so variables are shared+    --     /within/ a query but never leak across independent queries.+    seVarCache :: IORef (Map SymVarKey SomeSBV),+    -- | Stable model label for every memoized structural variable.+    seVarLabels :: IORef (Map SymVarKey String),+    -- | Projection keys in allocation/first-occurrence order.+    seProjectionKeyOrder :: IORef [SymVarKey],+    -- | Keys whose complete exact-domain constraint was emitted.+    seConstrainedProjectionKeys :: IORef (Set SymVarKey),+    -- | Exact evidence used to decode and reconstruct satisfiable models.+    seProjectionBindings :: IORef (Map SymVarKey SomeProjectionBinding),+    -- | Next internal projection label. Projection labels are intentionally+    --     generated by Keiki so arbitrary schema names never reach SBV's+    --     restricted label namespace.+    seProjectionOrdinal :: IORef Int+  }++-- | An SBV variable of some representation type, packed so the memo+-- cache in 'SymEnv' can hold variables of different representation+-- types under one map. 'SBV.SymVal' has a 'Typeable' superclass, so+-- pattern-matching @SomeSBV (v :: SBV.SBV a)@ brings @Typeable a@ into+-- scope — exactly what 'memoFree' needs to check the recovered type+-- matches the requested one on a cache hit.+data SomeSBV where+  SomeSBV :: (SBV.SymVal a) => SBV.SBV a -> SomeSBV++data SomeProjectionBinding where+  SomeProjectionBinding ::+    ( FieldProjection projection,+      Typeable projection,+      Typeable (FieldOwner projection),+      Typeable (FieldResult projection),+      Sym (FieldResult projection)+    ) =>+    ProjectionDescriptor ->+    String ->+    FieldWitness projection ->+    SomeProjectionBinding++-- | Allocate a fresh 'SymEnv'. Lives in 'SBV.Symbolic' because+-- 'seInputCtor' is a free symbolic variable and the memo cache is an+-- 'IORef' created in the underlying 'IO' ('SBV.Symbolic' is+-- @SymbolicT IO@, hence 'MonadIO').+mkSymEnv :: SBV.Symbolic SymEnv+mkSymEnv = do+  ctor <- SBV.free "inputCtor"+  arm <- SBV.free "inputArm"+  inputPaths <- liftIO (newIORef Map.empty)+  inputFallbacks <- liftIO (newIORef Map.empty)+  inputFallbackOrdinal <- liftIO (newIORef 0)+  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+        inputPaths+        inputFallbacks+        inputFallbackOrdinal+        cache+        labels+        projectionOrder+        constrainedProjectionKeys+        projectionBindings+        projectionOrdinal+    )++memoInputPathDecision :: SymEnv -> Int -> SBV.Symbolic SBV.SBool+memoInputPathDecision environment position = do+  decisions <- liftIO (readIORef (seInputPathCache environment))+  case Map.lookup position decisions of+    Just decision -> pure decision+    Nothing -> do+      decision <- SBV.free ("inputCtor/path/" <> show position)+      liftIO+        ( modifyIORef'+            (seInputPathCache environment)+            (Map.insert position decision)+        )+      pure decision++memoInputFallback :: SymEnv -> String -> SBV.Symbolic SBV.SBool+memoInputFallback environment diagnosticName = do+  fallbacks <- liftIO (readIORef (seInputFallbackCache environment))+  case Map.lookup diagnosticName fallbacks of+    Just fallback -> pure fallback+    Nothing -> do+      ordinal <- liftIO (readIORef (seInputFallbackOrdinal environment))+      liftIO (modifyIORef' (seInputFallbackOrdinal environment) (+ 1))+      fallback <- SBV.free ("inputCtor/fallback/" <> show ordinal)+      liftIO+        ( modifyIORef'+            (seInputFallbackCache environment)+            (Map.insert diagnosticName fallback)+        )+      pure fallback++-- | Encode one input constructor without consulting its diagnostic name when+-- trusted evidence exists. Proper-prefix paths deliberately overlap because+-- the shorter path contributes no contradictory decision at the extra depth.+inputCtorConstraint :: SymEnv -> InCtor ci fields -> SBV.Symbolic SBV.SBool+inputCtorConstraint environment inputCtor =+  case inCtorSchemaPath inputCtor.icSchema of+    Just path -> do+      constraints <- traverse constrainStep (zip [0 ..] path)+      pure (foldr (SBV..&&) SBV.sTrue constraints)+    Nothing -> memoInputFallback environment (icName inputCtor)+  where+    constrainStep (position, isLeft) = do+      decision <- memoInputPathDecision environment position+      pure (if isLeft then decision else SBV.sNot decision)++inputCtorsDefinitelySame :: InCtor ci leftFields -> InCtor ci rightFields -> Bool+inputCtorsDefinitelySame left right =+  case compareInCtorSchemas left.icSchema right.icSchema of+    InCtorSchemasEqual _ -> True+    InCtorSchemasDifferent -> False+    InCtorSchemasUnwitnessed ->+      case (inCtorSchemaPath left.icSchema, inCtorSchemaPath right.icSchema) of+        (Nothing, Nothing) -> icName left == icName right+        _ -> False++predicateStructurallyImpliesInCtor ::+  InCtor ci expectedFields ->+  HsPred rs ci ->+  Bool+predicateStructurallyImpliesInCtor expected = go+  where+    go PTop = False+    go PBot = True+    go (PAnd left right) = go left || go right+    go (POr left right) = go left && go right+    go (PNot _) = False+    go (PEq _ _) = False+    go (PInCtor actual) = inputCtorsDefinitelySame expected actual+    go PLeftArm = False+    go PRightArm = False+    go (PCmp _ _ _) = False++-- * 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', 'TOpaqueLit', 'TReg',+-- 'TInpCtorField', and (since EP-43) 'TArith': a 'TArith' over a type+-- whose 'SymRep' is SBV-numeric (a 'discoverSymNum' hit) emits a real+-- @+@ \/ @-@ \/ @*@ over the translated operands, so a guard over a+-- /computed/ value is visible to the solver. 'TApp1' and 'TApp2' wrap+-- opaque Haskell functions and translate to fresh SBV variables of the+-- result type — sound but imprecise; 'TArith' falls back to the same+-- fresh variable only if its (numeric) operand type is absent from the+-- 'discoverSymNum' registry.+--+-- Variable naming (consumed by 'symSatExt' for witness extraction):+--+--   * 'TReg' allocates @"reg/<slotName>"@ where @slotName@ is the+--     slot's label recovered from the 'Index'\'s 'KnownSymbol'+--     evidence on its leaf 'ZIdx'.+--   * 'TInpCtorField' allocates+--     @"inp/<icName>/<slotName>"@ — the 'InCtor''s name plus the+--     field's slot label.+--   * 'TFieldProj' uses a structured cache key containing the base position,+--     nominal projection tag, owner type, and result type. Its actual SBV+--     label is an internal @"proj/<ordinal>"@, so arbitrary schema strings+--     cannot collide with or violate SBV's label syntax.+--   * 'TApp1' / 'TApp2' keep their anonymous names; their values are+--     not extracted as part of the witness.+--+-- Note on repeated reads (EP-42): 'TReg', 'TInpCtorField', and+-- 'TFieldProj' reads are memoized through the env's 'seVarCache'. This is+-- /path-exact/: the first+-- read of a given structural key allocates one 'SBV.free' variable and caches+-- it; every later read of the same key returns the cached variable. So two+-- reads of the same slot (e.g.+-- @proj #x .== proj #x@) share /one/ SBV variable: the solver knows+-- they are equal, @x \/= x@ is unsat, and 'symSatExt''s by-name witness+-- extraction is correct for ordinary repeated reads. Exact projection+-- variables carry a declared image and inverse, so detailed verification can+-- decode model values and reconstruct path-local owner witnesses. Legacy+-- one-way projections remain over-approximate and are not reconstructed. The+-- 'TApp1' \/ 'TApp2'+-- escape hatches stay per-occurrence fresh (their opaque functions+-- have no 'Eq', so two applications cannot be recognized as equal);+-- their values are not part of the extracted witness.+translateTermSym ::+  forall rs ci ifs r.+  (Sym r) =>+  SymEnv ->+  Term rs ci ifs r ->+  SBV.Symbolic (SBV.SBV (SymRep r))+translateTermSym _env (TLit r) = pure (symLit r)+translateTermSym _env (TOpaqueLit 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 constraints over shared structural path decisions when+--     evidence is trusted. Unwitnessed constructors use name-keyed independent+--     fallback atoms, so unequal diagnostic names cannot prove exclusion.+--   * '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) = inputCtorConstraint env 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 inputCtor) =+      case inCtorSchemaPath inputCtor.icSchema of+        Just _ -> []+        Nothing ->+          [ TranslationIssueEvent+              (UnwitnessedInputConstructorIdentity (icName inputCtor))+          ]+    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 (TOpaqueLit _) = []+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 base of+        PBReg {} -> []+        PBInp inputCtor _+          | predicateStructurallyImpliesInCtor inputCtor root -> []+          | otherwise ->+              [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)++-- * Full symbolic replay-inversion analysis -------------------------------++-- | Which independently reconstructed replay candidate produced an issue.+data InversionCandidate+  = InversionCandidateA+  | InversionCandidateB+  deriving stock (Eq, Ord, Show)++-- | Conservative proof verdict for one legacy inversion-warning pair.+data InversionProofVerdict+  = InversionProvedDisjoint+  | InversionNotProvedDisjoint+  deriving stock (Eq, Show)++-- | Result of the optional solver query. Only+-- 'InversionSolverUnsatisfiable' is proof-bearing.+data InversionSolverStatus+  = InversionSolverNotRun+  | InversionSolverSatisfiable+  | InversionSolverUnsatisfiable+  | InversionSolverUnknown String+  | InversionSolverTimedOut+  | InversionSolverFailure String+  deriving stock (Eq, Show)++-- | A deterministic explanation for a relationship deliberately omitted+-- from the replay-pair formula. Every omission widens the formula.+data InversionTranslationIssue+  = InversionWireSchemasUnwitnessed+  | InversionUnsupportedObservedFieldCarrier Int SomeTypeRep+  | InversionOpaqueDerivedOutput InversionCandidate Int+  | InversionUnsupportedDerivedArithmetic InversionCandidate Int SomeTypeRep+  | InversionUnsupportedDerivedProjection+      InversionCandidate+      Int+      ProjectionDescriptor+      String+  | InversionInputConstructorIdentityUnwitnessed InversionCandidate String+  | InversionGuardTranslationIssue InversionCandidate TranslationIssue+  deriving stock (Eq, Show)++-- | One same-source, same-phase pair from 'inversionAmbiguityWarnings', with+-- its structural evidence and single opt-in solver result.+data InversionAnalysisDetail s = InversionAnalysisDetail+  { iadSource :: s,+    iadLeftEdge :: EdgeRef s,+    iadRightEdge :: EdgeRef s,+    iadLeftSchemaAvailability :: WireSchemaAvailability,+    iadRightSchemaAvailability :: WireSchemaAvailability,+    iadHeadRelation :: WireHeadRelation,+    iadVerdict :: InversionProofVerdict,+    iadSolverStatus :: InversionSolverStatus,+    iadTranslationIssues :: [InversionTranslationIssue]+  }+  deriving stock (Eq, Show)++-- Existentials retained from the two head 'OPack's of one warning pair.+data InversionCandidatePair rs ci co s where+  InversionCandidatePair ::+    s ->+    Int ->+    HsPred rs ci ->+    InCtor ci leftInputFields ->+    WireCtor co leftOutputFields ->+    OutFields rs ci leftInputFields leftOutputFields ->+    Int ->+    HsPred rs ci ->+    InCtor ci rightInputFields ->+    WireCtor co rightOutputFields ->+    OutFields rs ci rightInputFields rightOutputFields ->+    InversionCandidatePair rs ci co s++data InversionHead rs ci co where+  InversionHead ::+    InCtor ci inputFields ->+    WireCtor co outputFields ->+    OutFields rs ci inputFields outputFields ->+    InversionHead rs ci co++headInversionCandidate ::+  Edge (HsPred rs ci) rs ci co s ->+  Maybe (InversionHead rs ci co)+headInversionCandidate Edge {output = OPack inputCtor wireCtor fields : _} =+  Just (InversionHead inputCtor wireCtor fields)+headInversionCandidate _ = Nothing++-- Analyze exactly the pairs retained by the canonical pure warning pass. The+-- compatibility projection still matches by 'InversionPairKey' rather than+-- trusting these two traversals to remain positionally isomorphic.+inversionCandidatePairs ::+  (Bounded s, Enum s, Show s) =>+  SymTransducer (HsPred rs ci) rs s ci co ->+  [InversionCandidatePair rs ci co s]+inversionCandidatePairs transducer =+  [ InversionCandidatePair+      source+      leftIndex+      (guard leftEdge)+      leftInputCtor+      leftWireCtor+      leftFields+      rightIndex+      (guard rightEdge)+      rightInputCtor+      rightWireCtor+      rightFields+  | source <- [minBound .. maxBound],+    let indexedEdges = zip [(0 :: Int) ..] (edgesOut transducer source),+    (leftIndex, leftEdge) <- indexedEdges,+    (rightIndex, rightEdge) <- indexedEdges,+    leftIndex < rightIndex,+    mode leftEdge == mode rightEdge,+    not (isBot (guard leftEdge) || isBot (guard rightEdge)),+    Just (InversionHead leftInputCtor leftWireCtor leftFields) <-+      [headInversionCandidate leftEdge],+    Just (InversionHead rightInputCtor rightWireCtor rightFields) <-+      [headInversionCandidate rightEdge],+    InversionPairKey (fromEnum source) leftIndex rightIndex `elem` warningKeys+  ]+  where+    warningKeys =+      [ key+      | warning <- inversionAmbiguityWarnings transducer,+        Just key <- [inversionWarningKey warning]+      ]++data InversionPairKey = InversionPairKey Int Int Int+  deriving stock (Eq, Ord, Show)++inversionWarningKey ::+  (Enum s) =>+  TransducerValidationWarning s ->+  Maybe InversionPairKey+inversionWarningKey InversionAmbiguity {tvwSource, tvwEdgeA, tvwEdgeB} =+  Just (InversionPairKey (fromEnum tvwSource) tvwEdgeA tvwEdgeB)+inversionWarningKey _ = Nothing++inversionDetailKey ::+  (Enum s) =>+  InversionAnalysisDetail s ->+  InversionPairKey+inversionDetailKey detail =+  InversionPairKey+    (fromEnum detail.iadSource)+    detail.iadLeftEdge.edgeIndex+    detail.iadRightEdge.edgeIndex++data ReplayVarKey+  = ReplayRegisterVar Int SomeTypeRep+  | ReplayInputVar String Int SomeTypeRep+  | ReplayProjectionVar SymVarKey+  deriving stock (Eq, Ord, Show)++data ReplaySharedEnvironment = ReplaySharedEnvironment+  { rseRegisterCache :: IORef (Map ReplayVarKey SomeSBV),+    rseRegisterProjectionCache :: IORef (Map ReplayVarKey SomeSBV),+    rseNextLabel :: IORef Int+  }++data ReplayCandidateEnvironment = ReplayCandidateEnvironment+  { rceCandidate :: InversionCandidate,+    rceInputArm :: SBV.SBool,+    rceInputPathCache :: IORef (Map Int SBV.SBool),+    rceInputFallbackCache :: IORef (Map String SBV.SBool),+    rceInputFallbackOrdinal :: IORef Int,+    rceCandidateCache :: IORef (Map ReplayVarKey SomeSBV),+    rceShared :: ReplaySharedEnvironment,+    rceIssues :: IORef [InversionTranslationIssue]+  }++newReplaySharedEnvironment :: SBV.Symbolic ReplaySharedEnvironment+newReplaySharedEnvironment =+  ReplaySharedEnvironment+    <$> liftIO (newIORef Map.empty)+    <*> liftIO (newIORef Map.empty)+    <*> liftIO (newIORef 0)++newReplayCandidateEnvironment ::+  InversionCandidate ->+  ReplaySharedEnvironment ->+  IORef [InversionTranslationIssue] ->+  SBV.Symbolic ReplayCandidateEnvironment+newReplayCandidateEnvironment candidate shared issues = do+  inputArm <- SBV.free (candidateLabel candidate <> "/arm")+  inputPaths <- liftIO (newIORef Map.empty)+  inputFallbacks <- liftIO (newIORef Map.empty)+  inputFallbackOrdinal <- liftIO (newIORef 0)+  candidateCache <- liftIO (newIORef Map.empty)+  pure+    ReplayCandidateEnvironment+      { rceCandidate = candidate,+        rceInputArm = inputArm,+        rceInputPathCache = inputPaths,+        rceInputFallbackCache = inputFallbacks,+        rceInputFallbackOrdinal = inputFallbackOrdinal,+        rceCandidateCache = candidateCache,+        rceShared = shared,+        rceIssues = issues+      }++candidateLabel :: InversionCandidate -> String+candidateLabel InversionCandidateA = "replay/candidate-a"+candidateLabel InversionCandidateB = "replay/candidate-b"++memoReplayInputPathDecision ::+  ReplayCandidateEnvironment ->+  Int ->+  SBV.Symbolic SBV.SBool+memoReplayInputPathDecision environment position = do+  decisions <- liftIO (readIORef (rceInputPathCache environment))+  case Map.lookup position decisions of+    Just decision -> pure decision+    Nothing -> do+      decision <-+        SBV.free+          (candidateLabel (rceCandidate environment) <> "/constructor/path/" <> show position)+      liftIO+        ( modifyIORef'+            (rceInputPathCache environment)+            (Map.insert position decision)+        )+      pure decision++memoReplayInputFallback ::+  ReplayCandidateEnvironment ->+  String ->+  SBV.Symbolic SBV.SBool+memoReplayInputFallback environment diagnosticName = do+  fallbacks <- liftIO (readIORef (rceInputFallbackCache environment))+  case Map.lookup diagnosticName fallbacks of+    Just fallback -> pure fallback+    Nothing -> do+      ordinal <- liftIO (readIORef (rceInputFallbackOrdinal environment))+      liftIO (modifyIORef' (rceInputFallbackOrdinal environment) (+ 1))+      fallback <-+        SBV.free+          (candidateLabel (rceCandidate environment) <> "/constructor/fallback/" <> show ordinal)+      liftIO+        ( modifyIORef'+            (rceInputFallbackCache environment)+            (Map.insert diagnosticName fallback)+        )+      pure fallback++replayInputCtorConstraint ::+  ReplayCandidateEnvironment ->+  InCtor ci fields ->+  SBV.Symbolic SBV.SBool+replayInputCtorConstraint environment inputCtor =+  case inCtorSchemaPath inputCtor.icSchema of+    Just path -> do+      constraints <- traverse constrainStep (zip [0 ..] path)+      pure (foldr (SBV..&&) SBV.sTrue constraints)+    Nothing -> memoReplayInputFallback environment (icName inputCtor)+  where+    constrainStep (position, isLeft) = do+      decision <- memoReplayInputPathDecision environment position+      pure (if isLeft then decision else SBV.sNot decision)++freshReplayLabel :: ReplaySharedEnvironment -> SBV.Symbolic String+freshReplayLabel shared = liftIO $ do+  ordinal <- readIORef (rseNextLabel shared)+  modifyIORef' (rseNextLabel shared) (+ 1)+  pure ("replay/value/" <> show ordinal)++freshReplayFree ::+  forall value.+  (Sym value) =>+  ReplaySharedEnvironment ->+  SBV.Symbolic (SBV.SBV (SymRep value))+freshReplayFree shared = freshReplayLabel shared >>= symFree @value++freshReplayBool :: ReplayCandidateEnvironment -> SBV.Symbolic SBV.SBool+freshReplayBool environment = do+  label <- freshReplayLabel (rceShared environment)+  SBV.free label++memoReplayFree ::+  forall value.+  (Sym value) =>+  ReplaySharedEnvironment ->+  IORef (Map ReplayVarKey SomeSBV) ->+  ReplayVarKey ->+  SBV.Symbolic (SBV.SBV (SymRep value))+memoReplayFree shared cache key = do+  variables <- liftIO (readIORef cache)+  case Map.lookup key variables of+    Just (SomeSBV (variable :: SBV.SBV representation)) ->+      case eqTypeRep (typeRep @(SymRep value)) (typeRep @representation) of+        Just HRefl -> pure variable+        Nothing ->+          error ("memoReplayFree: type mismatch for structural key " <> show key)+    Nothing -> do+      variable <- freshReplayFree @value shared+      liftIO (modifyIORef' cache (Map.insert key (SomeSBV variable)))+      pure variable++replayRegisterFree ::+  forall value rs.+  (Sym value) =>+  ReplayCandidateEnvironment ->+  Index rs value ->+  SBV.Symbolic (SBV.SBV (SymRep value))+replayRegisterFree environment index =+  memoReplayFree @value+    shared+    (rseRegisterCache shared)+    ( ReplayRegisterVar+        (indexPosition index)+        (SomeTypeRep (typeRep @value))+    )+  where+    shared = rceShared environment++replayInputFree ::+  forall value ci inputFields.+  (Sym value) =>+  ReplayCandidateEnvironment ->+  InCtor ci inputFields ->+  Index inputFields value ->+  SBV.Symbolic (SBV.SBV (SymRep value))+replayInputFree environment inputCtor index =+  memoReplayFree @value+    shared+    (rceCandidateCache environment)+    ( ReplayInputVar+        (icName inputCtor)+        (indexPosition index)+        (SomeTypeRep (typeRep @value))+    )+  where+    shared = rceShared environment++replayProjectionFree ::+  forall projection rs ci inputFields.+  ( Typeable projection,+    Typeable (FieldOwner projection),+    Sym (FieldResult projection)+  ) =>+  ReplayCandidateEnvironment ->+  FieldWitness projection ->+  ProjBase rs ci inputFields (FieldOwner projection) ->+  SBV.Symbolic (SBV.SBV (SymRep (FieldResult projection)))+replayProjectionFree environment witness base =+  memoReplayFree @(FieldResult projection)+    shared+    cache+    (ReplayProjectionVar (projectionVarKey witness base))+  where+    shared = rceShared environment+    cache = case base of+      PBReg {} -> rseRegisterProjectionCache shared+      PBInp {} -> rceCandidateCache environment++translateReplayTerm ::+  forall rs ci inputFields value.+  (Sym value) =>+  ReplayCandidateEnvironment ->+  Term rs ci inputFields value ->+  SBV.Symbolic (SBV.SBV (SymRep value))+translateReplayTerm _environment (TLit value) = pure (symLit value)+translateReplayTerm _environment (TOpaqueLit value) = pure (symLit value)+translateReplayTerm environment (TReg index) =+  replayRegisterFree environment index+translateReplayTerm environment (TInpCtorField inputCtor index) =+  replayInputFree environment inputCtor index+translateReplayTerm environment (TApp1 _function _argument) =+  freshReplayFree @value (rceShared environment)+translateReplayTerm environment (TApp2 _function _left _right) =+  freshReplayFree @value (rceShared environment)+translateReplayTerm environment (TArith operation left right) =+  case discoverSymNum @value of+    Nothing -> freshReplayFree @value (rceShared environment)+    Just SymNumDict -> do+      symbolicLeft <- translateReplayTerm environment left+      symbolicRight <- translateReplayTerm environment right+      case (discoverSymbolicType @value, operation) of+        (Just SymbolicNatural, OpSub) ->+          pure (SBV.ite (symbolicLeft SBV..>= symbolicRight) (symbolicLeft - symbolicRight) 0)+        _ -> pure $ case operation of+          OpAdd -> symbolicLeft + symbolicRight+          OpSub -> symbolicLeft - symbolicRight+          OpMul -> symbolicLeft * symbolicRight+translateReplayTerm environment (TFieldProj witness base) = do+  symbolic <- replayProjectionFree environment witness base+  case fieldWitnessDomain witness of+    Nothing -> pure ()+    Just domain -> case compileProjectionDomain @value domain symbolic of+      Left _unsupported -> pure ()+      Right domainConstraint -> SBV.constrain domainConstraint+  pure symbolic++translateReplayPredicate ::+  forall rs ci.+  ReplayCandidateEnvironment ->+  HsPred rs ci ->+  SBV.Symbolic SBV.SBool+translateReplayPredicate environment = go+  where+    go :: HsPred rs ci -> SBV.Symbolic SBV.SBool+    go PTop = pure SBV.sTrue+    go PBot = pure SBV.sFalse+    go (PAnd left right) = (SBV..&&) <$> go left <*> go right+    go (POr left right) = (SBV..||) <$> go left <*> go right+    go (PNot predicate) = SBV.sNot <$> go predicate+    go (PEq left right) = goEquality left right+    go (PInCtor inputCtor) = replayInputCtorConstraint environment inputCtor+    go PLeftArm = pure (rceInputArm environment)+    go PRightArm = pure (SBV.sNot (rceInputArm environment))+    go (PCmp operation left right) = goOrdering operation left right++    goEquality ::+      forall value leftFields rightFields.+      (Typeable value) =>+      Term rs ci leftFields value ->+      Term rs ci rightFields value ->+      SBV.Symbolic SBV.SBool+    goEquality left right = case discoverSym @value of+      Nothing -> freshReplayBool environment+      Just SymDict -> do+        symbolicLeft <- translateReplayTerm environment left+        symbolicRight <- translateReplayTerm environment right+        pure (symbolicLeft SBV..== symbolicRight)++    goOrdering ::+      forall value leftFields rightFields.+      (Typeable value) =>+      Cmp ->+      Term rs ci leftFields value ->+      Term rs ci rightFields value ->+      SBV.Symbolic SBV.SBool+    goOrdering operation left right = case discoverSymOrd @value of+      Nothing -> freshReplayBool environment+      Just SymOrdDict -> do+        symbolicLeft <- translateReplayTerm environment left+        symbolicRight <- translateReplayTerm environment right+        pure $ case operation of+          CmpLt -> symbolicLeft SBV..< symbolicRight+          CmpLe -> symbolicLeft SBV..<= symbolicRight+          CmpGt -> symbolicLeft SBV..> symbolicRight+          CmpGe -> symbolicLeft SBV..>= symbolicRight++recordInversionIssue ::+  ReplayCandidateEnvironment ->+  InversionTranslationIssue ->+  SBV.Symbolic ()+recordInversionIssue environment issue =+  liftIO (modifyIORef' (rceIssues environment) (++ [issue]))++strictReplayDerivedTerm ::+  forall rs ci inputFields value.+  (Sym value) =>+  ReplayCandidateEnvironment ->+  Int ->+  Term rs ci inputFields value ->+  SBV.Symbolic (Maybe (SBV.SBV (SymRep value)))+strictReplayDerivedTerm environment _position term@TLit {} =+  Just <$> translateReplayTerm environment term+strictReplayDerivedTerm environment _position term@TOpaqueLit {} =+  Just <$> translateReplayTerm environment term+strictReplayDerivedTerm environment _position term@TReg {} =+  Just <$> translateReplayTerm environment term+strictReplayDerivedTerm environment _position term@TInpCtorField {} =+  Just <$> translateReplayTerm environment term+strictReplayDerivedTerm environment position TApp1 {} = do+  recordInversionIssue+    environment+    (InversionOpaqueDerivedOutput (rceCandidate environment) position)+  pure Nothing+strictReplayDerivedTerm environment position TApp2 {} = do+  recordInversionIssue+    environment+    (InversionOpaqueDerivedOutput (rceCandidate environment) position)+  pure Nothing+strictReplayDerivedTerm environment position (TArith operation left right) =+  case discoverSymNum @value of+    Nothing -> do+      recordInversionIssue+        environment+        ( InversionUnsupportedDerivedArithmetic+            (rceCandidate environment)+            position+            (SomeTypeRep (typeRep @value))+        )+      pure Nothing+    Just SymNumDict -> do+      maybeLeft <- strictReplayDerivedTerm environment position left+      maybeRight <- strictReplayDerivedTerm environment position right+      pure $ do+        symbolicLeft <- maybeLeft+        symbolicRight <- maybeRight+        pure $ case (discoverSymbolicType @value, operation) of+          (Just SymbolicNatural, OpSub) ->+            SBV.ite+              (symbolicLeft SBV..>= symbolicRight)+              (symbolicLeft - symbolicRight)+              0+          (_, OpAdd) -> symbolicLeft + symbolicRight+          (_, OpSub) -> symbolicLeft - symbolicRight+          (_, OpMul) -> symbolicLeft * symbolicRight+strictReplayDerivedTerm environment position (TFieldProj witness base) = do+  symbolic <- replayProjectionFree environment witness base+  let descriptor = projectionDescriptor witness base+      unsupported reason = do+        recordInversionIssue+          environment+          ( InversionUnsupportedDerivedProjection+              (rceCandidate environment)+              position+              descriptor+              reason+          )+        pure Nothing+  case fieldWitnessDomain witness of+    Nothing -> unsupported "projection witness has no exact domain"+    Just domain -> case compileProjectionDomain @value domain symbolic of+      Left failure -> unsupported (show failure)+      Right domainConstraint -> do+        SBV.constrain domainConstraint+        pure (Just symbolic)++constrainReplayOutputField ::+  forall rs ci inputFields value.+  (Sym value) =>+  ReplayCandidateEnvironment ->+  InCtor ci inputFields ->+  Int ->+  Set Int ->+  SBV.SBV (SymRep value) ->+  Term rs ci inputFields value ->+  SBV.Symbolic ()+constrainReplayOutputField environment headInputCtor position recovered observed term =+  case term of+    TInpCtorField inputCtor index+      | inputCtorsDefinitelySame inputCtor headInputCtor,+        indexPosition index `Set.notMember` recovered -> do+          candidateInput <- replayInputFree environment inputCtor index+          SBV.constrain (observed SBV..== candidateInput)+      | otherwise -> pure ()+    TArith {} -> constrainDerived+    TFieldProj {} -> constrainDerived+    TApp1 {} ->+      recordInversionIssue+        environment+        (InversionOpaqueDerivedOutput (rceCandidate environment) position)+    TApp2 {} ->+      recordInversionIssue+        environment+        (InversionOpaqueDerivedOutput (rceCandidate environment) position)+    TLit {} -> pure ()+    TOpaqueLit {} -> pure ()+    TReg {} -> pure ()+  where+    constrainDerived = do+      derived <- strictReplayDerivedTerm environment position term+      case derived of+        Nothing -> pure ()+        Just symbolic -> SBV.constrain (observed SBV..== symbolic)++recoveredInputPosition ::+  InCtor ci inputFields ->+  Set Int ->+  Term rs ci inputFields value ->+  Set Int+recoveredInputPosition headInputCtor recovered (TInpCtorField inputCtor index)+  | inputCtorsDefinitelySame inputCtor headInputCtor = Set.insert (indexPosition index) recovered+recoveredInputPosition _ recovered _ = recovered++constrainAlignedOutputFields ::+  forall rs ci leftInputFields leftOutputFields rightInputFields rightOutputFields.+  ReplayCandidateEnvironment ->+  InCtor ci leftInputFields ->+  OutFields rs ci leftInputFields leftOutputFields ->+  ReplayCandidateEnvironment ->+  InCtor ci rightInputFields ->+  OutFields rs ci rightInputFields rightOutputFields ->+  WireFieldAlignment leftOutputFields rightOutputFields ->+  SBV.Symbolic ()+constrainAlignedOutputFields leftEnvironment leftInputCtor leftFields rightEnvironment rightInputCtor rightFields alignment =+  go 0 Set.empty Set.empty leftFields rightFields alignment+  where+    go ::+      Int ->+      Set Int ->+      Set Int ->+      OutFields rs ci leftInputFields leftFieldsRemaining ->+      OutFields rs ci rightInputFields rightFieldsRemaining ->+      WireFieldAlignment leftFieldsRemaining rightFieldsRemaining ->+      SBV.Symbolic ()+    go _position _leftRecovered _rightRecovered OFNil OFNil WireFieldsAlignedNil = pure ()+    go _position _leftRecovered _rightRecovered OFNil (OFCons _ _) impossible =+      case impossible of {}+    go _position _leftRecovered _rightRecovered (OFCons _ _) OFNil impossible =+      case impossible of {}+    go+      position+      leftRecovered+      rightRecovered+      (OFCons (leftTerm :: Term rs ci leftInputFields field) leftRest)+      (OFCons rightTerm rightRest)+      (WireFieldsAlignedCons restAlignment) = do+        case discoverSym @field of+          Nothing ->+            liftIO+              ( modifyIORef'+                  (rceIssues leftEnvironment)+                  ( +++                      [ InversionUnsupportedObservedFieldCarrier+                          position+                          (SomeTypeRep (typeRep @field))+                      ]+                  )+              )+          Just SymDict -> do+            observed <- freshReplayFree @field (rceShared leftEnvironment)+            constrainReplayOutputField+              leftEnvironment+              leftInputCtor+              position+              leftRecovered+              observed+              leftTerm+            constrainReplayOutputField+              rightEnvironment+              rightInputCtor+              position+              rightRecovered+              observed+              rightTerm+        go+          (position + 1)+          (recoveredInputPosition leftInputCtor leftRecovered leftTerm)+          (recoveredInputPosition rightInputCtor rightRecovered rightTerm)+          leftRest+          rightRest+          restAlignment++candidateRecoveryPossible ::+  forall ci inputFields rs outputFields.+  InCtor ci inputFields ->+  OutFields rs ci inputFields outputFields ->+  Bool+candidateRecoveryPossible inputCtor fields =+  namesAgree && recovered == Set.fromList [0 .. length (slotNamesOf inputCtor) - 1]+  where+    (namesAgree, recovered) = walk fields++    walk :: forall remaining. OutFields rs ci inputFields remaining -> (Bool, Set Int)+    walk OFNil = (True, Set.empty)+    walk (OFCons term rest) =+      let (restAgrees, restRecovered) = walk rest+       in case term of+            TInpCtorField termInputCtor index ->+              ( inputCtorsDefinitelySame termInputCtor inputCtor && restAgrees,+                Set.insert (indexPosition index) restRecovered+              )+            _ -> (restAgrees, restRecovered)++guardInversionIssues ::+  InversionCandidate ->+  HsPred rs ci ->+  [InversionTranslationIssue]+guardInversionIssues candidate predicate =+  case predicateTranslationReport predicate of+    ExactTranslation -> []+    ConservativeOverApproximation issues ->+      InversionGuardTranslationIssue candidate <$> toList issues++headInputIdentityIssues ::+  InversionCandidate ->+  InCtor ci fields ->+  [InversionTranslationIssue]+headInputIdentityIssues candidate inputCtor =+  case inCtorSchemaPath inputCtor.icSchema of+    Just _ -> []+    Nothing ->+      [ InversionInputConstructorIdentityUnwitnessed+          candidate+          (icName inputCtor)+      ]++runInversionSolver ::+  SBV.Symbolic SBV.SBool ->+  IO InversionSolverStatus+runInversionSolver query = do+  attempt <- try @SomeException (timeout 10_000_000 (SBV.sat query))+  pure $ case attempt of+    Left failure -> InversionSolverFailure (displayException failure)+    Right Nothing -> InversionSolverTimedOut+    Right (Just (SBV.SatResult result)) -> case result of+      SBV.Satisfiable {} -> InversionSolverSatisfiable+      SBV.Unsatisfiable {} -> InversionSolverUnsatisfiable+      SBV.Unknown {} -> InversionSolverUnknown "solver returned Unknown"+      SBV.ProofError {} -> InversionSolverFailure "solver returned ProofError"+      SBV.DeltaSat {} -> InversionSolverUnknown "solver returned DeltaSat"+      SBV.SatExtField {} -> InversionSolverUnknown "solver returned SatExtField"++inversionVerdict :: InversionSolverStatus -> InversionProofVerdict+inversionVerdict InversionSolverUnsatisfiable = InversionProvedDisjoint+inversionVerdict _ = InversionNotProvedDisjoint++analyzeInversionCandidatePair ::+  InversionCandidatePair rs ci co s ->+  IO (InversionAnalysisDetail s)+analyzeInversionCandidatePair+  ( InversionCandidatePair+      source+      leftIndex+      leftGuard+      leftInputCtor+      leftWireCtor+      leftFields+      rightIndex+      rightGuard+      rightInputCtor+      rightWireCtor+      rightFields+    ) = do+    let leftAvailability = wireSchemaAvailability (wcSchema leftWireCtor)+        rightAvailability = wireSchemaAvailability (wcSchema rightWireCtor)+        leftRef = EdgeRef source leftIndex+        rightRef = EdgeRef source rightIndex+        detail relation status issues =+          InversionAnalysisDetail+            { iadSource = source,+              iadLeftEdge = leftRef,+              iadRightEdge = rightRef,+              iadLeftSchemaAvailability = leftAvailability,+              iadRightSchemaAvailability = rightAvailability,+              iadHeadRelation = relation,+              iadVerdict = inversionVerdict status,+              iadSolverStatus = status,+              iadTranslationIssues = issues+            }+    case compareWireSchemas (wcSchema leftWireCtor) (wcSchema rightWireCtor) of+      WireSchemasUnwitnessed ->+        pure+          ( detail+              WireHeadsUnwitnessed+              InversionSolverNotRun+              [InversionWireSchemasUnwitnessed]+          )+      WireSchemasDifferent -> do+        status <- runInversionSolver (pure SBV.sFalse)+        pure (detail WireHeadsStructurallyDifferent status [])+      WireSchemasEqual alignment -> do+        issuesRef <-+          newIORef+            ( guardInversionIssues InversionCandidateA leftGuard+                ++ guardInversionIssues InversionCandidateB rightGuard+                ++ headInputIdentityIssues InversionCandidateA leftInputCtor+                ++ headInputIdentityIssues InversionCandidateB rightInputCtor+            )+        status <- runInversionSolver $ do+          shared <- newReplaySharedEnvironment+          leftEnvironment <-+            newReplayCandidateEnvironment InversionCandidateA shared issuesRef+          rightEnvironment <-+            newReplayCandidateEnvironment InversionCandidateB shared issuesRef+          leftInputIdentity <- replayInputCtorConstraint leftEnvironment leftInputCtor+          rightInputIdentity <- replayInputCtorConstraint rightEnvironment rightInputCtor+          SBV.constrain leftInputIdentity+          SBV.constrain rightInputIdentity+          symbolicLeftGuard <- translateReplayPredicate leftEnvironment leftGuard+          symbolicRightGuard <- translateReplayPredicate rightEnvironment rightGuard+          constrainAlignedOutputFields+            leftEnvironment+            leftInputCtor+            leftFields+            rightEnvironment+            rightInputCtor+            rightFields+            alignment+          let leftRecovers = candidateRecoveryPossible leftInputCtor leftFields+              rightRecovers = candidateRecoveryPossible rightInputCtor rightFields+          pure+            ( symbolicLeftGuard+                SBV..&& symbolicRightGuard+                SBV..&& if leftRecovers && rightRecovers then SBV.sTrue else SBV.sFalse+            )+        issues <- readIORef issuesRef+        pure (detail WireHeadsStructurallyEqual status issues)++-- | Run the opt-in dual-candidate replay analysis once for every pair emitted+-- by 'inversionAmbiguityWarnings'. This is never called by default validation+-- or runtime replay.+checkInversionAmbiguitySymDetailed ::+  forall s rs ci co.+  (Bounded s, Enum s, Show s) =>+  SymTransducer (HsPred rs ci) rs s ci co ->+  IO [InversionAnalysisDetail s]+checkInversionAmbiguitySymDetailed transducer =+  show (minBound @s) `seq`+    traverse analyzeInversionCandidatePair (inversionCandidatePairs transducer)++-- | Compatibility projection of 'checkInversionAmbiguitySymDetailed'. It+-- returns the exact existing warning values, removing a pair only after a+-- definite solver 'Unsatisfiable' result for that exact source-and-edges key.+-- Missing or duplicate details fail closed by retaining the warning.+checkInversionAmbiguitySym ::+  (Bounded s, Enum s, Show s) =>+  SymTransducer (HsPred rs ci) rs s ci co ->+  IO [TransducerValidationWarning s]+checkInversionAmbiguitySym transducer = do+  let warnings = inversionAmbiguityWarnings transducer+  details <- checkInversionAmbiguitySymDetailed transducer+  pure+    [ warning+    | warning <- warnings,+      case inversionWarningKey warning of+        Nothing -> True+        Just key ->+          case filter ((== key) . inversionDetailKey) details of+            [detail] ->+              not+                ( iadSolverStatus detail == InversionSolverUnsatisfiable+                    && iadVerdict detail == InversionProvedDisjoint+                )+            _ -> True+    ]++-- * 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 =+  unavailableInCtor+    "()"+    (\() -> Just RNil)+    (\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 constructors = zip [(0 :: Int) ..] (allInCtors @ci)+      when (not (null constructors)) $ do+        branches <- forM constructors $ \(ordinal, SomeInCtor inputCtor) -> do+          identity <- inputCtorConstraint environment inputCtor+          pure+            ( (seInputCtor environment SBV..== SBV.literal (show ordinal))+                SBV..&& identity+            )+        SBV.constrain (SBV.sOr branches)++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 stable list ordinal+-- matches the model's input-constructor selector, then 'extractRegFile'+-- over the matched 'InCtor''s field list and call 'icBuild' to+-- assemble a @ci@. Returns 'Nothing' only if model decoding violates the+-- ordinal domain constrained by 'symSatExt'.+pickCi ::+  forall ci.+  (KnownInCtors ci) =>+  String ->+  (forall r. (Sym r) => String -> Int -> String -> r) ->+  Maybe ci+pickCi tag readField = go 0 (allInCtors @ci)+  where+    go :: Int -> [SomeInCtor ci] -> Maybe ci+    go _ [] = Nothing+    go ordinal (SomeInCtor ic@InCtor {} : rest)+      | show ordinal == tag =+          let regs = extractRegFileAt 0 (readField (icName ic))+           in Just (icBuild ic regs)+      | otherwise = go (ordinal + 1) rest

@@ -136,6 +136,20 @@         Just (_, regs) -> regs K.! (#counter :: Index Regs Int) `shouldBe` 42         Nothing -> expectationFailure "delta returned Nothing" +    it "passes a trusted wire schema through emit unchanged" $ do+      let tr = B.buildTransducer A emptyR (const False) do+            B.from A do+              B.onCmd inCtorTick $ \d -> B.do+                B.emit wireTicked (OFCons d.count OFNil)+                B.goto B+      case edgesOut tr A of+        [edge] -> case output edge of+          [K.OPack _ wire _] ->+            K.wireSchemaAvailability wire.wcSchema+              `shouldBe` K.WireSchemaTrusted+          _ -> expectationFailure "expected one structural output"+        _ -> expectationFailure "expected one edge"+     -- Case 2: sequential (.=) to distinct slots agrees with the     -- composite reference. Use a 2-slot register file inline.     it "case 2: sequential (.=) to distinct slots writes both" $ do

@@ -1,12 +1,16 @@+{-# OPTIONS_GHC -Wno-partial-fields #-}+ module Keiki.CompositionAlignmentSpec (spec) where  import Data.Proxy (Proxy (..)) import Data.Text qualified as T+import GHC.Generics (Generic) import Keiki.Composition import Keiki.Core import Keiki.FieldProjSpec qualified as FieldProj import Keiki.Fixtures.ComposeStateful import Keiki.Fixtures.CounterPipeline+import Keiki.Generics (mkInCtorRecordVia, mkWireCtorRecordVia) import Keiki.Profunctor (rmapCo) import Keiki.Render.Pretty (prettyPred, prettyTerm) import Test.Hspec@@ -17,25 +21,24 @@  typoInMsgB :: InCtor MsgB Payload1 typoInMsgB =-  InCtor-    { icName = "MsgTypo",-      icMatch = \(MsgB n) -> Just (RCons (Proxy @"payload") n RNil),-      icBuild = \(RCons _ n RNil) -> MsgB n-    }+  unavailableInCtor+    "MsgTypo"+    (\(MsgB n) -> Just (RCons (Proxy @"payload") n RNil))+    (\(RCons _ n RNil) -> MsgB n)  twoFieldInMsgB :: InCtor MsgB Payload2 twoFieldInMsgB =-  InCtor-    { icName = "MsgB",-      icMatch = \(MsgB n) ->+  unavailableInCtor+    "MsgB"+    ( \(MsgB n) ->         Just           ( RCons               (Proxy @"first")               n               (RCons (Proxy @"second") n RNil)-          ),-      icBuild = \(RCons _ n (RCons _ _ RNil)) -> MsgB n-    }+          )+    )+    (\(RCons _ n (RCons _ _ RNil)) -> MsgB n)  misnamedStageB :: SymTransducer (HsPred BRegs MsgB) BRegs StageVertex MsgB MsgC misnamedStageB =@@ -84,31 +87,21 @@  projectionSourceCtor :: InCtor ProjectionSourceCmd ProjectionSourceFields projectionSourceCtor =-  InCtor-    { icName = "ProjectionSourceCmd",-      icMatch = \(ProjectionSourceCmd doc) ->-        Just (RCons (Proxy @"doc") doc RNil),-      icBuild = \(RCons _ doc RNil) -> ProjectionSourceCmd doc-    }+  unavailableInCtor+    "ProjectionSourceCmd"+    ( \(ProjectionSourceCmd doc) ->+        Just (RCons (Proxy @"doc") doc RNil)+    )+    (\(RCons _ doc RNil) -> ProjectionSourceCmd doc) -data ProjectionMid = ProjectionMid FieldProj.DocInfo-  deriving stock (Eq, Show)+data ProjectionMid = ProjectionMid {doc :: FieldProj.DocInfo}+  deriving stock (Eq, Show, Generic)  projectionMidCtor :: InCtor ProjectionMid '[ '("doc", FieldProj.DocInfo)]-projectionMidCtor =-  InCtor-    { icName = "ProjectionMid",-      icMatch = \(ProjectionMid doc) -> Just (RCons (Proxy @"doc") doc RNil),-      icBuild = \(RCons _ doc RNil) -> ProjectionMid doc-    }+projectionMidCtor = mkInCtorRecordVia @"ProjectionMid"  projectionMidWire :: WireCtor ProjectionMid (FieldProj.DocInfo, ())-projectionMidWire =-  WireCtor-    { wcName = "ProjectionMid",-      wcMatch = \(ProjectionMid doc) -> Just (doc, ()),-      wcBuild = \(doc, ()) -> ProjectionMid doc-    }+projectionMidWire = mkWireCtorRecordVia @"ProjectionMid"  data ProjectionVertex = ProjectionVertex   deriving stock (Eq, Ord, Show, Enum, Bounded)@@ -170,6 +163,148 @@       isFinal = const True     } +data CollisionMid+  = CollisionWire {wireValue :: Int}+  | CollisionInput {inputValue :: Int}+  deriving stock (Eq, Show, Generic)++collisionWire :: WireCtor CollisionMid (Int, ())+collisionWire =+  renameWireCtor "Collision" (mkWireCtorRecordVia @"CollisionWire")++collisionInput :: InCtor CollisionMid '[ '("inputValue", Int)]+collisionInput =+  renameInCtor "Collision" (mkInCtorRecordVia @"CollisionInput")++collisionSource ::+  SymTransducer+    (HsPred '[] ProjectionSourceCmd)+    '[]+    ProjectionVertex+    ProjectionSourceCmd+    CollisionMid+collisionSource =+  SymTransducer+    { edgesOut = \ProjectionVertex ->+        [ Edge+            { guard = matchInCtor projectionSourceCtor,+              update = UKeep,+              output =+                [ pack+                    projectionSourceCtor+                    collisionWire+                    (OFCons (TLit (1 :: Int)) OFNil)+                ],+              target = ProjectionVertex,+              mode = Live+            }+        ],+      initial = ProjectionVertex,+      initialRegs = RNil,+      isFinal = const True+    }++collisionSink ::+  SymTransducer+    (HsPred '[] CollisionMid)+    '[]+    ProjectionVertex+    CollisionMid+    ()+collisionSink =+  SymTransducer+    { edgesOut = \ProjectionVertex ->+        [ Edge+            { guard =+                PAnd+                  (matchInCtor collisionInput)+                  (PEq (TInpCtorField collisionInput #inputValue) (TLit (1 :: Int))),+              update = UKeep,+              output = [],+              target = ProjectionVertex,+              mode = Live+            }+        ],+      initial = ProjectionVertex,+      initialRegs = RNil,+      isFinal = const True+    }++manualBoundaryWire :: WireCtor CollisionMid (Int, ())+manualBoundaryWire =+  unavailableWireCtor+    "ManualBoundary"+    (\case CollisionWire value -> Just (value, ()); CollisionInput {} -> Nothing)+    (\(value, ()) -> CollisionWire value)++manualBoundaryInput :: InCtor CollisionMid '[ '("payload", Int)]+manualBoundaryInput =+  unavailableInCtor+    "ManualBoundary"+    (\case CollisionWire value -> Just (RCons (Proxy @"payload") value RNil); CollisionInput {} -> Nothing)+    (\(RCons _ value RNil) -> CollisionWire value)++manualBoundarySource ::+  SymTransducer+    (HsPred '[] ProjectionSourceCmd)+    '[]+    ProjectionVertex+    ProjectionSourceCmd+    CollisionMid+manualBoundarySource =+  SymTransducer+    { edgesOut = \ProjectionVertex ->+        [ Edge+            { guard = matchInCtor projectionSourceCtor,+              update = UKeep,+              output =+                [ pack+                    projectionSourceCtor+                    manualBoundaryWire+                    (OFCons (TLit (1 :: Int)) OFNil)+                ],+              target = ProjectionVertex,+              mode = Live+            }+        ],+      initial = ProjectionVertex,+      initialRegs = RNil,+      isFinal = const True+    }++manualBoundarySink ::+  SymTransducer+    (HsPred '[] CollisionMid)+    '[]+    ProjectionVertex+    CollisionMid+    ()+manualBoundarySink =+  SymTransducer+    { edgesOut = \ProjectionVertex ->+        [ Edge+            { guard =+                PAnd+                  (matchInCtor manualBoundaryInput)+                  (PEq (TInpCtorField manualBoundaryInput #payload) (TLit (1 :: Int))),+              update = UKeep,+              output = [],+              target = ProjectionVertex,+              mode = Live+            }+        ],+      initial = ProjectionVertex,+      initialRegs = RNil,+      isFinal = const True+    }++containsPBot :: HsPred rs ci -> Bool+containsPBot PBot = True+containsPBot (PAnd left right) = containsPBot left || containsPBot right+containsPBot (POr left right) = containsPBot left || containsPBot right+containsPBot (PNot predicate) = containsPBot predicate+containsPBot _ = False+ spec :: Spec spec = do   describe "checkComposeAlignment" $ do@@ -214,6 +349,43 @@      it "walks every symbol in a multi-event source chain" $       checkComposeAlignment pairSource twoPhaseSink `shouldBe` []++    it "rejects a same-name structurally different input/wire boundary" $ do+      checkComposeAlignment collisionSource collisionSink+        `shouldBe` [ StructurallyDifferentInputWire+                       (EdgeRef ProjectionVertex 0)+                       (EdgeRef ProjectionVertex 0)+                       "Collision"+                       "Collision"+                   ]+      case composeChecked collisionSource collisionSink of+        Left warnings ->+          warnings+            `shouldContain` [ StructurallyDifferentInputWire+                                (EdgeRef ProjectionVertex 0)+                                (EdgeRef ProjectionVertex 0)+                                "Collision"+                                "Collision"+                            ]+        Right _ -> expectationFailure "same-name structural collision passed composeChecked"++    it "rejects an unwitnessed manual input/wire boundary and poisons raw composition" $ do+      let warning =+            UnwitnessedInputWireAlignment+              (EdgeRef ProjectionVertex 0)+              (EdgeRef ProjectionVertex 0)+              "ManualBoundary"+              "ManualBoundary"+      checkComposeAlignment manualBoundarySource manualBoundarySink+        `shouldBe` [warning]+      case edgesOut+        (compose manualBoundarySource manualBoundarySink)+        (Composite ProjectionVertex ProjectionVertex) of+        [edge] -> containsPBot (guard edge) `shouldBe` True+        edges -> expectationFailure ("manual raw composition produced " <> show (length edges) <> " edges")+      case composeChecked manualBoundarySource manualBoundarySink of+        Left warnings -> warnings `shouldBe` [warning]+        Right _ -> expectationFailure "unwitnessed manual boundary passed composeChecked"    describe "typed field projection composition" $ do     let matchingDoc = FieldProj.DocInfo "match" "title" []