penelope-static (empty) → 0.1.0.0
raw patch · 8 files changed
+1030/−0 lines, 8 filesdep +QuickCheckdep +basedep +containers
Dependencies added: QuickCheck, base, containers, hspec, penelope-core, penelope-static, polytropos-core, polytropos-plugin, primitive, text
Files
- CHANGELOG.md +8/−0
- LICENSE +189/−0
- README.md +10/−0
- penelope-static.cabal +118/−0
- src/Penelope/Static.hs +17/−0
- src/Penelope/Static/Analysis.hs +247/−0
- test/Main.hs +93/−0
- test/Properties.hs +348/−0
+ CHANGELOG.md view
@@ -0,0 +1,8 @@+# Changelog for penelope-static++## 0.1.0.0 — Initial Release++- Static reflection and Cayley analysis engine for polycategorical computations.+- Effect dependency graphs and static pipeline scheduling.+- Algebraic circuit simplification and static optimization passes.+- Institutional satisfaction and reduct property verification tests.
+ LICENSE view
@@ -0,0 +1,189 @@+EUROPEAN UNION PUBLIC LICENCE v. 1.2+EUPL © the European Union 2007, 2016++This European Union Public Licence (the ‘EUPL’) applies to the Work (as defined below) which is provided under the+terms of this Licence. Any use of the Work, other than as authorised under this Licence is prohibited (to the extent such+use is covered by a right of the copyright holder of the Work).+The Work is provided under the terms of this Licence when the Licensor (as defined below) has placed the following+notice immediately following the copyright notice for the Work:+ Licensed under the EUPL+or has expressed by any other means his willingness to license under the EUPL.++1.Definitions+In this Licence, the following terms have the following meaning:+— ‘The Licence’:this Licence.+— ‘The Original Work’:the work or software distributed or communicated by the Licensor under this Licence, available+as Source Code and also as Executable Code as the case may be.+— ‘Derivative Works’:the works or software that could be created by the Licensee, based upon the Original Work or+modifications thereof. This Licence does not define the extent of modification or dependence on the Original Work+required in order to classify a work as a Derivative Work; this extent is determined by copyright law applicable in+the country mentioned in Article 15.+— ‘The Work’:the Original Work or its Derivative Works.+— ‘The Source Code’:the human-readable form of the Work which is the most convenient for people to study and+modify.+— ‘The Executable Code’:any code which has generally been compiled and which is meant to be interpreted by+a computer as a program.+— ‘The Licensor’:the natural or legal person that distributes or communicates the Work under the Licence.+— ‘Contributor(s)’:any natural or legal person who modifies the Work under the Licence, or otherwise contributes to+the creation of a Derivative Work.+— ‘The Licensee’ or ‘You’:any natural or legal person who makes any usage of the Work under the terms of the+Licence.+— ‘Distribution’ or ‘Communication’:any act of selling, giving, lending, renting, distributing, communicating,+transmitting, or otherwise making available, online or offline, copies of the Work or providing access to its essential+functionalities at the disposal of any other natural or legal person.++2.Scope of the rights granted by the Licence+The Licensor hereby grants You a worldwide, royalty-free, non-exclusive, sublicensable licence to do the following, for+the duration of copyright vested in the Original Work:+— use the Work in any circumstance and for all usage,+— reproduce the Work,+— modify the Work, and make Derivative Works based upon the Work,+— communicate to the public, including the right to make available or display the Work or copies thereof to the public+and perform publicly, as the case may be, the Work,+— distribute the Work or copies thereof,+— lend and rent the Work or copies thereof,+— sublicense rights in the Work or copies thereof.+Those rights can be exercised on any media, supports and formats, whether now known or later invented, as far as the+applicable law permits so.+In the countries where moral rights apply, the Licensor waives his right to exercise his moral right to the extent allowed+by law in order to make effective the licence of the economic rights here above listed.+The Licensor grants to the Licensee royalty-free, non-exclusive usage rights to any patents held by the Licensor, to the+extent necessary to make use of the rights granted on the Work under this Licence.++3.Communication of the Source Code+The Licensor may provide the Work either in its Source Code form, or as Executable Code. If the Work is provided as+Executable Code, the Licensor provides in addition a machine-readable copy of the Source Code of the Work along with+each copy of the Work that the Licensor distributes or indicates, in a notice following the copyright notice attached to+the Work, a repository where the Source Code is easily and freely accessible for as long as the Licensor continues to+distribute or communicate the Work.++4.Limitations on copyright+Nothing in this Licence is intended to deprive the Licensee of the benefits from any exception or limitation to the+exclusive rights of the rights owners in the Work, of the exhaustion of those rights or of other applicable limitations+thereto.++5.Obligations of the Licensee+The grant of the rights mentioned above is subject to some restrictions and obligations imposed on the Licensee. Those+obligations are the following:++Attribution right: The Licensee shall keep intact all copyright, patent or trademarks notices and all notices that refer to+the Licence and to the disclaimer of warranties. The Licensee must include a copy of such notices and a copy of the+Licence with every copy of the Work he/she distributes or communicates. The Licensee must cause any Derivative Work+to carry prominent notices stating that the Work has been modified and the date of modification.++Copyleft clause: If the Licensee distributes or communicates copies of the Original Works or Derivative Works, this+Distribution or Communication will be done under the terms of this Licence or of a later version of this Licence unless+the Original Work is expressly distributed only under this version of the Licence — for example by communicating+‘EUPL v. 1.2 only’. The Licensee (becoming Licensor) cannot offer or impose any additional terms or conditions on the+Work or Derivative Work that alter or restrict the terms of the Licence.++Compatibility clause: If the Licensee Distributes or Communicates Derivative Works or copies thereof based upon both+the Work and another work licensed under a Compatible Licence, this Distribution or Communication can be done+under the terms of this Compatible Licence. For the sake of this clause, ‘Compatible Licence’ refers to the licences listed+in the appendix attached to this Licence. Should the Licensee's obligations under the Compatible Licence conflict with+his/her obligations under this Licence, the obligations of the Compatible Licence shall prevail.++Provision of Source Code: When distributing or communicating copies of the Work, the Licensee will provide+a machine-readable copy of the Source Code or indicate a repository where this Source will be easily and freely available+for as long as the Licensee continues to distribute or communicate the Work.+Legal Protection: This Licence does not grant permission to use the trade names, trademarks, service marks, or names+of the Licensor, except as required for reasonable and customary use in describing the origin of the Work and+reproducing the content of the copyright notice.++6.Chain of Authorship+The original Licensor warrants that the copyright in the Original Work granted hereunder is owned by him/her or+licensed to him/her and that he/she has the power and authority to grant the Licence.+Each Contributor warrants that the copyright in the modifications he/she brings to the Work are owned by him/her or+licensed to him/her and that he/she has the power and authority to grant the Licence.+Each time You accept the Licence, the original Licensor and subsequent Contributors grant You a licence to their contributions+to the Work, under the terms of this Licence.++7.Disclaimer of Warranty+The Work is a work in progress, which is continuously improved by numerous Contributors. It is not a finished work+and may therefore contain defects or ‘bugs’ inherent to this type of development.+For the above reason, the Work is provided under the Licence on an ‘as is’ basis and without warranties of any kind+concerning the Work, including without limitation merchantability, fitness for a particular purpose, absence of defects or+errors, accuracy, non-infringement of intellectual property rights other than copyright as stated in Article 6 of this+Licence.+This disclaimer of warranty is an essential part of the Licence and a condition for the grant of any rights to the Work.++8.Disclaimer of Liability+Except in the cases of wilful misconduct or damages directly caused to natural persons, the Licensor will in no event be+liable for any direct or indirect, material or moral, damages of any kind, arising out of the Licence or of the use of the+Work, including without limitation, damages for loss of goodwill, work stoppage, computer failure or malfunction, loss+of data or any commercial damage, even if the Licensor has been advised of the possibility of such damage. However,+the Licensor will be liable under statutory product liability laws as far such laws apply to the Work.++9.Additional agreements+While distributing the Work, You may choose to conclude an additional agreement, defining obligations or services+consistent with this Licence. However, if accepting obligations, You may act only on your own behalf and on your sole+responsibility, not on behalf of the original Licensor or any other Contributor, and only if You agree to indemnify,+defend, and hold each Contributor harmless for any liability incurred by, or claims asserted against such Contributor by+the fact You have accepted any warranty or additional liability.++10.Acceptance of the Licence+The provisions of this Licence can be accepted by clicking on an icon ‘I agree’ placed under the bottom of a window+displaying the text of this Licence or by affirming consent in any other similar way, in accordance with the rules of+applicable law. Clicking on that icon indicates your clear and irrevocable acceptance of this Licence and all of its terms+and conditions.+Similarly, you irrevocably accept this Licence and all of its terms and conditions by exercising any rights granted to You+by Article 2 of this Licence, such as the use of the Work, the creation by You of a Derivative Work or the Distribution+or Communication by You of the Work or copies thereof.++11.Information to the public+In case of any Distribution or Communication of the Work by means of electronic communication by You (for example,+by offering to download the Work from a remote location) the distribution channel or media (for example, a website)+must at least provide to the public the information requested by the applicable law regarding the Licensor, the Licence+and the way it may be accessible, concluded, stored and reproduced by the Licensee.++12.Termination of the Licence+The Licence and the rights granted hereunder will terminate automatically upon any breach by the Licensee of the terms+of the Licence.+Such a termination will not terminate the licences of any person who has received the Work from the Licensee under+the Licence, provided such persons remain in full compliance with the Licence.++13.Miscellaneous+Without prejudice of Article 9 above, the Licence represents the complete agreement between the Parties as to the+Work.+If any provision of the Licence is invalid or unenforceable under applicable law, this will not affect the validity or+enforceability of the Licence as a whole. Such provision will be construed or reformed so as necessary to make it valid+and enforceable.+The European Commission may publish other linguistic versions or new versions of this Licence or updated versions of+the Appendix, so far this is required and reasonable, without reducing the scope of the rights granted by the Licence.+New versions of the Licence will be published with a unique version number.+All linguistic versions of this Licence, approved by the European Commission, have identical value. Parties can take+advantage of the linguistic version of their choice.++14.Jurisdiction+Without prejudice to specific agreement between parties,+— any litigation resulting from the interpretation of this License, arising between the European Union institutions,+bodies, offices or agencies, as a Licensor, and any Licensee, will be subject to the jurisdiction of the Court of Justice+of the European Union, as laid down in article 272 of the Treaty on the Functioning of the European Union,+— any litigation arising between other parties and resulting from the interpretation of this License, will be subject to+the exclusive jurisdiction of the competent court where the Licensor resides or conducts its primary business.++15.Applicable Law+Without prejudice to specific agreement between parties,+— this Licence shall be governed by the law of the European Union Member State where the Licensor has his seat,+resides or has his registered office,+— this licence shall be governed by Belgian law if the Licensor has no seat, residence or registered office inside+a European Union Member State.++Appendix++‘Compatible Licences’ according to Article 5 EUPL are:+— GNU General Public License (GPL) v. 2, v. 3+— GNU Affero General Public License (AGPL) v. 3+— Open Software License (OSL) v. 2.1, v. 3.0+— Eclipse Public License (EPL) v. 1.0+— CeCILL v. 2.0, v. 2.1+— Mozilla Public Licence (MPL) v. 2+— GNU Lesser General Public Licence (LGPL) v. 2.1, v. 3+— Creative Commons Attribution-ShareAlike v. 3.0 Unported (CC BY-SA 3.0) for works other than software+— European Union Public Licence (EUPL) v. 1.1, v. 1.2+— Québec Free and Open-Source Licence — Reciprocity (LiLiQ-R) or Strong Reciprocity (LiLiQ-R+).++The European Commission may update this Appendix to later versions of the above licences without producing+a new version of the EUPL, as long as they provide the rights granted in Article 2 of this Licence and protect the+covered Source Code from exclusive appropriation.+All other changes or additions to this Appendix require the production of a new EUPL version.
+ README.md view
@@ -0,0 +1,10 @@+# penelope-static++Domain package for penelope-static++## Modules+++## License++EUPL-1.2
+ penelope-static.cabal view
@@ -0,0 +1,118 @@+cabal-version: 3.0+name: penelope-static+version: 0.1.0.0+synopsis: Static Reflection and Cayley Analysis for Penelope Effect Engine+description:+ Static analysis substrate and Cayley representation for the Penelope+ polycategorical effect engine. Provides effect dependency graph+ extraction, algebraic circuit simplification, pipeline scheduling,+ and formal verification of institutional satisfaction properties.+license: EUPL-1.2+license-file: LICENSE+author: Nadia Yvette Chambers+maintainer: nadia.yvette.chambers@ik.me+category: Control+homepage: https://github.com/NadiaYvette/penelope+bug-reports: https://github.com/NadiaYvette/penelope/issues+extra-doc-files:+ README.md+ CHANGELOG.md+build-type: Simple+tested-with: GHC == 9.14.1++source-repository head+ type: git+ location: https://github.com/NadiaYvette/penelope+ subdir: packages/penelope-static++library+ exposed-modules:+ Penelope.Static+ Penelope.Static.Analysis+ hs-source-dirs: src+ default-language: Haskell2010+ default-extensions:+ AllowAmbiguousTypes+ BangPatterns+ DataKinds+ DerivingStrategies+ FlexibleContexts+ GADTs+ KindSignatures+ MagicHash+ OverloadedStrings+ PolyKinds+ RankNTypes+ ScopedTypeVariables+ TypeApplications+ TypeFamilies+ TypeOperators+ UnboxedTuples+ ghc-options: -Wall -Wcompat -Wredundant-constraints+ build-depends:+ base >= 4.14 && < 5,+ text >= 2.0 && < 2.2,+ containers >= 0.6 && < 0.9,+ primitive >= 0.9 && < 0.10,+ polytropos-core >= 0.1 && < 0.2,+ penelope-core >= 0.1 && < 0.2++test-suite tests+ type: exitcode-stdio-1.0+ main-is: Main.hs+ hs-source-dirs: test+ default-language: Haskell2010+ default-extensions:+ AllowAmbiguousTypes+ DataKinds+ GADTs+ MagicHash+ OverloadedStrings+ PolyKinds+ RankNTypes+ TypeApplications+ TypeOperators+ ghc-options: -Wall -Wcompat -Wredundant-constraints -threaded -rtsopts+ build-depends:+ base >= 4.14 && < 5,+ hspec >= 2.10 && < 2.12,+ text >= 2.0 && < 2.2,+ containers >= 0.6 && < 0.9,+ primitive >= 0.9 && < 0.10,+ polytropos-core >= 0.1 && < 0.2,+ polytropos-plugin >= 0.1 && < 0.2,+ penelope-core >= 0.1 && < 0.2,+ penelope-static++test-suite properties+ type: exitcode-stdio-1.0+ main-is: Properties.hs+ hs-source-dirs: test+ default-language: Haskell2010+ default-extensions:+ AllowAmbiguousTypes+ BangPatterns+ DataKinds+ DerivingStrategies+ FlexibleContexts+ GADTs+ MagicHash+ OverloadedStrings+ PolyKinds+ RankNTypes+ ScopedTypeVariables+ TypeApplications+ TypeFamilies+ TypeOperators+ ghc-options: -Wall -Wcompat -Wredundant-constraints -threaded -rtsopts+ build-depends:+ base >= 4.14 && < 5,+ hspec >= 2.10 && < 2.12,+ QuickCheck >= 2.14 && < 2.16,+ text >= 2.0 && < 2.2,+ containers >= 0.6 && < 0.9,+ primitive >= 0.9 && < 0.10,+ polytropos-core >= 0.1 && < 0.2,+ polytropos-plugin >= 0.1 && < 0.2,+ penelope-core >= 0.1 && < 0.2,+ penelope-static
+ src/Penelope/Static.hs view
@@ -0,0 +1,17 @@+{- |+Module : Penelope.Static+Description : High-level re-export facade for penelope-static+Copyright : (c) 2026 The Penelope Authors+License : EUPL-1.2 OR Apache-2.0+Maintainer : nadia.yvette.chambers@ik.me+Stability : experimental+Portability : non-portable (GHC extensions)++Provides static analysis, reflection, and liveness telemetry for Penelope pipelines.+See Note [Static Reflection and Cayley Analysis] [ref:note-static-cayley].+-}+module Penelope.Static+ ( module Penelope.Static.Analysis+ ) where++import Penelope.Static.Analysis
+ src/Penelope/Static/Analysis.hs view
@@ -0,0 +1,247 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UnboxedTuples #-}++{- |+Module : Penelope.Static.Analysis+Description : Static pre-execution Cayley analysis, capability extraction, and liveness analysis+Copyright : (c) 2026 The Penelope Authors+License : EUPL-1.2 OR Apache-2.0+Maintainer : nadia.yvette.chambers@ik.me+Stability : experimental+Portability : non-portable (GHC extensions)++Provides compile-time and pre-execution static inspection of Penelope pipelines without+evaluating runtime payloads.+See Note [Static Reflection and Cayley Analysis] [ref:note-static-cayley].+-}+module Penelope.Static.Analysis+ ( -- * Static Accumulator+ StaticPenelope (..)+ , annotateStatic+ , seqStatic+ , frameWireStatic++ -- * Phantom Port Frame Construction+ , phantomFrame++ -- * Liveness and Capability Telemetry+ , LivenessReport (..)+ , morphReadSet+ , analyzeLivenessAndEffects+ ) where++import Data.Functor.Identity (Identity (..))+import Data.IntSet (IntSet)+import qualified Data.IntSet as IntSet+import Data.Kind (Type)+import Data.Primitive.PrimArray (sizeofPrimArray)+import Data.Primitive.SmallArray (indexSmallArray, newSmallArray, runSmallArray, sizeofSmallArray)+import GHC.Exts (Int (..), unsafeCoerce#, word2Int#)+import Penelope.Core+ ( BranchCont (..)+ , Penelope (..)+ , PolyEffect+ , PolyHEffect+ , PortSig (..)+ , Region (..)+ , (>&>)+ , seqPenelope+ )+import Polytropos (Record, RowOf)+import Polytropos.Core (Rep (..), RowRep (..))+import Polytropos.RowMorph+ ( FrameWire (..)+ , RowMorph (..)+ , indexRowMorph+ )++{- |+Cayley static wrapper generalizing static effect accumulators to (m, n, k, r)-ary graphs.+Pairs an Applicative metadata accumulator @f ()@ with an executable 'Penelope' pipeline.++See Note [Static Reflection and Cayley Analysis] [ref:note-static-cayley].+-}+data StaticPenelope+ (f :: Type -> Type)+ (eh :: RowOf PolyHEffect)+ (ef :: RowOf PolyEffect)+ (ins :: RowOf Type)+ (outs :: RowOf Type)+ = StaticPenelope+ { spStatic :: !(f ())+ , spPipeline :: !(Penelope eh ef ins outs)+ }++-- | Attach a static Applicative metadata requirement to any Penelope computation.+{-# INLINE annotateStatic #-}+annotateStatic ::+ f ()+ -> Penelope eh ef ins outs+ -> StaticPenelope f eh ef ins outs+annotateStatic !meta !pipe = StaticPenelope meta pipe++-- | Sequential composition accumulates static metadata via '*>' in O(1).+{-# INLINE seqStatic #-}+seqStatic ::+ Applicative f =>+ StaticPenelope f eh ef a b+ -> StaticPenelope f eh ef b c+ -> StaticPenelope f eh ef a c+seqStatic (StaticPenelope s1 p1) (StaticPenelope s2 p2) =+ StaticPenelope (s1 *> s2) (p1 `seqPenelope` p2)++-- | Frame-rule auto-wiring preserving and combining static metadata.+{-# INLINE frameWireStatic #-}+frameWireStatic ::+ forall (frameIn :: RowOf Type) (ins1 :: RowOf Type) (outs1 :: RowOf Type)+ (frameMid :: RowOf Type) (ins2 :: RowOf Type) (outs2 :: RowOf Type)+ (frameOut :: RowOf Type)+ (eh :: RowOf PolyHEffect) (ef :: RowOf PolyEffect)+ f.+ ( Applicative f+ , FrameWire frameIn ins1 outs1 frameMid+ , FrameWire frameMid ins2 outs2 frameOut+ ) =>+ StaticPenelope f eh ef ins1 outs1+ -> StaticPenelope f eh ef ins2 outs2+ -> StaticPenelope f eh ef frameIn frameOut+frameWireStatic (StaticPenelope s1 p1) (StaticPenelope s2 p2) =+ StaticPenelope (s1 *> s2) ((>&>) @_ @_ @_ @frameMid p1 p2)++{- |+Construct a phantom port frame for traversing downstream continuations without evaluating payloads.+Uses uninitialized/dummy identity slots that do not throw exceptions.++See Note [Static Reflection and Cayley Analysis] [ref:note-static-cayley].+-}+{-# INLINE phantomFrame #-}+phantomFrame :: Int -> Record r+phantomFrame !numPorts = RowRep $ Rep 0 $ runSmallArray $ do+ m <- newSmallArray numPorts (Identity (unsafeCoerce# ()))+ pure m++{- |+Static telemetry collected across the hypergraph without executing a single effect handler.++See Note [Static Reflection and Cayley Analysis] [ref:note-static-cayley].+-}+data LivenessReport = LivenessReport+ { lrReadFrameSlots :: !IntSet+ -- ^ Indices of input ports in @ins@ that are actually read by at least one operation.+ , lrActiveFirstOrder :: !IntSet+ -- ^ Slot indices in @ef@ actually invoked in the graph (for dead-handler pruning).+ , lrActiveHigherOrder :: !IntSet+ -- ^ Slot indices in @eh@ actually invoked in the graph.+ , lrTotalRegions :: !Int+ -- ^ Total number of nested higher-order regions ('OpH') in the graph.+ , lrMaxBranchingFactor :: !Int+ -- ^ Maximum exit arity encountered across all operations.+ } deriving stock (Show, Eq)++instance Semigroup LivenessReport where+ LivenessReport r1 f1 h1 reg1 b1 <> LivenessReport r2 f2 h2 reg2 b2 =+ LivenessReport+ (IntSet.union r1 r2)+ (IntSet.union f1 f2)+ (IntSet.union h1 h2)+ (reg1 + reg2)+ (max b1 b2)++instance Monoid LivenessReport where+ mempty = LivenessReport IntSet.empty IntSet.empty IntSet.empty 0 1++-- | Extract the set of frame slot indices read by a 'RowMorph'.+{-# INLINE morphReadSet #-}+morphReadSet :: RowMorph a b -> IntSet+morphReadSet (RowMorph primArr) =+ let !n = sizeofPrimArray primArr+ collect !i !acc+ | i >= n = acc+ | otherwise = collect (i + 1) (IntSet.insert (indexRowMorph (RowMorph primArr) i) acc)+ in collect 0 IntSet.empty++{- |+Universal structural liveness and effect footprint analysis pass.+Directly inspects unpacked constructor tags, 'RowMorph' primitive arrays, and 'Record' lengths.++See Note [Static Reflection and Cayley Analysis] [ref:note-static-cayley].+-}+analyzeLivenessAndEffects ::+ forall eh ef ins outs.+ Penelope eh ef ins outs+ -> LivenessReport+analyzeLivenessAndEffects = go+ where+ analyzeRegionArr :: Record regions -> (Int, LivenessReport)+ analyzeRegionArr (RowRep (Rep _ arr)) =+ let !rCount = sizeofSmallArray arr+ step !i !acc+ | i >= rCount = acc+ | otherwise =+ case (unsafeCoerce# (indexSmallArray arr i) :: Region eh ef ('PortSig ins outs)) of+ Region sub -> step (i + 1) (acc <> analyzeLivenessAndEffects sub)+ in (rCount, step 0 mempty)++ analyzeContArr :: Record exits -> (Int, LivenessReport)+ analyzeContArr (RowRep (Rep _ arr)) =+ let !kCount = sizeofSmallArray arr+ step !i !acc+ | i >= kCount = acc+ | otherwise =+ let !(BranchCont kFn) = unsafeCoerce# (indexSmallArray arr i)+ in step (i + 1) (acc <> go (kFn (phantomFrame 64)))+ in (kCount, step 0 mempty)++ go :: Penelope eh ef ins outs -> LivenessReport+ go = \case+ Route morph ->+ mempty { lrReadFrameSlots = morphReadSet morph }++ LiftPure inMap _ (BranchCont kFn) ->+ mempty { lrReadFrameSlots = morphReadSet inMap }+ <> go (kFn (phantomFrame 64))++ OpF tag# inMap _ conts ->+ let !slotIdx = I# (word2Int# tag#)+ (!k, contReport) = analyzeContArr conts+ in LivenessReport+ { lrReadFrameSlots = morphReadSet inMap+ , lrActiveFirstOrder = IntSet.singleton slotIdx+ , lrActiveHigherOrder = IntSet.empty+ , lrTotalRegions = 0+ , lrMaxBranchingFactor = k+ } <> contReport++ OpH tag# inMap regions _ conts ->+ let !slotIdx = I# (word2Int# tag#)+ (!r, regReport) = analyzeRegionArr regions+ (!k, contReport) = analyzeContArr conts+ in LivenessReport+ { lrReadFrameSlots = morphReadSet inMap+ , lrActiveFirstOrder = IntSet.empty+ , lrActiveHigherOrder = IntSet.singleton slotIdx+ , lrTotalRegions = r+ , lrMaxBranchingFactor = k+ } <> regReport <> contReport++ ScopeRow (RowMorph ehMap) (RowMorph efMap) subPipe ->+ let inner = analyzeLivenessAndEffects subPipe+ remapSet primArr s =+ IntSet.fromList [ indexRowMorph (RowMorph primArr) i | i <- IntSet.toList s ]+ in inner+ { lrActiveHigherOrder = remapSet ehMap (lrActiveHigherOrder inner)+ , lrActiveFirstOrder = remapSet efMap (lrActiveFirstOrder inner)+ }
+ test/Main.hs view
@@ -0,0 +1,93 @@+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# OPTIONS_GHC -fplugin=Polytropos.Plugin #-}++module Main (main) where++import qualified Data.IntSet as IntSet+import GHC.Exts (unsafeCoerce#)+import Penelope.Core+import Penelope.Static+import Polytropos (Field (..), emptyRecord, insertField)+import Polytropos.Core (Pair (..))+import Polytropos.RowMorph (KnownRowMorph (..))+import Test.Hspec++data TestGet :: PolyEffect+data TestPut :: PolyEffect+type TestEF = '["get" ':= TestGet, "put" ':= TestPut]++data TestCatch :: PolyHEffect+type TestEH = '["catch" ':= TestCatch]++main :: IO ()+main = hspec $ do+ describe "Penelope.Static.Analysis" $ do+ it "constructs StaticPenelope and accumulates metadata via seqStatic" $ do+ let p1 :: Penelope '[] '[] '["x" ':= Int] '["x" ':= Int]+ p1 = route+ p2 :: Penelope '[] '[] '["x" ':= Int] '["x" ':= Int]+ p2 = route++ s1 = annotateStatic (Just ()) p1+ s2 = annotateStatic (Just ()) p2+ sComp = seqStatic s1 s2++ case spStatic sComp of+ Just () -> (1 :: Int) `shouldBe` 1+ _ -> expectationFailure "Expected Just () metadata"++ it "extracts active first-order effects and port liveness" $ do+ let m = rowMorph @'["x" ':= Int] @'["x" ':= Int, "y" ':= String]+ retCont = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int])+ conts = insertField (Field @"ret") retCont emptyRecord+ term :: Penelope '[] TestEF '["x" ':= Int, "y" ':= String] '["x" ':= Int]+ term = OpF 0## m (unsafeCoerce# (42 :: Int)) conts++ report = analyzeLivenessAndEffects term++ IntSet.member 0 (lrActiveFirstOrder report) `shouldBe` True+ IntSet.member 0 (lrReadFrameSlots report) `shouldBe` True+ lrTotalRegions report `shouldBe` 0+ lrMaxBranchingFactor report `shouldBe` 1++ it "extracts higher-order regions and branch continuations" $ do+ let m = rowMorph @'["x" ':= Int] @'["x" ':= Int]+ retCont = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int])+ conts = insertField (Field @"ret") retCont emptyRecord+ subProg :: Penelope '[] '[] '["x" ':= Int] '["x" ':= Int]+ subProg = Route m+ reg = Region @'[] @'[] @('PortSig '["x" ':= Int] '["x" ':= Int]) subProg+ regions = insertField (Field @"body") reg emptyRecord+ term :: Penelope TestEH '[] '["x" ':= Int] '["x" ':= Int]+ term = OpH 0## m regions (unsafeCoerce# ()) conts++ report = analyzeLivenessAndEffects term++ IntSet.member 0 (lrActiveHigherOrder report) `shouldBe` True+ lrTotalRegions report `shouldBe` 1+ lrMaxBranchingFactor report `shouldBe` 1++ it "analyzes 3-way exit branching factor" $ do+ let m = rowMorph @'["x" ':= Int] @'["x" ':= Int]+ branchOk = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int])+ branchRetry = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int])+ branchAbort = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int])+ handlers = insertField (Field @"ok") branchOk+ $ insertField (Field @"retry") branchRetry+ $ insertField (Field @"abort") branchAbort+ $ emptyRecord+ term :: Penelope '[] '[] '["x" ':= Int] '["x" ':= Int]+ term = OpF 0## m (unsafeCoerce# ()) handlers++ report = analyzeLivenessAndEffects term++ lrMaxBranchingFactor report `shouldBe` 3
+ test/Properties.hs view
@@ -0,0 +1,348 @@+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# OPTIONS_GHC -fplugin=Polytropos.Plugin #-}++{- |+Module : Main+Description : Milestone 6.2 Institutional Satisfaction & Reduct Property Tests+Copyright : (c) 2026 The Penelope Authors+License : EUPL-1.2 OR Apache-2.0+Maintainer : nadia.yvette.chambers@ik.me+Stability : experimental+Portability : non-portable (GHC extensions)++Property-tests fundamental institutional invariants of the Penelope engine:+1. Reduct-Evaluation Identity:+ eval_J(H, sigma_*(P)) === eval_I(sigma^*(H), P)+ across randomized row permutations, embeddings, and register frame inputs.+2. Static-Elaboration Commutativity:+ Static telemetry and metadata extracted by 'StaticPenelope' and+ 'analyzeLivenessAndEffects' commute with higher-order macro elaboration+ 'elaborateAll'.++See Note [Core Architecture] [ref:note-core-architecture],+Note [Institutional Satisfaction and Zero-Traversal Weakening] [ref:note-satisfaction-weakening],+Note [Two-Phase Weaving and Unweaving] [ref:note-two-phase-engine], and+Note [Static Reflection and Cayley Analysis] [ref:note-static-cayley].+-}+module Main (main) where++import Control.Monad (forM_)+import Data.Functor.Const (Const (..))+import Data.Functor.Identity (Identity (..))+import Data.Monoid (Sum (..))+import Data.Primitive.SmallArray (indexSmallArray, newSmallArray, runSmallArray, writeSmallArray)+import GHC.Exts (Any, unsafeCoerce#)+import Penelope.Core+import Penelope.Static+import Polytropos (Field (..), Record, emptyRecord, gatherRecord, insertField)+import Polytropos.Core (Pair (..), Rep (..), RowRep (..))+import Polytropos.RowMorph (composeRowMorph, rowMorph, unsafeMkRowMorph)+import Test.Hspec+import Test.Hspec.QuickCheck (prop)+import Test.QuickCheck++-- Effect signatures for sub-row I+data OpAdd :: PolyEffect+data OpMul :: PolyEffect+data OpSet :: PolyEffect+type SubEF = '["add" ':= OpAdd, "mul" ':= OpMul, "set" ':= OpSet]++data OpScoped :: PolyHEffect+type SubEH = '["scoped" ':= OpScoped]++-- Algebraic command language+data Command+ = CmdAdd !Int+ | CmdMul !Int+ | CmdSet !Int+ | CmdScopedAdd !Int+ deriving stock (Show, Eq)++instance Arbitrary Command where+ arbitrary = oneof+ [ CmdAdd <$> choose (-50, 50)+ , CmdMul <$> choose (-5, 5)+ , CmdSet <$> choose (-100, 100)+ , CmdScopedAdd <$> choose (-20, 20)+ ]++-- Distinct permutation generator for embedding [0, 1, 2] into [0 .. n-1]+data RowEmbedding = RowEmbedding+ { reWideSize :: !Int+ , reAddIdx :: !Int+ , reMulIdx :: !Int+ , reSetIdx :: !Int+ , reScopedIdx :: !Int+ , reWideHSize :: !Int+ } deriving stock (Show, Eq)++instance Arbitrary RowEmbedding where+ arbitrary = do+ wideN <- choose (4, 8)+ wideM <- choose (2, 5)+ -- Pick 3 distinct indices in [0 .. wideN - 1]+ p1 <- choose (0, wideN - 1)+ p2 <- suchThat (choose (0, wideN - 1)) (/= p1)+ p3 <- suchThat (choose (0, wideN - 1)) (\x -> x /= p1 && x /= p2)+ q1 <- choose (0, wideM - 1)+ pure $ RowEmbedding wideN p1 p2 p3 q1 wideM++-- Smart constructors for SubEF and SubEH operations+buildAdd :: Int -> Penelope SubEH SubEF '["x" ':= Int] '["x" ':= Int]+buildAdd k =+ let retCont = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int])+ conts = insertField (Field @"ret") retCont emptyRecord+ in OpF 0## (rowMorph @'["x" ':= Int] @'["x" ':= Int]) (unsafeCoerce# k) conts++buildMul :: Int -> Penelope SubEH SubEF '["x" ':= Int] '["x" ':= Int]+buildMul k =+ let retCont = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int])+ conts = insertField (Field @"ret") retCont emptyRecord+ in OpF 1## (rowMorph @'["x" ':= Int] @'["x" ':= Int]) (unsafeCoerce# k) conts++buildSet :: Int -> Penelope SubEH SubEF '["x" ':= Int] '["x" ':= Int]+buildSet k =+ let retCont = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int])+ conts = insertField (Field @"ret") retCont emptyRecord+ in OpF 2## (rowMorph @'["x" ':= Int] @'["x" ':= Int]) (unsafeCoerce# k) conts++buildScopedAdd :: Int -> Penelope SubEH SubEF '["x" ':= Int] '["x" ':= Int]+buildScopedAdd k =+ let retCont = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int])+ conts = insertField (Field @"ret") retCont emptyRecord+ subProg :: Penelope SubEH SubEF '["x" ':= Int] '["x" ':= Int]+ subProg = buildAdd k+ reg = Region @SubEH @SubEF @('PortSig '["x" ':= Int] '["x" ':= Int]) subProg+ regions = insertField (Field @"body") reg emptyRecord+ in OpH 0## (rowMorph @'["x" ':= Int] @'["x" ':= Int]) regions (unsafeCoerce# ()) conts++buildCommand :: Command -> Penelope SubEH SubEF '["x" ':= Int] '["x" ':= Int]+buildCommand (CmdAdd k) = buildAdd k+buildCommand (CmdMul k) = buildMul k+buildCommand (CmdSet k) = buildSet k+buildCommand (CmdScopedAdd k) = buildScopedAdd k++buildPipeline :: [Command] -> Penelope SubEH SubEF '["x" ':= Int] '["x" ':= Int]+buildPipeline [] = route+buildPipeline (c:cs) = buildCommand c `seqPenelope` buildPipeline cs++-- Concrete Handlers+addHandler :: Handler '[] (FrameKleisli Identity) OpAdd+addHandler = Handler $ \_inMap payload kConts ->+ let !(Identity elabK) = indexSmallArray (let RowRep (Rep _ arr) = kConts in arr) 0+ !(BranchCont retK) = unsafeCoerce# elabK+ !kVal = unsafeCoerce# payload :: Int+ in FrameKleisli $ \inF ->+ let !(Identity xVal) = indexSmallArray (let RowRep (Rep _ arr) = inF in arr) 0+ !curX = unsafeCoerce# xVal :: Int+ !newX = curX + kVal+ !outF = insertField (Field @"x") newX emptyRecord+ in runFrameKleisli (retK outF) outF++mulHandler :: Handler '[] (FrameKleisli Identity) OpMul+mulHandler = Handler $ \_inMap payload kConts ->+ let !(Identity elabK) = indexSmallArray (let RowRep (Rep _ arr) = kConts in arr) 0+ !(BranchCont retK) = unsafeCoerce# elabK+ !kVal = unsafeCoerce# payload :: Int+ in FrameKleisli $ \inF ->+ let !(Identity xVal) = indexSmallArray (let RowRep (Rep _ arr) = inF in arr) 0+ !curX = unsafeCoerce# xVal :: Int+ !newX = curX * kVal+ !outF = insertField (Field @"x") newX emptyRecord+ in runFrameKleisli (retK outF) outF++setHandler :: Handler '[] (FrameKleisli Identity) OpSet+setHandler = Handler $ \_inMap payload kConts ->+ let !(Identity elabK) = indexSmallArray (let RowRep (Rep _ arr) = kConts in arr) 0+ !(BranchCont retK) = unsafeCoerce# elabK+ !newX = unsafeCoerce# payload :: Int+ !outF = insertField (Field @"x") newX emptyRecord+ in FrameKleisli $ \_inF -> runFrameKleisli (retK outF) outF++dummyHandler :: Handler '[] (FrameKleisli Identity) OpAdd+dummyHandler = Handler $ \_ _ _ ->+ errorWithoutStackTrace "Properties: dummyHandler invoked — index dispatch violation!"++-- Concrete Elaborator for OpScoped+scopedElaborator :: Elaborator '[] SubEF OpScoped+scopedElaborator = Elaborator $ \inMap regs _ kConts ->+ let !(Identity elabBody) = indexSmallArray (let RowRep (Rep _ arr) = regs in arr) 0+ !(Region body) = unsafeCoerce# elabBody+ !(Identity elabK) = indexSmallArray (let RowRep (Rep _ arr) = kConts in arr) 0+ !(BranchCont retK) = unsafeCoerce# elabK+ in preComposeRoute inMap (unsafeCoerce# (body `seqPenelope` retK emptyRecord))++dummyElaborator :: Elaborator '[] SubEF OpScoped+dummyElaborator = Elaborator $ \_ _ _ _ ->+ errorWithoutStackTrace "Properties: dummyElaborator invoked — index dispatch violation!"++-- Make arbitrary-sized Record of handlers/elaborators+makeWideRecord :: Int -> [(Int, Any)] -> Any -> Record r+makeWideRecord !n !indexedEntries !dummy =+ RowRep $ Rep 0 $ runSmallArray $ do+ arr <- newSmallArray n (Identity dummy)+ forM_ indexedEntries $ \(idx, val) ->+ writeSmallArray arr idx (Identity val)+ pure arr++-- Extract 'x' from a frame+getX :: Record '["x" ':= Int] -> Int+getX (RowRep (Rep _ arr)) =+ let !(Identity x) = indexSmallArray arr 0+ in unsafeCoerce# x++main :: IO ()+main = hspec $ do+ describe "Penelope.Core Milestone 6.2: Institutional Satisfaction & Reduct Properties" $ do++ prop "Reduct-Evaluation Identity: eval_J(H, sigma_*(P)) === eval_I(sigma^*(H), P)" $+ \(commands :: [Command]) (emb :: RowEmbedding) (initX :: Int) ->+ let !pipe = buildPipeline commands+ !inFrame = insertField (Field @"x") initX emptyRecord++ -- Embeddings sigma_ef and sigma_eh+ !sigmaEf = unsafeMkRowMorph [reAddIdx emb, reMulIdx emb, reSetIdx emb]+ !sigmaEh = unsafeMkRowMorph [reScopedIdx emb]++ -- Wide handlers and elaborators for J+ !wideHandlers = makeWideRecord+ (reWideSize emb)+ [ (reAddIdx emb, unsafeCoerce# addHandler)+ , (reMulIdx emb, unsafeCoerce# mulHandler)+ , (reSetIdx emb, unsafeCoerce# setHandler)+ ]+ (unsafeCoerce# dummyHandler)++ !wideElabs = makeWideRecord+ (reWideHSize emb)+ [ (reScopedIdx emb, unsafeCoerce# scopedElaborator) ]+ (unsafeCoerce# dummyElaborator)++ -- 1. Weakened evaluation in J: eval_J(H, sigma_*(P))+ !pWeakened = weakenRowExplicit sigmaEh sigmaEf pipe+ !pWeakenedElab = elaborateAll wideElabs pWeakened+ !(Identity outJ) = runFrameKleisli (interpretAll wideHandlers pWeakenedElab) inFrame+ !resJ = getX outJ++ -- 2. Reduct evaluation in I: eval_I(sigma^*(H), P)+ !reductElabs = unsafeCoerce# (gatherRecord (unsafeCoerce# sigmaEh) wideElabs)+ !reductHandlers = unsafeCoerce# (gatherRecord (unsafeCoerce# sigmaEf) wideHandlers)+ !pReductElab = elaborateAll reductElabs pipe+ !(Identity outI) = runFrameKleisli (interpretAll reductHandlers pReductElab) inFrame+ !resI = getX outI++ in resJ === resI++ prop "Functorial Reduct Transitivity: (sigma2 . sigma1)^*(H) === sigma1^*(sigma2^*(H))" $+ \(commands :: [Command]) (initX :: Int) ->+ let !pipe = buildPipeline commands+ !inFrame = insertField (Field @"x") initX emptyRecord++ -- Intermediate row K (size 4), Final row J (size 6)+ !sigma1 = unsafeMkRowMorph [1, 2, 0] -- 3 -> 4+ !sigma2 = unsafeMkRowMorph [3, 1, 4, 0] -- 4 -> 6+ !sigmaComp = composeRowMorph sigma1 sigma2 -- 3 -> 6++ !wideHandlers6 = makeWideRecord+ 6+ [ (1, unsafeCoerce# addHandler)+ , (4, unsafeCoerce# mulHandler)+ , (3, unsafeCoerce# setHandler)+ ]+ (unsafeCoerce# dummyHandler)++ -- Single higher-order identity+ !idEh = unsafeMkRowMorph [0]+ !elabs1 = makeWideRecord 1 [(0, unsafeCoerce# scopedElaborator)] (unsafeCoerce# dummyElaborator)++ -- Two-step weakening vs composite weakening+ !pStep1 = weakenRowExplicit idEh sigma1 pipe+ !pStep2 = weakenRowExplicit idEh sigma2 pStep1+ !pStepElab = elaborateAll elabs1 pStep2+ !(Identity outTwoStep) = runFrameKleisli (interpretAll wideHandlers6 pStepElab) inFrame+ !resTwoStep = getX outTwoStep++ !pComp = weakenRowExplicit idEh sigmaComp pipe+ !pCompElab = elaborateAll elabs1 pComp+ !(Identity outComp) = runFrameKleisli (interpretAll wideHandlers6 pCompElab) inFrame+ !resComp = getX outComp++ in resTwoStep === resComp++ describe "Penelope.Static Milestone 6.2: Static-Elaboration Commutativity Properties" $ do++ prop "Metadata Conservation: spStatic (elaborateStatic elabs sp) === spStatic sp" $+ \(commands :: [Command]) (metaVal :: Int) ->+ let !pipe = buildPipeline commands+ !sp = annotateStatic (Const (Sum metaVal)) pipe+ !elabs = makeWideRecord 1 [(0, unsafeCoerce# scopedElaborator)] (unsafeCoerce# dummyElaborator)+ !spElab = StaticPenelope (spStatic sp) (elaborateAll elabs (spPipeline sp))+ in spStatic spElab === spStatic sp++ prop "Sequential Composition Commutativity: elaborate(sp1 >>> sp2) === elaborate(sp1) >>> elaborate(sp2)" $+ \(cmds1 :: [Command]) (cmds2 :: [Command]) (m1 :: Int) (m2 :: Int) (initX :: Int) ->+ let !p1 = buildPipeline cmds1+ !p2 = buildPipeline cmds2+ !sp1 = annotateStatic (Const (Sum m1)) p1+ !sp2 = annotateStatic (Const (Sum m2)) p2++ !elabs = makeWideRecord 1 [(0, unsafeCoerce# scopedElaborator)] (unsafeCoerce# dummyElaborator)+ !handlers = makeWideRecord+ 3+ [ (0, unsafeCoerce# addHandler)+ , (1, unsafeCoerce# mulHandler)+ , (2, unsafeCoerce# setHandler)+ ]+ (unsafeCoerce# dummyHandler)++ -- Composed then elaborated+ !composed = sp1 `seqStatic` sp2+ !spCompElab = StaticPenelope (spStatic composed) (elaborateAll elabs (spPipeline composed))++ -- Separately elaborated then composed+ !sp1Elab = StaticPenelope (spStatic sp1) (elaborateAll elabs (spPipeline sp1))+ !sp2Elab = StaticPenelope (spStatic sp2) (elaborateAll elabs (spPipeline sp2))+ !spSepElab = sp1Elab `seqStatic` sp2Elab++ -- Static metadata match+ !metaMatch = spStatic spCompElab == spStatic spSepElab++ -- Runtime execution match+ !inFrame = insertField (Field @"x") initX emptyRecord+ !(Identity outComp) = runFrameKleisli (interpretAll handlers (spPipeline spCompElab)) inFrame+ !(Identity outSep) = runFrameKleisli (interpretAll handlers (spPipeline spSepElab)) inFrame+ !execMatch = getX outComp == getX outSep++ in metaMatch && execMatch++ prop "Structural Liveness Invariant: port read footprint is invariant under elaborateAll" $+ \(commands :: [Command]) ->+ let !pipe = buildPipeline commands+ !elabs = makeWideRecord 1 [(0, unsafeCoerce# scopedElaborator)] (unsafeCoerce# dummyElaborator)+ !pipeElab = elaborateAll elabs pipe++ !repPre = analyzeLivenessAndEffects pipe+ !repPost = analyzeLivenessAndEffects pipeElab++ -- Port read set is strictly preserved+ !readSlotsPreserved = lrReadFrameSlots repPre == lrReadFrameSlots repPost++ -- Higher-order regions are unrolled to zero+ !regionsUnrolled = lrTotalRegions repPost == 0++ -- Branching factor bound is maintained+ !branchFactorSound = lrMaxBranchingFactor repPost <= max 1 (lrMaxBranchingFactor repPre)++ in readSlotsPreserved && regionsUnrolled && branchFactorSound