diff --git a/gachi-core.cabal b/gachi-core.cabal new file mode 100644 --- /dev/null +++ b/gachi-core.cabal @@ -0,0 +1,46 @@ +cabal-version: 3.0 +name: gachi-core +version: 0.1.0.0 +synopsis: Foundational osteological memory representations and lock-free synchronization +license: EUPL-1.2 +author: Nadia Yvette Chambers +maintainer: nadia.yvette.chambers@ik.me +build-type: Simple +tested-with: + GHC == 9.10.3, + GHC == 9.12.4, + GHC == 9.14.1 + +library + exposed-modules: + Gachi.Core + Gachi.Core.Atomic + Gachi.Core.Rewriting + Gachi.Core.Traversal + Gachi.Osteology + Gachi.Osteology.Atomic + Gachi.Osteology.Polytropos + hs-source-dirs: src + default-language: Haskell2010 + ghc-options: -Wall -Wcompat -Wredundant-constraints + build-depends: + base >= 4.14 && < 5, + primitive >= 0.8, + containers >= 0.6, + text >= 2.0, + polytropos-core >= 0.1 && < 0.2 + +test-suite tests + type: exitcode-stdio-1.0 + main-is: Main.hs + hs-source-dirs: test + default-language: Haskell2010 + ghc-options: -Wall + build-depends: + base >= 4.14 && < 5, + gachi-core, + primitive >= 0.8, + containers >= 0.6, + text >= 2.0, + hspec >= 2.10, + polytropos-core diff --git a/src/Gachi/Core.hs b/src/Gachi/Core.hs new file mode 100644 --- /dev/null +++ b/src/Gachi/Core.hs @@ -0,0 +1,313 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE ScopedTypeVariables #-} + +-- | Module: Gachi.Core +-- Description: Core skeletal definitions, bone/joint identifiers, and chattering synchronization +-- +-- Provides foundational osteological abstractions and deterministic state synchronization +-- inspired by the gashadokuro mythical skeletal folklore. +-- +-- All skeletal structures are backed by contiguous primitive 'OsteoSegment' storage, +-- ensuring $O(1)$ zero-allocation lookups and flat memory locality. +-- +-- = When to Use This Module +-- +-- * **Osteological Skeletal Graphs:** Modeling directed bone-and-joint graphs with contiguous +-- memory representations and monotonic node identifier tracking. +-- * **Lock-Free Concurrency Substrate:** Serving as the structural topology for concurrent +-- chattering agent traversals without mutex contention. +-- * **Zero-Allocation Node Lookup:** Querying bone payloads in $O(1)$ time via 'lookupBone' or +-- 'unsafeLookupBone'. +-- +-- = Worked Example +-- +-- >>> import Gachi.Core +-- >>> let skel0 = emptySkeleton +-- >>> let (b0, skel1) = insertBone "femur" skel0 +-- >>> let (b1, skel2) = insertBone "tibia" skel1 +-- >>> let (j0, skel3) = connectJoint b0 b1 skel2 +-- >>> lookupBone b0 skel3 +-- Just "femur" +-- >>> totalJoints skel3 +-- 1 +module Gachi.Core + ( -- * Osteological Identifiers + BoneId(..) + , JointId(..) + , Joint(..) + , Bone(..) + + -- * Skeletal Structures + , Skeleton(..) + , emptySkeleton + , totalBones + , totalJoints + , insertBone + , lookupBone + , unsafeLookupBone + , connectJoint + , lookupJoint + , allBones + , allBonesWithId + , allJoints + , incidentJoints + , sliceBones + , initAtomicJoints + , getAtomicJoint + + -- * Lock-Free Atomic Joint State Machine + , module Gachi.Core.Atomic + ) where + +import Gachi.Core.Atomic + +import Data.Word (Word64) +import GHC.Generics (Generic) +import Gachi.Osteology + ( OsteoSegment + , emptySegment + , segmentLength + , appendOsteo + , indexOsteo + , unsafeIndexOsteo + , sliceOsteo + , toListOsteo + , fromListOsteo + ) + +{- Note [Chattering Lock-Free Atomic Synchronization] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +[tag:note-chattering-synchronization] +The hallmark of a gashadokuro in folklore is the distinct, rhythmic 'gachi-gachi' +chattering of its teeth before it appears. In the Gachi substrate, 'chattering' represents +the deterministic synchronization cadence of concurrent agents navigating osteological graphs. + +Traditional multi-threaded graph traversal utilizes mutexes or Reader-Writer locks, which +suffer from: + 1. Cache-line bouncing across multi-core processors. + 2. Severe thread contention under high read/write ratios. + 3. Convoy effects and deadlocks under asynchronous cancellation. + +Gachi resolves this by employing lock-free, optimistic atomic state progression: + - Joints are represented as atomic references capable of single-instruction compare-and-swap + (CAS) updates. + - Reader agents traverse immutable snapshots of the skeletal topology without acquiring locks. + - When concurrent modifications collide, the chattering synchronization protocol retries + with bounded exponential backoff, preserving global progress and lock-freedom. +-} + +{- Note [Monotonic Identifier Allocation and Contiguous Indexing] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +[tag:note-monotonic-id-allocation] +In high-performance graph processing and AST transformation passes, node lookups +frequently bottleneck on map operations. Standard implementations rely on balanced +binary search trees (such as 'Data.Map.Map', incurring O(log N) pointer dereferences) +or hash tables (incurring hashing overhead, pointer collisions, and bucket indirection). + +Gachi adopts a strict monotonic identifier allocation strategy: + 1. Contiguous Identity Mapping: 'BoneId' and 'JointId' are monotonically increasing + 64-bit unsigned integers ('Word64'). Because bones are inserted into an append-only + contiguous 'OsteoSegment', each 'BoneId' corresponds exactly to its contiguous array + offset in 'skeletonBones'. + 2. O(1) Zero-Allocation Lookups: Querying 'lookupBone' or 'unsafeLookupBone' reduces + to a single integer conversion and direct array indexing via 'indexOsteo' / + 'unsafeIndexOsteo'. No hashing, tree balancing, or intermediate allocation occurs. + 3. Determinism & Generation Stability: Identifiers are strictly monotonic within a + skeletal generation, eliminating identifier recycling hazards and guaranteeing + byte-for-byte reproducibility during serialization and AST comparison. + +See also: + - Note [Osteological Contiguous Memory Layout] [ref:note-osteology-memory-layout] +-} + +{- Note [Directional Joints and Incident Traversal] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +[tag:note-directional-joints-traversal] +Skeletal structures represent directed multigraphs where nodes ('BoneId') are joined +by directed edges ('Joint'). A joint captures a directional dependency or structural +link between a source bone and a target bone. + +Key Structural Properties: + 1. Contiguous Edge Storage: All joints are stored in a dedicated contiguous 'OsteoSegment' + ('skeletonJoints'). This layout ensures that traversing or filtering the edge set + benefits from sequential memory prefetching rather than traversing linked-list edge + structures. + 2. Incident Edge Resolution: 'incidentJoints' resolves all edges touching a specific + bone (as either source or target). This primitive underlies bidirectional dependency + resolution, AST parent-child navigation, and topological sorting passes. + 3. Compositional Isolation: Bone payloads and joint topologies reside in independent + osteological segments, permitting payload transformation (via 'fmap' on bones) + without invalidating or reallocating the joint topology. +-} + +-- | Strongly-typed unique identifier for an osteological bone node. +newtype BoneId = BoneId { unBoneId :: Word64 } + deriving (Eq, Ord, Show, Generic) + +-- | An osteological bone node comprising its unique 'BoneId' and associated payload @a@. +data Bone a = Bone + { boneId :: !BoneId + , bonePayload :: !a + } deriving (Eq, Ord, Show, Generic) + +-- | Strongly-typed unique identifier for a skeletal joint connection. +newtype JointId = JointId { unJointId :: Word64 } + deriving (Eq, Ord, Show, Generic) + +-- | A directional joint connecting a source bone to a target bone. +data Joint = Joint + { jointId :: !JointId + -- ^ Unique identifier for this joint connection. + , jointSource :: !BoneId + -- ^ The originating bone handle. + , jointTarget :: !BoneId + -- ^ The terminating bone handle. + } deriving (Eq, Ord, Show, Generic) + +-- | A skeletal graph structure parameterized over payload @a@. +-- Contains a contiguous collection of osteological bones and joints. +-- +-- All nodes and connections are packed into contiguous 'OsteoSegment' structures +-- guaranteeing cache-line spatial locality and zero-allocation indexing. +-- +-- See Note [Osteological Contiguous Memory Layout] [ref:note-osteology-memory-layout], +-- Note [Chattering Lock-Free Atomic Synchronization] [ref:note-chattering-synchronization], +-- Note [Monotonic Identifier Allocation and Contiguous Indexing] [ref:note-monotonic-id-allocation], +-- Note [Directional Joints and Incident Traversal] [ref:note-directional-joints-traversal], +-- and Note [Concurrent Skeletal Graph Traversal] [ref:note-concurrent-traversal]. +data Skeleton a = Skeleton + { skeletonBones :: !(OsteoSegment a) + -- ^ Contiguous flat primitive array storing bone payloads. + , skeletonJoints :: !(OsteoSegment Joint) + -- ^ Contiguous flat primitive array storing skeletal joints. + , skeletonNextId :: !Word64 + -- ^ Monotonically increasing identifier counter for next bone allocation. + , skeletonAtomicJoints :: !(OsteoSegment AtomicJoint) + -- ^ Contiguous primitive array storing atomic references for lock-free joint state transitions. + } deriving (Eq, Show, Generic) + +-- | Create an empty skeletal structure with zero bones and zero joints. +emptySkeleton :: Skeleton a +emptySkeleton = Skeleton + { skeletonBones = emptySegment + , skeletonJoints = emptySegment + , skeletonNextId = 0 + , skeletonAtomicJoints = emptySegment + } + +-- | Count the total number of bones currently assembled in the skeleton. +-- +-- Time complexity: @O(1)@. +totalBones :: Skeleton a -> Int +totalBones = segmentLength . skeletonBones + +-- | Count the total number of joints connecting bones in the skeleton. +-- +-- Time complexity: @O(1)@. +totalJoints :: Skeleton a -> Int +totalJoints = segmentLength . skeletonJoints + +-- | Insert a new bone with payload @a@ into the skeleton, returning the assigned 'BoneId' +-- and the updated 'Skeleton'. +-- +-- Time complexity: @O(1)@ amortized. +-- +-- See Note [Monotonic Identifier Allocation and Contiguous Indexing] [ref:note-monotonic-id-allocation]. +insertBone :: a -> Skeleton a -> (BoneId, Skeleton a) +insertBone !val skel = + let bid = BoneId (skeletonNextId skel) + newBones = appendOsteo val (skeletonBones skel) + newSkel = skel + { skeletonBones = newBones + , skeletonNextId = skeletonNextId skel + 1 + } + in (bid, newSkel) + +-- | Retrieve the payload associated with a specific 'BoneId' with bounds checking. +-- Returns 'Nothing' if the 'BoneId' is unallocated or out of bounds. +-- +-- Time complexity: @O(1)@ zero-allocation. +-- +-- See Note [Monotonic Identifier Allocation and Contiguous Indexing] [ref:note-monotonic-id-allocation]. +lookupBone :: BoneId -> Skeleton a -> Maybe a +lookupBone (BoneId w) skel = + indexOsteo (fromIntegral w) (skeletonBones skel) +{-# INLINE lookupBone #-} + +-- | Retrieve the payload associated with a specific 'BoneId' without bounds checking. +-- Precondition: The 'BoneId' was returned by a prior 'insertBone' on this skeleton. +-- +-- Time complexity: @O(1)@ zero-allocation. +-- +-- See Note [Monotonic Identifier Allocation and Contiguous Indexing] [ref:note-monotonic-id-allocation]. +unsafeLookupBone :: BoneId -> Skeleton a -> a +unsafeLookupBone (BoneId w) skel = + unsafeIndexOsteo (fromIntegral w) (skeletonBones skel) +{-# INLINE unsafeLookupBone #-} + +-- | Connect two bones via a directed skeletal 'Joint'. +-- Returns the assigned 'JointId' and the updated 'Skeleton'. +-- +-- Time complexity: @O(1)@ amortized. +-- +-- See Note [Directional Joints and Incident Traversal] [ref:note-directional-joints-traversal]. +connectJoint :: BoneId -> BoneId -> Skeleton a -> (JointId, Skeleton a) +connectJoint src dst skel = + let jid = JointId (fromIntegral (totalJoints skel)) + newJoint = Joint jid src dst + newJoints = appendOsteo newJoint (skeletonJoints skel) + newSkel = skel { skeletonJoints = newJoints } + in (jid, newSkel) + +-- | Retrieve a skeletal joint by its 'JointId'. +-- +-- Time complexity: @O(1)@. +-- +-- See Note [Directional Joints and Incident Traversal] [ref:note-directional-joints-traversal]. +lookupJoint :: JointId -> Skeleton a -> Maybe Joint +lookupJoint (JointId w) skel = + indexOsteo (fromIntegral w) (skeletonJoints skel) +{-# INLINE lookupJoint #-} + +-- | Extract all bone payloads as a standard Haskell list. +allBones :: Skeleton a -> [a] +allBones = toListOsteo . skeletonBones + +-- | Extract all skeletal joints as a standard Haskell list. +allJoints :: Skeleton a -> [Joint] +allJoints = toListOsteo . skeletonJoints + +-- | Find all joints incident to a given 'BoneId' (as either source or target). +-- +-- See Note [Directional Joints and Incident Traversal] [ref:note-directional-joints-traversal]. +incidentJoints :: BoneId -> Skeleton a -> [Joint] +incidentJoints bid skel = + filter (\j -> jointSource j == bid || jointTarget j == bid) (allJoints skel) + +-- | Create a zero-copy sub-segment slice of bone payloads. +-- +-- See Note [Zero-Copy Sub-Segment Slicing] [ref:note-zero-copy-slicing]. +sliceBones :: Int -> Int -> Skeleton a -> Maybe (OsteoSegment a) +sliceBones off len skel = sliceOsteo off len (skeletonBones skel) + +-- | Extract all bone nodes paired with their monotonically assigned 'BoneId' handles. +allBonesWithId :: Skeleton a -> [Bone a] +allBonesWithId skel = + let n = totalBones skel + in [ Bone (BoneId (fromIntegral i)) (unsafeLookupBone (BoneId (fromIntegral i)) skel) + | i <- [0 .. n - 1] + ] + +-- | Initialize atomic joint state references for all joints in a skeleton. +initAtomicJoints :: Skeleton a -> IO (Skeleton a) +initAtomicJoints skel = do + let n = totalJoints skel + refs <- mapM (\_ -> newAtomicJoint JointInert) [0 .. n - 1] + pure $! skel { skeletonAtomicJoints = fromListOsteo refs } + +-- | Retrieve the atomic joint reference for a given 'JointId', if initialized. +getAtomicJoint :: JointId -> Skeleton a -> Maybe AtomicJoint +getAtomicJoint (JointId w) skel = + indexOsteo (fromIntegral w) (skeletonAtomicJoints skel) +{-# INLINE getAtomicJoint #-} diff --git a/src/Gachi/Core/Atomic.hs b/src/Gachi/Core/Atomic.hs new file mode 100644 --- /dev/null +++ b/src/Gachi/Core/Atomic.hs @@ -0,0 +1,180 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DerivingStrategies #-} + +-- | Module: Gachi.Core.Atomic +-- Description: Lock-free atomic state machines and bounded backoff for skeletal joints +-- +-- Implements compare-and-swap (CAS) transitions and contention-resilient exponential +-- backoff retry protocols for skeletal joints across concurrent multi-agent traversals. +-- +-- Joint transitions operate strictly lock-free with zero mutex deadlocks, guaranteeing +-- wait-free progression for read traversals and livelock prevention under write saturation. +-- +-- See Note [Chattering Lock-Free Atomic Synchronization] [ref:note-chattering-synchronization]. +-- +-- = Architectural Invariants +-- +-- * **Zero Mutex Contention:** Transitions rely on native CPU compare-and-swap ('casJointState') +-- rather than OS mutexes or runtime MVars. +-- * **Wait-Free Snapshot Reads:** 'readJointState' performs a single atomic memory read +-- without spinning or waiting on writer threads. +-- * **Bounded Exponential Backoff:** 'transitionJointWithBackoff' desynchronizes contending +-- agents using jittered, bounded exponential delays to eliminate livelocks. +-- +-- = Worked Example +-- +-- >>> import Gachi.Core.Atomic +-- >>> joint <- newAtomicJoint JointInert +-- >>> readJointState joint +-- JointInert +-- >>> casJointState joint JointInert (JointChattering 1) +-- True +-- >>> readJointState joint +-- JointChattering 1 +-- >>> transitionJointWithBackoff joint (\s -> case s of JointChattering n -> Just (JointChattering (n + 1)); _ -> Nothing) 10 +-- Right (JointChattering 2) +module Gachi.Core.Atomic + ( -- * Atomic Joint State Machine + casJointState + , transitionJointWithBackoff + , readJointState + , writeJointState + + -- * Error Conditions + , AtomicError(..) + + -- * Re-exports from Osteology Substrate + , JointState(..) + , AtomicJoint(..) + , newAtomicJoint + , newAtomicJointRaw + , readAtomicJointRaw + , writeAtomicJointRaw + , casAtomicJointRaw + , encodeJointState + , decodeJointState + , isJointInert + , isJointChattering + , isJointSynchronized + , isJointFused + ) where + +import Control.Concurrent (threadDelay) +import Control.Exception (Exception) +import Data.Bits (shiftL) +import GHC.Generics (Generic) +import Gachi.Osteology.Atomic + ( AtomicJoint(..) + , JointState(..) + , casAtomicJointRaw + , decodeJointState + , encodeJointState + , isJointChattering + , isJointFused + , isJointInert + , isJointSynchronized + , newAtomicJoint + , newAtomicJointRaw + , readAtomicJointRaw + , writeAtomicJointRaw + ) + +-------------------------------------------------------------------------------- +-- Error Conditions +-------------------------------------------------------------------------------- + +-- | Error conditions encountered during lock-free atomic transitions. +-- +-- Tested against Note [Chattering Lock-Free Atomic Synchronization] [ref:note-chattering-synchronization]. +data AtomicError + = InvalidTransition !JointState + -- ^ The transition function returned 'Nothing' for the observed state, + -- indicating an illegal or unsupported lifecycle transition. + | MaxRetriesExceeded !Int + -- ^ Bounded exponential backoff exhausted after the specified number of retries + -- due to persistent contention from competing concurrent threads. + deriving stock (Eq, Ord, Show, Generic) + +instance Exception AtomicError + +-------------------------------------------------------------------------------- +-- Atomic Joint State Machine Primitives +-------------------------------------------------------------------------------- + +-- | Wait-free atomic memory read of the current 'JointState'. +-- +-- Reads the unboxed 64-bit tagged word using a single atomic load instruction +-- and decodes it into a 'JointState'. Readers never block, allocate locks, or +-- stall writer threads. +-- +-- See Note [Chattering Lock-Free Atomic Synchronization] [ref:note-chattering-synchronization]. +readJointState :: AtomicJoint -> IO JointState +readJointState !joint = do + !w <- readAtomicJointRaw joint + pure $! decodeJointState w +{-# INLINE readJointState #-} + +-- | Atomic memory write of a 'JointState'. +-- +-- Encodes the given 'JointState' into an unboxed 64-bit tagged word and stores +-- it with release semantics. +writeJointState :: AtomicJoint -> JointState -> IO () +writeJointState !joint !st = + writeAtomicJointRaw joint (encodeJointState st) +{-# INLINE writeJointState #-} + +-- | Atomic compare-and-swap (CAS) updating the joint state if and only if +-- the current state matches the expected state. +-- +-- Returns 'True' if the transition succeeded; returns 'False' if the observed +-- state differed from 'expected', leaving the joint untouched. +-- +-- See Note [Chattering Lock-Free Atomic Synchronization] [ref:note-chattering-synchronization]. +casJointState :: AtomicJoint -> JointState -> JointState -> IO Bool +casJointState !joint !expected !target = + casAtomicJointRaw joint (encodeJointState expected) (encodeJointState target) +{-# INLINE casJointState #-} + +-- | Execute an optimistic atomic state transition with bounded exponential backoff. +-- +-- Implements the lock-free retry loop: +-- 1. Optimistic Read: Reads the current 'JointState' wait-free. +-- 2. Target Evaluation: Applies the pure transition function @(JointState -> Maybe JointState)@. +-- If the function returns 'Nothing', fails immediately with 'InvalidTransition'. +-- 3. Compare-And-Swap: Attempts 'casJointState' from the observed state to the target state. +-- 4. Contention Backoff: If CAS fails, yields execution with bounded exponential delay +-- up to @maxRetries@ before returning 'MaxRetriesExceeded'. +-- +-- See Note [Chattering Lock-Free Atomic Synchronization] [ref:note-chattering-synchronization]. +transitionJointWithBackoff + :: AtomicJoint + -> (JointState -> Maybe JointState) + -> Int + -> IO (Either AtomicError JointState) +transitionJointWithBackoff !joint !stepFn !maxRetries = go 0 + where + -- Base backoff delay in microseconds (10 µs) + baseDelayMicros :: Int + baseDelayMicros = 10 + + -- Maximum ceiling backoff delay in microseconds (5,000 µs = 5 ms) + maxDelayMicros :: Int + maxDelayMicros = 5000 + + go !attempt = do + !curr <- readJointState joint + case stepFn curr of + Nothing -> pure (Left (InvalidTransition curr)) + Just !next -> do + !succCAS <- casJointState joint curr next + if succCAS + then pure (Right next) + else if attempt >= maxRetries + then pure (Left (MaxRetriesExceeded maxRetries)) + else do + -- Exponential backoff: baseDelay * 2^(min attempt 10) + let !shiftAmount = min attempt 10 + !delay = min maxDelayMicros (baseDelayMicros `shiftL` shiftAmount) + threadDelay delay + go (attempt + 1) diff --git a/src/Gachi/Core/Rewriting.hs b/src/Gachi/Core/Rewriting.hs new file mode 100644 --- /dev/null +++ b/src/Gachi/Core/Rewriting.hs @@ -0,0 +1,542 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ScopedTypeVariables #-} + +-- | Module: Gachi.Core.Rewriting +-- Description: Double-Pushout (DPO) category-theoretic graph rewriting over osteological skeletal graphs +-- +-- Provides a declarative, provably sound Double-Pushout (DPO) algebraic graph rewriting engine +-- operating over contiguous osteological skeletal graphs ('Skeleton a'). Implements monomorphic +-- subgraph matching, adhesive category gluing condition verification (dangling and identification +-- conditions), pushout complement derivation (deletion), and pushout construction (addition). +-- +-- See Note [Double-Pushout Algebraic Graph Rewriting] [ref:note-dpo-graph-rewriting]. +-- +-- = Architectural Invariants +-- +-- * **Adhesive Category Correctness:** Every production rule application strictly verifies +-- the gluing condition before mutating the graph topology. +-- * **Contiguous Memory Preservation:** Derived context and pushout skeletons preserve +-- contiguous bone indexing and zero-allocation \(O(1)\) lookup performance. +-- * **Monotonic Identifier Allocation:** Newly synthesized bones and joints receive monotonically +-- increasing handles without identifier recycling hazards. +-- * **Referential Transparency:** Graph transformations are purely functional; snapshots +-- and original skeletons remain completely immutable. +module Gachi.Core.Rewriting + ( -- * Double-Pushout Data Types + ProductionRule(..) + , GraphMatch(..) + , RewritingError(..) + + -- * Rule Construction & Validation + , emptyMatch + , validateRule + , validateGluingCondition + + -- * Algebraic DPO Rewriting Engine + , findMatches + , derivePushoutComplement + , constructPushout + , applyRule + , applyRuleFirstMatch + ) where + +import Control.Monad (foldM, forM, forM_, unless, when) +import Data.List (partition) +import Data.Map.Strict (Map) +import qualified Data.Map.Strict as Map +import Data.Set (Set) +import qualified Data.Set as Set +import Data.Text (Text, pack) +import GHC.Generics (Generic) + +import Gachi.Core + ( Bone(..) + , BoneId(..) + , Joint(..) + , JointId(..) + , Skeleton(..) + , allBonesWithId + , allJoints + , connectJoint + , emptySkeleton + , insertBone + , lookupBone + , lookupJoint + ) + +{- Note [Double-Pushout Algebraic Graph Rewriting] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +[tag:note-dpo-graph-rewriting] +Category-theoretic graph transformation provides declarative, provably sound topological +mutations over osteological skeletal graphs. In the Double-Pushout (DPO) algebraic approach, +a transformation rule is formalized as a span of monomorphisms in an adhesive category: + + l r + L <--------- K ---------> R + | | | + m | | | + v (1) v (2) v + G <--------- D ---------> H + +where: + - 'L' is the left-hand pattern graph to match within host graph 'G'. + - 'K' is the interface / gluing graph capturing the topological boundary preserved + across the transformation. + - 'R' is the right-hand replacement graph substituting 'L \ K' in derived graph 'H'. + - 'l : K -> L' and 'r : K -> R' are monic graph embeddings. + - 'm : L -> G' is a graph match identifying a candidate redex. + +The transformation proceeds in two categorical pushout steps: + 1. First Pushout Complement (Deletion): + Square (1) is a pushout complement, deriving the context graph 'D' by excising the + deleted items: 'D = G \ m(L \ K)'. + By the gluing condition in adhesive categories, this complement exists and is unique + up to isomorphism if and only if two conditions hold: + a. Dangling Condition: No edge in 'G \ m(L)' is incident to any vertex in 'm(L \ K)'. + Deleting a vertex must never leave external host edges dangling without endpoints. + b. Identification Condition: If 'm' identifies two distinct elements in 'L' (i.e. + 'm(x) = m(y)' with 'x /= y'), both elements must reside in 'l(K)'. Items scheduled + for deletion cannot be conflated with preserved items or other deleted items. + + 2. Second Pushout (Addition): + Square (2) is a categorical pushout gluing replacement 'R' to context 'D' along interface 'K': + 'H = D \amalg_K R'. Preserved interface vertices and edges are identified, while newly + synthesized vertices in 'R \ r(K)' and edges are adjoined. + +Osteological Memory Layout Invariants: +In the Gachi osteological substrate, skeletons are represented as contiguous unboxed +primitive segments ('OsteoSegment a' for bones, 'OsteoSegment Joint' for edges). +Arbitrary node deletion in standard pointer-graph implementations creates heap fragmentation +and invalidates contiguous array indexing. + +The Gachi DPO engine enforces strict contiguous memory compaction during rewriting: + 1. Monotonic Index Compaction: + When constructing pushout complement 'D', retained bones from 'G' are compacted into + a contiguous range [0 .. |V_D| - 1] via monotonic index compression: + 'newId(v) = oldId(v) - count(deleted vertices < oldId(v))'. + 2. Sequential ID Allocation: + Newly added bones from 'R \ r(K)' are appended sequentially to 'D', receiving monotonic + identifiers [|V_D| .. |V_D| + |V_new| - 1], preserving contiguous indexing and O(1) + zero-allocation 'lookupBone' / 'unsafeLookupBone' access. + 3. Topological Soundness: + Incident joint endpoints are remapped consistently to the new contiguous bone indices, + guaranteeing that derived graph 'H' satisfies all invariants of 'Gachi.Core.Skeleton'. + +Integration with Gargamelle: +DPO productions integrate directly into 'gargamelle' term and graph rewriting pipelines, +enabling declarative osteological transformations such as node fission, node fusion, +chain simplification, and bridge synthesis while maintaining categorical correctness. + +See also: + - Note [Directional Joints and Incident Traversal] [ref:note-directional-joints-traversal] + - Note [Monotonic Identifier Allocation and Contiguous Indexing] [ref:note-monotonic-id-allocation] + - Note [Osteological Contiguous Memory Layout] [ref:note-osteology-memory-layout] +-} + +-------------------------------------------------------------------------------- +-- Double-Pushout Data Types +-------------------------------------------------------------------------------- + +-- | A Double-Pushout (DPO) production rule @p = (L <--l-- K --r--> R)@. +-- +-- A rule specifies a left pattern @L@ to match in host graph @G@, an interface @K@ +-- representing preserved topological structure, and a right replacement @R@ +-- to glue along @K@. The morphisms @morphismL@ and @morphismR@ map interface joints +-- and bones into @L@ and @R@ respectively. +data ProductionRule a = ProductionRule + { ruleName :: !Text + -- ^ Human-readable descriptive name for this production rule. + , ruleLeft :: !(Skeleton a) + -- ^ Left-hand pattern graph @L@ to search and match within the host skeleton. + , ruleInterface :: !(Skeleton a) + -- ^ Gluing interface @K@ preserved across deletion and pushout addition. + , ruleRight :: !(Skeleton a) + -- ^ Right-hand replacement graph @R@ substituting @L \setminus K@ in result @H@. + , morphismL :: !(Map JointId JointId, Map BoneId BoneId) + -- ^ Monic embedding @l : K -> L@ (mapping joints and bones of @K@ into @L@). + , morphismR :: !(Map JointId JointId, Map BoneId BoneId) + -- ^ Monic embedding @r : K -> R@ (mapping joints and bones of @K@ into @R@). + } deriving stock (Eq, Show, Generic) + +-- | A match morphism @m : L -> G@ embedding pattern graph @L@ into host skeleton @G@. +data GraphMatch = GraphMatch + { matchJoints :: !(Map JointId JointId) + -- ^ Mapping from joint identifiers in @L@ to joint identifiers in host @G@. + , matchBones :: !(Map BoneId BoneId) + -- ^ Mapping from bone identifiers in @L@ to bone identifiers in host @G@. + } deriving stock (Eq, Ord, Show, Generic) + +-- | Categorical and topological errors encountered during DPO rewriting passes. +data RewritingError + = MatchNotFound !Text + -- ^ Subgraph pattern matching failed to find a valid embedding. + | DanglingConditionViolated !Text + -- ^ Gluing condition failure: external edges in @G \setminus m(L)@ are incident to + -- vertices scheduled for deletion in @m(L \setminus K)@. + | IdentificationConditionViolated !Text + -- ^ Gluing condition failure: match identifies distinct items in @L@ that are not + -- both members of interface @l(K)@. + | PushoutComplementFailed !Text + -- ^ Pushout complement derivation failed due to structural inconsistency. + | InvalidRuleMorphism !Text + -- ^ Monic embedding @l : K -> L@ or @r : K -> R@ violates graph homomorphism constraints. + deriving stock (Eq, Ord, Show, Generic) + +-- | Construct an empty 'GraphMatch' with no mapped bones or joints. +emptyMatch :: GraphMatch +emptyMatch = GraphMatch + { matchJoints = Map.empty + , matchBones = Map.empty + } + +-------------------------------------------------------------------------------- +-- Rule Validation +-------------------------------------------------------------------------------- + +-- | Validate structural integrity of production rule embeddings @l : K -> L@ and @r : K -> R@. +-- Verifies that embeddings are total on @K@, preserve joint connectivity, and are monomorphic (injective). +validateRule :: ProductionRule a -> Either RewritingError () +validateRule rule = do + validateEmbedding "morphismL" (ruleInterface rule) (ruleLeft rule) (morphismL rule) + validateEmbedding "morphismR" (ruleInterface rule) (ruleRight rule) (morphismR rule) + where + validateEmbedding name k target (jMap, bMap) = do + let kBones = allBonesWithId k + kJoints = allJoints k + + -- Check all bones of K are mapped to valid target bones + forM_ kBones $ \b -> do + case Map.lookup (boneId b) bMap of + Nothing -> + Left (InvalidRuleMorphism (name <> ": interface bone " <> showT (unBoneId (boneId b)) <> " not mapped")) + Just tBid -> + case lookupBone tBid target of + Nothing -> + Left (InvalidRuleMorphism (name <> ": interface bone mapped to non-existent bone " <> showT (unBoneId tBid))) + Just _ -> Right () + + -- Check all joints of K are mapped to valid target joints and preserve incidence + forM_ kJoints $ \j -> do + case Map.lookup (jointId j) jMap of + Nothing -> + Left (InvalidRuleMorphism (name <> ": interface joint " <> showT (unJointId (jointId j)) <> " not mapped")) + Just tJid -> + case lookupJoint tJid target of + Nothing -> + Left (InvalidRuleMorphism (name <> ": interface joint mapped to non-existent joint " <> showT (unJointId tJid))) + Just tJoint -> do + let expectedSrc = Map.lookup (jointSource j) bMap + expectedDst = Map.lookup (jointTarget j) bMap + if Just (jointSource tJoint) == expectedSrc && Just (jointTarget tJoint) == expectedDst + then Right () + else Left (InvalidRuleMorphism (name <> ": joint morphism does not preserve connectivity")) + + -- Check monomorphism (injectivity) + let bVals = Map.elems bMap + jVals = Map.elems jMap + unless (Map.size bMap == Set.size (Set.fromList bVals)) $ + Left (InvalidRuleMorphism (name <> ": bone embedding is not injective")) + unless (Map.size jMap == Set.size (Set.fromList jVals)) $ + Left (InvalidRuleMorphism (name <> ": joint embedding is not injective")) + +-------------------------------------------------------------------------------- +-- Gluing Condition Verification +-------------------------------------------------------------------------------- + +-- | Validate the adhesive category gluing conditions for match @m : L -> G@. +-- +-- The gluing condition guarantees that the first pushout complement (deletion) +-- exists and produces a sound context graph: +-- +-- 1. __Dangling Condition:__ No joint in @G \setminus m(L)@ is incident to a bone in @m(L \setminus K)@. +-- 2. __Identification Condition:__ For distinct items @x /= y@ in @L@, @m(x) == m(y)@ only if +-- both @x@ and @y@ are in @l(K)@. +validateGluingCondition :: ProductionRule a -> GraphMatch -> Skeleton a -> Either RewritingError () +validateGluingCondition rule match host = do + validateRule rule + + let lBones = allBonesWithId (ruleLeft rule) + lJoints = allJoints (ruleLeft rule) + bMatch = matchBones match + jMatch = matchJoints match + + -- Check all bones in L are mapped to existing host bones + forM_ lBones $ \b -> do + case Map.lookup (boneId b) bMatch of + Nothing -> + Left (MatchNotFound ("Bone " <> showT (unBoneId (boneId b)) <> " of L not mapped in host match")) + Just gBid -> + case lookupBone gBid host of + Nothing -> + Left (MatchNotFound ("Bone " <> showT (unBoneId gBid) <> " out of bounds in host graph")) + Just _ -> Right () + + -- Check all joints in L are mapped to existing host joints and preserve connectivity + forM_ lJoints $ \j -> do + case Map.lookup (jointId j) jMatch of + Nothing -> + Left (MatchNotFound ("Joint " <> showT (unJointId (jointId j)) <> " of L not mapped in host match")) + Just gJid -> + case lookupJoint gJid host of + Nothing -> + Left (MatchNotFound ("Joint " <> showT (unJointId gJid) <> " out of bounds in host graph")) + Just gJoint -> do + let expectedSrc = Map.lookup (jointSource j) bMatch + expectedDst = Map.lookup (jointTarget j) bMatch + if Just (jointSource gJoint) == expectedSrc && Just (jointTarget gJoint) == expectedDst + then Right () + else Left (InvalidRuleMorphism "Match joint does not preserve source/target bone connectivity") + + -- 1. Identification Condition Verification + let (l_joints, l_bones) = morphismL rule + kBoneImg = Set.fromList (Map.elems l_bones) + kJointImg = Set.fromList (Map.elems l_joints) + + -- Identification on bones + forM_ lBones $ \b1 -> do + forM_ lBones $ \b2 -> do + when (boneId b1 < boneId b2) $ do + case (Map.lookup (boneId b1) bMatch, Map.lookup (boneId b2) bMatch) of + (Just g1, Just g2) | g1 == g2 -> + unless (Set.member (boneId b1) kBoneImg && Set.member (boneId b2) kBoneImg) $ + Left (IdentificationConditionViolated + ("Match identifies distinct bones " <> showT (unBoneId (boneId b1)) <> " and " <> + showT (unBoneId (boneId b2)) <> " outside interface K")) + _ -> Right () + + -- Identification on joints + forM_ lJoints $ \j1 -> do + forM_ lJoints $ \j2 -> do + when (jointId j1 < jointId j2) $ do + case (Map.lookup (jointId j1) jMatch, Map.lookup (jointId j2) jMatch) of + (Just g1, Just g2) | g1 == g2 -> + unless (Set.member (jointId j1) kJointImg && Set.member (jointId j2) kJointImg) $ + Left (IdentificationConditionViolated + ("Match identifies distinct joints " <> showT (unJointId (jointId j1)) <> " and " <> + showT (unJointId (jointId j2)) <> " outside interface K")) + _ -> Right () + + -- 2. Dangling Condition Verification + let delBonesInL = [ boneId b | b <- lBones, not (Set.member (boneId b) kBoneImg) ] + delBonesInG = Set.fromList [ gId | bId <- delBonesInL, Just gId <- [Map.lookup bId bMatch] ] + matchedJointsG = Set.fromList (Map.elems jMatch) + externalJoints = [ j | j <- allJoints host, not (Set.member (jointId j) matchedJointsG) ] + + forM_ externalJoints $ \j -> do + if Set.member (jointSource j) delBonesInG || Set.member (jointTarget j) delBonesInG + then Left (DanglingConditionViolated + ("External joint " <> showT (unJointId (jointId j)) <> + " connects to deleted bone (source: " <> showT (unBoneId (jointSource j)) <> + ", target: " <> showT (unBoneId (jointTarget j)) <> ")")) + else Right () + +-------------------------------------------------------------------------------- +-- Matching +-------------------------------------------------------------------------------- + +-- | Search for all monomorphic (injective) subgraph embeddings @m : L -> G@. +-- +-- Matches bone payloads via 'Eq' and ensures that all joint connections and +-- edge orientations in @L@ correspond to distinct joints in @G@. +findMatches :: forall a. (Eq a) => ProductionRule a -> Skeleton a -> [GraphMatch] +findMatches rule host = + let lBones = allBonesWithId (ruleLeft rule) + lJoints = allJoints (ruleLeft rule) + gBones = allBonesWithId host + gJoints = allJoints host + + -- Injective search over bone assignments + matchBonesSearch :: [Bone a] -> Map BoneId BoneId -> Set BoneId -> [Map BoneId BoneId] + matchBonesSearch [] !acc !_usedG = [acc] + matchBonesSearch (Bone lBid lVal : rest) !acc !usedG = + let candidates = + [ boneId g + | g <- gBones + , not (Set.member (boneId g) usedG) + , bonePayload g == lVal + ] + in [ res + | c <- candidates + , res <- matchBonesSearch rest (Map.insert lBid c acc) (Set.insert c usedG) + ] + + -- Injective search over joint assignments given a valid bone assignment + matchJointsSearch :: [Joint] -> Map BoneId BoneId -> Map JointId JointId -> Set JointId -> [Map JointId JointId] + matchJointsSearch [] !_bMap !acc !_usedG = [acc] + matchJointsSearch (Joint lJid lSrc lDst : rest) !bMap !acc !usedG = + case (Map.lookup lSrc bMap, Map.lookup lDst bMap) of + (Just gSrc, Just gDst) -> + let candidates = + [ jointId j + | j <- gJoints + , not (Set.member (jointId j) usedG) + , jointSource j == gSrc + , jointTarget j == gDst + ] + in [ res + | c <- candidates + , res <- matchJointsSearch rest bMap (Map.insert lJid c acc) (Set.insert c usedG) + ] + _ -> [] + + in [ GraphMatch jMap bMap + | bMap <- matchBonesSearch lBones Map.empty Set.empty + , jMap <- matchJointsSearch lJoints bMap Map.empty Set.empty + ] + +-------------------------------------------------------------------------------- +-- Pushout Complement & Pushout Construction +-------------------------------------------------------------------------------- + +-- | Derive the first pushout complement context skeleton @D = G \setminus m(L \setminus K)@. +-- +-- Excises vertices and edges specified for deletion while validating the gluing condition. +-- Preserves contiguous bone indexing by monotonically re-indexing retained bones into +-- @[0 .. |V_D| - 1]@. +derivePushoutComplement :: ProductionRule a -> GraphMatch -> Skeleton a -> Either RewritingError (Skeleton a) +derivePushoutComplement rule match host = do + validateGluingCondition rule match host + + let (_, l_bones) = morphismL rule + (l_joints, _) = morphismL rule + kBoneImg = Set.fromList (Map.elems l_bones) + kJointImg = Set.fromList (Map.elems l_joints) + bMatch = matchBones match + jMatch = matchJoints match + + delBonesInL = [ boneId b | b <- allBonesWithId (ruleLeft rule), not (Set.member (boneId b) kBoneImg) ] + delBonesInG = Set.fromList [ gId | bId <- delBonesInL, Just gId <- [Map.lookup bId bMatch] ] + + delJointsInL = [ jointId j | j <- allJoints (ruleLeft rule), not (Set.member (jointId j) kJointImg) ] + delJointsInG = Set.fromList [ gId | jId <- delJointsInL, Just gId <- [Map.lookup jId jMatch] ] + + retainedBones = [ b | b <- allBonesWithId host, not (Set.member (boneId b) delBonesInG) ] + retainedJoints = [ j | j <- allJoints host, not (Set.member (jointId j) delJointsInG) ] + + -- Old BoneId in G -> New contiguous BoneId in D (0 .. length retainedBones - 1) + boneMapGtoD = Map.fromList (zipWith (\b i -> (boneId b, BoneId i)) retainedBones [0..]) + + -- Build D with contiguous OsteoSegments + let skel0 = emptySkeleton + skelWithBones = foldl' (\s b -> snd (insertBone (bonePayload b) s)) skel0 retainedBones + + -- Add retained joints with re-indexed source and target + foldM (\s j -> do + case (Map.lookup (jointSource j) boneMapGtoD, Map.lookup (jointTarget j) boneMapGtoD) of + (Just newSrc, Just newDst) -> + pure (snd (connectJoint newSrc newDst s)) + _ -> + Left (PushoutComplementFailed "Dangling edge endpoint encountered during complement derivation") + ) skelWithBones retainedJoints + +-- | Construct the second pushout skeleton @H = D \amalg_K R@. +-- +-- Glues the replacement pattern @R@ to the pushout complement context skeleton @D@ +-- along interface @K@. Appends newly synthesized bones and joints while maintaining +-- contiguous memory indexing and monotonic identifier allocation. +constructPushout :: ProductionRule a -> GraphMatch -> Skeleton a -> Either RewritingError (Skeleton a) +constructPushout rule match d = do + validateRule rule + + let (_, l_bones) = morphismL rule + kBoneImgL = Set.fromList (Map.elems l_bones) + bMatch = matchBones match + + -- Deleted bones from G + delBonesInL = [ boneId b | b <- allBonesWithId (ruleLeft rule), not (Set.member (boneId b) kBoneImgL) ] + delBonesInG = Set.fromList [ gId | bId <- delBonesInL, Just gId <- [Map.lookup bId bMatch] ] + + (r_joints, r_bones) = morphismR rule + + -- For each bone k in K: resolve its corresponding BoneId in D. + kToD_BoneList <- forM (allBonesWithId (ruleInterface rule)) $ \kB -> do + let kBid = boneId kB + case Map.lookup kBid l_bones of + Nothing -> + Left (InvalidRuleMorphism ("Interface bone " <> showT (unBoneId kBid) <> " not found in morphismL")) + Just lBid -> + case Map.lookup lBid bMatch of + Nothing -> + Left (InvalidRuleMorphism ("Pattern bone " <> showT (unBoneId lBid) <> " not found in match")) + Just gBid -> do + let deletedBefore = Set.size (Set.filter (< gBid) delBonesInG) + dBid = BoneId (unBoneId gBid - fromIntegral deletedBefore) + case lookupBone dBid d of + Nothing -> + Left (PushoutComplementFailed ("Interface bone mapped to out-of-bounds bone in D: " <> showT (unBoneId dBid))) + Just _ -> pure (kBid, dBid) + + let kToD_BoneMap = Map.fromList kToD_BoneList + + -- Map from BoneId in R to BoneId in H: + -- If rB is in range of r_bones: it corresponds to k in K, mapping to kToD_BoneMap(k). + -- If rB is not in range of r_bones: it is newly synthesized, appended to D. + let rBonesInK = Map.fromList [ (rBid, kBid) | (kBid, rBid) <- Map.toList r_bones ] + rAllBones = allBonesWithId (ruleRight rule) + (existingRBones, newRBones) = partition (\b -> Map.member (boneId b) rBonesInK) rAllBones + + existingMapList <- forM existingRBones $ \b -> do + let rBid = boneId b + case Map.lookup rBid rBonesInK of + Nothing -> Left (InvalidRuleMorphism "Internal error: existing bone missing in rBonesInK") + Just kBid -> + case Map.lookup kBid kToD_BoneMap of + Nothing -> Left (InvalidRuleMorphism "Interface bone missing in context mapping") + Just dBid -> pure (rBid, dBid) + + let initRBoneToH = Map.fromList existingMapList + + -- Insert new bones into d sequentially + let insertNewRBones (!currSkel, !currMap) [] = pure (currSkel, currMap) + insertNewRBones (!currSkel, !currMap) (b : rest) = do + let (newBid, nextSkel) = insertBone (bonePayload b) currSkel + nextMap = Map.insert (boneId b) newBid currMap + insertNewRBones (nextSkel, nextMap) rest + + (skelWithBones, rBoneToH) <- insertNewRBones (d, initRBoneToH) newRBones + + -- Now connect joints: + -- Joints in R that are in image of r_joints already exist in D. + -- Joints in R NOT in image of r_joints are newly synthesized in H! + let rJointImg = Set.fromList (Map.elems r_joints) + newRJoints = [ j | j <- allJoints (ruleRight rule), not (Set.member (jointId j) rJointImg) ] + + foldM (\s j -> do + case (Map.lookup (jointSource j) rBoneToH, Map.lookup (jointTarget j) rBoneToH) of + (Just srcH, Just dstH) -> + pure (snd (connectJoint srcH dstH s)) + _ -> + Left (PushoutComplementFailed "New joint in R connects to unmapped bone in H") + ) skelWithBones newRJoints + +-------------------------------------------------------------------------------- +-- End-to-End Rewriting +-------------------------------------------------------------------------------- + +-- | Execute an atomic Double-Pushout rewrite given an explicit match @m : L -> G@. +-- +-- Validates the gluing condition, derives the pushout complement @D@, and glues +-- the replacement @R@ to produce derived graph @H@. +applyRule :: ProductionRule a -> GraphMatch -> Skeleton a -> Either RewritingError (Skeleton a) +applyRule rule match host = do + validateGluingCondition rule match host + d <- derivePushoutComplement rule match host + constructPushout rule match d + +-- | Find the first monomorphic match in host graph @G@ and apply the production rule. +applyRuleFirstMatch :: (Eq a) => ProductionRule a -> Skeleton a -> Either RewritingError (Skeleton a) +applyRuleFirstMatch rule host = + case findMatches rule host of + [] -> Left (MatchNotFound ("No monomorphic match found for rule: " <> ruleName rule)) + (m : _) -> applyRule rule m host + +-------------------------------------------------------------------------------- +-- Helpers +-------------------------------------------------------------------------------- + +showT :: (Show a) => a -> Text +showT = pack . show diff --git a/src/Gachi/Core/Traversal.hs b/src/Gachi/Core/Traversal.hs new file mode 100644 --- /dev/null +++ b/src/Gachi/Core/Traversal.hs @@ -0,0 +1,622 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE ScopedTypeVariables #-} + +-- | Module: Gachi.Core.Traversal +-- Description: Lock-free concurrent graph traversal and snapshot isolation over osteological graphs +-- +-- Provides high-performance, wait-free concurrent traversal algorithms over skeletal +-- bone-and-joint graphs. Readers observe consistent topological snapshots without acquiring +-- global read/write locks, even while underlying joint states chatter or transition concurrently. +-- +-- See Note [Concurrent Skeletal Graph Traversal] [ref:note-concurrent-traversal]. +-- +-- = Architectural Invariants +-- +-- * **Zero Mutex Contention:** Multi-agent traversals never acquire OS mutexes or runtime +-- locks on graph nodes. +-- * **Wait-Free Snapshot Reads:** 'readJointSnapshot' performs a single atomic memory read +-- without spinning or stalling writer threads. +-- * **Deterministic Concurrency:** 'traverseSkeletonConcurrently' yields bone traversal +-- results that match pure sequential evaluation byte-for-byte. +-- * **Topological Soundness:** Path-finding queries ('findJointPathConcurrently') traverse +-- consistent skeletal frontiers under concurrent joint oscillation. +-- +-- = Worked Example +-- +-- >>> import Gachi.Core +-- >>> import Gachi.Core.Traversal +-- >>> let (b0, s0) = insertBone "femur" emptySkeleton +-- >>> let (b1, s1) = insertBone "tibia" s0 +-- >>> let (j0, s2) = connectJoint b0 b1 s1 +-- >>> skel <- initAtomicJoints s2 +-- >>> traverseSkeletonConcurrently skel (\b -> pure (bonePayload b)) +-- ["femur","tibia"] +-- >>> findJointPathConcurrently skel j0 j0 +-- Just [OsteoJoint {osteoJointId = JointId {unJointId = 0}, ...}] +module Gachi.Core.Traversal + ( -- * Traversal Configuration + TraversalConfig(..) + , TraversalDirection(..) + , defaultTraversalConfig + + -- * Snapshot Representations + , OsteoJoint(..) + , osteoJointToJoint + , SkeletalSnapshot(..) + , readJointSnapshot + , snapshotJointStates + , snapshotSkeleton + + -- * Concurrent Traversal Primitives + , traverseSkeletonConcurrently + , traverseSkeletonConcurrentlyWith + , foldBonesConcurrently + , foldBonesConcurrentlyWith + , foldMapBonesConcurrently + , foldMapBonesConcurrentlyWith + + -- * Concurrent Path Finding & Graph Walks + , findJointPathConcurrently + , findJointPathConcurrentlyWith + , findBonePathConcurrently + , findBonePathConcurrentlyWith + , traverseSkeletonBFS + , traverseSkeletonDFS + + -- * Error Conditions + , TraversalException(..) + ) where + +import Control.Concurrent (forkIO, newEmptyMVar, putMVar, takeMVar, tryTakeMVar) +import Control.Exception (Exception, SomeException, throwIO, try) +import Control.Monad (forM_) +import qualified Data.Map.Strict as Map +import Data.Maybe (fromMaybe) +import qualified Data.Primitive.SmallArray as SA +import qualified Data.Set as Set +import GHC.Generics (Generic) +import System.Timeout (timeout) + +import Gachi.Core.Atomic + ( JointState(..) + , readJointState + ) +import Gachi.Core + ( Bone(..) + , BoneId(..) + , Joint(..) + , JointId(..) + , Skeleton(..) + , allBonesWithId + , allJoints + , getAtomicJoint + , lookupBone + , lookupJoint + , totalBones + , unsafeLookupBone + ) + +{- Note [Concurrent Skeletal Graph Traversal] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +[tag:note-concurrent-traversal] +In high-throughput multi-agent simulation, robotic kinematics, and parallel AST transforms, +multiple autonomous agent threads concurrently query, navigate, and evaluate osteological +skeletal graphs. + +Traditional graph traversal under concurrent edge modification relies on global reader-writer +locks or coarse-grained mutexes. This induces: + 1. Lock Contention Bottlenecks: Parallel workers serialize on shared locks, collapsing throughput. + 2. Priority Inversion & Convoy Effects: Preempted reader threads stall high-priority writers. + 3. Livelock & Reader Starvation: Continuous write activity blocks read traversals indefinitely. + +The Gachi Traversal Engine solves this via a lock-free dual-layer architecture: + 1. Immutable Structural Topology: + The underlying skeletal graph ('Skeleton a')—consisting of contiguous 'OsteoSegment' + arrays of bones and joints—is referentially transparent and immutable. Graph structure + (nodes, directed joints, monotonic IDs) never undergoes in-place pointer mutation. + Autonomous agent workers read topological frontiers wait-free without locks. + + 2. Lock-Free Joint State Machine: + Dynamic lifecycle states (inert, chattering, synchronized, fused) are isolated inside + unboxed 64-bit atomic references ('AtomicJoint'). Reader agents read joint states + via single-instruction atomic loads ('readJointState'). Readers never block writers, + and writer CAS transitions never block or invalidate reader traversals. + + 3. Snapshot Isolation: + Traversals observe instantaneous snapshots ('OsteoJoint') along topological paths. + Even while joint states oscillate at high frequency under concurrent chattering, + the topological path remains valid, acyclic (where configured), and formally race-free. + + 4. Bounded Multi-Agent Concurrency: + Traversal workloads ('traverseSkeletonConcurrently', 'foldMapBonesConcurrently') + distribute bone sets across bounded worker threads via contiguous memory slice partitioning, + achieving optimal hardware L1/L2 cache prefetching with zero synchronization overhead + during traversal execution. +-} + +-------------------------------------------------------------------------------- +-- Traversal Configuration & Directions +-------------------------------------------------------------------------------- + +-- | Direction of skeletal edge exploration for graph walk routines. +data TraversalDirection + = Forward + -- ^ Follow directed joints from source bone to target bone. + | Reverse + -- ^ Follow directed joints from target bone to source bone. + | Bidirectional + -- ^ Follow joints in either orientation along shared bone attachments. + deriving stock (Eq, Ord, Show, Generic) + +-- | Configuration parameters controlling concurrent multi-agent graph traversals. +data TraversalConfig = TraversalConfig + { traversalConcurrency :: !Int + -- ^ Maximum number of worker threads to spawn for parallel traversal passes. + , traversalTimeoutMicros :: !(Maybe Int) + -- ^ Optional timeout in microseconds. If exceeded, traversal terminates. + , traversalDirection :: !TraversalDirection + -- ^ Direction of edge exploration for path-finding and graph walk routines. + } deriving stock (Eq, Show, Generic) + +-- | Default traversal configuration: 8 worker threads, no timeout, bidirectional search. +defaultTraversalConfig :: TraversalConfig +defaultTraversalConfig = TraversalConfig + { traversalConcurrency = 8 + , traversalTimeoutMicros = Nothing + , traversalDirection = Bidirectional + } + +-------------------------------------------------------------------------------- +-- Snapshot Representations +-------------------------------------------------------------------------------- + +-- | An osteological joint connection capturing its structural connectivity +-- and an instantaneous wait-free snapshot of its atomic lifecycle state. +-- +-- See Note [Concurrent Skeletal Graph Traversal] [ref:note-concurrent-traversal]. +data OsteoJoint = OsteoJoint + { osteoJointId :: !JointId + -- ^ Unique identifier for this skeletal joint. + , osteoJointSource :: !BoneId + -- ^ Originating bone handle. + , osteoJointTarget :: !BoneId + -- ^ Terminating bone handle. + , osteoJointState :: !JointState + -- ^ Instantaneous atomic lifecycle state observed during traversal. + } deriving stock (Eq, Ord, Show, Generic) + +-- | Project the pure structural 'Joint' from an 'OsteoJoint'. +osteoJointToJoint :: OsteoJoint -> Joint +osteoJointToJoint (OsteoJoint jid src dst _) = Joint jid src dst +{-# INLINE osteoJointToJoint #-} + +-- | Complete immutable snapshot of a skeleton with observed atomic joint states. +data SkeletalSnapshot a = SkeletalSnapshot + { snapshotBones :: ![Bone a] + -- ^ All bones in the skeleton paired with their identifiers. + , snapshotJoints :: ![OsteoJoint] + -- ^ All joints paired with their observed atomic states. + } deriving stock (Eq, Show, Generic) + +-- | Exception raised when concurrent traversals encounter unrecoverable failures. +data TraversalException + = TraversalTimeout !Int + -- ^ Traversal exceeded the deadline specified in 'traversalTimeoutMicros'. + | TraversalWorkerPanic !String + -- ^ A concurrent worker thread failed with an unhandled exception. + deriving stock (Eq, Show, Generic) + +instance Exception TraversalException + +-------------------------------------------------------------------------------- +-- Snapshot Reading Primitives +-- See Note [Concurrent Skeletal Graph Traversal] [ref:note-concurrent-traversal] +-------------------------------------------------------------------------------- + +-- | Wait-free snapshot read of a single joint's atomic state. +-- Returns 'Nothing' if the joint does not exist in the skeleton. +-- If the joint has no initialized atomic reference, defaults to 'JointInert'. +readJointSnapshot :: Skeleton a -> JointId -> IO (Maybe JointState) +readJointSnapshot skel jid = + case lookupJoint jid skel of + Nothing -> pure Nothing + Just _ -> + case getAtomicJoint jid skel of + Just aj -> do + !st <- readJointState aj + pure (Just st) + Nothing -> pure (Just JointInert) +{-# INLINE readJointSnapshot #-} + +-- | Read instantaneous snapshot states for all skeletal joints in the graph. +snapshotJointStates :: Skeleton a -> IO [OsteoJoint] +snapshotJointStates skel = + mapM (\j -> do + mSt <- readJointSnapshot skel (jointId j) + let !st = fromMaybe JointInert mSt + pure (OsteoJoint (jointId j) (jointSource j) (jointTarget j) st) + ) (allJoints skel) + +-- | Create a complete snapshot view of bones and atomic joint states. +snapshotSkeleton :: Skeleton a -> IO (SkeletalSnapshot a) +snapshotSkeleton skel = do + let bones = allBonesWithId skel + joints <- snapshotJointStates skel + pure (SkeletalSnapshot bones joints) + +-------------------------------------------------------------------------------- +-- Concurrent Traversal Primitives +-- See Note [Concurrent Skeletal Graph Traversal] [ref:note-concurrent-traversal] +-------------------------------------------------------------------------------- + +-- | Traverse all bones in a skeleton concurrently with default configuration. +traverseSkeletonConcurrently :: Skeleton a -> (Bone a -> IO b) -> IO [b] +traverseSkeletonConcurrently = traverseSkeletonConcurrentlyWith defaultTraversalConfig +{-# INLINE traverseSkeletonConcurrently #-} + +-- | Traverse all bones in a skeleton concurrently with custom 'TraversalConfig'. +-- +-- Divides bones into disjoint contiguous slices and evaluates them across a bounded +-- pool of concurrent worker threads. Results are assembled in strict monotonically +-- increasing index order, guaranteeing exact correspondence with pure sequential evaluation. +traverseSkeletonConcurrentlyWith + :: TraversalConfig + -> Skeleton a + -> (Bone a -> IO b) + -> IO [b] +traverseSkeletonConcurrentlyWith cfg skel f = do + let !microsOpt = traversalTimeoutMicros cfg + case microsOpt of + Nothing -> runTraverse + Just micros -> do + mRes <- timeout micros runTraverse + case mRes of + Just res -> pure res + Nothing -> throwIO (TraversalTimeout micros) + where + !n = totalBones skel + + runTraverse + | n == 0 = pure [] + | otherwise = do + let !wMax = max 1 (traversalConcurrency cfg) + !w = min wMax n + if w == 1 + then do + let bones = allBonesWithId skel + mapM f bones + else do + marr <- SA.newSmallArray n (error "Gachi.Core.Traversal: uninitialized element") + let !baseChunk = n `quot` w + !remainder = n `rem` w + computeSlices !k !start + | k >= w = [] + | otherwise = + let !len = baseChunk + if k < remainder then 1 else 0 + !end = start + len - 1 + in if len > 0 + then (start, end) : computeSlices (k + 1) (end + 1) + else [] + slices = computeSlices 0 0 + sliceCount = length slices + + doneMVar <- newEmptyMVar + errMVar <- newEmptyMVar + + forM_ slices \(start, end) -> forkIO do + res <- try (forM_ [start .. end] \i -> do + let !bid = BoneId (fromIntegral i) + !payload = unsafeLookupBone bid skel + !bone = Bone bid payload + !val <- f bone + SA.writeSmallArray marr i val + ) + case res of + Left (e :: SomeException) -> putMVar errMVar (show e) + Right () -> putMVar doneMVar () + + let waitWorkers 0 = pure () + waitWorkers remaining = do + mErr <- tryTakeMVar errMVar + case mErr of + Just errStr -> throwIO (TraversalWorkerPanic errStr) + Nothing -> do + takeMVar doneMVar + waitWorkers (remaining - 1) + + waitWorkers sliceCount + frozen <- SA.freezeSmallArray marr 0 n + pure [ SA.indexSmallArray frozen i | i <- [0 .. n - 1] ] + +-- | Fold over all bones in a skeleton with default configuration. +foldBonesConcurrently :: Skeleton a -> (b -> Bone a -> IO b) -> b -> IO b +foldBonesConcurrently = foldBonesConcurrentlyWith defaultTraversalConfig +{-# INLINE foldBonesConcurrently #-} + +-- | Fold over all bones in a skeleton with custom 'TraversalConfig'. +-- Respects timeout boundaries and guarantees deterministic sequential reduction order. +foldBonesConcurrentlyWith + :: TraversalConfig + -> Skeleton a + -> (b -> Bone a -> IO b) + -> b + -> IO b +foldBonesConcurrentlyWith cfg skel step z = do + let !microsOpt = traversalTimeoutMicros cfg + case microsOpt of + Nothing -> runFold + Just micros -> do + mRes <- timeout micros runFold + case mRes of + Just res -> pure res + Nothing -> throwIO (TraversalTimeout micros) + where + bones = allBonesWithId skel + runFold = foldlM' step z bones + where + foldlM' _ !acc [] = pure acc + foldlM' stp !acc (x:xs) = do + !acc' <- stp acc x + foldlM' stp acc' xs + +-- | Map bones to a Monoid concurrently across worker threads and combine with '<>'. +foldMapBonesConcurrently :: Monoid m => Skeleton a -> (Bone a -> IO m) -> IO m +foldMapBonesConcurrently = foldMapBonesConcurrentlyWith defaultTraversalConfig +{-# INLINE foldMapBonesConcurrently #-} + +-- | Map bones to a Monoid concurrently with custom 'TraversalConfig'. +foldMapBonesConcurrentlyWith + :: Monoid m + => TraversalConfig + -> Skeleton a + -> (Bone a -> IO m) + -> IO m +foldMapBonesConcurrentlyWith cfg skel f = do + results <- traverseSkeletonConcurrentlyWith cfg skel f + pure $! foldl' (<>) mempty results + +-------------------------------------------------------------------------------- +-- Pure Queue Abstraction (Zero Partial Functions) +-------------------------------------------------------------------------------- + +data Queue a = Q ![a] ![a] + +emptyQ :: Queue a +emptyQ = Q [] [] + +pushQ :: a -> Queue a -> Queue a +pushQ x (Q ins outs) = Q (x : ins) outs + +popQ :: Queue a -> Maybe (a, Queue a) +popQ (Q ins (x:outs)) = Just (x, Q ins outs) +popQ (Q [] []) = Nothing +popQ (Q ins []) = + case reverse ins of + [] -> Nothing + (y:ys) -> Just (y, Q [] ys) + +-------------------------------------------------------------------------------- +-- Path Finding & Graph Walk Routines +-- See Note [Concurrent Skeletal Graph Traversal] [ref:note-concurrent-traversal] +-------------------------------------------------------------------------------- + +-- | Find a path of connected joints between two 'JointId' endpoints concurrently. +-- +-- Each returned 'OsteoJoint' includes an instantaneous atomic snapshot of its +-- lifecycle state observed at the moment of traversal. +findJointPathConcurrently + :: Skeleton a + -> JointId + -> JointId + -> IO (Maybe [OsteoJoint]) +findJointPathConcurrently = findJointPathConcurrentlyWith defaultTraversalConfig +{-# INLINE findJointPathConcurrently #-} + +-- | Find a path of connected joints with custom 'TraversalConfig'. +findJointPathConcurrentlyWith + :: TraversalConfig + -> Skeleton a + -> JointId + -> JointId + -> IO (Maybe [OsteoJoint]) +findJointPathConcurrentlyWith cfg skel startJid endJid = do + let !microsOpt = traversalTimeoutMicros cfg + case microsOpt of + Nothing -> runSearch + Just micros -> do + mRes <- timeout micros runSearch + case mRes of + Just res -> pure res + Nothing -> pure Nothing + where + mStartJoint = lookupJoint startJid skel + mEndJoint = lookupJoint endJid skel + + runSearch = + case (mStartJoint, mEndJoint) of + (Nothing, _) -> pure Nothing + (_, Nothing) -> pure Nothing + (Just startJoint, Just _) + | startJid == endJid -> do + mSt <- readJointSnapshot skel startJid + let !st = fromMaybe JointInert mSt + pure (Just [OsteoJoint startJid (jointSource startJoint) (jointTarget startJoint) st]) + | otherwise -> do + let joints = allJoints skel + outMap = Map.fromListWith (++) [ (jointSource j, [j]) | j <- joints ] + inMap = Map.fromListWith (++) [ (jointTarget j, [j]) | j <- joints ] + incMap = Map.fromListWith (++) + ([ (jointSource j, [j]) | j <- joints ] ++ [ (jointTarget j, [j]) | j <- joints ]) + + getNeighbors curr = + let jid = jointId curr + candidates = case traversalDirection cfg of + Forward -> + Map.findWithDefault [] (jointTarget curr) outMap + Reverse -> + Map.findWithDefault [] (jointSource curr) inMap + Bidirectional -> + let sNeighbors = Map.findWithDefault [] (jointSource curr) incMap + tNeighbors = Map.findWithDefault [] (jointTarget curr) incMap + in sNeighbors ++ tNeighbors + in filter (\nxt -> jointId nxt /= jid) candidates + + bfsLoop !q !visited = + case popQ q of + Nothing -> pure Nothing + Just ((curr, path), restQ) + | jointId curr == endJid -> do + let fullPath = reverse (curr : path) + osteoPath <- mapM (\j -> do + mSt <- readJointSnapshot skel (jointId j) + let !st = fromMaybe JointInert mSt + pure (OsteoJoint (jointId j) (jointSource j) (jointTarget j) st) + ) fullPath + pure (Just osteoPath) + | otherwise -> + let neighbors = getNeighbors curr + unvisited = filter (\nxt -> not (Set.member (jointId nxt) visited)) neighbors + newVisited = foldl' (\s nxt -> Set.insert (jointId nxt) s) visited unvisited + newQ = foldl' (\qAcc nxt -> pushQ (nxt, curr : path) qAcc) restQ unvisited + in bfsLoop newQ newVisited + + initQ = pushQ (startJoint, []) emptyQ + initVisited = Set.singleton startJid + + bfsLoop initQ initVisited + +-- | Find a path of bones connecting 'startBid' to 'endBid' concurrently. +findBonePathConcurrently + :: Skeleton a + -> BoneId + -> BoneId + -> IO (Maybe [Bone a]) +findBonePathConcurrently = findBonePathConcurrentlyWith defaultTraversalConfig +{-# INLINE findBonePathConcurrently #-} + +-- | Find a path of bones with custom 'TraversalConfig'. +findBonePathConcurrentlyWith + :: TraversalConfig + -> Skeleton a + -> BoneId + -> BoneId + -> IO (Maybe [Bone a]) +findBonePathConcurrentlyWith cfg skel startBid endBid = do + let !microsOpt = traversalTimeoutMicros cfg + case microsOpt of + Nothing -> runSearch + Just micros -> do + mRes <- timeout micros runSearch + case mRes of + Just res -> pure res + Nothing -> pure Nothing + where + mStartBone = lookupBone startBid skel + mEndBone = lookupBone endBid skel + + runSearch = + case (mStartBone, mEndBone) of + (Nothing, _) -> pure Nothing + (_, Nothing) -> pure Nothing + (Just startPayload, Just _) + | startBid == endBid -> + pure (Just [Bone startBid startPayload]) + | otherwise -> do + let joints = allJoints skel + outMap = Map.fromListWith (++) [ (jointSource j, [jointTarget j]) | j <- joints ] + inMap = Map.fromListWith (++) [ (jointTarget j, [jointSource j]) | j <- joints ] + incMap = Map.fromListWith (++) + ([ (jointSource j, [jointTarget j]) | j <- joints ] ++ [ (jointTarget j, [jointSource j]) | j <- joints ]) + + getNeighbors currBid = + case traversalDirection cfg of + Forward -> Map.findWithDefault [] currBid outMap + Reverse -> Map.findWithDefault [] currBid inMap + Bidirectional -> Map.findWithDefault [] currBid incMap + + bfsLoop !q !visited = + case popQ q of + Nothing -> pure Nothing + Just ((currBid, path), restQ) + | currBid == endBid -> do + let fullBids = reverse (currBid : path) + mBones = mapM (\bid -> do + p <- lookupBone bid skel + pure (Bone bid p) + ) fullBids + pure mBones + | otherwise -> + let neighbors = getNeighbors currBid + unvisited = filter (\nxt -> not (Set.member nxt visited)) neighbors + newVisited = foldl' (flip Set.insert) visited unvisited + newQ = foldl' (\qAcc nxt -> pushQ (nxt, currBid : path) qAcc) restQ unvisited + in bfsLoop newQ newVisited + + initQ = pushQ (startBid, []) emptyQ + initVisited = Set.singleton startBid + + bfsLoop initQ initVisited + +-- | Perform a breadth-first search (BFS) walk of all reachable bones from a starting bone. +traverseSkeletonBFS :: Skeleton a -> BoneId -> IO [Bone a] +traverseSkeletonBFS skel startBid = + case lookupBone startBid skel of + Nothing -> pure [] + Just startPayload -> do + let joints = allJoints skel + incMap = Map.fromListWith (++) + ([ (jointSource j, [jointTarget j]) | j <- joints ] ++ [ (jointTarget j, [jointSource j]) | j <- joints ]) + + bfs !q !visited !acc = + case popQ q of + Nothing -> pure (reverse acc) + Just (currBid, restQ) -> + let neighbors = Map.findWithDefault [] currBid incMap + unvisited = filter (\nxt -> not (Set.member nxt visited)) neighbors + newVisited = foldl' (flip Set.insert) visited unvisited + newQ = foldl' (flip pushQ) restQ unvisited + mBone = case lookupBone currBid skel of + Just p -> [Bone currBid p] + Nothing -> [] + in bfs newQ newVisited (mBone ++ acc) + + initQ = pushQ startBid emptyQ + initVisited = Set.singleton startBid + initAcc = [Bone startBid startPayload] + + -- Pop initial root and expand + case popQ initQ of + Nothing -> pure [] + Just (rootBid, q0) -> + let nbrs = Map.findWithDefault [] rootBid incMap + unvisited = filter (\nxt -> not (Set.member nxt initVisited)) nbrs + v1 = foldl' (flip Set.insert) initVisited unvisited + q1 = foldl' (flip pushQ) q0 unvisited + in bfs q1 v1 initAcc + +-- | Perform a depth-first search (DFS) walk of all reachable bones from a starting bone. +traverseSkeletonDFS :: Skeleton a -> BoneId -> IO [Bone a] +traverseSkeletonDFS skel startBid = + case lookupBone startBid skel of + Nothing -> pure [] + Just _ -> do + let joints = allJoints skel + incMap = Map.fromListWith (++) + ([ (jointSource j, [jointTarget j]) | j <- joints ] ++ [ (jointTarget j, [jointSource j]) | j <- joints ]) + + dfs [] !_ !acc = pure (reverse acc) + dfs (currBid : stack) !visited !acc + | Set.member currBid visited = dfs stack visited acc + | otherwise = + let !newVisited = Set.insert currBid visited + neighbors = Map.findWithDefault [] currBid incMap + unvisited = filter (\nxt -> not (Set.member nxt newVisited)) neighbors + mBone = case lookupBone currBid skel of + Just p -> [Bone currBid p] + Nothing -> [] + in dfs (unvisited ++ stack) newVisited (mBone ++ acc) + + dfs [startBid] Set.empty [] diff --git a/src/Gachi/Osteology.hs b/src/Gachi/Osteology.hs new file mode 100644 --- /dev/null +++ b/src/Gachi/Osteology.hs @@ -0,0 +1,390 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE ScopedTypeVariables #-} + +-- | Module: Gachi.Osteology +-- Description: Contiguous primitive osteological memory layouts and zero-overhead arrays +-- +-- Implements contiguous primitive array structures ('OsteoSegment' and 'OsteoBytes') +-- for osteological node graphs, guaranteeing spatial locality, minimal GC pressure, +-- zero-allocation indexing, and zero-copy slicing. +-- +-- Inspired by the bone structure of the mythical /gashadokuro/ (がしゃどくろ), +-- osteological segments provide unyielding structural rigidity with cache-coherent +-- memory layouts. +-- +-- = When to Use This Module +-- +-- * **High-Throughput Node Graphs:** Constructing graph structures or ASTs where node traversal +-- must not incur pointer-indirection penalties. +-- * **Zero-Copy Slicing:** Extracting contiguous sub-graphs or sub-sequences without reallocating +-- underlying array buffers via 'sliceOsteo'. +-- * **GC Scavenge Elimination:** Storing millions of elements in flat contiguous blocks +-- ('OsteoSegment' and 'OsteoBytes') that present a minimal traversal footprint to the GHC garbage collector. +-- +-- = Worked Example +-- +-- >>> import Gachi.Osteology +-- >>> let seg0 = emptySegment +-- >>> let seg1 = appendOsteo "femur" (appendOsteo "cranium" seg0) +-- >>> indexOsteo 0 seg1 +-- Just "cranium" +-- >>> let Just sl = sliceOsteo 0 1 seg1 +-- >>> toListOsteo sl +-- ["cranium"] +module Gachi.Osteology + ( -- * Primitive Osteological Segment + OsteoSegment(..) + , emptySegment + , segmentCapacity + , segmentLength + , appendOsteo + , indexOsteo + , unsafeIndexOsteo + , sliceOsteo + , fromListOsteo + , toListOsteo + + -- * Unboxed Osteological Byte Storage + , OsteoBytes(..) + , emptyBytes + , bytesCapacity + , bytesLength + , indexByte + , unsafeIndexByte + , sliceBytes + , fromByteList + , toByteList + + -- * Unboxed Atomic Joint Storage + , module Gachi.Osteology.Atomic + ) where + +import Gachi.Osteology.Atomic + +import Control.Monad.ST (runST) +import qualified Data.Primitive.ByteArray as BA +import qualified Data.Primitive.SmallArray as SA +import Data.Word (Word8) + +{- Note [Osteological Contiguous Memory Layout] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +[tag:note-osteology-memory-layout] +In high-throughput AST transformations, skeletal graph synthesis, and compiler passes, +traditional boxed linked structures (trees of heap-allocated constructors) introduce +severe performance penalties: + 1. Excessive Heap Overhead: Each constructor node incurs a 2-word info table and + GC header, quadrupling memory consumption relative to payload. + 2. Pointer Indirection: Traversal entails non-sequential pointer chasing across the + GHC managed heap, defeating CPU hardware L1/L2 prefetchers and inducing TLB misses. + 3. Garbage Collector Pause Latency: A graph with 100,000 nodes introduces 100,000 + pointers that the GHC garbage collector must trace during minor scavenges. + +Osteological Memory Representation: +Gachi resolves these costs by packing nodes into contiguous 'OsteoSegment' unboxed structures: + + +--------------------------------------------------------------------------+ + | GHC Heap Object: OsteoSegment a | + | osteoArray ---> [ SmallArray# Header | Slot 0 | Slot 1 | ... | Slot N ]| + | osteoOffset ---> !Int (Slice start offset within SmallArray#) | + | osteoLength ---> !Int (Slice length in elements) | + +--------------------------------------------------------------------------+ + +Key Architectural Properties: + - Cache Coherence: Sequential element slots fit within 64-byte L1 cache lines + (8 word-sized pointers per cache line), maximizing burst prefetching. + - Zero-Allocation Indexing: Addressing reduces to a single integer addition + (@osteoOffset + idx@) followed by an unboxed array dereference (@indexSmallArray#@). + - GC Minimization: Flat arrays present a single card-marked memory object to the GHC + garbage collector rather than an interconnected web of individual heap closures. + +See also: + - Note [Zero-Copy Sub-Segment Slicing] [ref:note-zero-copy-slicing] + - Note [Geometric Capacity Expansion and Reallocation] [ref:note-geometric-capacity-expansion] +-} + +{- Note [Zero-Copy Sub-Segment Slicing] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +[tag:note-zero-copy-slicing] +Sub-graphs, bone chains, and spinal segments frequently require localized traversal +or regional extraction without perturbing the enclosing skeletal topology. In standard +functional collections (lists, sequences, vectors), slicing either creates an expensive +copy of the sub-array or introduces deep tree node rebalancing. + +In 'OsteoSegment', slicing is implemented as a pure, zero-allocation pointer window: + + Underlying Contiguous SmallArray#: + [ Slot 0 | Slot 1 | Slot 2 | Slot 3 | Slot 4 | Slot 5 | Slot 6 | Slot 7 ] + ^ ^ + |-- osteoOffset = 1 | + <-------------- osteoLength = 4 --->| + Active Window: [ Slot 1, Slot 2, Slot 3, Slot 4 ] + +When 'sliceOsteo' is invoked: + 1. Range Validation: Validates that @sliceOff >= 0@, @sliceLen >= 0@, and + @sliceOff + sliceLen <= osteoLength@ in O(1) time. + 2. Pointer Windowing: Constructs a new 'OsteoSegment' sharing the identical + underlying 'osteoArray' reference with updated offset: + @osteoOffset' = osteoOffset + sliceOff@ and @osteoLength' = sliceLen@. + 3. Allocation Freedom: Zero element copy occurs; only the 3-field record + envelope is allocated on the GHC young generation. +-} + +{- Note [Geometric Capacity Expansion and Reallocation] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +[tag:note-geometric-capacity-expansion] +Dynamic incremental bone insertion in 'appendOsteo' follows an amortized doubling +discipline modeled after high-performance dynamic arrays. + +Resizing Mechanics: + 1. Zero Offset Fast-Path: When a segment is un-sliced (@osteoOffset == 0@) and + active elements are fewer than total capacity (@osteoLength < capacity@), + 'appendOsteo' allocates a fresh mutable array of identical capacity via + 'thawSmallArray', writes the new element into @osteoLength@, and freezes + it in ST. + 2. Saturated Geometric Doubling: When capacity is reached or when appending to a + sliced sub-segment (@osteoOffset > 0@), a new capacity is computed: + @newCap = max 4 (max (len + 1) (len * 2))@. + The active elements from [@osteoOffset .. osteoOffset + osteoLength - 1@] + are copied into the new array at offset 0, followed by the appended element. + 3. Complexity Guarantees: An insertion sequence of N elements incurs O(N) total + memory allocations, yielding O(1) amortized insertion cost per node. +-} + +-- | A contiguous, immutable osteological memory segment storing elements of type @a@. +-- +-- Features an offset and length window into an underlying primitive 'SA.SmallArray', +-- enabling true $O(1)$ zero-copy sub-segment slicing without heap allocations. +-- +-- See Note [Osteological Contiguous Memory Layout] [ref:note-osteology-memory-layout] +-- and Note [Zero-Copy Sub-Segment Slicing] [ref:note-zero-copy-slicing]. +data OsteoSegment a = OsteoSegment + { osteoArray :: !(SA.SmallArray a) + -- ^ Underlying flat contiguous primitive array. + , osteoOffset :: !Int + -- ^ Starting offset index of this segment slice within 'osteoArray'. + , osteoLength :: !Int + -- ^ Number of active initialized elements within this segment slice. + } + +instance Show a => Show (OsteoSegment a) where + show seg = "OsteoSegment " ++ show (toListOsteo seg) + +instance Eq a => Eq (OsteoSegment a) where + seg1 == seg2 = + osteoLength seg1 == osteoLength seg2 && toListOsteo seg1 == toListOsteo seg2 + +instance Functor OsteoSegment where + fmap f (OsteoSegment arr off len) = runST $ do + marr <- SA.newSmallArray len (error "Gachi.Osteology.fmap: uninitialized element") + let fill !i + | i < len = do + let !val = SA.indexSmallArray arr (off + i) + SA.writeSmallArray marr i (f val) + fill (i + 1) + | otherwise = pure () + fill 0 + frozen <- SA.freezeSmallArray marr 0 len + pure (OsteoSegment frozen 0 len) + +instance Foldable OsteoSegment where + foldr f z (OsteoSegment arr off len) = go 0 + where + go !i + | i < len = f (SA.indexSmallArray arr (off + i)) (go (i + 1)) + | otherwise = z + {-# INLINE foldr #-} + + length = osteoLength + {-# INLINE length #-} + + null seg = osteoLength seg == 0 + {-# INLINE null #-} + +instance Traversable OsteoSegment where + traverse f seg = fromListOsteo <$> traverse f (toListOsteo seg) + +instance Semigroup (OsteoSegment a) where + seg1 <> seg2 = + let len1 = osteoLength seg1 + len2 = osteoLength seg2 + totalLen = len1 + len2 + in if totalLen == 0 + then emptySegment + else runST $ do + marr <- SA.newSmallArray totalLen (error "Gachi.Osteology.<>: uninitialized element") + SA.copySmallArray marr 0 (osteoArray seg1) (osteoOffset seg1) len1 + SA.copySmallArray marr len1 (osteoArray seg2) (osteoOffset seg2) len2 + frozen <- SA.freezeSmallArray marr 0 totalLen + pure (OsteoSegment frozen 0 totalLen) + +instance Monoid (OsteoSegment a) where + mempty = emptySegment + +-- | Construct an empty osteological segment with zero capacity and length. +emptySegment :: OsteoSegment a +emptySegment = OsteoSegment + { osteoArray = SA.smallArrayFromList [] + , osteoOffset = 0 + , osteoLength = 0 + } + +-- | Total storage capacity allocated within the underlying contiguous array +-- from the current offset point. +segmentCapacity :: OsteoSegment a -> Int +segmentCapacity (OsteoSegment arr off _) = SA.sizeofSmallArray arr - off + +-- | Number of populated elements within this segment. +-- +-- Time complexity: @O(1)@. +segmentLength :: OsteoSegment a -> Int +segmentLength = osteoLength + +-- | Append an element to an 'OsteoSegment', allocating a geometrically resized +-- contiguous array if current capacity is exceeded. +-- +-- Time complexity: @O(1)@ amortized. +-- +-- See Note [Geometric Capacity Expansion and Reallocation] [ref:note-geometric-capacity-expansion]. +appendOsteo :: a -> OsteoSegment a -> OsteoSegment a +appendOsteo !val (OsteoSegment arr off len) = + let cap = SA.sizeofSmallArray arr + in if off == 0 && len < cap + then runST $ do + marr <- SA.thawSmallArray arr 0 cap + SA.writeSmallArray marr len val + frozen <- SA.freezeSmallArray marr 0 cap + pure (OsteoSegment frozen 0 (len + 1)) + else runST $ do + let newCap = max 4 (max (len + 1) (len * 2)) + marr <- SA.newSmallArray newCap val + SA.copySmallArray marr 0 arr off len + SA.writeSmallArray marr len val + frozen <- SA.freezeSmallArray marr 0 newCap + pure (OsteoSegment frozen 0 (len + 1)) + +-- | Retrieve an element at a specified contiguous index with bounds checking. +-- Returns 'Nothing' if the index is out of bounds. +-- +-- Time complexity: @O(1)@. +-- +-- See Note [Osteological Contiguous Memory Layout] [ref:note-osteology-memory-layout]. +indexOsteo :: Int -> OsteoSegment a -> Maybe a +indexOsteo idx (OsteoSegment arr off len) + | idx >= 0 && idx < len = Just (SA.indexSmallArray arr (off + idx)) + | otherwise = Nothing +{-# INLINE indexOsteo #-} + +-- | Retrieve an element at a specified contiguous index without bounds checking. +-- Precondition: @0 <= idx < segmentLength seg@. +-- +-- Time complexity: @O(1)@ zero-allocation. +-- +-- See Note [Osteological Contiguous Memory Layout] [ref:note-osteology-memory-layout]. +unsafeIndexOsteo :: Int -> OsteoSegment a -> a +unsafeIndexOsteo idx (OsteoSegment arr off _) = + SA.indexSmallArray arr (off + idx) +{-# INLINE unsafeIndexOsteo #-} + +-- | Create a zero-copy sub-segment slice referencing the sub-range [@offset .. offset + length - 1@]. +-- Returns 'Nothing' if the slice range extends beyond the segment bounds. +-- +-- Time complexity: @O(1)@ with zero heap array allocation. +-- +-- See Note [Zero-Copy Sub-Segment Slicing] [ref:note-zero-copy-slicing]. +sliceOsteo :: Int -> Int -> OsteoSegment a -> Maybe (OsteoSegment a) +sliceOsteo sliceOff sliceLen (OsteoSegment arr off len) + | sliceOff >= 0 && sliceLen >= 0 && sliceOff + sliceLen <= len = + Just (OsteoSegment arr (off + sliceOff) sliceLen) + | otherwise = Nothing +{-# INLINE sliceOsteo #-} + +-- | Construct an 'OsteoSegment' from a standard Haskell list. +fromListOsteo :: [a] -> OsteoSegment a +fromListOsteo xs = + let arr = SA.smallArrayFromList xs + in OsteoSegment arr 0 (SA.sizeofSmallArray arr) + +-- | Convert an 'OsteoSegment' back into a standard Haskell list. +toListOsteo :: OsteoSegment a -> [a] +toListOsteo (OsteoSegment arr off len) = + [ SA.indexSmallArray arr (off + i) | i <- [0 .. len - 1] ] + +-------------------------------------------------------------------------------- +-- Unboxed Osteological Byte Storage +-------------------------------------------------------------------------------- + +-- | A contiguous, unboxed byte storage segment backed by 'BA.ByteArray'. +-- +-- Used for storing raw numeric bone representations, serialized coordinate tables, +-- and binary cryptographic signatures with spatial cache locality. +data OsteoBytes = OsteoBytes + { osteoByteArray :: !BA.ByteArray + -- ^ Underlying flat contiguous primitive byte array. + , osteoByteOffset :: !Int + -- ^ Starting byte offset index within 'osteoByteArray'. + , osteoByteLength :: !Int + -- ^ Number of active initialized bytes within this slice. + } + +instance Show OsteoBytes where + show bs = "OsteoBytes " ++ show (toByteList bs) + +instance Eq OsteoBytes where + b1 == b2 = + osteoByteLength b1 == osteoByteLength b2 && toByteList b1 == toByteList b2 + +-- | Construct an empty unboxed osteological byte storage with zero bytes. +emptyBytes :: OsteoBytes +emptyBytes = OsteoBytes + { osteoByteArray = runST (BA.newByteArray 0 >>= BA.unsafeFreezeByteArray) + , osteoByteOffset = 0 + , osteoByteLength = 0 + } + +-- | Total storage capacity allocated within the underlying byte array +-- from the current offset point. +bytesCapacity :: OsteoBytes -> Int +bytesCapacity (OsteoBytes arr off _) = BA.sizeofByteArray arr - off + +-- | Number of populated bytes within this segment. +bytesLength :: OsteoBytes -> Int +bytesLength = osteoByteLength + +-- | Retrieve a byte at a specified index with bounds checking. +indexByte :: Int -> OsteoBytes -> Maybe Word8 +indexByte idx (OsteoBytes arr off len) + | idx >= 0 && idx < len = Just (BA.indexByteArray arr (off + idx)) + | otherwise = Nothing +{-# INLINE indexByte #-} + +-- | Retrieve a byte at a specified index without bounds checking. +unsafeIndexByte :: Int -> OsteoBytes -> Word8 +unsafeIndexByte idx (OsteoBytes arr off _) = + BA.indexByteArray arr (off + idx) +{-# INLINE unsafeIndexByte #-} + +-- | Create a zero-copy sub-segment slice referencing the byte sub-range. +sliceBytes :: Int -> Int -> OsteoBytes -> Maybe OsteoBytes +sliceBytes sliceOff sliceLen (OsteoBytes arr off len) + | sliceOff >= 0 && sliceLen >= 0 && sliceOff + sliceLen <= len = + Just (OsteoBytes arr (off + sliceOff) sliceLen) + | otherwise = Nothing +{-# INLINE sliceBytes #-} + +-- | Construct an 'OsteoBytes' from a list of 'Word8' bytes. +fromByteList :: [Word8] -> OsteoBytes +fromByteList xs = runST $ do + let len = length xs + marr <- BA.newByteArray len + let fill !i (b:bs) = do + BA.writeByteArray marr i b + fill (i + 1) bs + fill _ [] = pure () + fill 0 xs + frozen <- BA.unsafeFreezeByteArray marr + pure (OsteoBytes frozen 0 len) + +-- | Convert an 'OsteoBytes' into a list of 'Word8' bytes. +toByteList :: OsteoBytes -> [Word8] +toByteList (OsteoBytes arr off len) = + [ BA.indexByteArray arr (off + i) | i <- [0 .. len - 1] ] diff --git a/src/Gachi/Osteology/Atomic.hs b/src/Gachi/Osteology/Atomic.hs new file mode 100644 --- /dev/null +++ b/src/Gachi/Osteology/Atomic.hs @@ -0,0 +1,243 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE UnboxedTuples #-} + +-- | Module: Gachi.Osteology.Atomic +-- Description: Unboxed atomic state references and tagged word layouts for skeletal joints +-- +-- Provides low-level, high-performance unboxed atomic memory primitives for representing +-- skeletal joint lifecycles without heap overhead or global locks. +-- +-- Each joint is backed by an unboxed 64-bit tagged word stored inside a contiguous primitive +-- byte array ('AtomicJoint'), enabling native CPU compare-and-swap (CAS) instructions. +-- +-- = Joint Lifecycle +-- +-- Joint lifecycles progress through four canonical phases: +-- +-- 1. 'JointInert' (Tag @00_2@): Stationary joint awaiting excitation. Zero-initialized memory +-- (@0x0000000000000000@) naturally decodes to this state. +-- 2. 'JointChattering' (Tag @01_2@): High-frequency lock-free oscillation carrying a 62-bit +-- chattering generation or sequence counter. +-- 3. 'JointSynchronized' (Tag @10_2@): Harmonically locked joint carrying a 62-bit phase +-- or frequency identifier. +-- 4. 'JointFused' (Tag @11_2@): Immutable terminal joint state resisting further mutation. +-- +-- = Memory Layout (64-bit Tagged Word) +-- +-- @ +-- 63 62 61 0 +-- +-----+---------------------------------------------------------------+ +-- | Tag | Payload (62-bit generation / frequency / phase word) | +-- +-----+---------------------------------------------------------------+ +-- 00: JointInert +-- 01: JointChattering +-- 10: JointSynchronized +-- 11: JointFused +-- @ +module Gachi.Osteology.Atomic + ( -- * Joint Lifecycle State + JointState(..) + , isJointInert + , isJointChattering + , isJointSynchronized + , isJointFused + + -- * Tagged Word Codecs + , encodeJointState + , decodeJointState + , tagMask + , payloadMask + + -- * Unboxed Atomic Joint Reference + , AtomicJoint(..) + , newAtomicJoint + , newAtomicJointRaw + , readAtomicJointRaw + , writeAtomicJointRaw + , casAtomicJointRaw + , casAtomicJointRawOld + ) where + +import Control.Monad.Primitive (RealWorld) +import Data.Bits (shiftL, shiftR, (.&.), (.|.)) +import qualified Data.Primitive.ByteArray as BA +import Data.Word (Word64) +import GHC.Exts + ( Int(..) + , atomicReadIntArray# + , atomicWriteIntArray# + , casIntArray# + , isTrue# + , (==#) + ) +import GHC.Generics (Generic) +import GHC.IO (IO(..)) + +-------------------------------------------------------------------------------- +-- Joint Lifecycle State +-------------------------------------------------------------------------------- + +-- | Algebraic data type representing the lifecycle state of a skeletal joint. +-- +-- Encoded compactly into a single 64-bit word using the top 2 bits as discriminator tag +-- and the bottom 62 bits as the numeric payload. +data JointState + = JointInert + -- ^ Stationary joint awaiting signal excitation (Tag @00_2@). + | JointChattering !Word64 + -- ^ High-frequency lock-free oscillation under multi-agent signal propagation (Tag @01_2@). + | JointSynchronized !Word64 + -- ^ Harmonically locked joint in phase equilibrium (Tag @10_2@). + | JointFused + -- ^ Immutable terminal joint state (Tag @11_2@). + deriving stock (Eq, Ord, Show, Generic) + +-- | Query whether a 'JointState' is 'JointInert'. +isJointInert :: JointState -> Bool +isJointInert JointInert = True +isJointInert _ = False +{-# INLINE isJointInert #-} + +-- | Query whether a 'JointState' is 'JointChattering'. +isJointChattering :: JointState -> Bool +isJointChattering (JointChattering _) = True +isJointChattering _ = False +{-# INLINE isJointChattering #-} + +-- | Query whether a 'JointState' is 'JointSynchronized'. +isJointSynchronized :: JointState -> Bool +isJointSynchronized (JointSynchronized _) = True +isJointSynchronized _ = False +{-# INLINE isJointSynchronized #-} + +-- | Query whether a 'JointState' is 'JointFused'. +isJointFused :: JointState -> Bool +isJointFused JointFused = True +isJointFused _ = False +{-# INLINE isJointFused #-} + +-------------------------------------------------------------------------------- +-- Tagged Word Codecs +-------------------------------------------------------------------------------- + +-- | Bitmask selecting the upper 2 tag bits of a 64-bit word (@0xC000000000000000@). +tagMask :: Word64 +tagMask = 0xC000000000000000 +{-# INLINE tagMask #-} + +-- | Bitmask selecting the lower 62 payload bits of a 64-bit word (@0x3FFFFFFFFFFFFFFF@). +payloadMask :: Word64 +payloadMask = 0x3FFFFFFFFFFFFFFF +{-# INLINE payloadMask #-} + +-- | Encode a 'JointState' into an unboxed 64-bit tagged word. +-- +-- * 'JointInert': Encoded as @0x0000000000000000@. +-- * 'JointChattering': Encoded with tag @01_2@ in bits 63..62 and masked payload in bits 61..0. +-- * 'JointSynchronized': Encoded with tag @10_2@ in bits 63..62 and masked payload in bits 61..0. +-- * 'JointFused': Encoded with tag @11_2@ in bits 63..62 (@0xC000000000000000@). +encodeJointState :: JointState -> Word64 +encodeJointState JointInert = 0 +encodeJointState (JointChattering !payload) = + (1 `shiftL` 62) .|. (payload .&. payloadMask) +encodeJointState (JointSynchronized !payload) = + (2 `shiftL` 62) .|. (payload .&. payloadMask) +encodeJointState JointFused = 3 `shiftL` 62 +{-# INLINE encodeJointState #-} + +-- | Decode an unboxed 64-bit tagged word back into its corresponding 'JointState'. +-- +-- Discriminates on the high 2 bits (63..62): +-- * @00_2@ -> 'JointInert' +-- * @01_2@ -> 'JointChattering' with masked 62-bit payload +-- * @10_2@ -> 'JointSynchronized' with masked 62-bit payload +-- * @11_2@ -> 'JointFused' +decodeJointState :: Word64 -> JointState +decodeJointState !w = + let !tag = w `shiftR` 62 + !payload = w .&. payloadMask + in case tag of + 0 -> JointInert + 1 -> JointChattering payload + 2 -> JointSynchronized payload + 3 -> JointFused + _ -> JointInert +{-# INLINE decodeJointState #-} + +-------------------------------------------------------------------------------- +-- Unboxed Atomic Joint Reference +-------------------------------------------------------------------------------- + +-- | An unboxed atomic reference storing a tagged joint state word. +-- +-- Backed by an 8-byte contiguous 'BA.MutableByteArray' to permit direct hardware-level +-- atomic compare-and-swap ('casIntArray#') instructions and wait-free memory reads +-- without acquiring OS mutexes or runtime reader-writer locks. +newtype AtomicJoint = AtomicJoint (BA.MutableByteArray RealWorld) + +instance Eq AtomicJoint where + AtomicJoint mba1 == AtomicJoint mba2 = BA.sameMutableByteArray mba1 mba2 + +instance Show AtomicJoint where + show _ = "" + +-- | Allocate a new 'AtomicJoint' initialized to the given raw 64-bit word. +newAtomicJointRaw :: Word64 -> IO AtomicJoint +newAtomicJointRaw !val = do + mba <- BA.newByteArray 8 + let !joint = AtomicJoint mba + writeAtomicJointRaw joint val + pure joint + +-- | Allocate a new 'AtomicJoint' initialized to the given 'JointState'. +newAtomicJoint :: JointState -> IO AtomicJoint +newAtomicJoint !st = newAtomicJointRaw (encodeJointState st) + +-- | Wait-free atomic memory read of the raw 64-bit tagged word. +readAtomicJointRaw :: AtomicJoint -> IO Word64 +readAtomicJointRaw (AtomicJoint mba) = IO $ \s0# -> + let !(BA.MutableByteArray mba#) = mba + in case atomicReadIntArray# mba# 0# s0# of + (# s1#, val# #) -> + (# s1#, fromIntegral (I# val#) #) +{-# INLINE readAtomicJointRaw #-} + +-- | Atomic memory write of the raw 64-bit tagged word. +writeAtomicJointRaw :: AtomicJoint -> Word64 -> IO () +writeAtomicJointRaw (AtomicJoint mba) !val = IO $ \s0# -> + let !(I# v#) = fromIntegral val + !(BA.MutableByteArray mba#) = mba + in case atomicWriteIntArray# mba# 0# v# s0# of + s1# -> (# s1#, () #) +{-# INLINE writeAtomicJointRaw #-} + +-- | Hardware compare-and-swap (CAS) operation on the raw 64-bit tagged word. +-- +-- Atomically compares the current word at slot 0 with @expected@. If they match, +-- writes @newVal@ and returns 'True'. If they do not match, leaves memory untouched +-- and returns 'False'. +casAtomicJointRaw :: AtomicJoint -> Word64 -> Word64 -> IO Bool +casAtomicJointRaw (AtomicJoint mba) !expected !newVal = IO $ \s0# -> + let !(I# exp#) = fromIntegral expected + !(I# new#) = fromIntegral newVal + !(BA.MutableByteArray mba#) = mba + in case casIntArray# mba# 0# exp# new# s0# of + (# s1#, old# #) -> + (# s1#, isTrue# (old# ==# exp#) #) +{-# INLINE casAtomicJointRaw #-} + +-- | Hardware compare-and-swap returning both success status and the observed previous word. +casAtomicJointRawOld :: AtomicJoint -> Word64 -> Word64 -> IO (Bool, Word64) +casAtomicJointRawOld (AtomicJoint mba) !expected !newVal = IO $ \s0# -> + let !(I# exp#) = fromIntegral expected + !(I# new#) = fromIntegral newVal + !(BA.MutableByteArray mba#) = mba + in case casIntArray# mba# 0# exp# new# s0# of + (# s1#, old# #) -> + let !oldW = fromIntegral (I# old#) + !succCAS = isTrue# (old# ==# exp#) + in (# s1#, (succCAS, oldW) #) +{-# INLINE casAtomicJointRawOld #-} diff --git a/src/Gachi/Osteology/Polytropos.hs b/src/Gachi/Osteology/Polytropos.hs new file mode 100644 --- /dev/null +++ b/src/Gachi/Osteology/Polytropos.hs @@ -0,0 +1,266 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} + +-- | Module: Gachi.Osteology.Polytropos +-- Description: Zero-cost coercions and algebraic isomorphisms between OsteoSegment and Polytropos Rep +-- +-- Establishes zero-cost memory coercions and bidirectional algebraic isomorphisms +-- between 'gachi-core' contiguous osteological arrays ('OsteoSegment') and 'polytropos-core' +-- flat structural runtime representations ('Rep': constructor tag plus flat 'SA.SmallArray'). +-- +-- See Note [Zero-Cost Polytropos Rep Coercions] [ref:note-osteo-polytropos-coercion]. +module Gachi.Osteology.Polytropos + ( -- * Coercion Primitives + segmentToRep + , repToSegment + , checkedSegmentToRep + , checkedRepToSegment + , validateSegment + + -- * Buffer Sharing Diagnostics + , sameSmallArray + , sharesArrayBuffer + + -- * Error Diagnostics + , CoercionError(..) + + -- * Record & Bone Payload Codecs + , bonePayloadToRecord + , recordToBonePayload + , recordToBonePayloadWithId + , segmentToRecord + , recordToSegment + , BoneRecord + , BoneRecordCodec(..) + , boneToRecordVia + , recordToBoneVia + ) where + +import Data.Functor.Identity (Identity(..)) +import qualified Data.Primitive.SmallArray as SA +import GHC.Exts (Any, isTrue#, sameSmallArray#, unsafeCoerce#) + +import Polytropos (Record) +import Polytropos.Core + ( Rep(..) + , Row + , RowRep(..) + ) + +import Gachi.Core (Bone(..), BoneId(..)) +import Gachi.Osteology (OsteoSegment(..)) + +{- Note [Zero-Cost Polytropos Rep Coercions] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +[tag:note-osteo-polytropos-coercion] +In high-throughput osteological graph processing and generic transformation pipelines, +bridging data between domain representations (contiguous osteological arrays like +'OsteoSegment') and runtime row abstractions (such as Polytropos 'Rep' and 'Record') +must not incur pointer indirection overhead, auxiliary heap allocations, or +intermediate garbage collector pressure. + +1. Memory Substrate Parity: + Both 'OsteoSegment' and Polytropos 'Rep' share identical underlying primitive + memory substrates backed by GHC's unlifted 'SmallArray#' primitive: + - 'OsteoSegment a': + osteoArray :: !(SmallArray a) + osteoOffset :: !Int + osteoLength :: !Int + - 'Rep f a': + {-# UNPACK #-} !Word (constructor tag / discriminant) + !(SmallArray (f Any)) (contiguous flat array of payload slots) + +2. Zero Linked-List Detour: + Traditional Haskell generic conversions (such as standard GHC.Generics or Scrap + Your Boilerplate) map products and sums through intermediate heap-allocated lists + ('[a]') or nested binary trees ('(:*:)'), inducing heavy nursery allocation churn + and frequent cache misses. Polytropos zero-cost coercions bypass intermediate + representations entirely, mapping between contiguous array slices directly via + single-memcpy or O(1) array re-interpretation. + +3. Fast-Path Zero-Allocation Re-Interpretation: + When an 'OsteoSegment' spans the entirety of its underlying primitive buffer + (i.e., 'osteoOffset == 0' and 'osteoLength == sizeofSmallArray osteoArray'), + 'segmentToRep' performs a zero-allocation coercion: the underlying 'SmallArray#' + is passed through directly to 'Rep' without allocating any auxiliary array buffers. + Conversely, when the segment represents a sliced sub-window (offset > 0 or + length < capacity), 'segmentToRep' performs an optimal single slice clone via + 'cloneSmallArray', which compiles down to primitive GHC SIMD-accelerated memory + copying without traversing intermediate pointers. + +4. Formal Bidirectional Algebraic Isomorphism: + For any canonically sized segment (offset 0, length equal to array capacity), + the coercion primitives satisfy strict roundtrip algebraic isomorphisms: + repToSegment . uncurry segmentToRep = id + uncurry segmentToRep . repToSegment = id + Similarly, extensible record wrappers satisfy: + bonePayloadToRecord . recordToBonePayload = id +-} + +-- | An error occurring during osteological segment or representation coercion. +data CoercionError + = SegmentOutOfBounds !Int !Int + -- ^ The segment offset or length exceeds the underlying array bounds. + -- Carries (actual bound index requested, underlying array capacity). + | TagMismatch !Word !Word + -- ^ Constructor tag mismatch between expected discriminant and actual representation. + -- Carries (expected tag, actual tag). + deriving (Eq, Show) + +-- | Check pointer identity between two primitive 'SA.SmallArray' allocations. +-- +-- Returns 'True' if and only if both arrays reference the exact same memory buffer. +-- +-- See Note [Zero-Cost Polytropos Rep Coercions] [ref:note-osteo-polytropos-coercion]. +sameSmallArray :: SA.SmallArray a -> SA.SmallArray b -> Bool +sameSmallArray (SA.SmallArray a#) (SA.SmallArray b#) = + isTrue# (sameSmallArray# a# (unsafeCoerce# b#)) +{-# INLINE sameSmallArray #-} + +-- | Check whether an 'OsteoSegment' and a Polytropos 'Rep' share the identical underlying array buffer. +-- +-- Used to verify that zero-allocation fast-path coercions occurred without buffer reallocation. +-- +-- See Note [Zero-Cost Polytropos Rep Coercions] [ref:note-osteo-polytropos-coercion]. +sharesArrayBuffer :: OsteoSegment (f Any) -> Rep f a -> Bool +sharesArrayBuffer (OsteoSegment arr _ _) (Rep _ repArr) = sameSmallArray arr repArr +{-# INLINE sharesArrayBuffer #-} + +-- | Validate that an 'OsteoSegment' adheres to the physical bounds of its underlying array. +-- +-- See Note [Zero-Cost Polytropos Rep Coercions] [ref:note-osteo-polytropos-coercion]. +validateSegment :: OsteoSegment a -> Either CoercionError () +validateSegment (OsteoSegment arr off len) + | off < 0 = Left (SegmentOutOfBounds off (SA.sizeofSmallArray arr)) + | len < 0 = Left (SegmentOutOfBounds len (SA.sizeofSmallArray arr)) + | off + len > SA.sizeofSmallArray arr = + Left (SegmentOutOfBounds (off + len) (SA.sizeofSmallArray arr)) + | otherwise = Right () +{-# INLINE validateSegment #-} + +-- | Coerce an 'OsteoSegment' of dynamically typed field values into a Polytropos 'Rep'. +-- +-- When the segment encompasses the entirety of the underlying array buffer +-- (@osteoOffset == 0@ and @osteoLength == sizeofSmallArray osteoArray@), this coercion +-- is strictly zero-cost: the underlying 'SA.SmallArray' is reused directly without +-- allocating a new array buffer. +-- +-- When the segment is a sliced sub-segment (@osteoOffset > 0@ or @osteoLength < capacity@), +-- an optimal single-memcpy slice copy ('SA.cloneSmallArray') is performed to package the +-- slice into a tightly-sized contiguous array buffer without traversing intermediate +-- linked lists. +-- +-- See Note [Zero-Cost Polytropos Rep Coercions] [ref:note-osteo-polytropos-coercion]. +segmentToRep :: Word -> OsteoSegment (f Any) -> Rep f a +segmentToRep !tag (OsteoSegment arr off len) + | off == 0 && len == SA.sizeofSmallArray arr = + Rep tag arr + | otherwise = + Rep tag (SA.cloneSmallArray arr off len) +{-# INLINE segmentToRep #-} + +-- | Coerce a Polytropos 'Rep' back into an 'OsteoSegment' paired with its constructor tag. +-- +-- Wraps the underlying 'SA.SmallArray' directly into an 'OsteoSegment' with offset 0 +-- and length equal to the array capacity, requiring zero element allocations. +-- +-- See Note [Zero-Cost Polytropos Rep Coercions] [ref:note-osteo-polytropos-coercion]. +repToSegment :: Rep f a -> (Word, OsteoSegment (f Any)) +repToSegment (Rep tag arr) = + (tag, OsteoSegment arr 0 (SA.sizeofSmallArray arr)) +{-# INLINE repToSegment #-} + +-- | Checked coercion from 'OsteoSegment' to Polytropos 'Rep' validating bounds. +-- +-- See Note [Zero-Cost Polytropos Rep Coercions] [ref:note-osteo-polytropos-coercion]. +checkedSegmentToRep :: Word -> OsteoSegment (f Any) -> Either CoercionError (Rep f a) +checkedSegmentToRep !tag !seg = do + validateSegment seg + Right (segmentToRep tag seg) +{-# INLINE checkedSegmentToRep #-} + +-- | Checked extraction from Polytropos 'Rep' asserting an expected constructor tag. +-- +-- See Note [Zero-Cost Polytropos Rep Coercions] [ref:note-osteo-polytropos-coercion]. +checkedRepToSegment :: Word -> Rep f a -> Either CoercionError (OsteoSegment (f Any)) +checkedRepToSegment !expectedTag rep@(Rep actualTag _) + | expectedTag /= actualTag = Left (TagMismatch expectedTag actualTag) + | otherwise = Right (snd (repToSegment rep)) +{-# INLINE checkedRepToSegment #-} + +-------------------------------------------------------------------------------- +-- Record & Bone Payload Codecs +-------------------------------------------------------------------------------- + +-- | Disambiguating type synonym for an osteological 'Bone' bearing an extensible Polytropos 'Record'. +type BoneRecord r = Bone (Record r) + +-- | Extract an extensible Polytropos 'Record' payload from an osteological 'Bone'. +-- +-- Operates at \(O(1)\) with zero intermediate allocation. +-- +-- See Note [Zero-Cost Polytropos Rep Coercions] [ref:note-osteo-polytropos-coercion]. +bonePayloadToRecord :: Bone (Record r) -> Record r +bonePayloadToRecord = bonePayload +{-# INLINE bonePayloadToRecord #-} + +-- | Wrap a Polytropos extensible 'Record' into an osteological 'Bone' with default identifier 0. +-- +-- Operates at \(O(1)\). +-- +-- See Note [Zero-Cost Polytropos Rep Coercions] [ref:note-osteo-polytropos-coercion]. +recordToBonePayload :: Record r -> Bone (Record r) +recordToBonePayload = Bone (BoneId 0) +{-# INLINE recordToBonePayload #-} + +-- | Wrap a Polytropos extensible 'Record' into an osteological 'Bone' with an explicit 'BoneId'. +-- +-- Operates at \(O(1)\). +-- +-- See Note [Zero-Cost Polytropos Rep Coercions] [ref:note-osteo-polytropos-coercion]. +recordToBonePayloadWithId :: BoneId -> Record r -> Bone (Record r) +recordToBonePayloadWithId = Bone +{-# INLINE recordToBonePayloadWithId #-} + +-- | Directly coerce an 'OsteoSegment' of 'Identity' values into an extensible Polytropos 'Record'. +-- +-- Operates at \(O(1)\) when the segment is un-sliced, reusing the underlying array directly. +-- +-- See Note [Zero-Cost Polytropos Rep Coercions] [ref:note-osteo-polytropos-coercion]. +segmentToRecord :: OsteoSegment (Identity Any) -> Record (r :: Row) +segmentToRecord !seg = RowRep (segmentToRep 0 seg) +{-# INLINE segmentToRecord #-} + +-- | Directly coerce an extensible Polytropos 'Record' into an 'OsteoSegment' of 'Identity' values. +-- +-- Operates at \(O(1)\) with zero allocation. +-- +-- See Note [Zero-Cost Polytropos Rep Coercions] [ref:note-osteo-polytropos-coercion]. +recordToSegment :: Record (r :: Row) -> OsteoSegment (Identity Any) +recordToSegment (RowRep rep) = snd (repToSegment rep) +{-# INLINE recordToSegment #-} + +-- | Bidirectional codec between an arbitrary osteological bone payload type @a@ +-- and an extensible Polytropos record @Record r@. +class BoneRecordCodec a (r :: Row) | a -> r where + -- | Encode an osteological bone payload into an open record. + encodeBonePayload :: a -> Record r + -- | Decode an open record back into an osteological bone payload. + decodeBonePayload :: Record r -> a + +-- | Encode a bone whose payload implements 'BoneRecordCodec' into an extensible record. +boneToRecordVia :: BoneRecordCodec a r => Bone a -> Record r +boneToRecordVia (Bone _ p) = encodeBonePayload p +{-# INLINE boneToRecordVia #-} + +-- | Decode an extensible record into an osteological bone with an explicit 'BoneId'. +recordToBoneVia :: BoneRecordCodec a r => BoneId -> Record r -> Bone a +recordToBoneVia !bid !r = Bone bid (decodeBonePayload r) +{-# INLINE recordToBoneVia #-} diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -0,0 +1,826 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} + +module Main (main) where + +import Control.Concurrent (forkIO, newEmptyMVar, putMVar, readMVar, takeMVar) +import Control.Monad (forM_, replicateM) +import qualified Data.Map.Strict as Map +import Data.Monoid (Sum(..)) +import Data.Text (Text) +import Data.Word (Word64, Word8) +import Test.Hspec + +import Gachi.Core +import Gachi.Core.Rewriting +import Gachi.Core.Traversal +import Gachi.Osteology + +main :: IO () +main = hspec do + -- Tested against Note [Chattering Lock-Free Atomic Synchronization] [ref:note-chattering-synchronization] + describe "Gachi.Core Skeletal Primitives" do + it "constructs empty skeletal structure with zero bones and joints" do + let skel = emptySkeleton :: Skeleton Text + totalBones skel `shouldBe` 0 + totalJoints skel `shouldBe` 0 + lookupBone (BoneId 0) skel `shouldBe` Nothing + lookupJoint (JointId 0) skel `shouldBe` Nothing + + -- Tested against Note [Monotonic Identifier Allocation and Contiguous Indexing] [ref:note-monotonic-id-allocation] + it "inserts and retrieves bones with monotonically assigned identifiers in O(1)" do + let skel0 = emptySkeleton :: Skeleton Text + (b0, skel1) = insertBone "femur" skel0 + (b1, skel2) = insertBone "tibia" skel1 + (b2, skel3) = insertBone "cranium" skel2 + + b0 `shouldBe` BoneId 0 + b1 `shouldBe` BoneId 1 + b2 `shouldBe` BoneId 2 + totalBones skel3 `shouldBe` 3 + + lookupBone b0 skel3 `shouldBe` Just "femur" + lookupBone b1 skel3 `shouldBe` Just "tibia" + lookupBone b2 skel3 `shouldBe` Just "cranium" + unsafeLookupBone b1 skel3 `shouldBe` "tibia" + lookupBone (BoneId 99) skel3 `shouldBe` Nothing + + -- Tested against Note [Directional Joints and Incident Traversal] [ref:note-directional-joints-traversal] + it "connects joints between bones and traverses incident connections" do + let skel0 = emptySkeleton :: Skeleton Text + (b0, skel1) = insertBone "femur" skel0 + (b1, skel2) = insertBone "patella" skel1 + (b2, skel3) = insertBone "tibia" skel2 + (j0, skel4) = connectJoint b0 b1 skel3 + (j1, skel5) = connectJoint b1 b2 skel4 + + totalJoints skel5 `shouldBe` 2 + lookupJoint j0 skel5 `shouldBe` Just (Joint (JointId 0) b0 b1) + lookupJoint j1 skel5 `shouldBe` Just (Joint (JointId 1) b1 b2) + lookupJoint (JointId 99) skel5 `shouldBe` Nothing + + let incidents = incidentJoints b1 skel5 + length incidents `shouldBe` 2 + map jointId incidents `shouldBe` [JointId 0, JointId 1] + + -- Tested against Note [Zero-Copy Sub-Segment Slicing] [ref:note-zero-copy-slicing] + it "extracts zero-copy bone slices from a skeleton" do + let skel0 = emptySkeleton :: Skeleton Text + (_, skel1) = insertBone "cervical" skel0 + (_, skel2) = insertBone "thoracic" skel1 + (_, skel3) = insertBone "lumbar" skel2 + (_, skel4) = insertBone "sacrum" skel3 + + case sliceBones 1 2 skel4 of + Nothing -> expectationFailure "sliceBones returned Nothing" + Just sl -> do + segmentLength sl `shouldBe` 2 + toListOsteo sl `shouldBe` ["thoracic", "lumbar"] + + -- Tested against Note [Osteological Contiguous Memory Layout] [ref:note-osteology-memory-layout] + describe "Gachi.Osteology Contiguous Memory Layout" do + it "constructs empty osteological segment" do + let seg = emptySegment :: OsteoSegment Int + segmentLength seg `shouldBe` 0 + segmentCapacity seg `shouldBe` 0 + indexOsteo 0 seg `shouldBe` Nothing + + -- Tested against Note [Geometric Capacity Expansion and Reallocation] [ref:note-geometric-capacity-expansion] + it "appends elements sequentially and dynamically expands capacity" do + let seg0 = emptySegment + seg1 = appendOsteo (10 :: Int) seg0 + seg2 = appendOsteo 20 seg1 + seg3 = appendOsteo 30 seg2 + seg4 = appendOsteo 40 seg3 + seg5 = appendOsteo 50 seg4 + + segmentLength seg5 `shouldBe` 5 + segmentCapacity seg5 `shouldSatisfy` (>= 5) + + indexOsteo 0 seg5 `shouldBe` Just 10 + indexOsteo 1 seg5 `shouldBe` Just 20 + indexOsteo 2 seg5 `shouldBe` Just 30 + indexOsteo 3 seg5 `shouldBe` Just 40 + indexOsteo 4 seg5 `shouldBe` Just 50 + unsafeIndexOsteo 2 seg5 `shouldBe` 30 + indexOsteo 5 seg5 `shouldBe` Nothing + indexOsteo (-1) seg5 `shouldBe` Nothing + + -- Tested against Note [Zero-Copy Sub-Segment Slicing] [ref:note-zero-copy-slicing] + it "performs zero-copy slicing within contiguous memory" do + let seg = fromListOsteo [10, 20, 30, 40, 50 :: Int] + case sliceOsteo 1 3 seg of + Nothing -> expectationFailure "sliceOsteo returned Nothing" + Just s1 -> do + segmentLength s1 `shouldBe` 3 + toListOsteo s1 `shouldBe` [20, 30, 40] + indexOsteo 0 s1 `shouldBe` Just 20 + indexOsteo 2 s1 `shouldBe` Just 40 + indexOsteo 3 s1 `shouldBe` Nothing + + sliceOsteo 0 6 seg `shouldBe` Nothing + sliceOsteo (-1) 2 seg `shouldBe` Nothing + sliceOsteo 2 (-1) seg `shouldBe` Nothing + + it "satisfies Semigroup concatenation into a single contiguous segment" do + let segA = fromListOsteo [1, 2, 3 :: Int] + segB = fromListOsteo [4, 5, 6 :: Int] + combined = segA <> segB + + segmentLength combined `shouldBe` 6 + toListOsteo combined `shouldBe` [1, 2, 3, 4, 5, 6] + + it "implements Functor, Foldable, and Traversable lawfully" do + let seg = fromListOsteo [1, 2, 3, 4, 5 :: Int] + mapped = fmap (* 10) seg + toListOsteo mapped `shouldBe` [10, 20, 30, 40, 50] + sum seg `shouldBe` 15 + length seg `shouldBe` 5 + null seg `shouldBe` False + null (emptySegment :: OsteoSegment Int) `shouldBe` True + + describe "Gachi.Osteology Unboxed Byte Storage" do + it "constructs empty byte storage" do + let bs = emptyBytes + bytesLength bs `shouldBe` 0 + indexByte 0 bs `shouldBe` Nothing + + it "roundtrips fromByteList and toByteList faithfully" do + let input = [0xDE, 0xAD, 0xBE, 0xEF, 0x00, 0xFF] :: [Word8] + bs = fromByteList input + bytesLength bs `shouldBe` 6 + toByteList bs `shouldBe` input + indexByte 0 bs `shouldBe` Just 0xDE + indexByte 3 bs `shouldBe` Just 0xEF + unsafeIndexByte 1 bs `shouldBe` 0xAD + indexByte 6 bs `shouldBe` Nothing + + it "performs zero-copy slicing over unboxed byte arrays" do + let input = [10, 20, 30, 40, 50 :: Word8] + bs = fromByteList input + case sliceBytes 1 3 bs of + Nothing -> expectationFailure "sliceBytes returned Nothing" + Just sl -> do + bytesLength sl `shouldBe` 3 + toByteList sl `shouldBe` [20, 30, 40] + sliceBytes 0 10 bs `shouldBe` Nothing + + -- Tested against Note [Chattering Lock-Free Atomic Synchronization] [ref:note-chattering-synchronization] + describe "Gachi.Osteology.Atomic Tagged Word Layouts" do + it "faithfully roundtrips all JointState constructors through 64-bit tagged words" do + decodeJointState (encodeJointState JointInert) `shouldBe` JointInert + decodeJointState (encodeJointState (JointChattering 0)) `shouldBe` JointChattering 0 + decodeJointState (encodeJointState (JointChattering 42)) `shouldBe` JointChattering 42 + decodeJointState (encodeJointState (JointChattering 0x1FFFFFFFFFFFFFFF)) + `shouldBe` JointChattering 0x1FFFFFFFFFFFFFFF + decodeJointState (encodeJointState (JointSynchronized 0)) `shouldBe` JointSynchronized 0 + decodeJointState (encodeJointState (JointSynchronized 99999)) `shouldBe` JointSynchronized 99999 + decodeJointState (encodeJointState JointFused) `shouldBe` JointFused + + it "decodes zeroed memory naturally as JointInert (zero-initialization invariant)" do + decodeJointState 0 `shouldBe` JointInert + + it "classifies joint lifecycle states with pure predicates" do + isJointInert JointInert `shouldBe` True + isJointInert (JointChattering 1) `shouldBe` False + + isJointChattering (JointChattering 10) `shouldBe` True + isJointChattering JointInert `shouldBe` False + + isJointSynchronized (JointSynchronized 440) `shouldBe` True + isJointSynchronized JointInert `shouldBe` False + + isJointFused JointFused `shouldBe` True + isJointFused JointInert `shouldBe` False + + describe "Gachi.Core.Atomic Hardware Compare-And-Swap (Single-Threaded)" do + it "initializes an unboxed joint reference to JointInert" do + joint <- newAtomicJoint JointInert + st <- readJointState joint + st `shouldBe` JointInert + + it "succeeds on valid expected state and fails on mismatched expected state" do + joint <- newAtomicJoint JointInert + + -- 1. Valid transition: JointInert -> JointChattering 1 + res1 <- casJointState joint JointInert (JointChattering 1) + res1 `shouldBe` True + readJointState joint `shouldReturn` JointChattering 1 + + -- 2. Mismatched transition: expected JointInert but current is JointChattering 1 + res2 <- casJointState joint JointInert (JointChattering 2) + res2 `shouldBe` False + -- Memory must remain untouched + readJointState joint `shouldReturn` JointChattering 1 + + -- 3. Transition to JointSynchronized 440 + res3 <- casJointState joint (JointChattering 1) (JointSynchronized 440) + res3 `shouldBe` True + readJointState joint `shouldReturn` JointSynchronized 440 + + -- 4. Transition to terminal JointFused + res4 <- casJointState joint (JointSynchronized 440) JointFused + res4 `shouldBe` True + readJointState joint `shouldReturn` JointFused + + it "transitions joint with transitionJointWithBackoff" do + joint <- newAtomicJoint JointInert + res <- transitionJointWithBackoff joint (\s -> case s of + JointInert -> Just (JointChattering 1) + _ -> Nothing) 5 + res `shouldBe` Right (JointChattering 1) + readJointState joint `shouldReturn` JointChattering 1 + + it "fails with InvalidTransition when transition function disallows state" do + joint <- newAtomicJoint JointFused + res <- transitionJointWithBackoff joint (\s -> case s of + JointChattering n -> Just (JointChattering (n + 1)) + _ -> Nothing) 5 + res `shouldBe` Left (InvalidTransition JointFused) + readJointState joint `shouldReturn` JointFused + + describe "Gachi.Core.Atomic Multi-Threaded High-Contention CAS Race" do + it "resolves a 20-thread CAS race where exactly one thread succeeds and zero corrupt states emerge" do + joint <- newAtomicJoint JointInert + resultsMVar <- newEmptyMVar + barrier <- newEmptyMVar + let numThreads = 20 :: Int + + forM_ [1 .. numThreads] \tid -> forkIO do + -- Synchronize starting line + readMVar barrier + success <- casJointState joint JointInert (JointChattering (fromIntegral tid)) + putMVar resultsMVar (tid, success) + + -- Release all threads simultaneously + putMVar barrier () + + results <- replicateM numThreads (takeMVar resultsMVar) + let winners = [ tid | (tid, True) <- results ] + + -- Exactly one thread must win the race + length winners `shouldBe` 1 + + case winners of + [winnerId] -> do + finalState <- readJointState joint + finalState `shouldBe` JointChattering (fromIntegral winnerId) + _ -> expectationFailure ("Expected exactly 1 winner, but got: " ++ show winners) + + it "linearizes 500 concurrent transitions across 20 threads with bounded backoff" do + joint <- newAtomicJoint JointInert + let numThreads = 20 :: Int + incrementsPerThread = 25 :: Int + barrier <- newEmptyMVar + doneMVar <- newEmptyMVar + + forM_ [1 .. numThreads] \_ -> forkIO do + readMVar barrier + forM_ [1 .. incrementsPerThread] \_ -> do + res <- transitionJointWithBackoff joint (\case + JointInert -> Just (JointChattering 1) + JointChattering n -> Just (JointChattering (n + 1)) + _ -> Nothing) 100 + case res of + Left err -> putMVar doneMVar (Just err) + Right _ -> pure () + putMVar doneMVar Nothing + + -- Release all worker threads + putMVar barrier () + + errors <- replicateM numThreads (takeMVar doneMVar) + -- Assert zero backoff errors occurred + let failed = [ err | Just err <- errors ] + failed `shouldBe` [] + + -- Total increments = 20 * 25 = 500 + finalState <- readJointState joint + finalState `shouldBe` JointChattering (fromIntegral (numThreads * incrementsPerThread)) + + describe "Gachi.Core.Atomic Wait-Free Reads Under Write Saturation" do + it "maintains wait-free monotonic read progression under heavy writer contention" do + joint <- newAtomicJoint (JointChattering 0) + let writeIterations = 2000 :: Word64 + numReaders = 4 :: Int + readsPerReader = 500 :: Int + startBarrier <- newEmptyMVar + readerDone <- newEmptyMVar + + -- Spawn concurrent reader threads + forM_ [1 .. numReaders] \_ -> forkIO do + readMVar startBarrier + let loop 0 !_prev = pure () + loop !k !prev = do + st <- readJointState joint + case st of + JointChattering cur -> do + if cur >= prev + then loop (k - 1) cur + else putMVar readerDone (Just ("Non-monotonic read: observed " ++ show cur ++ " after " ++ show prev)) + _ -> putMVar readerDone (Just ("Unexpected state during saturation: " ++ show st)) + loop readsPerReader 0 + putMVar readerDone Nothing + + -- Spawn writer thread saturating the atomic joint with transitions + writerDone <- newEmptyMVar + _ <- forkIO do + readMVar startBarrier + forM_ [1 .. writeIterations] \i -> do + writeJointState joint (JointChattering i) + putMVar writerDone () + + -- Trigger all threads simultaneously + putMVar startBarrier () + + -- Wait for writer and readers + takeMVar writerDone + readerErrors <- replicateM numReaders (takeMVar readerDone) + + let badReads = [ err | Just err <- readerErrors ] + badReads `shouldBe` [] + + finalState <- readJointState joint + finalState `shouldBe` JointChattering writeIterations + + -- Tested against Note [Concurrent Skeletal Graph Traversal] [ref:note-concurrent-traversal] + describe "Gachi.Core.Traversal Concurrent & Snapshot Primitives" do + it "handles empty skeletons gracefully across all traversal routines" do + let skel = emptySkeleton :: Skeleton Text + bonesRes <- traverseSkeletonConcurrently skel (\b -> pure (bonePayload b)) + bonesRes `shouldBe` [] + + fRes <- foldBonesConcurrently skel (\acc _ -> pure (acc + 1 :: Int)) 0 + fRes `shouldBe` 0 + + mSum <- foldMapBonesConcurrently skel (\_ -> pure (Sum (1 :: Int))) + mSum `shouldBe` Sum 0 + + bPath <- findBonePathConcurrently skel (BoneId 0) (BoneId 1) + bPath `shouldBe` Nothing + + jPath <- findJointPathConcurrently skel (JointId 0) (JointId 1) + jPath `shouldBe` Nothing + + bfsRes <- traverseSkeletonBFS skel (BoneId 0) + bfsRes `shouldBe` [] + + dfsRes <- traverseSkeletonDFS skel (BoneId 0) + dfsRes `shouldBe` [] + + snap <- snapshotSkeleton skel + snapshotBones snap `shouldBe` [] + snapshotJoints snap `shouldBe` [] + + it "traverses bones concurrently preserving strict monotonic evaluation order" do + let n = 100 :: Int + buildSkel !s 0 = s + buildSkel !s !k = + let !i = n - k + (_, !s') = insertBone i s + in buildSkel s' (k - 1) + skel = buildSkel emptySkeleton n + + traversed <- traverseSkeletonConcurrently skel (\b -> pure (bonePayload b)) + traversed `shouldBe` [0 .. n - 1] + + it "folds bones concurrently matching sequential evaluation" do + let n = 50 :: Int + buildSkel !s 0 = s + buildSkel !s !k = + let !i = n - k + (_, !s') = insertBone i s + in buildSkel s' (k - 1) + skel = buildSkel emptySkeleton n + + foldedSum <- foldBonesConcurrently skel (\acc b -> pure (acc + bonePayload b)) 0 + foldedSum `shouldBe` sum [0 .. n - 1] + + it "foldMapBonesConcurrently combines monoidal payloads faithfully" do + let n = 50 :: Int + buildSkel !s 0 = s + buildSkel !s !k = + let !i = n - k + (_, !s') = insertBone i s + in buildSkel s' (k - 1) + skel = buildSkel emptySkeleton n + + Sum total <- foldMapBonesConcurrently skel (\b -> pure (Sum (bonePayload b))) + total `shouldBe` sum [0 .. n - 1] + + it "finds directed and bidirectional paths through bone and joint networks" do + let skel0 = emptySkeleton :: Skeleton Text + (b0, skel1) = insertBone "femur" skel0 + (b1, skel2) = insertBone "patella" skel1 + (b2, skel3) = insertBone "tibia" skel2 + (j0, skel4) = connectJoint b0 b1 skel3 + (j1, skel5) = connectJoint b1 b2 skel4 + + -- Forward path: b0 -> b2 + mPathFwd <- findBonePathConcurrently skel5 b0 b2 + case mPathFwd of + Nothing -> expectationFailure "Expected path between b0 and b2" + Just p -> map bonePayload p `shouldBe` ["femur", "patella", "tibia"] + + -- Reverse query with Forward config should fail: + let fwdCfg = defaultTraversalConfig { traversalDirection = Forward } + mPathRevFwd <- findBonePathConcurrentlyWith fwdCfg skel5 b2 b0 + mPathRevFwd `shouldBe` Nothing + + -- Reverse query with Reverse config should succeed: + let revCfg = defaultTraversalConfig { traversalDirection = Reverse } + mPathRev <- findBonePathConcurrentlyWith revCfg skel5 b2 b0 + case mPathRev of + Nothing -> expectationFailure "Expected reverse path between b2 and b0" + Just p -> map bonePayload p `shouldBe` ["tibia", "patella", "femur"] + + -- Joint path: j0 -> j1 + mJointPath <- findJointPathConcurrently skel5 j0 j1 + case mJointPath of + Nothing -> expectationFailure "Expected joint path between j0 and j1" + Just jp -> map osteoJointId jp `shouldBe` [j0, j1] + + -- Root path when start == end + mSelfPath <- findBonePathConcurrently skel5 b1 b1 + case mSelfPath of + Nothing -> expectationFailure "Expected self path for b1" + Just p -> map bonePayload p `shouldBe` ["patella"] + + it "performs BFS and DFS graph walks over skeletal components" do + let skel0 = emptySkeleton :: Skeleton Text + (b0, skel1) = insertBone "root" skel0 + (b1, skel2) = insertBone "left" skel1 + (b2, skel3) = insertBone "right" skel2 + (_, skel4) = connectJoint b0 b1 skel3 + (_, skel5) = connectJoint b0 b2 skel4 + + bfsNodes <- traverseSkeletonBFS skel5 b0 + map bonePayload bfsNodes `shouldMatchList` ["root", "left", "right"] + + dfsNodes <- traverseSkeletonDFS skel5 b0 + map bonePayload dfsNodes `shouldMatchList` ["root", "left", "right"] + + it "captures instantaneous atomic joint snapshots under state transitions" do + let skel0 = emptySkeleton :: Skeleton Text + (b0, skel1) = insertBone "pelvis" skel0 + (b1, skel2) = insertBone "spine" skel1 + (j0, skel3) = connectJoint b0 b1 skel2 + + skel <- initAtomicJoints skel3 + snap0 <- snapshotSkeleton skel + map osteoJointState (snapshotJoints snap0) `shouldBe` [JointInert] + + case getAtomicJoint j0 skel of + Nothing -> expectationFailure "Atomic joint j0 not found" + Just aj -> do + _ <- casJointState aj JointInert (JointChattering 42) + snap1 <- snapshotSkeleton skel + map osteoJointState (snapshotJoints snap1) `shouldBe` [JointChattering 42] + + -- Tested against Note [Concurrent Skeletal Graph Traversal] [ref:note-concurrent-traversal] + describe "Gachi.Core.Traversal Multi-Agent High-Concurrency Stress Test" do + it "executes 50 concurrent agents traversing a 1,000-bone graph with continuous joint transitions" do + let boneCount = 1000 :: Int + buildBones !s 0 !acc = (reverse acc, s) + buildBones !s !k !acc = + let !i = boneCount - k + (!bid, !s') = insertBone i s + in buildBones s' (k - 1) (bid : acc) + (_bids, skel1) = buildBones emptySkeleton boneCount [] + + buildJoints !s 0 !acc = (reverse acc, s) + buildJoints !s !k !acc = + let !i = (boneCount - 1) - k + !src = BoneId (fromIntegral i) + !dst = BoneId (fromIntegral (i + 1)) + (!jid, !s') = connectJoint src dst s + in buildJoints s' (k - 1) (jid : acc) + (_jids, skel2) = buildJoints skel1 (boneCount - 1) [] + + skel <- initAtomicJoints skel2 + let expectedSum = sum [0 .. boneCount - 1] + numWorkers = 50 :: Int + numWriters = 5 :: Int + writerTransitions = 100 :: Int + + startBarrier <- newEmptyMVar + workerDone <- newEmptyMVar + writerDone <- newEmptyMVar + + -- Background writers continuously transitioning joints + forM_ [0 .. numWriters - 1] \wIdx -> forkIO do + readMVar startBarrier + forM_ [0 .. writerTransitions - 1] \stepIdx -> do + let targetJointIdx = (wIdx * 199 + stepIdx * 7) `rem` (boneCount - 1) + jid = JointId (fromIntegral targetJointIdx) + case getAtomicJoint jid skel of + Nothing -> pure () + Just aj -> do + _ <- transitionJointWithBackoff aj (\case + JointInert -> Just (JointChattering (fromIntegral stepIdx)) + JointChattering _ -> Just (JointSynchronized (fromIntegral stepIdx)) + JointSynchronized _ -> Just (JointChattering (fromIntegral (stepIdx + 1))) + JointFused -> Just JointInert + ) 10 + pure () + putMVar writerDone () + + -- 50 Concurrent Agent Workers performing mixed traversals + forM_ [0 .. numWorkers - 1] \wId -> forkIO do + readMVar startBarrier + res <- case wId `rem` 4 of + -- Worker class 0: Full concurrent traversal verifying exact baseline match + 0 -> do + traversed <- traverseSkeletonConcurrently skel (\b -> pure (bonePayload b)) + if traversed == [0 .. boneCount - 1] + then pure (Right ()) + else pure (Left ("Worker " ++ show wId ++ ": traversed mismatch")) + + -- Worker class 1: Concurrent fold computing sum + 1 -> do + val <- foldBonesConcurrently skel (\acc b -> pure (acc + bonePayload b)) 0 + if val == expectedSum + then pure (Right ()) + else pure (Left ("Worker " ++ show wId ++ ": fold sum mismatch " ++ show val)) + + -- Worker class 2: Concurrent path finding along graph segments + 2 -> do + let startIdx = (wId * 17) `rem` (boneCount - 20) + endIdx = startIdx + 15 + srcBid = BoneId (fromIntegral startIdx) + dstBid = BoneId (fromIntegral endIdx) + mPath <- findBonePathConcurrently skel srcBid dstBid + case mPath of + Nothing -> pure (Left ("Worker " ++ show wId ++ ": path not found")) + Just p -> + if length p == 16 + then pure (Right ()) + else pure (Left ("Worker " ++ show wId ++ ": unexpected path length " ++ show (length p))) + + -- Worker class 3: Concurrent snapshot view under active writer chattering + _ -> do + snap <- snapshotSkeleton skel + let bCount = length (snapshotBones snap) + jCount = length (snapshotJoints snap) + if bCount == boneCount && jCount == boneCount - 1 + then pure (Right ()) + else pure (Left ("Worker " ++ show wId ++ ": snapshot count mismatch")) + + putMVar workerDone res + + -- Release all workers and writers simultaneously + putMVar startBarrier () + + -- Wait for writers + _ <- replicateM numWriters (takeMVar writerDone) + + -- Collect worker results + workerResults <- replicateM numWorkers (takeMVar workerDone) + let failures = [ err | Left err <- workerResults ] + failures `shouldBe` [] + + -- Tested against Note [Double-Pushout Algebraic Graph Rewriting] [ref:note-dpo-graph-rewriting] + describe "Gachi.Core.Rewriting Double-Pushout (DPO) Engine" do + it "replaces a chain of two bones with a single bridged bone while preserving unaffected topology" do + -- 1. Construct host graph G: + -- b0 ("root") -> b1 ("femur") -> b2 ("tibia") -> b3 ("foot") + -- With unaffected topology: + -- j3: b0 ("root") -> b3 ("foot") (bypass edge) + -- j4: b0 ("root") -> b4 ("tail") (side branch) + let (b0, g0) = insertBone ("root" :: Text) emptySkeleton + (b1, g1) = insertBone "femur" g0 + (b2, g2) = insertBone "tibia" g1 + (b3, g3) = insertBone "foot" g2 + (b4, g4) = insertBone "tail" g3 + (_j0, g5) = connectJoint b0 b1 g4 + (_j1, g6) = connectJoint b1 b2 g5 + (_j2, g7) = connectJoint b2 b3 g6 + (_j3, g8) = connectJoint b0 b3 g7 + (_j4, host) = connectJoint b0 b4 g8 + + totalBones host `shouldBe` 5 + totalJoints host `shouldBe` 5 + + -- 2. Construct DPO production rule: + -- L: l0 ("root") -> l1 ("femur") -> l2 ("tibia") -> l3 ("foot") + let (l0, lS0) = insertBone ("root" :: Text) emptySkeleton + (l1, lS1) = insertBone "femur" lS0 + (l2, lS2) = insertBone "tibia" lS1 + (l3, lS3) = insertBone "foot" lS2 + (jl0, lS4) = connectJoint l0 l1 lS3 + (jl1, lS5) = connectJoint l1 l2 lS4 + (jl2, ruleL) = connectJoint l2 l3 lS5 + + -- K: k0 ("root"), k1 ("foot") (interface bones preserved) + let (k0, kS0) = insertBone ("root" :: Text) emptySkeleton + (k1, ruleK) = insertBone "foot" kS0 + + -- R: r0 ("root"), r1 ("foot"), r2 ("bridged_leg") + -- r0 -> r2 -> r1 + let (r0, rS0) = insertBone ("root" :: Text) emptySkeleton + (r1, rS1) = insertBone "foot" rS0 + (r2, rS2) = insertBone "bridged_leg" rS1 + (_jr0, rS3) = connectJoint r0 r2 rS2 + (_jr1, ruleR) = connectJoint r2 r1 rS3 + + let morphL = + ( Map.empty + , Map.fromList [(k0, l0), (k1, l3)] + ) + morphR = + ( Map.empty + , Map.fromList [(k0, r0), (k1, r1)] + ) + rule = ProductionRule + { ruleName = "bridge-two-bone-chain" + , ruleLeft = ruleL + , ruleInterface = ruleK + , ruleRight = ruleR + , morphismL = morphL + , morphismR = morphR + } + + -- Find matches in host + let matches = findMatches rule host + length matches `shouldBe` 1 + + case matches of + [] -> expectationFailure "Expected at least 1 match" + (m : _) -> do + -- Verify match structure + Map.lookup jl0 (matchJoints m) `shouldBe` Just (JointId 0) + Map.lookup jl1 (matchJoints m) `shouldBe` Just (JointId 1) + Map.lookup jl2 (matchJoints m) `shouldBe` Just (JointId 2) + + -- Derive pushout complement D (context graph) + case derivePushoutComplement rule m host of + Left err -> expectationFailure ("Pushout complement failed: " ++ show err) + Right d -> do + -- In D: femur and tibia deleted; root, foot, tail retained + totalBones d `shouldBe` 3 + allBones d `shouldBe` ["root", "foot", "tail"] + -- Unaffected edges j3 (root -> foot) and j4 (root -> tail) are preserved + totalJoints d `shouldBe` 2 + lookupJoint (JointId 0) d `shouldBe` Just (Joint (JointId 0) (BoneId 0) (BoneId 1)) + lookupJoint (JointId 1) d `shouldBe` Just (Joint (JointId 1) (BoneId 0) (BoneId 2)) + + -- Construct second pushout H + case constructPushout rule m d of + Left err -> expectationFailure ("Construct pushout failed: " ++ show err) + Right h -> do + totalBones h `shouldBe` 4 + allBones h `shouldBe` ["root", "foot", "tail", "bridged_leg"] + totalJoints h `shouldBe` 4 + -- Unaffected adjacent topology preserved: + lookupBone (BoneId 0) h `shouldBe` Just "root" + lookupBone (BoneId 1) h `shouldBe` Just "foot" + lookupBone (BoneId 2) h `shouldBe` Just "tail" + lookupBone (BoneId 3) h `shouldBe` Just "bridged_leg" + -- Connects: root->foot (j0), root->tail (j1), root->bridge (j2), bridge->foot (j3) + lookupJoint (JointId 0) h `shouldBe` Just (Joint (JointId 0) (BoneId 0) (BoneId 1)) + lookupJoint (JointId 1) h `shouldBe` Just (Joint (JointId 1) (BoneId 0) (BoneId 2)) + lookupJoint (JointId 2) h `shouldBe` Just (Joint (JointId 2) (BoneId 0) (BoneId 3)) + lookupJoint (JointId 3) h `shouldBe` Just (Joint (JointId 3) (BoneId 3) (BoneId 1)) + + -- End-to-end applyRule yields identical result + case applyRule rule m host of + Left err -> expectationFailure ("applyRule failed: " ++ show err) + Right h -> do + totalBones h `shouldBe` 4 + totalJoints h `shouldBe` 4 + allBones h `shouldBe` ["root", "foot", "tail", "bridged_leg"] + + it "rejects rule application when external incident edges violate dangling condition" do + -- Host graph: femur -> tibia -> fibula + -- Joint 0: femur -> tibia + -- Joint 1: tibia -> fibula + let (b0, g0) = insertBone ("femur" :: Text) emptySkeleton + (b1, g1) = insertBone "tibia" g0 + (b2, g2) = insertBone "fibula" g1 + (_j0, g3) = connectJoint b0 b1 g2 + (_j1, host) = connectJoint b1 b2 g3 + + -- Rule attempting to delete tibia (and joint 0) without matching joint 1 + -- L: femur -> tibia + let (l0, lS0) = insertBone ("femur" :: Text) emptySkeleton + (l1, lS1) = insertBone "tibia" lS0 + (_jl0, ruleL) = connectJoint l0 l1 lS1 + + -- K: only femur preserved; tibia is in L \ K (scheduled for deletion) + let (k0, ruleK) = insertBone ("femur" :: Text) emptySkeleton + + -- R: only femur + let (r0, ruleR) = insertBone ("femur" :: Text) emptySkeleton + + let rule = ProductionRule + { ruleName = "delete-tibia" + , ruleLeft = ruleL + , ruleInterface = ruleK + , ruleRight = ruleR + , morphismL = (Map.empty, Map.fromList [(k0, l0)]) + , morphismR = (Map.empty, Map.fromList [(k0, r0)]) + } + + let matches = findMatches rule host + length matches `shouldBe` 1 + + case matches of + [] -> expectationFailure "Expected 1 match" + (m : _) -> do + -- Deleting tibia leaves external joint 1 (tibia -> fibula) dangling! + case validateGluingCondition rule m host of + Left (DanglingConditionViolated msg) -> + msg `shouldSatisfy` (\t -> not (null (show t))) + other -> + expectationFailure ("Expected DanglingConditionViolated, got: " ++ show other) + + case applyRule rule m host of + Left (DanglingConditionViolated _) -> pure () + other -> + expectationFailure ("applyRule should fail with DanglingConditionViolated, got: " ++ show other) + + it "rejects non-injective match outside interface violating identification condition" do + -- Host graph with single vertex + let (_b0, host) = insertBone ("vertebra" :: Text) emptySkeleton + + -- Rule with pattern L containing two distinct vertices + let (l0, lS0) = insertBone ("vertebra" :: Text) emptySkeleton + (l1, ruleL) = insertBone "vertebra" lS0 + ruleK = emptySkeleton :: Skeleton Text + ruleR = emptySkeleton :: Skeleton Text + + let rule = ProductionRule + { ruleName = "fuse-vertebrae" + , ruleLeft = ruleL + , ruleInterface = ruleK + , ruleRight = ruleR + , morphismL = (Map.empty, Map.empty) + , morphismR = (Map.empty, Map.empty) + } + + -- Non-injective match mapping both l0 and l1 to host b0 + let nonInjectiveMatch = GraphMatch + { matchJoints = Map.empty + , matchBones = Map.fromList [(l0, BoneId 0), (l1, BoneId 0)] + } + + case validateGluingCondition rule nonInjectiveMatch host of + Left (IdentificationConditionViolated msg) -> + msg `shouldSatisfy` (\t -> not (null (show t))) + other -> + expectationFailure ("Expected IdentificationConditionViolated, got: " ++ show other) + + case applyRule rule nonInjectiveMatch host of + Left (IdentificationConditionViolated _) -> pure () + other -> + expectationFailure ("applyRule should fail with IdentificationConditionViolated, got: " ++ show other) + + it "preserves graph isomorphism and uniqueness under identity rules (L = K = R)" do + -- Host graph with 3 bones and 2 joints + let (b0, g0) = insertBone ("humerus" :: Text) emptySkeleton + (b1, g1) = insertBone "radius" g0 + (b2, g2) = insertBone "ulna" g1 + (j0, g3) = connectJoint b0 b1 g2 + (j1, host) = connectJoint b0 b2 g3 + + -- Identity rule where L = K = R = host + let rule = ProductionRule + { ruleName = "identity-rule" + , ruleLeft = host + , ruleInterface = host + , ruleRight = host + , morphismL = (Map.fromList [(j0, j0), (j1, j1)], Map.fromList [(b0, b0), (b1, b1), (b2, b2)]) + , morphismR = (Map.fromList [(j0, j0), (j1, j1)], Map.fromList [(b0, b0), (b1, b1), (b2, b2)]) + } + + let identityMatch = GraphMatch + { matchJoints = Map.fromList [(j0, j0), (j1, j1)] + , matchBones = Map.fromList [(b0, b0), (b1, b1), (b2, b2)] + } + + -- Pushout complement uniqueness + case derivePushoutComplement rule identityMatch host of + Left err -> expectationFailure ("Complement failed: " ++ show err) + Right d -> do + totalBones d `shouldBe` totalBones host + totalJoints d `shouldBe` totalJoints host + allBones d `shouldBe` allBones host + allJoints d `shouldBe` allJoints host + d `shouldBe` host + + -- Second pushout H ≅ G + case constructPushout rule identityMatch d of + Left err -> expectationFailure ("Pushout failed: " ++ show err) + Right h -> do + totalBones h `shouldBe` totalBones host + totalJoints h `shouldBe` totalJoints host + allBones h `shouldBe` allBones host + allJoints h `shouldBe` allJoints host + h `shouldBe` host + + -- End-to-end rewrite H ≅ G + case applyRule rule identityMatch host of + Left err -> expectationFailure ("applyRule failed: " ++ show err) + Right h -> h `shouldBe` host