ENSAID.adoc

PanLL as eNSAID Reference Implementation

Table of Contents

• eNSAID Specification
• PanLL-Specific Extensions (Not in Spec)
  • TypeLL Verification Kernel
  • Code Readiness Grade (CRG)
  • Gossamer Backend
  • Academic Paper
• See Also

eNSAID Specification

The eNSAID specification lives in its own repository: ensaid-spec.

The spec defines the abstract architecture for neurosymbolic development workbenches. PanLL is the reference implementation. This document describes how PanLL implements each spec section — not the spec itself.

Spec Section	PanLL Implementation
01-binary-star	Model.res state tree, OrbitalSync.res engine, Δ divergence metric in GovernanceEngine.res
02-three-panel-model	View.res dispatches to Panel-L/N/W components. PanelSwitcher.res navigation. 108 panels across 3 panes.
03-cognitive-governance	AntiCrash.res gate (Γ function), VexometerEngine.res, InformationHumidityEngine.res, OrbitalDriftAuraEngine.res
04-panel-lifecycle	PanelRegistry.res state machine. TEA Model→Msg→Update→View cycle.
05-panel-contract	contracts/*.toml with Mustfile/Trustfile validators. ContractilesEngine.res enforcement.
06-panel-taxonomy	CladeBrowserEngine.res with 13 CladeKinds. Idris2 ABI in panel-clades/src/abi/Types.idr.
07-contractiles	ContractilesEngine.res — Strict/Warn/Adaptive modes. K9Engine.res validator execution.
08-constraint-propagation	TypeLL cross-panel verification. TypeLLEngine.res wires 48 panels.
09-translation-honesty	SeamEngine.res — 6 seams with drift detection. ProvenanceEngine.res trust levels.

PanLL-Specific Extensions (Not in Spec)

These are PanLL implementation choices, not eNSAID requirements:

TypeLL Verification Kernel

10-level type safety hierarchy:

• Levels 0-3: Standard type checking (ReScript compiler)

• Levels 4-6: Semantic types, refinement types, property verification

• Levels 7-9: Dependent types, temporal types, session types

• Level 10: Full formal verification (Idris2/ECHIDNA)

Code Readiness Grade (CRG)

PanLL grades every component X→A (Untested→Stable). Currently all panels are CRG D (Alpha). See docs/CRG-DOGFOOD-CHECKLIST.md for D→C promotion.

Gossamer Backend

PanLL uses Gossamer (Zig + WebKitGTK) as its native runtime, with Rust backend modules in src-gossamer/. The eNSAID spec is runtime-agnostic.

Academic Paper

The Binary Star model is formalised in: Binary Star: A Neurosymbolic IDE Architecture with Cognitive Governance and Constraint-Validated Human-AI Co-Orbit (LaTeX, targeted at arXiv).

See Also

• ensaid-spec — The specification

• README — Project overview

• Topology — System architecture map

• Design Decisions — DD records