!import "arboricx-nodes.tri" !Local readManifestMagic = (bs : expectBytes arboricxManifestMagic bs) -- Read a u32 BE length, then that many raw bytes. -- Returns the payload bytes and remaining input. readLengthPrefixedString = (bs : bindResult (readBytes 4 bs) (lengthBytes afterLengthBytes : bindResult (readBytes (u32BEBytesToNat lengthBytes) afterLengthBytes) (payload afterPayload : ok payload afterPayload))) -- Helper: read a single capability string (length-prefixed string) readCapability = (bs : readLengthPrefixedString bs) -- Helper worker: read N capability strings (counts up from 0) readCapabilities_ = y (self bs count i acc : matchBool (ok (reverse acc) bs) (bindResult (readCapability bs) (cap afterCap : self afterCap count (succ i) (pair cap acc))) (equal? i count)) -- Helper: read N capabilities readCapabilities = (count bs : readCapabilities_ bs count 0 t) -- Helper: read a single root entry (32-byte raw hash + length-prefixed role) readRootEntry = (bs : bindResult (readBytes 32 bs) (hashRaw afterHash : bindResult (readLengthPrefixedString afterHash) (role afterRole : ok (pair hashRaw role) afterRole))) -- Helper worker: read N root entries (counts up from 0) readRoots_ = y (self bs count i acc : matchBool (ok (reverse acc) bs) (bindResult (readRootEntry bs) (root afterRoot : self afterRoot count (succ i) (pair root acc))) (equal? i count)) -- Helper: read N roots readRoots = (count bs : readRoots_ bs count 0 t) -- Helper: read a single export entry readExportEntry = (bs : bindResult (readLengthPrefixedString bs) (name afterName : bindResult (readBytes 32 afterName) (rootHashRaw afterRootHash : bindResult (readLengthPrefixedString afterRootHash) (kind afterKind : bindResult (readLengthPrefixedString afterKind) (abi afterAbi : ok (pair name (pair rootHashRaw (pair kind abi))) afterAbi))))) -- Helper worker: read N export entries (counts up from 0) readExports_ = y (self bs count i acc : matchBool (ok (reverse acc) bs) (bindResult (readExportEntry bs) (exp afterExp : self afterExp count (succ i) (pair exp acc))) (equal? i count)) -- Helper: read N exports readExports = (count bs : readExports_ bs count 0 t) -- Main core manifest parser. -- Reads: magic, version, core strings, capabilities, closure, roots, exports. readManifestCore = (bs : bindResult (readManifestMagic bs) (_ afterMagic : bindResult (readBytes 2 afterMagic) (majorVersion afterMajor : bindResult (readBytes 2 afterMajor) (minorVersion afterMinor : bindResult (readLengthPrefixedString afterMinor) (schema afterSchema : bindResult (readLengthPrefixedString afterSchema) (bundleType afterBundleType : bindResult (readLengthPrefixedString afterBundleType) (treeCalculus afterTreeCalculus : bindResult (readLengthPrefixedString afterTreeCalculus) (treeHashAlgorithm afterTreeHashAlgorithm : bindResult (readLengthPrefixedString afterTreeHashAlgorithm) (treeHashDomain afterTreeHashDomain : bindResult (readLengthPrefixedString afterTreeHashDomain) (treeNodePayload afterTreeNodePayload : bindResult (readLengthPrefixedString afterTreeNodePayload) (runtimeSemantics afterRuntimeSemantics : bindResult (readLengthPrefixedString afterRuntimeSemantics) (runtimeEvaluation afterRuntimeEvaluation : bindResult (readLengthPrefixedString afterRuntimeEvaluation) (runtimeAbi afterRuntimeAbi : bindResult (readBytes 4 afterRuntimeAbi) (capCountRaw afterCapCountRaw : bindResult (readCapabilities (u32BEBytesToNat capCountRaw) afterCapCountRaw) (capabilities afterCapabilities : bindResult (readBytes 1 afterCapabilities) (closureByte afterClosureByte : bindResult (readBytes 4 afterClosureByte) (rootCountRaw afterRootCountRaw : bindResult (readRoots (u32BEBytesToNat rootCountRaw) afterRootCountRaw) (roots afterRoots : bindResult (readBytes 4 afterRoots) (exportCountRaw afterExportCountRaw : bindResult (readExports (u32BEBytesToNat exportCountRaw) afterExportCountRaw) (exports afterExports : ok (pair schema (pair bundleType (pair treeCalculus (pair treeHashAlgorithm (pair treeHashDomain (pair treeNodePayload (pair runtimeSemantics (pair runtimeEvaluation (pair runtimeAbi (pair capabilities (pair closureByte (pair roots exports)))))))))))) afterExports)))))))))))))))))))) -- Metadata tag constants (u16 values) tagPackage = [(0) (1)] tagVersion = [(0) (2)] tagDescription = [(0) (3)] tagLicense = [(0) (4)] tagCreatedBy = [(0) (5)] -- Read a single TLV entry: u16 tag + u32 length + value bytes. -- Returns the pair (tag, value) and remaining input. readTLV = (bs : bindResult (readBytes 2 bs) (tag afterTag : bindResult (readBytes 4 afterTag) (tlvLenRaw afterTlvLenRaw : bindResult (readBytes (u32BEBytesToNat tlvLenRaw) afterTlvLenRaw) (tlvValue afterTlvValue : ok (pair tag tlvValue) afterTlvValue)))) -- Worker: read N TLV entries (counts up from 0) readTLVs_ = y (self bs count i acc : matchBool (ok (reverse acc) bs) (bindResult (readTLV bs) (tlv afterTlv : self afterTlv count (succ i) (pair tlv acc))) (equal? i count)) -- Read a count followed by that many TLV entries. readTLVList = (count bs : readTLVs_ bs count 0 t) -- Skip N extension TLV entries (counts up from 0) skipTLVs_ = y (self bs count i : matchBool (ok unit bs) (bindResult (readTLV bs) (_ afterTlv : self afterTlv count (succ i))) (equal? i count)) -- Full manifest parser: core fields + metadata TLV list + extension TLV list. readManifest = (bs : bindResult (readManifestCore bs) (coreManifest afterCore : bindResult (readBytes 4 afterCore) (metaCountRaw afterMetaCountRaw : bindResult (readTLVList (u32BEBytesToNat metaCountRaw) afterMetaCountRaw) (metadataFields afterMetadataFields : bindResult (readBytes 4 afterMetadataFields) (extCountRaw afterExtCountRaw : bindResult (skipTLVs_ afterExtCountRaw (u32BEBytesToNat extCountRaw) 0) (afterExtensions _ : ok (pair coreManifest (pair metadataFields afterExtensions)) afterExtensions)))))) -- Lookup a metadata value by tag from a TLV list. -- Returns nothing if not found, just value if found. lookupMetadata_ = y (self tlvs tag : matchList nothing (tlv rest : matchBool (just (matchPair (_ value : value) tlv)) (self rest tag) (bytesEq? (matchPair (tlvTag _ : tlvTag) tlv) tag)) tlvs) lookupMetadata = (tlvs tag : lookupMetadata_ tlvs tag) -- Get export name from an export entry (pair name (pair rootHash (pair kind abi))) exportName = (exp : matchPair (name _ : name) exp) exportRoot = (exp : matchPair (_ payload : matchPair (root _ : root) payload) exp) -- Check if an export name matches a given byte string. exportNameEq? = (nameBytes exp : bytesEq? nameBytes (exportName exp)) -- Find first export matching a name, or nothing. findExportByName_ = y (self exports name : matchList nothing (exp rest : matchBool (just exp) (self rest name) (exportNameEq? name exp)) exports) findExportByName = (exports name : findExportByName_ exports name) -- Get list of all export names from a list of exports. getExportNames_ = y (self acc exports : matchList (reverse acc) (exp rest : self (pair (exportName exp) acc) rest) exports) getExportNames = (exports : getExportNames_ t exports) mainExportName = "main" maybeExportToResult = (maybeExport : triage (err errMissingSection t) (export : ok export t) (_ _ : err errMissingSection t) maybeExport) selectSingleExport = (exports : matchList (err errMissingSection t) (export rest : matchBool (ok export t) (err errMissingSection t) (emptyList? rest)) exports) selectDefaultExport = (exports : triage (selectSingleExport exports) (export : ok export t) (_ _ : err errMissingSection t) (findExportByName exports mainExportName)) -- Select an export: explicit name if provided, otherwise "main", otherwise -- the sole export if the bundle has exactly one export. selectExport = (exports nameBytes : matchBool (selectDefaultExport exports) (maybeExportToResult (findExportByName exports nameBytes)) (emptyList? nameBytes)) selectExportOpt = (exports optNameBytes : selectExport exports optNameBytes) -- Expected core string values (raw UTF-8 bytes, not decoded to Unicode characters). expectedSchema = "arboricx.bundle.manifest.v1" expectedBundleType = "tree-calculus-executable-object" expectedTreeCalculus = "tree-calculus.v1" expectedTreeHashAlgorithm = "sha256" expectedTreeHashDomain = "arboricx.merkle.node.v1" expectedTreeNodePayload = "arboricx.merkle.payload.v1" expectedRuntimeSemantics = "tree-calculus.v1" expectedRuntimeEvaluation = "normal-order" expectedRuntimeAbi = "arboricx.abi.tree.v1" -- Manifest core field accessors. -- readManifestCore returns: (pair schema (pair bundleType (... (pair closureByte (pair roots exports))))) pairFirst = (p : matchPair (a _ : a) p) pairSecond = (p : matchPair (_ b : b) p) manifestSchema = (core : pairFirst core) manifestBundleType = (core : pairFirst (pairSecond core)) manifestTreeCalculus = (core : pairFirst (pairSecond (pairSecond core))) manifestTreeHashAlgorithm = (core : pairFirst (pairSecond (pairSecond (pairSecond core)))) manifestTreeHashDomain = (core : pairFirst (pairSecond (pairSecond (pairSecond (pairSecond core))))) manifestTreeNodePayload = (core : pairFirst (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond core)))))) manifestRuntimeSemantics = (core : pairFirst (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond core))))))) manifestRuntimeEvaluation = (core : pairFirst (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond core)))))))) manifestRuntimeAbi = (core : pairFirst (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond core))))))))) manifestCapabilities = (core : pairFirst (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond core)))))))))) manifestClosureByte = (core : pairFirst (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond core))))))))))) manifestRoots = (core : pairFirst (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond core)))))))))))) manifestExports = (core : pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond core)))))))))))) -- Helper: compare a manifest field against an expected byte string. manifestFieldMatch? = (actual expected : bytesEq? actual expected) -- Validate core manifest fields against expected values. validateManifestCore = (core rest : matchBool (ok core rest) (err errManifestValidationFailed rest) (and? (manifestFieldMatch? (manifestSchema core) expectedSchema) (and? (manifestFieldMatch? (manifestBundleType core) expectedBundleType) (and? (manifestFieldMatch? (manifestTreeCalculus core) expectedTreeCalculus) (and? (manifestFieldMatch? (manifestTreeHashAlgorithm core) expectedTreeHashAlgorithm) (and? (manifestFieldMatch? (manifestTreeHashDomain core) expectedTreeHashDomain) (and? (manifestFieldMatch? (manifestTreeNodePayload core) expectedTreeNodePayload) (and? (manifestFieldMatch? (manifestRuntimeSemantics core) expectedRuntimeSemantics) (and? (manifestFieldMatch? (manifestRuntimeEvaluation core) expectedRuntimeEvaluation) (and? (manifestFieldMatch? (manifestRuntimeAbi core) expectedRuntimeAbi) (and? (bytesEq? (manifestClosureByte core) [(0)]) (and? (not? (emptyList? (manifestRoots core))) (not? (emptyList? (manifestExports core)))))))))))))))