commit 0ea1905068fded8f67cf5bbd7fa865a139e994c6
parent 1be8b9cbd562741d411ee2423018ed99dce78595
Author: James Eversole <james@eversole.co>
Date: Sat, 17 Oct 2026 12:19:37 -0500
Cache constructor-safe K pruning in stable lowering
Carry constructor shape and minimum free index on private residual nodes. Prune only independent constructor-only applications, preserve index shifting and diagnostics, and keep unknown/Fork calls and eta residual. Ordinary residual interfaces remain unchanged; emitted function representations intentionally differ from the retained stable compiler.
Add an opt-in authenticated source rebuild and independent set-based oracle: 196 bodies, 5292 complete results, nested/sparse summaries, opaque arguments, K/eta construction hazards, diagnostics and 46 local controls. Source cleanup exactly reproduces the benchmarked prototype's 17 public stable trees and 11 unit trees. nix flake check passes.
Candidate integration only: packaged compilers and fixtures remain unchanged. Scratch full-closure A/B evidence averaged 561.6s reference versus 438.3s candidate, but self-reproduction, cross-host acceptance, publication and rolling retention are still pending.
Diffstat:
4 files changed, 438 insertions(+), 40 deletions(-)
diff --git a/docs/validation.md b/docs/validation.md
@@ -1132,3 +1132,29 @@ conflicting parent declaration, verifies cache invalidation after a source edit,
negative cycle, missing-import, and source-collision controls. The deployment
check compiles the actual repository application via `tricu.workspace` and
exercises its server behavior.
+
+## Constructor-only K pruning (opt-in source check)
+
+This check rebuilds `source_stable` and `source_unit` from the working source
+with the packaged compiler, authenticating unchanged fixture dependencies. It
+checks the source implementation, not just the installed compiler's behavior:
+
+```sh
+nix develop -c python3 test/stable_constructor_k.py result/bin/tricu \
+ --directory "$WORK/constructor-k"
+```
+
+Use a fresh output directory. GHC and its dependencies are selected through
+Nix. The harness adds probe-only exports in its disposable workspace; cached
+residual helpers are not exported by the production module. The independent
+Haskell oracle uses full free-variable sets rather than the implementation's
+minimum-index summary. Checks cover successive annotated abstractions, sparse
+indices, constructor and unsafe-call classification, complete application
+results against a no-shortcut baseline, opaque arguments, closed-divergence
+construction, and diagnostic/remainder preservation. It also runs the local
+control corpus against the rebuilt unit compiler and audits native dependency
+pins and receipts. Children have explicit heap and time bounds.
+
+These finite controls are not a general termination or demand-equivalence
+proof. Compiler publication additionally requires the full reproduction,
+cross-host checks, and retention workflow in [compiler rebuilding](compiler-rebuilding.md.html).
diff --git a/lib/source/stable.tri b/lib/source/stable.tri
@@ -6,7 +6,23 @@
!import source_resolve *
!import source_program *
!import source_order *
-!export *
+!export stableTermApply
+!export stableApplication
+!export stableBracket
+!export stableEliminate
+!export stableI
+!export stableSelf
+!export stableWait
+!export stableWaitSelf
+!export stableFix
+!export stableBind
+!export stableCompileCore
+!export sourceDefinitionSelfRecursive
+!export sourceRecursiveFunction
+!export sourceRecursiveBody
+!export sourceStablePrepare
+!export orderStableProgram
+!export sourceCompileStableDefinition
-- Stable native abstraction backend. Selected explicitly by the unit/build API.
-- Barry Jay, Reflective Programs in Tree Calculus, sections 4.2, 4.4-4.5.
@@ -26,50 +42,109 @@ stableTermApply function argument location = (lazyBool
-- tricu's stem rule is t (t a) b c = a c (b c), unlike the book's
-- reversed b c (a c). Thus [x](u v) = t (t ([x]u)) ([x]v).
--- No independent-application K shortcut. Literal payloads are already
--- represented trees, not deferred applications.
+-- The annotated path below may prune independent constructor-only subtrees.
+-- Literal payloads are represented trees, not deferred applications.
stableApplication left right location = (stableTermApply
(stableTermApply (sourceTermLiteral t location)
(stableTermApply (sourceTermLiteral t location) left location) location)
right location)
-stableBracket term =
- lazyBool
- (_ : stableTermApply
- (sourceTermLiteral sourceCombK (sourceTermLocation term)) term
- (sourceTermLocation term))
- (_ : lazyBool
- (_ : lazyBool
- (_ : sourceTermLiteral sourceCombI (sourceTermLocation term))
- (_ : stableTermApply
- (sourceTermLiteral sourceCombK (sourceTermLocation term))
- (sourceTermVariable (pred_ (sourceTermPayload term))
- (sourceTermLocation term))
- (sourceTermLocation term))
- (isZero_? (sourceTermPayload term)))
- (_ : lazyBool
- (_ : stableApplication (stableBracket (fst (sourceTermPayload term)))
- (stableBracket (snd (sourceTermPayload term))) (sourceTermLocation term))
- (_ : term)
- (equal? (sourceTermKind term) 3))
- (equal? (sourceTermKind term) 2))
- (equal? (sourceTermKind term) 1)
-
-
--- Inspect only the kind before selecting payload access. Literal externals
--- remain opaque trees; lists retain residual constructor applications.
-stableEliminate node = (case sourceCoreKind node of
- ^sourceCoreLeafKind = sourceTermLiteral t (sourceCoreStart node)
- ^sourceCoreBoundKind = sourceTermVariable (sourceCorePayload node) (sourceCoreStart node)
- ^sourceCoreApplyKind = stableTermApply
- (stableEliminate (fst (sourceCorePayload node)))
- (stableEliminate (snd (sourceCorePayload node))) (sourceCoreStart node)
- ^sourceCoreLambdaKind = stableBracket (stableEliminate (sourceCorePayload node))
- ^sourceCoreExternalKind = sourceTermLiteral (sourceCorePayload node) (sourceCoreStart node)
- ^sourceCoreNumberKind = sourceTermLiteral (sourceCorePayload node) (sourceCoreStart node)
- ^sourceCoreStringKind = sourceTermLiteral (sourceCorePayload node) (sourceCoreStart node)
- ^sourceCoreListKind = sourceEliminateList (sourceCorePayload node) stableEliminate (sourceCoreStart node)
- _ = sourceTermInvalid node (sourceCoreStart node))
+-- Internal annotated residual: ((shape, minimum-free-index+1), ordinary node).
+-- Its application children are annotated, not ordinary sourceTerm values.
+-- Metadata is maintained as nodes are built, never by scanning a subtree at
+-- each bracket visit. A zero minimum denotes a closed subtree; one means the
+-- binder being eliminated occurs. Any larger minimum shifts down by one when
+-- removing an unused binder. Literal payloads are already represented trees.
+-- Shape certificates permit only Leaf/Stem construction with certified
+-- arguments. A variable is an opaque value, never a known callable shape.
+-- Fork applications, unknown calls and constructors containing computations
+-- remain residual; neither binder independence alone nor eta is sufficient.
+-- The ordinary residual API is restored at the public boundary. Keep both
+-- shape and dependency summaries out of executable trees and diagnostics.
+-- Zero bound means closed. Shapes: 0 computation, 1 Leaf, 2 Stem,
+-- 3 Fork, 4 opaque variable. Application children carry annotations too.
+stableCachedNode kind payload location shape bound =
+ pair (pair shape bound) (sourceTermNode kind payload location)
+stableCachedShape node = fst (fst node)
+stableCachedBound node = snd (fst node)
+stableCachedKind node = sourceTermKind (snd node)
+stableCachedPayload node = sourceTermPayload (snd node)
+stableCachedLocation node = sourceTermLocation (snd node)
+stableCachedLiteral tree location = stableCachedNode 1 tree location (triage 1 (_ : 2) (_ _ : 3) tree) 0
+stableCachedVariable index location = stableCachedNode 2 index location 4 (succ index)
+stableCachedMin left right = lazyBool (_ : right)
+ (_ : lazyBool (_ : left)
+ (_ : lazyBool (_ : left) (_ : right) (lte_? left right))
+ (isZero_? right)) (isZero_? left)
+stableCachedRawApply function argument location = (let shape = stableCachedShape function in
+ stableCachedNode 3 (pair function argument) location
+ (lazyBool
+ (_ : lazyBool (_ : 0) (_ : succ shape) (isZero_? (stableCachedShape argument)))
+ (_ : 0) (or? (equal? shape 1) (equal? shape 2)))
+ (stableCachedMin (stableCachedBound function) (stableCachedBound argument)))
+stableCachedApply function argument location = lazyBool
+ (_ : triage
+ (stableCachedLiteral (t (stableCachedPayload argument)) location)
+ (child : stableCachedLiteral (t child (stableCachedPayload argument)) location)
+ (_ _ : stableCachedRawApply function argument location)
+ (stableCachedPayload function))
+ (_ : stableCachedRawApply function argument location)
+ (and? (equal? (stableCachedKind function) 1) (equal? (stableCachedKind argument) 1))
+stableCachedApplication left right location = stableCachedApply
+ (stableCachedApply (stableCachedLiteral t location) (stableCachedApply (stableCachedLiteral t location) left location) location)
+ right location
+-- Precondition: the current binder is absent (minimum is not one).
+-- Closed subtrees need neither shifting nor copying. Remaining metadata can
+-- be shifted directly: no shape or dependency traversal is needed here.
+stableCachedLower term = lazyBool
+ (_ : term)
+ (_ : case stableCachedKind term of
+ 2 = stableCachedVariable (pred_ (stableCachedPayload term)) (stableCachedLocation term)
+ 3 = stableCachedNode 3 (pair (stableCachedLower (fst (stableCachedPayload term))) (stableCachedLower (snd (stableCachedPayload term))))
+ (stableCachedLocation term) (stableCachedShape term) (pred_ (stableCachedBound term))
+ _ = term)
+ (isZero_? (stableCachedBound term))
+stableCachedBracket term = case stableCachedKind term of
+ 1 = stableCachedApply (stableCachedLiteral sourceCombK (stableCachedLocation term)) term (stableCachedLocation term)
+ 2 = lazyBool
+ (_ : stableCachedLiteral sourceCombI (stableCachedLocation term))
+ (_ : stableCachedApply (stableCachedLiteral sourceCombK (stableCachedLocation term))
+ (stableCachedVariable (pred_ (stableCachedPayload term)) (stableCachedLocation term)) (stableCachedLocation term))
+ (isZero_? (stableCachedPayload term))
+ 3 = lazyBool
+ (_ : stableCachedApply (stableCachedLiteral sourceCombK (stableCachedLocation term)) (stableCachedLower term) (stableCachedLocation term))
+ (_ : stableCachedApplication (stableCachedBracket (fst (stableCachedPayload term)))
+ (stableCachedBracket (snd (stableCachedPayload term))) (stableCachedLocation term))
+ (and? (not? (equal? (stableCachedBound term) 1)) (not? (isZero_? (stableCachedShape term))))
+ _ = term
+stableCachedFromPlain term = case sourceTermKind term of
+ 1 = stableCachedLiteral (sourceTermPayload term) (sourceTermLocation term)
+ 2 = stableCachedVariable (sourceTermPayload term) (sourceTermLocation term)
+ 3 = stableCachedRawApply (stableCachedFromPlain (fst (sourceTermPayload term)))
+ (stableCachedFromPlain (snd (sourceTermPayload term))) (sourceTermLocation term)
+ _ = stableCachedNode (sourceTermKind term) (sourceTermPayload term) (sourceTermLocation term) 0 0
+stableCachedToPlain term = case stableCachedKind term of
+ 3 = sourceTermApply (stableCachedToPlain (fst (stableCachedPayload term)))
+ (stableCachedToPlain (snd (stableCachedPayload term))) (stableCachedLocation term)
+ _ = snd term
+stableCachedEliminate node = case sourceCoreKind node of
+ 1 = stableCachedLiteral t (sourceCoreStart node)
+ 2 = stableCachedVariable (sourceCorePayload node) (sourceCoreStart node)
+ 3 = stableCachedApply (stableCachedEliminate (fst (sourceCorePayload node)))
+ (stableCachedEliminate (snd (sourceCorePayload node))) (sourceCoreStart node)
+ 4 = stableCachedBracket (stableCachedEliminate (sourceCorePayload node))
+ 5 = stableCachedLiteral (sourceCorePayload node) (sourceCoreStart node)
+ 6 = stableCachedLiteral (sourceCorePayload node) (sourceCoreStart node)
+ 7 = stableCachedLiteral (sourceCorePayload node) (sourceCoreStart node)
+ 8 = (let rec elements pending = (lazyList
+ (_ : stableCachedLiteral t (sourceCoreStart node))
+ (head rest : stableCachedRawApply
+ (stableCachedRawApply (stableCachedLiteral t (sourceCoreStart node)) (stableCachedEliminate head) (sourceCoreStart node))
+ (elements rest) (sourceCoreStart node)) pending)
+ in elements (sourceCorePayload node))
+ _ = stableCachedNode 4 node (sourceCoreStart node) 0 0
+stableBracket term = stableCachedToPlain (stableCachedBracket (stableCachedFromPlain term))
+stableEliminate node = stableCachedToPlain (stableCachedEliminate node)
-- Native wait and Z, with self-first workers: Z f x = f (Z f) x.
-- All applications below construct trees out of already-normal arguments.
diff --git a/test/StableConstructorK.hs b/test/StableConstructorK.hs
@@ -0,0 +1,170 @@
+{-# LANGUAGE BangPatterns #-}
+-- Independent finite oracle for constructor-only K pruning. The model stores
+-- full free-variable sets (not the portable minimum-index cache). It retains
+-- a no-shortcut baseline and checks complete results, not DAG sizes.
+module Main where
+import Runtime
+import Wire
+import TreeObservation
+import qualified Data.ByteString as BS
+import qualified Data.Vector as V
+import qualified Data.Text as Text
+import qualified Data.Map.Strict as M
+import qualified Data.IntSet as S
+import Control.Monad
+import System.Environment
+load path = do
+ bytes<-BS.readFile path
+ b<-either error pure(decodeBundle bytes)
+ either error pure(verifyBundle b)
+ let ts=reconstructBundleTerms(bundleNodes b)
+ pure $ M.fromList[(Text.unpack(exportName e),ts V.! fromIntegral(exportRoot e))|e<-manifestExports(bundleManifest b)]
+p1(Fork a _)=a
+p1 _=error "pair"
+p2(Fork _ b)=b
+p2 _=error "pair"
+result(Fork (Stem Leaf) (Fork v _))=v
+result _=error "portable failure"
+list=either error id . toList
+number t=fromInteger(either error id(toNumber t))::Int
+payload=p1.p2
+-- Shape -1: unproved computation; -2: opaque value (free variable).
+-- 0/1/2: proved Leaf/Stem/Fork. Applications require safe operands and a
+-- known Leaf/Stem function; a Fork application is NEVER certified.
+data Term = Term !Int !S.IntSet !Int Residual
+data Residual = Lit T | Var Int | App Term Term
+shape(Term s _ _ _)=s
+vars(Term _ v _ _)=v
+size(Term _ _ n _)=n
+lit t=Term (case t of Leaf->0;Stem _->1;Fork _ _->2) S.empty 1 (Lit t)
+var n=Term (-2) (S.singleton n) 1 (Var n)
+app a b=Term sh (S.union(vars a)(vars b)) (1+size a+size b) (App a b)
+ where sh=if shape b/=(-1) && shape a `elem` [0,1] then shape a+1 else -1
+foldApp a@(Term _ _ _ (Lit f)) b@(Term _ _ _ (Lit x))=case f of
+ Leaf->lit(Stem x)
+ Stem y->lit(Fork y x)
+ _->app a b
+foldApp a b=app a b
+k=lit(Stem Leaf)
+i=lit(Fork(Stem(Stem Leaf))Leaf)
+application l r=foldApp (foldApp (lit Leaf)(foldApp(lit Leaf)l)) r
+-- Baseline abstraction deliberately has no K/eta shortcuts.
+baseline term@(Term _ _ _ node)=case node of
+ Lit _->foldApp k term
+ Var 0->i
+ Var n->foldApp k(var(n-1))
+ App a b->application(baseline a)(baseline b)
+run(Term _ _ _ node)=case node of
+ Lit t->t
+ Var _->error "open output"
+ App f x->apply(run f)(run x)
+lower term@(Term _ _ _ n)=case n of
+ Lit _->term
+ Var v->if v>0 then var(v-1) else error "lowered used binder"
+ App a b->app(lower a)(lower b)
+eligible term@(Term sh vs _ node)=case node of
+ App _ _->sh/=(-1) && not(S.member 0 vs)
+ _->False
+safeBracket term@(Term _ _ _ node)
+ | eligible term=foldApp k(lower term)
+ | otherwise=case node of
+ Lit _->foldApp k term
+ Var 0->i
+ Var n->foldApp k(var(n-1))
+ App a b->application(safeBracket a)(safeBracket b)
+encodeTerm (Term _ _ _ n)=case n of
+ Lit t->node 1 t
+ Var v->node 2(ofNumber(fromIntegral v))
+ App a b->node 3(Fork(encodeTerm a)(encodeTerm b))
+ where node k p=Fork(ofNumber k)(Fork p Leaf)
+checkMetadata term annotated=do
+ let wantedShape=case shape term of -1->0; -2->4; n->n+1
+ wantedBound=if S.null(vars term) then 0 else S.findMin(vars term)+1
+ unless(number(p1(p1 annotated))==wantedShape && number(p2(p1 annotated))==wantedBound)(error "cached summary mismatch")
+ case term of
+ Term _ _ _ (App a b)->do
+ let children=payload(p2 annotated)
+ checkMetadata a(p1 children)
+ checkMetadata b(p2 children)
+ _->pure ()
+main=do
+ [bundle,referenceBundle]<-getArgs
+ portable<-load bundle
+ let abstract=apply(portable M.! "stableBracket")
+ forceTreeShared(portable M.! "stableBracket")
+ let leaf=lit Leaf
+ unknown=app(var 1)(var 2)
+ checks=[("open stem",app leaf(var 1),True),
+ ("open fork",app(app leaf(var 1))(var 2),True),
+ ("third argument",app(app(app leaf(var 1))(var 2))(var 3),False),
+ ("unknown function",unknown,False),
+ ("unsafe child",app leaf unknown,False),
+ ("used binder",app leaf(var 0),False),
+ ("known stem",app(lit(Stem Leaf))(var 1),True)]
+ forM_ checks $ \(name,t,expected)->unless(eligible t==expected)(error name)
+ let atoms=[var 0,var 1,var 2,leaf,lit(Stem Leaf),lit(Fork Leaf Leaf),i]
+ level1=atoms++[foldApp a b|a<-atoms,b<-atoms]
+ terms=filter ((/=(-1)).shape)(atoms++[foldApp a b|a<-level1,b<-level1])
+ values=[Leaf,Stem Leaf,Fork Leaf Leaf]
+ forM_ terms $ \body->do
+ let step expected actual n=do
+ checkMetadata expected actual
+ unless(apply(portable M.! "stableCachedToPlain")actual==encodeTerm expected)(error "cached residual mismatch")
+ when(n>0)(step(safeBracket expected)(apply(portable M.! "stableCachedBracket")actual)(n-1))
+ step body (apply(portable M.! "stableCachedFromPlain")(encodeTerm body)) (3::Int)
+ let old=iterate baseline body!!3
+ forM_ (take 3(iterate safeBracket body)) $ \term ->
+ unless(abstract(encodeTerm term)==encodeTerm(safeBracket term))(error "portable/model abstraction differs")
+ let new=iterate safeBracket body!!3
+ oldTree=run old;newTree=run new
+ forceTreeShared oldTree
+ forceTreeShared newTree
+ forM_ values $ \a->forM_ values $ \b->forM_ values $ \c->
+ unless(foldl apply oldTree[a,b,c]==foldl apply newTree[a,b,c])(error "nested abstraction changed result")
+ -- Sparse/high indices and unsafe applications exercise summary maintenance
+ -- without assuming application termination. Compare cached annotations after
+ -- each abstraction, not after re-importing ordinary residuals.
+ let mixed=[app(lit Leaf)(var v)|v<-[0,1,7,63,256]]++
+ [app(var 7)(var 63),app(lit(Fork Leaf Leaf))(var 7),
+ app(lit Leaf)(app(var 7)(var 63)),
+ app(app(lit Leaf)(var 63))(var 0)]
+ forM_ mixed $ \body->do
+ let step expected actual n=do
+ checkMetadata expected actual
+ unless(apply(portable M.! "stableCachedToPlain")actual==encodeTerm expected)(error "sparse/unsafe residual mismatch")
+ when(n>0)(step(safeBracket expected)(apply(portable M.! "stableCachedBracket")actual)(n-1))
+ step body (apply(portable M.! "stableCachedFromPlain")(encodeTerm body)) (4::Int)
+ -- An opaque variable is only stored, never invoked or forced by a constructor.
+ let poison=error "opaque argument forced"::T
+ saved=run(safeBracket(safeBracket(app leaf(var 1))))
+ case apply(apply saved poison)Leaf of Stem _->pure();_->error "opaque constructor"
+ -- omega has a Fork function: it must not be evaluated during construction.
+ let ident=Fork(Stem(Stem Leaf))Leaf
+ self=Fork(Stem ident)ident
+ omega=app(lit self)(lit self)
+ unless(not(eligible omega) && not(eligible(app leaf omega)))(error "omega certified")
+ forceTreeShared(run(safeBracket omega))
+ -- Full portable bracket construction, without executing omega.
+ forceTreeShared(abstract(encodeTerm omega))
+ -- Demand-sensitive checks run actual portable-produced function trees too.
+ let node kind value=Fork(ofNumber kind)(Fork value(Fork Leaf Leaf))
+ lambda body=node 4 body
+ applyCore a b=node 3(Fork a b)
+ portableSaved=result(apply(portable M.! "stableCompileCore")
+ (lambda(lambda(applyCore(node 1 Leaf)(node 2(ofNumber 1))))))
+ forceTreeShared portableSaved
+ case apply(apply portableSaved poison)Leaf of Stem _->pure();_->error "portable opaque constructor"
+ let portableOmega=result(apply(portable M.! "stableCompileCore")
+ (lambda(applyCore(node 5 self)(node 5 self))))
+ forceTreeShared portableOmega
+ let portableEta=result(apply(portable M.! "stableCompileCore")
+ (lambda(applyCore (applyCore(node 5 self)(node 5 self)) (node 2 Leaf))))
+ forceTreeShared portableEta
+ reference<-load referenceBundle
+ let core kind value=Fork(ofNumber kind)(Fork value(Fork(ofNumber 23)(ofNumber 24)))
+ badVariable=core 2(ofNumber 3)
+ invalid=core 99 Leaf
+ application a b=core 3(Fork a b)
+ forM_ [badVariable,invalid,application badVariable invalid,application(core 1 Leaf)invalid] $ \input->
+ unless(apply(portable M.! "stableCompileCore")input==apply(reference M.! "source_stable.stableCompileCore")input)(error "core diagnostic/remainder mismatch")
+ putStrLn("PASS: "++show(length terms)++" constructor bodies under three nested binders; "++show(length terms*27)++" complete application results; classification, sparse indices, opaque arguments, K/eta construction hazards and diagnostic controls")
diff --git a/test/stable_constructor_k.py b/test/stable_constructor_k.py
@@ -0,0 +1,127 @@
+#!/usr/bin/env python3
+"""Opt-in current-source constructor-K check; never publishes compiler artifacts.
+
+The selected host must contain the authenticated packaged compiler. Unchanged
+fixture dependencies are source-verified; only source_stable and source_unit
+are rebuilt. Probe-only exports expose internal summaries to an independent
+finite oracle without making them part of the production interface.
+"""
+import argparse
+import hashlib
+import json
+from pathlib import Path
+import re
+import subprocess
+import time
+
+from bundle_dag import Intern, merge_bundles, read
+from fixture_sources import snapshot_bytes, verify
+from pattern_lowering import audit
+from shipped_compiler import verify as verify_compiler
+
+ROOT = Path(__file__).resolve().parent.parent
+
+
+def main():
+ p = argparse.ArgumentParser(description=__doc__)
+ p.add_argument('tricu', type=Path)
+ p.add_argument('--directory', type=Path, required=True)
+ p.add_argument('--expected-stable', type=Path, help='optional exact public-tree comparison against a prior prototype')
+ p.add_argument('--expected-unit', type=Path, help='optional exact source_unit comparison against a prior prototype')
+ args = p.parse_args()
+ root = args.directory.resolve()
+ root.mkdir(parents=True, exist_ok=False)
+ workspace = root / 'workspace'
+ workspace.mkdir()
+ (workspace / 'tricu.workspace').write_text('tricu.workspace.v1\n')
+ store = root / 'store'
+ host = args.tricu.resolve()
+ metadata = verify_compiler()
+ fixture_rows = {row[2]: row for row in verify(ROOT / 'test/fixtures')}
+ entries = {}
+ for row in (ROOT / 'bootstrap/compiler-source-map.v1').read_text().splitlines()[1:]:
+ _, alias, _, path, deps = row.split('\t')
+ entries[alias] = (path, [] if deps == '-' else deps.split(','))
+ affected = {'source_stable', 'source_unit'}
+ needed = set()
+
+ def visit(alias):
+ if alias in needed:
+ return
+ needed.add(alias)
+ for dep in entries[alias][1]:
+ visit(dep)
+ visit('source_unit')
+ for alias in needed - affected:
+ assert snapshot_bytes(ROOT / 'test/fixtures', fixture_rows[alias][4]) == (ROOT / entries[alias][0]).read_bytes(), ('stale reuse', alias)
+ report = dict(complete=False, compiler_sha256=metadata['sha256'],
+ harness_sha256=hashlib.sha256(Path(__file__).read_bytes()).hexdigest(),
+ oracle_sha256=hashlib.sha256((ROOT / 'test/StableConstructorK.hs').read_bytes()).hexdigest(),
+ runtime_sha256=hashlib.sha256(host.read_bytes()).hexdigest(), commands=[], reused={})
+ started = time.monotonic()
+
+ def command(argv, seconds=180):
+ result = subprocess.run(list(map(str, argv)), cwd=ROOT, capture_output=True,
+ text=True, timeout=seconds)
+ report['commands'].append(dict(argv=list(map(str, argv)), returncode=result.returncode,
+ stdout=result.stdout, stderr=result.stderr))
+ (root / 'report.json').write_text(json.dumps(report, indent=2) + '\n')
+ if result.returncode:
+ raise RuntimeError(result.stdout[-4000:] + result.stderr[-4000:])
+ return result.stdout
+
+ def run(options, seconds=180):
+ return command([host, 'arboricx', *options, '+RTS', '-N1', '-M4096m', '-RTS'], seconds)
+
+ active = affected | {dep for alias in affected for dep in entries[alias][1]}
+ for alias in sorted(active - affected):
+ cohort, _, _, _, source_pin = fixture_rows[alias]
+ fixture = ROOT / 'test/fixtures' / (cohort + '.arboricx')
+ bundle = root / (alias + '.arboricx')
+ merge_bundles(bundle, [(fixture, [(name, name[len(alias)+1:]) for name in read(fixture)[3]
+ if name.startswith(alias + '.')])], prune_unreachable=True)
+ pin = re.search(r'Created module alias .* -> ([0-9a-f]{64})',
+ run(['import', '--file', bundle, '--store', store]))[1]
+ (workspace / (alias + '.tri')).write_text('!export * from ' + pin + '\n')
+ report['reused'][alias] = dict(manifest=pin, source_pin=source_pin)
+ for alias in affected:
+ source = (ROOT / entries[alias][0]).read_bytes()
+ report[alias + '_source_sha256'] = hashlib.sha256(source).hexdigest()
+ (workspace / (alias + '.tri')).write_bytes(source)
+ probes = ['stableCachedFromPlain', 'stableCachedToPlain', 'stableCachedBracket']
+ stable_path = workspace / 'source_stable.tri'
+ stable_path.write_text(''.join('!export ' + name + '\n' for name in probes) + stable_path.read_text())
+ for alias in ['source_unit', 'source_stable']:
+ run(['compile', '--file', workspace / (alias + '.tri'), '--store', store,
+ '--output', root / (alias + '.arboricx'), '--compile-timeout', '280'], 300)
+ report['modules'] = audit(workspace, store, metadata['sha256'], report['reused'])
+ for alias, expected in [('source_stable', args.expected_stable), ('source_unit', args.expected_unit)]:
+ if expected:
+ intern = Intern()
+ def roots(path):
+ _, _, nodes, exports, _ = read(path)
+ ids = intern.graph(nodes)
+ return {name: ids[value] for name, value in exports.items()}
+ actual, before = roots(root / (alias + '.arboricx')), roots(expected)
+ selected = set(actual) - set(probes)
+ assert all(name in before and actual[name] == before[name] for name in selected), alias
+ report[alias + '_exact_public_exports'] = len(selected)
+ # GHC and all packages come from Nix. No cabal calls or ambient GHC.
+ expression = ('let f=builtins.getFlake "git+file://' + str(ROOT) + '";'
+ 'p=f.inputs.nixpkgs.legacyPackages.x86_64-linux;'
+ 'in p.haskellPackages.ghcWithPackages(h:[h.cryptonite h.memory h.base16-bytestring h.vector])')
+ command(['nix', 'shell', '--impure', '--expr', expression, '--command', 'ghc', '-O2', '-rtsopts',
+ '-XOverloadedStrings', '-XLambdaCase', '-XMultiWayIf', '-XScopedTypeVariables',
+ '-isrc', '-outputdir', root / 'objects', ROOT / 'test/StableConstructorK.hs',
+ '-o', root / 'controls'], 300)
+ command([root / 'controls', root / 'source_stable.arboricx',
+ ROOT / 'test/fixtures/compiler-library.arboricx', '+RTS', '-M2048m', '-RTS'])
+ command(['python3', ROOT / 'test/local_control.py', host, '--unit', root / 'source_unit.arboricx',
+ '--directory', root / 'local-controls'], 300)
+ report.update(complete=True, seconds=time.monotonic() - started)
+ (root / 'report.json').write_text(json.dumps(report, indent=2) + '\n')
+ print('PASS: constructor-K cached invariants, independent results/demand/diagnostics, local controls and provenance')
+
+
+if __name__ == '__main__':
+ main()
