commit cfae3f982017b0ab2af85358c0311a43c010bb7b
parent 08a004a8043e5926cd0724e53eb1ceb58b3055a6
Author: James Eversole <james@eversole.co>
Date: Sat, 17 Oct 2026 19:39:34 -0500
Bound digest-byte validation with structural steps
Preserve legacy malformed-tree fallback and demand order; replace numeric bit countdown with eight fixed structural steps. Independent source-rebuilt controls, complete native outputs, and matched full compiler closure checks passed. Haskell full-build mean improved 6.0%; Zig paired sample 5.3%. Compiler reproduction and publication are pending.
Diffstat:
4 files changed, 205 insertions(+), 8 deletions(-)
diff --git a/docs/validation.md b/docs/validation.md
@@ -1200,3 +1200,26 @@ These finite controls establish behavior for the tested cases. General
termination and demand equivalence require separate proof. Compiler publication
additionally requires the full reproduction, cross-host checks, and retention
workflow in [compiler rebuilding](compiler-rebuilding.md.html).
+
+## Digest-byte validation (opt-in source check)
+
+Rebuild the current `source_object` module against source-authenticated fixture
+dependencies and check its private byte guard and public digest predicate:
+
+```sh
+nix develop -c python3 test/digest_byte.py result/bin/tricu \
+ --directory "$WORK/digest-byte"
+```
+
+Use a fresh directory. The harness adds private probe exports only in its
+disposable workspace, audits native manifests and receipts, and builds the
+independent Haskell observer through Nix. Canonical bytes are checked against a
+bounded structural model; malformed trees retain the separately modeled legacy
+predecessor/comparison behavior. Cases cover all byte values, out-of-range
+naturals, malformed bits/tails, the eight-bit boundary, complete 64-byte digests,
+wrong lengths, and ignored/demanded poison payloads. Each observed result is
+compared completely, not by a prefix or hash alone.
+
+These finite controls are not compiler acceptance or a general demand-equivalence
+proof. Publication still requires the reproduction, cross-host, site-refresh and
+retention workflow in [compiler rebuilding](compiler-rebuilding.md.html).
diff --git a/lib/source/object.tri b/lib/source/object.tri
@@ -95,18 +95,26 @@ sourceObjectDigest domain payload =
sourceObjectByteLeaf? value = triage true (_ : false) (_ _ : false) value
sourceObjectByteBit? value = triage true (child : sourceObjectByteLeaf? child) (_ _ : false) value
sourceObjectByteOne? value = triage false (child : sourceObjectByteLeaf? child) (_ _ : false) value
-sourceObjectByteWithin value budget = (triage
+-- Eight statically bounded structural steps avoid numeric countdown work for
+-- every digest byte. Inspect the rest shape before the bit, as in the bounded
+-- recognizer; an invalid bit or exhausted bound must not force deeper fields.
+sourceObjectByteStep next value = (triage
true
(_ : false)
(bit rest : lazyBool
- (_ : lazyBool
- (_ : sourceObjectByteOne? bit)
- (_ : andLazy? (sourceObjectByteBit? bit) (_ : sourceObjectByteWithin rest (pred_ budget)))
- (sourceObjectByteLeaf? rest))
- (_ : false)
- (not? (isZero_? budget)))
+ (_ : sourceObjectByteOne? bit)
+ (_ : andLazy? (sourceObjectByteBit? bit) (_ : next rest))
+ (sourceObjectByteLeaf? rest))
+ value)
+sourceObjectCanonicalByte value = (sourceObjectByteStep
+ (sourceObjectByteStep
+ (sourceObjectByteStep
+ (sourceObjectByteStep
+ (sourceObjectByteStep
+ (sourceObjectByteStep
+ (sourceObjectByteStep
+ (sourceObjectByteStep sourceObjectByteLeaf?)))))))
value)
-sourceObjectCanonicalByte value = sourceObjectByteWithin value 8
-- This compatibility path must not call base's canonical-only arithmetic.
-- The historical predecessor leaves Stem values unchanged and interprets any
-- non-Leaf bit/tail as truthy. Comparison counts down its finite byte bound;
diff --git a/test/DigestByte.hs b/test/DigestByte.hs
@@ -0,0 +1,65 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+module Main where
+import Runtime
+import Wire
+import qualified Data.ByteString as B
+import qualified Data.Text as T
+import qualified Data.Vector as V
+import qualified Data.Map.Strict as M
+import Control.Exception
+import Control.Monad
+import System.Environment
+-- Independent bounded recognizer and historical arbitrary-tree arithmetic.
+-- The byte guard is not allowed to silently redefine malformed naturals.
+canonical :: T -> Int -> Bool
+canonical Leaf _=True
+canonical (Stem _) _=False
+canonical (Fork bit rest) depth
+ | depth==0=False
+ | rest==Leaf=bit==Stem Leaf
+ | otherwise=(bit==Leaf || bit==Stem Leaf) && canonical rest (depth-1)
+predRef :: T -> T
+predRef Leaf=Leaf
+predRef x@(Stem _)=x
+predRef(Fork bit rest)=if bit/=Leaf then if rest/=Leaf then Fork Leaf rest else Leaf else Fork(Stem Leaf)(predRef rest)
+lte :: T -> Integer -> Bool
+lte Leaf _=True
+lte _ 0=False
+lte value n=lte(predRef value)(n-1)
+lt :: T -> Integer -> Bool
+lt value n=lte value n && value/=ofNumber n
+hex :: T -> Bool
+hex value=(not(lt value 48) && lte value 57)||(not(lt value 97)&<e value 102)
+small :: Int -> [T]
+small 0=[Leaf]
+small n=Leaf:[Stem x|x<-small(n-1)]++[Fork x y|x<-small(n-1),y<-small(n-1)]
+truth True=Stem Leaf
+truth False=Leaf
+observe x=(evaluate x >>= \v->evaluate(if v==Leaf then "false" else if v==Stem Leaf then "true" else "bad")) `catch` \(_::ErrorCall)->pure "demanded-poison"
+main=do
+ [file]<-getArgs
+ bundle<-B.readFile file >>= either fail pure.decodeBundle
+ either fail pure(verifyBundle bundle)
+ let nodes=reconstructBundleTerms(bundleNodes bundle);workers=M.fromList[(T.unpack(exportName e),nodes V.!fromIntegral(exportRoot e))|e<-manifestExports(bundleManifest bundle)]
+ call name value=apply(workers M.!name)value
+ do
+ let values=map ofNumber[0..1024]++small 3++[foldr Fork x(replicate n b)|n<-[0..10],b<-[Leaf,Stem Leaf,Fork Leaf Leaf,Stem(Stem Leaf)],x<-small 2]
+ do
+ forM_ values $ \v->do
+ unless(call "sourceObjectCanonicalByte" v==truth(canonical v 8))(fail "canonical mismatch")
+ unless(call "sourceObjectHashByte?" v==truth(hex v))(fail "legacy hash-byte mismatch")
+ unless(call "sourceObjectHashValid" (ofList(replicate 63(ofNumber 48)++[v]))==truth(hex v))
+ (fail "complete digest mismatch")
+ forM_ [0..255] $ \n->unless(call "sourceObjectHashByte?" (ofNumber n)==truth(n>=48 && n<=57 || n>=97 && n<=102))(fail "ASCII mismatch")
+ let bad=error "poison";poisons=[Stem bad,Fork bad Leaf,Fork(Stem bad)Leaf,Fork Leaf(Stem bad),Fork(Fork Leaf Leaf)bad,foldr Fork (Fork bad bad)(replicate 8 Leaf)]
+ forM_ poisons $ \v->do
+ got<-observe(call "sourceObjectCanonicalByte" v);wanted<-observe(truth(canonical v 8));unless(got==wanted)(fail "canonical demand mismatch")
+ forM_ [0,1,63,64,65] $ \n->do
+ let good=ofList(replicate n(ofNumber 48));bad=ofList(replicate n(ofNumber 71))
+ unless(call "sourceObjectHashValid" good==truth(n==64))(fail "hash length mismatch")
+ unless(call "sourceObjectHashValid" bad==Leaf)(fail "invalid hash accepted")
+ forM_ [0,1,63,65] $ \n->do
+ got<-observe(call "sourceObjectHashValid" (ofList(replicate n(error "ignored byte"))));unless(got=="false")(fail "length rejection forced bytes")
+ rejected<-observe(call "sourceObjectHashValid" (ofList(ofNumber 71:replicate 63(error "unused byte"))))
+ unless(rejected=="false")(fail "invalid byte forced suffix payloads")
+ print(length values,"byte and complete-digest cases; ASCII, length and poison controls passed")
diff --git a/test/digest_byte.py b/test/digest_byte.py
@@ -0,0 +1,101 @@
+#!/usr/bin/env python3
+"""Rebuild source_object and test digest bytes against independent host models.
+
+Dependencies are reused only after checking their frozen sources against the
+working tree. Probe exports are confined to the disposable workspace. This does
+not publish or accept a compiler generation.
+"""
+import argparse
+import hashlib
+import json
+from pathlib import Path
+import re
+import subprocess
+
+from bundle_dag import merge_bundles, read
+from fixture_sources import snapshot_bytes, verify
+from native_header import native_header
+from pattern_lowering import audit
+from shipped_compiler import verify as verify_compiler
+
+ROOT = Path(__file__).resolve().parent.parent
+
+
+def main():
+ parser = argparse.ArgumentParser(description=__doc__)
+ parser.add_argument('tricu', type=Path)
+ parser.add_argument('--directory', type=Path, required=True)
+ args = parser.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()
+ compiler = verify_compiler()
+ source = (ROOT / 'lib/source/object.tri').read_bytes()
+ rows = {r[2]: r for r in verify(ROOT / 'test/fixtures')}
+ paths = {r.split('\t')[1]: r.split('\t')[3] for r in
+ (ROOT / 'bootstrap/compiler-source-map.v1').read_text().splitlines()[1:]}
+ report = dict(complete=False, compiler_sha256=compiler['sha256'],
+ runtime_sha256=hashlib.sha256(host.read_bytes()).hexdigest(),
+ source_sha256=hashlib.sha256(source).hexdigest(), reused={}, commands=[])
+
+ def command(argv, timeout=180):
+ cmd = list(map(str, argv))
+ out = subprocess.run(cmd, cwd=ROOT, capture_output=True, text=True, timeout=timeout)
+ report['commands'].append(dict(argv=cmd, code=out.returncode,
+ stdout=out.stdout, stderr=out.stderr))
+ (root / 'report.json').write_text(json.dumps(report, indent=2) + '\n')
+ if out.returncode:
+ raise RuntimeError(out.stdout[-4000:] + out.stderr[-4000:])
+ return out.stdout
+
+ def run(argv):
+ return command([host, 'arboricx', *argv, '+RTS', '-N1', '-M4096m', '-RTS'])
+
+ dependencies = native_header(source.decode())[0]
+ checked = set()
+
+ def check_source(alias):
+ if alias in checked:
+ return
+ checked.add(alias)
+ current = (ROOT / paths[alias]).read_bytes()
+ assert snapshot_bytes(ROOT / 'test/fixtures', rows[alias][4]) == current, ('stale dependency', alias)
+ for dep in native_header(current.decode())[0]:
+ check_source(dep)
+
+ for alias in dependencies:
+ check_source(alias)
+ cohort, _, _, _, source_pin = 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, '--indexed']))[1]
+ (workspace / (alias + '.tri')).write_text('!export * from ' + pin + '\n')
+ report['reused'][alias] = dict(manifest=pin, source_pin=source_pin)
+ (workspace / 'source_object.tri').write_bytes(
+ b'!export sourceObjectCanonicalByte\n!export sourceObjectHashByte?\n' + source)
+ candidate = root / 'source_object.arboricx'
+ run(['compile', '--file', workspace / 'source_object.tri', '--store', store,
+ '--output', candidate, '--compile-timeout', '150'])
+ report['modules'] = audit(workspace, store, compiler['sha256'], report['reused'])
+ expr = ('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', expr, '--command', 'ghc', '-O2', '-rtsopts',
+ '-XOverloadedStrings', '-XLambdaCase', '-XMultiWayIf', '-XScopedTypeVariables',
+ '-isrc', '-outputdir', root / 'objects', ROOT / 'test/DigestByte.hs',
+ '-o', root / 'controls'], 300)
+ command([root / 'controls', candidate, '+RTS', '-M2048m', '-RTS'])
+ report.update(complete=True, controls_sha256=hashlib.sha256((ROOT / 'test/DigestByte.hs').read_bytes()).hexdigest())
+ (root / 'report.json').write_text(json.dumps(report, indent=2) + '\n')
+ print('PASS digest-byte canonical, legacy, length, demand and provenance controls')
+
+
+if __name__ == '__main__':
+ main()
