diff --git a/AGENTS.md b/AGENTS.md index e7a2594..689a46f 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -2,6 +2,10 @@ > For AI agents and contributors working in this repository. +## 0. TDD + +Write and discuss tests with the user before implementing any implementation code. + ## 1. Build & Test ```bash diff --git a/lib/arboricx-common.tri b/lib/arboricx-common.tri new file mode 100644 index 0000000..90dc91d --- /dev/null +++ b/lib/arboricx-common.tri @@ -0,0 +1,432 @@ +!import "base.tri" !Local +!import "list.tri" !Local +!import "bytes.tri" !Local +!import "binary.tri" !Local + +arboricxMagic = [(65) (82) (66) (79) (82) (73) (67) (88)] +arboricxMajorVersion = [(0) (1)] +arboricxMinorVersion = [(0) (0)] +arboricxManifestSectionId = [(0) (0) (0) (1)] +arboricxNodesSectionId = [(0) (0) (0) (2)] + +-- Manifest magic and version constants +arboricxManifestMagic = [(65) (82) (66) (77) (78) (70) (83) (84)] +arboricxManifestMajorVersion = [(0) (1)] +arboricxManifestMinorVersion = [(0) (0)] + +errMissingSection = 4 +errUnsupportedVersion = 5 +errDuplicateSection = 6 +errDuplicateNode = 7 +errInvalidNodePayload = 8 +errMissingNode = 9 +errInvalidManifestMagic = 10 +errUnsupportedManifestVersion = 11 +errTrailingManifestBytes = 12 +errManifestValidationFailed = 13 + +nodePayloadLeafTag = 0 +nodePayloadStemTag = 1 +nodePayloadForkTag = 2 + +readArboricxMagic = (bs : expectBytes arboricxMagic bs) + +readArboricxHeader = (bs : + bindResult (readArboricxMagic bs) + (_ afterMagic : + bindResult (readBytes 2 afterMagic) + (majorVersion afterMajor : + bindResult (readBytes 2 afterMajor) + (minorVersion afterMinor : + bindResult (readBytes 4 afterMinor) + (sectionCount afterSectionCount : + bindResult (readBytes 8 afterSectionCount) + (flags afterFlags : + bindResult (readBytes 8 afterFlags) + (dirOffset afterDirOffset : + ok + (pair majorVersion + (pair minorVersion + (pair sectionCount + (pair flags dirOffset)))) + afterDirOffset))))))) + +readSectionRecord = (bs : + bindResult (readBytes 4 bs) + (sectionId afterSectionId : + bindResult (readBytes 2 afterSectionId) + (sectionVersion afterSectionVersion : + bindResult (readBytes 2 afterSectionVersion) + (sectionFlags afterSectionFlags : + bindResult (readBytes 2 afterSectionFlags) + (compression afterCompression : + bindResult (readBytes 2 afterCompression) + (digestAlgorithm afterDigestAlgorithm : + bindResult (readBytes 8 afterDigestAlgorithm) + (offset afterOffset : + bindResult (readBytes 8 afterOffset) + (length afterLength : + bindResult (readBytes 32 afterLength) + (digest afterDigest : + ok + (pair sectionId + (pair sectionVersion + (pair sectionFlags + (pair compression + (pair digestAlgorithm + (pair offset + (pair length digest))))))) + afterDigest))))))))) + +readSectionDirectory_ = y (self bs sectionCount i acc : + matchBool + (ok (reverse acc) bs) + (bindResult (readSectionRecord bs) + (sectionRecord afterSectionRecord : + self afterSectionRecord sectionCount (succ i) (pair sectionRecord acc))) + (equal? i sectionCount)) + +readSectionDirectory = (sectionCount bs : readSectionDirectory_ bs sectionCount 0 t) + +sectionRecordId = (sectionRecord : + matchPair + (sectionId _ : sectionId) + sectionRecord) + +sectionRecordVersion = (sectionRecord : + matchPair + (_ payload : + matchPair + (sectionVersion _ : sectionVersion) + payload) + sectionRecord) + +sectionRecordFlags = (sectionRecord : + matchPair + (_ payload : + matchPair + (_ payload2 : + matchPair + (sectionFlags _ : sectionFlags) + payload2) + payload) + sectionRecord) + +sectionRecordCompression = (sectionRecord : + matchPair + (_ payload : + matchPair + (_ payload2 : + matchPair + (_ payload3 : + matchPair + (compression _ : compression) + payload3) + payload2) + payload) + sectionRecord) + +sectionRecordDigestAlgorithm = (sectionRecord : + matchPair + (_ payload : + matchPair + (_ payload2 : + matchPair + (_ payload3 : + matchPair + (_ payload4 : + matchPair + (digestAlgorithm _ : digestAlgorithm) + payload4) + payload3) + payload2) + payload) + sectionRecord) + +sectionRecordOffset = (sectionRecord : + matchPair + (_ payload : + matchPair + (_ payload2 : + matchPair + (_ payload3 : + matchPair + (_ payload4 : + matchPair + (_ payload5 : + matchPair + (offset _ : offset) + payload5) + payload4) + payload3) + payload2) + payload) + sectionRecord) + +sectionRecordLength = (sectionRecord : + matchPair + (_ payload : + matchPair + (_ payload2 : + matchPair + (_ payload3 : + matchPair + (_ payload4 : + matchPair + (_ payload5 : + matchPair + (_ payload6 : + matchPair + (length _ : length) + payload6) + payload5) + payload4) + payload3) + payload2) + payload) + sectionRecord) + +sectionRecordDigest = (sectionRecord : + matchPair + (_ payload : + matchPair + (_ payload2 : + matchPair + (_ payload3 : + matchPair + (_ payload4 : + matchPair + (_ payload5 : + matchPair + (_ payload6 : + matchPair + (_ digest : digest) + payload6) + payload5) + payload4) + payload3) + payload2) + payload) + sectionRecord) + +lookupSectionRecord_ = y (self directory sectionId : + matchList + nothing + (sectionRecord rest : + matchBool + (just sectionRecord) + (self rest sectionId) + (bytesEq? sectionId (sectionRecordId sectionRecord))) + directory) + +lookupSectionRecord = (sectionId directory : lookupSectionRecord_ directory sectionId) + +sectionDirectoryHasId?_ = y (self directory sectionId : + matchList + false + (sectionRecord rest : + or? + (bytesEq? sectionId (sectionRecordId sectionRecord)) + (self rest sectionId)) + directory) + +sectionDirectoryHasId? = (sectionId directory : sectionDirectoryHasId?_ directory sectionId) + +sectionDirectoryHasDuplicateIds? = y (self directory : + matchList + false + (sectionRecord rest : + or? + (sectionDirectoryHasId?_ rest (sectionRecordId sectionRecord)) + (self rest)) + directory) + +validateSectionDirectory = (directory rest : + matchBool + (err errDuplicateSection rest) + (ok directory rest) + (sectionDirectoryHasDuplicateIds? directory)) + +byteSlice = (offset length bytes : bytesTake length (bytesDrop offset bytes)) + +natMake = (bit rest : + matchBool + 0 + (pair bit rest) + (and? (equal? bit 0) (equal? rest 0))) + +natAdd = y (self a b : + triage + b + (_ : b) + (aBit aRest : + triage + a + (_ : a) + (bBit bRest : + matchBool + (natMake 0 (succ (self aRest bRest))) + (natMake (matchBool (matchBool 0 1 bBit) (matchBool 1 0 bBit) aBit) + (self aRest bRest)) + (and? (equal? aBit 1) (equal? bBit 1))) + b) + a) + +natDouble = (n : matchBool 0 (pair 0 n) (equal? n 0)) + +natTimes256 = (n : + natDouble + (natDouble + (natDouble + (natDouble + (natDouble + (natDouble + (natDouble + (natDouble n)))))))) + +byteNatShiftAppend_ = y (self byte acc i : + matchBool + acc + (triage + (natMake 0 (self 0 acc (succ i))) + (_ : acc) + (bit rest : natMake bit (self rest acc (succ i))) + byte) + (equal? i 8)) + +byteNatShiftAppend = (byte acc : byteNatShiftAppend_ byte acc 0) + +beBytesToNat = (bytes : + foldl + (acc byte : byteNatShiftAppend byte acc) + 0 + bytes) + +u32BEBytesToNat = beBytesToNat +u64BEBytesToNat = beBytesToNat + +arboricxHeaderMajorVersion = (header : + matchPair + (majorVersion _ : majorVersion) + header) + +arboricxHeaderMinorVersion = (header : + matchPair + (_ payload : + matchPair + (minorVersion _ : minorVersion) + payload) + header) + +arboricxHeaderSectionCount = (header : + matchPair + (_ payload : + matchPair + (_ payload2 : + matchPair + (sectionCount _ : sectionCount) + payload2) + payload) + header) + +arboricxHeaderFlags = (header : + matchPair + (_ payload : + matchPair + (_ payload2 : + matchPair + (_ payload3 : + matchPair + (flags _ : flags) + payload3) + payload2) + payload) + header) + +arboricxHeaderDirOffset = (header : + matchPair + (_ payload : + matchPair + (_ payload2 : + matchPair + (_ payload3 : + matchPair + (_ dirOffset : dirOffset) + payload3) + payload2) + payload) + header) + +validateArboricxHeader = (header rest : + matchBool + (ok header rest) + (err errUnsupportedVersion rest) + (and? + (bytesEq? arboricxMajorVersion (arboricxHeaderMajorVersion header)) + (bytesEq? arboricxMinorVersion (arboricxHeaderMinorVersion header)))) + +readArboricxContainer = (bs : + bindResult (readArboricxHeader bs) + (header afterHeader : + bindResult (validateArboricxHeader header afterHeader) + (validHeader afterValidHeader : + bindResult (readSectionDirectory + (u32BEBytesToNat (arboricxHeaderSectionCount validHeader)) + (bytesDrop (u64BEBytesToNat (arboricxHeaderDirOffset validHeader)) bs)) + (directory afterDirectory : + bindResult (validateSectionDirectory directory afterDirectory) + (validDirectory afterValidDirectory : + ok (pair validHeader validDirectory) afterValidDirectory))))) + +sectionRecordOffsetNat = (sectionRecord : + u64BEBytesToNat (sectionRecordOffset sectionRecord)) + +sectionRecordLengthNat = (sectionRecord : + u64BEBytesToNat (sectionRecordLength sectionRecord)) + +extractSectionBytes = (sectionRecord containerBytes : + byteSlice + (sectionRecordOffsetNat sectionRecord) + (sectionRecordLengthNat sectionRecord) + containerBytes) + +extractSectionBytesResult = (sectionRecord containerBytes rest : + (sectionBytes : + matchBool + (ok sectionBytes rest) + (err errUnexpectedEof rest) + (equal? (bytesLength sectionBytes) (sectionRecordLengthNat sectionRecord))) + (extractSectionBytes sectionRecord containerBytes)) + +lookupSectionBytes = (sectionId directory containerBytes : + triage + nothing + (sectionRecord : just (extractSectionBytes sectionRecord containerBytes)) + (_ _ : nothing) + (lookupSectionRecord sectionId directory)) + +sectionBytesOrErr = (sectionId directory containerBytes rest : + triage + (err errMissingSection rest) + (sectionRecord : extractSectionBytesResult sectionRecord containerBytes rest) + (_ _ : err errMissingSection rest) + (lookupSectionRecord sectionId directory)) + +readArboricxSectionBytes = (sectionId bs : + bindResult (readArboricxContainer bs) + (container afterContainer : + matchPair + (_ directory : sectionBytesOrErr sectionId directory bs afterContainer) + container)) + +readArboricxRequiredSections = (bs : + bindResult (readArboricxContainer bs) + (container afterContainer : + matchPair + (_ directory : + bindResult (sectionBytesOrErr arboricxManifestSectionId directory bs afterContainer) + (manifestBytes _ : + bindResult (sectionBytesOrErr arboricxNodesSectionId directory bs afterContainer) + (nodesBytes _ : + ok (pair manifestBytes nodesBytes) afterContainer))) + container)) diff --git a/lib/arboricx-manifest.tri b/lib/arboricx-manifest.tri new file mode 100644 index 0000000..09a375e --- /dev/null +++ b/lib/arboricx-manifest.tri @@ -0,0 +1,339 @@ +!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) + +-- Select an export: prefer explicit name, then "main", then single, then error. +selectExport_ = y (self exports name nameBytes : + matchBool + -- Explicit name given + (matchBool + nothing + (err errMissingSection t) + (_ _ : nothing) + (findExportByName exports nameBytes)) + -- No explicit name: try "main" + (matchBool + nothing + (matchBool + (equal? (length exports) 1) + (ok (head exports) t) + (err errMissingSection t) + (bytesEq? (exportName (head exports)) nameBytes)) + (_ _ : nothing) + (findExportByName exports nameBytes)) + -- Single export: auto-select + (matchBool + (equal? (length exports) 1) + (ok (head exports) t) + (err errMissingSection t) + (emptyList? exports)) + exports) + +selectExport = (exports nameBytes : + selectExport_ exports nameBytes 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 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))))))))))))))) diff --git a/lib/arboricx-nodes.tri b/lib/arboricx-nodes.tri new file mode 100644 index 0000000..abda776 --- /dev/null +++ b/lib/arboricx-nodes.tri @@ -0,0 +1,232 @@ +!import "arboricx-common.tri" !Local + +readNodeRecord = (bs : + bindResult (readBytes 32 bs) + (nodeHash afterNodeHash : + bindResult (readBytes 4 afterNodeHash) + (payloadLength afterPayloadLength : + bindResult (readBytes (u32BEBytesToNat payloadLength) afterPayloadLength) + (payload afterPayload : + ok + (pair nodeHash + (pair payloadLength payload)) + afterPayload)))) + +nodeRecordHash = (nodeRecord : + matchPair + (nodeHash _ : nodeHash) + nodeRecord) + +nodeRecordPayloadLength = (nodeRecord : + matchPair + (_ payload : + matchPair + (payloadLength _ : payloadLength) + payload) + nodeRecord) + +nodeRecordPayload = (nodeRecord : + matchPair + (_ payload : + matchPair + (_ nodePayload : nodePayload) + payload) + nodeRecord) + +nodePayloadKind = (nodePayload : bytesHead nodePayload) + +nodePayloadHasTag? = (tag nodePayload : + triage + false + (actualTag : byteEq? actualTag tag) + (_ _ : false) + (nodePayloadKind nodePayload)) + +nodePayloadLeaf? = (nodePayload : bytesEq? [(0)] nodePayload) + +nodePayloadStem? = (nodePayload : + and? + (nodePayloadHasTag? nodePayloadStemTag nodePayload) + (equal? (bytesLength nodePayload) 33)) + +nodePayloadFork? = (nodePayload : + and? + (nodePayloadHasTag? nodePayloadForkTag nodePayload) + (equal? (bytesLength nodePayload) 65)) + +nodePayloadValid? = (nodePayload : + or? + (nodePayloadLeaf? nodePayload) + (or? + (nodePayloadStem? nodePayload) + (nodePayloadFork? nodePayload))) + +nodePayloadStemChildHash = (nodePayload : bytesTake 32 (bytesDrop 1 nodePayload)) +nodePayloadForkLeftHash = (nodePayload : bytesTake 32 (bytesDrop 1 nodePayload)) +nodePayloadForkRightHash = (nodePayload : bytesTake 32 (bytesDrop 33 nodePayload)) + +nodeRecordPayloadValid? = (nodeRecord : nodePayloadValid? (nodeRecordPayload nodeRecord)) + +nodeRecordsHaveInvalidPayload? = y (self nodeRecords : + matchList + false + (nodeRecord rest : + or? + (not? (nodeRecordPayloadValid? nodeRecord)) + (self rest)) + nodeRecords) + +nodeRecordsHaveHash? = y (self nodeRecords nodeHash : + matchList + false + (nodeRecord rest : + or? + (bytesEq? nodeHash (nodeRecordHash nodeRecord)) + (self rest nodeHash)) + nodeRecords) + +nodeRecordsHaveDuplicateHashes? = y (self nodeRecords : + matchList + false + (nodeRecord rest : + or? + (nodeRecordsHaveHash? rest (nodeRecordHash nodeRecord)) + (self rest)) + nodeRecords) + +lookupNodeRecord_ = y (self nodeRecords nodeHash : + matchList + nothing + (nodeRecord rest : + matchBool + (just nodeRecord) + (self rest nodeHash) + (bytesEq? nodeHash (nodeRecordHash nodeRecord))) + nodeRecords) + +lookupNodeRecord = (nodeHash nodeRecords : lookupNodeRecord_ nodeRecords nodeHash) + +nodeRecordChildHashes = (nodeRecord : + (nodePayload : + matchBool + t + (matchBool + (pair (nodePayloadStemChildHash nodePayload) t) + (pair (nodePayloadForkLeftHash nodePayload) + (pair (nodePayloadForkRightHash nodePayload) t)) + (nodePayloadStem? nodePayload)) + (nodePayloadLeaf? nodePayload)) + (nodeRecordPayload nodeRecord)) + +nodeHashPresent? = (nodeHash nodeRecords : nodeRecordsHaveHash? nodeRecords nodeHash) + +nodeChildHashesPresent? = y (self childHashes nodeRecords : + matchList + true + (childHash rest : + and? + (nodeHashPresent? childHash nodeRecords) + (self rest nodeRecords)) + childHashes) + +nodeRecordChildrenPresent? = (nodeRecord nodeRecords : + nodeChildHashesPresent? (nodeRecordChildHashes nodeRecord) nodeRecords) + +nodeRecordsClosed? = y (self nodeRecords allNodeRecords : + matchList + true + (nodeRecord rest : + and? + (nodeRecordChildrenPresent? nodeRecord allNodeRecords) + (self rest allNodeRecords)) + nodeRecords) + +validateNodeRecords = (nodeRecords rest : + matchBool + (err errInvalidNodePayload rest) + (matchBool + (err errDuplicateNode rest) + (matchBool + (ok nodeRecords rest) + (err errMissingNode rest) + (nodeRecordsClosed? nodeRecords nodeRecords)) + (nodeRecordsHaveDuplicateHashes? nodeRecords)) + (nodeRecordsHaveInvalidPayload? nodeRecords)) + +readNodeRecords_ = y (self bs nodeCount i acc : + matchBool + (ok (reverse acc) bs) + (bindResult (readNodeRecord bs) + (nodeRecord afterNodeRecord : + self afterNodeRecord nodeCount (succ i) (pair nodeRecord acc))) + (equal? i nodeCount)) + +readNodeRecords = (nodeCount bs : readNodeRecords_ bs nodeCount 0 t) + +readNodesSection = (bs : + bindResult (readBytes 8 bs) + (nodeCount afterNodeCount : + bindResult (readNodeRecords (u64BEBytesToNat nodeCount) afterNodeCount) + (nodeRecords afterNodeRecords : + bindResult (validateNodeRecords nodeRecords afterNodeRecords) + (validNodeRecords afterValidNodeRecords : + ok (pair nodeCount validNodeRecords) afterValidNodeRecords)))) + +readNodesSectionComplete = (bs : + bindResult (readNodesSection bs) + (nodesSection afterNodesSection : + matchBool + (ok nodesSection afterNodesSection) + (err errUnexpectedBytes afterNodesSection) + (bytesNil? afterNodesSection))) + +readArboricxNodesSection = (bs : + bindResult (readArboricxContainer bs) + (container afterContainer : + matchPair + (_ directory : + bindResult (sectionBytesOrErr arboricxNodesSectionId directory bs afterContainer) + (nodesBytes _ : + bindResult (readNodesSectionComplete nodesBytes) + (nodesSection _ : ok nodesSection afterContainer))) + container)) + +nodesSectionCount = (nodesSection : + matchPair + (nodeCount _ : nodeCount) + nodesSection) + +nodesSectionRecords = (nodesSection : + matchPair + (_ nodeRecords : nodeRecords) + nodesSection) + +nodeRecordToTreeWith = (self nodeRecords nodeRecord : + (nodePayload : + matchBool + (ok t t) + (matchBool + (bindResult (self (nodePayloadStemChildHash nodePayload) nodeRecords) + (child _ : ok (t child) t)) + (bindResult (self (nodePayloadForkLeftHash nodePayload) nodeRecords) + (left _ : + bindResult (self (nodePayloadForkRightHash nodePayload) nodeRecords) + (right _ : ok (pair left right) t))) + (nodePayloadStem? nodePayload)) + (nodePayloadLeaf? nodePayload)) + (nodeRecordPayload nodeRecord)) + +nodeHashToTree = y (self nodeHash nodeRecords : + triage + (err errMissingNode t) + (nodeRecord : nodeRecordToTreeWith self nodeRecords nodeRecord) + (_ _ : err errMissingNode t) + (lookupNodeRecord nodeHash nodeRecords)) + +readArboricxTreeFromHash = (rootHash bs : + bindResult (readArboricxNodesSection bs) + (nodesSection afterContainer : + bindResult (nodeHashToTree rootHash (nodesSectionRecords nodesSection)) + (tree _ : ok tree afterContainer))) + +readArboricxExecutableFromHash = readArboricxTreeFromHash diff --git a/lib/arboricx.tri b/lib/arboricx.tri index 8eca16b..8c459b6 100644 --- a/lib/arboricx.tri +++ b/lib/arboricx.tri @@ -1,654 +1,18 @@ -!import "base.tri" !Local -!import "list.tri" !Local -!import "bytes.tri" !Local -!import "binary.tri" !Local +!import "arboricx-manifest.tri" !Local -arboricxMagic = [(65) (82) (66) (79) (82) (73) (67) (88)] -arboricxMajorVersion = [(0) (1)] -arboricxMinorVersion = [(0) (0)] -arboricxManifestSectionId = [(0) (0) (0) (1)] -arboricxNodesSectionId = [(0) (0) (0) (2)] - -errMissingSection = 4 -errUnsupportedVersion = 5 -errDuplicateSection = 6 -errDuplicateNode = 7 -errInvalidNodePayload = 8 -errMissingNode = 9 - -nodePayloadLeafTag = 0 -nodePayloadStemTag = 1 -nodePayloadForkTag = 2 - -readArboricxMagic = (bs : expectBytes arboricxMagic bs) - -readArboricxHeader = (bs : - bindResult (readArboricxMagic bs) - (_ afterMagic : - bindResult (readBytes 2 afterMagic) - (majorVersion afterMajor : - bindResult (readBytes 2 afterMajor) - (minorVersion afterMinor : - bindResult (readBytes 4 afterMinor) - (sectionCount afterSectionCount : - bindResult (readBytes 8 afterSectionCount) - (flags afterFlags : - bindResult (readBytes 8 afterFlags) - (dirOffset afterDirOffset : - ok - (pair majorVersion - (pair minorVersion - (pair sectionCount - (pair flags dirOffset)))) - afterDirOffset))))))) - -readSectionRecord = (bs : - bindResult (readBytes 4 bs) - (sectionId afterSectionId : - bindResult (readBytes 2 afterSectionId) - (sectionVersion afterSectionVersion : - bindResult (readBytes 2 afterSectionVersion) - (sectionFlags afterSectionFlags : - bindResult (readBytes 2 afterSectionFlags) - (compression afterCompression : - bindResult (readBytes 2 afterCompression) - (digestAlgorithm afterDigestAlgorithm : - bindResult (readBytes 8 afterDigestAlgorithm) - (offset afterOffset : - bindResult (readBytes 8 afterOffset) - (length afterLength : - bindResult (readBytes 32 afterLength) - (digest afterDigest : - ok - (pair sectionId - (pair sectionVersion - (pair sectionFlags - (pair compression - (pair digestAlgorithm - (pair offset - (pair length digest))))))) - afterDigest))))))))) - -readSectionDirectory_ = y (self bs sectionCount i acc : - matchBool - (ok (reverse acc) bs) - (bindResult (readSectionRecord bs) - (sectionRecord afterSectionRecord : - self afterSectionRecord sectionCount (succ i) (pair sectionRecord acc))) - (equal? i sectionCount)) - -readSectionDirectory = (sectionCount bs : readSectionDirectory_ bs sectionCount 0 t) - -sectionRecordId = (sectionRecord : - matchPair - (sectionId _ : sectionId) - sectionRecord) - -sectionRecordVersion = (sectionRecord : - matchPair - (_ payload : +-- Read and validate a full Arboricx bundle. +-- Returns (pair validManifest afterContainer). +-- The manifest core fields are validated against expected values. +readArboricxBundle = (bs : + bindResult (readArboricxRequiredSections bs) + (sections afterContainer : matchPair - (sectionVersion _ : sectionVersion) - payload) - sectionRecord) - -sectionRecordFlags = (sectionRecord : - matchPair - (_ payload : - matchPair - (_ payload2 : - matchPair - (sectionFlags _ : sectionFlags) - payload2) - payload) - sectionRecord) - -sectionRecordCompression = (sectionRecord : - matchPair - (_ payload : - matchPair - (_ payload2 : - matchPair - (_ payload3 : + (manifestBytes _ : + bindResult (readManifest manifestBytes) + (parsedManifest afterManifest : matchPair - (compression _ : compression) - payload3) - payload2) - payload) - sectionRecord) - -sectionRecordDigestAlgorithm = (sectionRecord : - matchPair - (_ payload : - matchPair - (_ payload2 : - matchPair - (_ payload3 : - matchPair - (_ payload4 : - matchPair - (digestAlgorithm _ : digestAlgorithm) - payload4) - payload3) - payload2) - payload) - sectionRecord) - -sectionRecordOffset = (sectionRecord : - matchPair - (_ payload : - matchPair - (_ payload2 : - matchPair - (_ payload3 : - matchPair - (_ payload4 : - matchPair - (_ payload5 : - matchPair - (offset _ : offset) - payload5) - payload4) - payload3) - payload2) - payload) - sectionRecord) - -sectionRecordLength = (sectionRecord : - matchPair - (_ payload : - matchPair - (_ payload2 : - matchPair - (_ payload3 : - matchPair - (_ payload4 : - matchPair - (_ payload5 : - matchPair - (_ payload6 : - matchPair - (length _ : length) - payload6) - payload5) - payload4) - payload3) - payload2) - payload) - sectionRecord) - -sectionRecordDigest = (sectionRecord : - matchPair - (_ payload : - matchPair - (_ payload2 : - matchPair - (_ payload3 : - matchPair - (_ payload4 : - matchPair - (_ payload5 : - matchPair - (_ payload6 : - matchPair - (_ digest : digest) - payload6) - payload5) - payload4) - payload3) - payload2) - payload) - sectionRecord) - -lookupSectionRecord_ = y (self directory sectionId : - matchList - nothing - (sectionRecord rest : - matchBool - (just sectionRecord) - (self rest sectionId) - (bytesEq? sectionId (sectionRecordId sectionRecord))) - directory) - -lookupSectionRecord = (sectionId directory : lookupSectionRecord_ directory sectionId) - -sectionDirectoryHasId?_ = y (self directory sectionId : - matchList - false - (sectionRecord rest : - or? - (bytesEq? sectionId (sectionRecordId sectionRecord)) - (self rest sectionId)) - directory) - -sectionDirectoryHasId? = (sectionId directory : sectionDirectoryHasId?_ directory sectionId) - -sectionDirectoryHasDuplicateIds? = y (self directory : - matchList - false - (sectionRecord rest : - or? - (sectionDirectoryHasId?_ rest (sectionRecordId sectionRecord)) - (self rest)) - directory) - -validateSectionDirectory = (directory rest : - matchBool - (err errDuplicateSection rest) - (ok directory rest) - (sectionDirectoryHasDuplicateIds? directory)) - -byteSlice = (offset length bytes : bytesTake length (bytesDrop offset bytes)) - -natMake = (bit rest : - matchBool - 0 - (pair bit rest) - (and? (equal? bit 0) (equal? rest 0))) - -natAdd = y (self a b : - triage - b - (_ : b) - (aBit aRest : - triage - a - (_ : a) - (bBit bRest : - matchBool - (natMake 0 (succ (self aRest bRest))) - (natMake (matchBool (matchBool 0 1 bBit) (matchBool 1 0 bBit) aBit) - (self aRest bRest)) - (and? (equal? aBit 1) (equal? bBit 1))) - b) - a) - -natDouble = (n : matchBool 0 (pair 0 n) (equal? n 0)) - -natTimes256 = (n : - natDouble - (natDouble - (natDouble - (natDouble - (natDouble - (natDouble - (natDouble - (natDouble n)))))))) - -byteNatShiftAppend_ = y (self byte acc i : - matchBool - acc - (triage - (natMake 0 (self 0 acc (succ i))) - (_ : acc) - (bit rest : natMake bit (self rest acc (succ i))) - byte) - (equal? i 8)) - -byteNatShiftAppend = (byte acc : byteNatShiftAppend_ byte acc 0) - -beBytesToNat = (bytes : - foldl - (acc byte : byteNatShiftAppend byte acc) - 0 - bytes) - -u32BEBytesToNat = beBytesToNat -u64BEBytesToNat = beBytesToNat - -arboricxHeaderMajorVersion = (header : - matchPair - (majorVersion _ : majorVersion) - header) - -arboricxHeaderMinorVersion = (header : - matchPair - (_ payload : - matchPair - (minorVersion _ : minorVersion) - payload) - header) - -arboricxHeaderSectionCount = (header : - matchPair - (_ payload : - matchPair - (_ payload2 : - matchPair - (sectionCount _ : sectionCount) - payload2) - payload) - header) - -arboricxHeaderFlags = (header : - matchPair - (_ payload : - matchPair - (_ payload2 : - matchPair - (_ payload3 : - matchPair - (flags _ : flags) - payload3) - payload2) - payload) - header) - -arboricxHeaderDirOffset = (header : - matchPair - (_ payload : - matchPair - (_ payload2 : - matchPair - (_ payload3 : - matchPair - (_ dirOffset : dirOffset) - payload3) - payload2) - payload) - header) - -validateArboricxHeader = (header rest : - matchBool - (ok header rest) - (err errUnsupportedVersion rest) - (and? - (bytesEq? arboricxMajorVersion (arboricxHeaderMajorVersion header)) - (bytesEq? arboricxMinorVersion (arboricxHeaderMinorVersion header)))) - -readArboricxContainer = (bs : - bindResult (readArboricxHeader bs) - (header afterHeader : - bindResult (validateArboricxHeader header afterHeader) - (validHeader afterValidHeader : - bindResult (readSectionDirectory - (u32BEBytesToNat (arboricxHeaderSectionCount validHeader)) - (bytesDrop (u64BEBytesToNat (arboricxHeaderDirOffset validHeader)) bs)) - (directory afterDirectory : - bindResult (validateSectionDirectory directory afterDirectory) - (validDirectory afterValidDirectory : - ok (pair validHeader validDirectory) afterValidDirectory))))) - -sectionRecordOffsetNat = (sectionRecord : - u64BEBytesToNat (sectionRecordOffset sectionRecord)) - -sectionRecordLengthNat = (sectionRecord : - u64BEBytesToNat (sectionRecordLength sectionRecord)) - -extractSectionBytes = (sectionRecord containerBytes : - byteSlice - (sectionRecordOffsetNat sectionRecord) - (sectionRecordLengthNat sectionRecord) - containerBytes) - -extractSectionBytesResult = (sectionRecord containerBytes rest : - (sectionBytes : - matchBool - (ok sectionBytes rest) - (err errUnexpectedEof rest) - (equal? (bytesLength sectionBytes) (sectionRecordLengthNat sectionRecord))) - (extractSectionBytes sectionRecord containerBytes)) - -lookupSectionBytes = (sectionId directory containerBytes : - triage - nothing - (sectionRecord : just (extractSectionBytes sectionRecord containerBytes)) - (_ _ : nothing) - (lookupSectionRecord sectionId directory)) - -sectionBytesOrErr = (sectionId directory containerBytes rest : - triage - (err errMissingSection rest) - (sectionRecord : extractSectionBytesResult sectionRecord containerBytes rest) - (_ _ : err errMissingSection rest) - (lookupSectionRecord sectionId directory)) - -readArboricxSectionBytes = (sectionId bs : - bindResult (readArboricxContainer bs) - (container afterContainer : - matchPair - (_ directory : sectionBytesOrErr sectionId directory bs afterContainer) - container)) - -readArboricxRequiredSections = (bs : - bindResult (readArboricxContainer bs) - (container afterContainer : - matchPair - (_ directory : - bindResult (sectionBytesOrErr arboricxManifestSectionId directory bs afterContainer) - (manifestBytes _ : - bindResult (sectionBytesOrErr arboricxNodesSectionId directory bs afterContainer) - (nodesBytes _ : - ok (pair manifestBytes nodesBytes) afterContainer))) - container)) - -readNodeRecord = (bs : - bindResult (readBytes 32 bs) - (nodeHash afterNodeHash : - bindResult (readBytes 4 afterNodeHash) - (payloadLength afterPayloadLength : - bindResult (readBytes (u32BEBytesToNat payloadLength) afterPayloadLength) - (payload afterPayload : - ok - (pair nodeHash - (pair payloadLength payload)) - afterPayload)))) - -nodeRecordHash = (nodeRecord : - matchPair - (nodeHash _ : nodeHash) - nodeRecord) - -nodeRecordPayloadLength = (nodeRecord : - matchPair - (_ payload : - matchPair - (payloadLength _ : payloadLength) - payload) - nodeRecord) - -nodeRecordPayload = (nodeRecord : - matchPair - (_ payload : - matchPair - (_ nodePayload : nodePayload) - payload) - nodeRecord) - -nodePayloadKind = (nodePayload : bytesHead nodePayload) - -nodePayloadHasTag? = (tag nodePayload : - triage - false - (actualTag : byteEq? actualTag tag) - (_ _ : false) - (nodePayloadKind nodePayload)) - -nodePayloadLeaf? = (nodePayload : bytesEq? [(0)] nodePayload) - -nodePayloadStem? = (nodePayload : - and? - (nodePayloadHasTag? nodePayloadStemTag nodePayload) - (equal? (bytesLength nodePayload) 33)) - -nodePayloadFork? = (nodePayload : - and? - (nodePayloadHasTag? nodePayloadForkTag nodePayload) - (equal? (bytesLength nodePayload) 65)) - -nodePayloadValid? = (nodePayload : - or? - (nodePayloadLeaf? nodePayload) - (or? - (nodePayloadStem? nodePayload) - (nodePayloadFork? nodePayload))) - -nodePayloadStemChildHash = (nodePayload : bytesTake 32 (bytesDrop 1 nodePayload)) -nodePayloadForkLeftHash = (nodePayload : bytesTake 32 (bytesDrop 1 nodePayload)) -nodePayloadForkRightHash = (nodePayload : bytesTake 32 (bytesDrop 33 nodePayload)) - -nodeRecordPayloadValid? = (nodeRecord : nodePayloadValid? (nodeRecordPayload nodeRecord)) - -nodeRecordsHaveInvalidPayload? = y (self nodeRecords : - matchList - false - (nodeRecord rest : - or? - (not? (nodeRecordPayloadValid? nodeRecord)) - (self rest)) - nodeRecords) - -nodeRecordsHaveHash? = y (self nodeRecords nodeHash : - matchList - false - (nodeRecord rest : - or? - (bytesEq? nodeHash (nodeRecordHash nodeRecord)) - (self rest nodeHash)) - nodeRecords) - -nodeRecordsHaveDuplicateHashes? = y (self nodeRecords : - matchList - false - (nodeRecord rest : - or? - (nodeRecordsHaveHash? rest (nodeRecordHash nodeRecord)) - (self rest)) - nodeRecords) - -lookupNodeRecord_ = y (self nodeRecords nodeHash : - matchList - nothing - (nodeRecord rest : - matchBool - (just nodeRecord) - (self rest nodeHash) - (bytesEq? nodeHash (nodeRecordHash nodeRecord))) - nodeRecords) - -lookupNodeRecord = (nodeHash nodeRecords : lookupNodeRecord_ nodeRecords nodeHash) - -nodeRecordChildHashes = (nodeRecord : - (nodePayload : - matchBool - t - (matchBool - (pair (nodePayloadStemChildHash nodePayload) t) - (pair (nodePayloadForkLeftHash nodePayload) - (pair (nodePayloadForkRightHash nodePayload) t)) - (nodePayloadStem? nodePayload)) - (nodePayloadLeaf? nodePayload)) - (nodeRecordPayload nodeRecord)) - -nodeHashPresent? = (nodeHash nodeRecords : nodeRecordsHaveHash? nodeRecords nodeHash) - -nodeChildHashesPresent? = y (self childHashes nodeRecords : - matchList - true - (childHash rest : - and? - (nodeHashPresent? childHash nodeRecords) - (self rest nodeRecords)) - childHashes) - -nodeRecordChildrenPresent? = (nodeRecord nodeRecords : - nodeChildHashesPresent? (nodeRecordChildHashes nodeRecord) nodeRecords) - -nodeRecordsClosed? = y (self nodeRecords allNodeRecords : - matchList - true - (nodeRecord rest : - and? - (nodeRecordChildrenPresent? nodeRecord allNodeRecords) - (self rest allNodeRecords)) - nodeRecords) - -validateNodeRecords = (nodeRecords rest : - matchBool - (err errInvalidNodePayload rest) - (matchBool - (err errDuplicateNode rest) - (matchBool - (ok nodeRecords rest) - (err errMissingNode rest) - (nodeRecordsClosed? nodeRecords nodeRecords)) - (nodeRecordsHaveDuplicateHashes? nodeRecords)) - (nodeRecordsHaveInvalidPayload? nodeRecords)) - -readNodeRecords_ = y (self bs nodeCount i acc : - matchBool - (ok (reverse acc) bs) - (bindResult (readNodeRecord bs) - (nodeRecord afterNodeRecord : - self afterNodeRecord nodeCount (succ i) (pair nodeRecord acc))) - (equal? i nodeCount)) - -readNodeRecords = (nodeCount bs : readNodeRecords_ bs nodeCount 0 t) - -readNodesSection = (bs : - bindResult (readBytes 8 bs) - (nodeCount afterNodeCount : - bindResult (readNodeRecords (u64BEBytesToNat nodeCount) afterNodeCount) - (nodeRecords afterNodeRecords : - bindResult (validateNodeRecords nodeRecords afterNodeRecords) - (validNodeRecords afterValidNodeRecords : - ok (pair nodeCount validNodeRecords) afterValidNodeRecords)))) - -readNodesSectionComplete = (bs : - bindResult (readNodesSection bs) - (nodesSection afterNodesSection : - matchBool - (ok nodesSection afterNodesSection) - (err errUnexpectedBytes afterNodesSection) - (bytesNil? afterNodesSection))) - -readArboricxNodesSection = (bs : - bindResult (readArboricxContainer bs) - (container afterContainer : - matchPair - (_ directory : - bindResult (sectionBytesOrErr arboricxNodesSectionId directory bs afterContainer) - (nodesBytes _ : - bindResult (readNodesSectionComplete nodesBytes) - (nodesSection _ : ok nodesSection afterContainer))) - container)) - -nodesSectionCount = (nodesSection : - matchPair - (nodeCount _ : nodeCount) - nodesSection) - -nodesSectionRecords = (nodesSection : - matchPair - (_ nodeRecords : nodeRecords) - nodesSection) - -nodeRecordToTreeWith = (self nodeRecords nodeRecord : - (nodePayload : - matchBool - (ok t t) - (matchBool - (bindResult (self (nodePayloadStemChildHash nodePayload) nodeRecords) - (child _ : ok (t child) t)) - (bindResult (self (nodePayloadForkLeftHash nodePayload) nodeRecords) - (left _ : - bindResult (self (nodePayloadForkRightHash nodePayload) nodeRecords) - (right _ : ok (pair left right) t))) - (nodePayloadStem? nodePayload)) - (nodePayloadLeaf? nodePayload)) - (nodeRecordPayload nodeRecord)) - -nodeHashToTree = y (self nodeHash nodeRecords : - triage - (err errMissingNode t) - (nodeRecord : nodeRecordToTreeWith self nodeRecords nodeRecord) - (_ _ : err errMissingNode t) - (lookupNodeRecord nodeHash nodeRecords)) - -readArboricxTreeFromHash = (rootHash bs : - bindResult (readArboricxNodesSection bs) - (nodesSection afterContainer : - bindResult (nodeHashToTree rootHash (nodesSectionRecords nodesSection)) - (tree _ : ok tree afterContainer))) - -readArboricxExecutableFromHash = readArboricxTreeFromHash + (coreManifest metadataWithExtensions : + bindResult (validateManifestCore coreManifest afterManifest) + (validCore _ : ok (pair validCore metadataWithExtensions) afterContainer)) + parsedManifest)) + sections)) diff --git a/notes/tricu-cli-debugging.md b/notes/tricu-cli-debugging.md new file mode 100644 index 0000000..673073a --- /dev/null +++ b/notes/tricu-cli-debugging.md @@ -0,0 +1,17 @@ +# tricu CLI debugging notes + +For ad-hoc expressions, prefer stdin mode and set `TRICU_DB_PATH` to a DB that already has library definitions imported: + +```sh +TRICU_DB_PATH=/tmp/gpt.db ./result/bin/tricu eval -t decode <<'EOF' +main = +EOF +``` + +Important details: + +- `eval` from stdin evaluates the submitted program and uses its final/main result. +- When using `-f FILE`, the CLI expects a `main` definition in the evaluated file context. +- With `TRICU_DB_PATH=/tmp/gpt.db`, definitions already loaded into that content store are in scope; do not add `!import` lines unless you intentionally want file import preprocessing. +- `!import "lib/arboricx.tri" !Local` is relative to the file being preprocessed; from temp files it will look under `/tmp`, so avoid that pattern for scratch files. +- Do not inspect huge Arboricx values with `-t fsl`; write small predicates/accessors and return booleans, numbers, or byte strings decoded with `-t decode`. diff --git a/test/Spec.hs b/test/Spec.hs index 1176cb7..c9be3af 100644 --- a/test/Spec.hs +++ b/test/Spec.hs @@ -49,6 +49,7 @@ tests = testGroup "Tricu Tests" , wireTests , byteListUtilities , binaryReaderTests + , manifestReadingTests ] lexer :: TestTree @@ -2182,3 +2183,555 @@ binaryReaderTests = testGroup "Binary Reader Tests" let env = evalTricu library (parseTricu input) result env @?= Fork Leaf Leaf ] + +-- --------------------------------------------------------------------------- +-- Manifest reading tests (Steps 1-9) +-- --------------------------------------------------------------------------- + +-- Build a minimal manifest: +-- magic "ARBMNFST" (8) + version 1.0 (4) + +-- schema "arboricx.bundle.manifest.v1" (4+27=31) + +-- bundleType "tree-calculus-executable-object" (4+31=35) + +-- treeCalculus "tree-calculus.v1" (4+16=20) + +-- treeHashAlgorithm "sha256" (4+6=10) + +-- treeHashDomain "arboricx.merkle.node.v1" (4+23=27) + +-- treeNodePayload "arboricx.merkle.payload.v1" (4+26=30) + +-- runtimeSemantics "tree-calculus.v1" (4+16=20) + +-- runtimeEvaluation "normal-order" (4+12=16) + +-- runtimeAbi "arboricx.abi.tree.v1" (4+20=24) + +-- capabilityCount 0 (4) + +-- closure 0 (1) + +-- rootCount 1 (4) + +-- root: hash (32) + role "default" (4+7=11) = 43 + +-- exportCount 1 (4) + +-- export: name "term" (4+4=8) + root (32) + kind "term" (4+4=8) + abi "arboricx.abi.tree.v1" (4+20=24) = 72 + +-- Total core = 8+4+31+35+20+10+27+30+20+16+24+4+1+4+43+4+72 = 378 bytes + +minimalManifestCoreBytes :: [Integer] +minimalManifestCoreBytes = [65,82,66,77,78,70,83,84] -- ARBMNFST magic + ++ u16 1 ++ u16 0 -- version 1.0 + ++ lengthPrefixed "arboricx.bundle.manifest.v1" -- schema + ++ lengthPrefixed "tree-calculus-executable-object" -- bundleType + ++ lengthPrefixed "tree-calculus.v1" -- treeCalculus + ++ lengthPrefixed "sha256" -- treeHashAlgorithm + ++ lengthPrefixed "arboricx.merkle.node.v1" -- treeHashDomain + ++ lengthPrefixed "arboricx.merkle.payload.v1" -- treeNodePayload + ++ lengthPrefixed "tree-calculus.v1" -- runtimeSemantics + ++ lengthPrefixed "normal-order" -- runtimeEvaluation + ++ lengthPrefixed "arboricx.abi.tree.v1" -- runtimeAbi + ++ u32 0 -- 0 capabilities + ++ [0] -- closure complete + ++ u32 1 -- 1 root + ++ replicate 32 0 -- placeholder root hash + ++ lengthPrefixed "default" -- root role + ++ u32 1 -- 1 export + ++ lengthPrefixed "term" -- export name + ++ replicate 32 0 -- placeholder export root hash + ++ lengthPrefixed "term" -- export kind + ++ lengthPrefixed "arboricx.abi.tree.v1" -- export abi + +lengthPrefixed :: String -> [Integer] +lengthPrefixed s = u32 (fromIntegral (length s)) ++ map (fromIntegral . fromEnum) s + +-- Full manifest: core + 0 metadata + 0 extension = core + u32(0) + u32(0) +fullMinimalManifestBytes :: [Integer] +fullMinimalManifestBytes = minimalManifestCoreBytes ++ u32 0 ++ u32 0 + +-- Create TLV list with two entries: +-- tag 1 (package), value "my-pkg", then tag 2 (version), value "1.0" +-- then "rest" bytes + +tlvForTagAndValue :: Integer -> String -> [Integer] +tlvForTagAndValue tag val = + u16 (fromIntegral tag) ++ lengthPrefixed val + +-- Build a pair of (tag, value) TLV +makeTLVPair :: Integer -> String -> String +makeTLVPair tag val = + "[(pair " ++ bytesExpr [0, fromIntegral tag] ++ " " + ++ bytesExpr (map (fromIntegral . fromEnum) val) ++ ")]" + +exportEntryExpr :: String -> [Integer] -> String -> String -> String +exportEntryExpr name rootHashBytes kind abi = + "(pair " ++ bytesExpr (map (fromIntegral . fromEnum) name) ++ " " + ++ "(pair " ++ bytesExpr rootHashBytes ++ " " + ++ "(pair " ++ bytesExpr (map (fromIntegral . fromEnum) kind) ++ " " + ++ bytesExpr (map (fromIntegral . fromEnum) abi) ++ ")))" + +-- Build list of export entries for the test +singleExportExpr :: String +singleExportExpr = + "[" ++ exportEntryExpr "main" (replicate 32 0) "term" "arboricx.abi.tree.v1" ++ "]" + +multiExportExpr :: String +multiExportExpr = + "[" + ++ exportEntryExpr "main" (replicate 32 0) "term" "arboricx.abi.tree.v1" +-- ++ ", " + ++ exportEntryExpr "test" (replicate 32 1) "term" "arboricx.abi.tree.v1" + ++ "]" + +-- Helper to build a minimal valid manifest core +-- Returns a tricu expression representing the parsed core structure +buildValidCoreExpr :: String +buildValidCoreExpr = + "(pair " + ++ bytesExpr (map (fromIntegral . fromEnum) "arboricx.bundle.manifest.v1") ++ " " -- schema + ++ "(pair " + ++ bytesExpr (map (fromIntegral . fromEnum) "tree-calculus-executable-object") ++ " " -- bundleType + ++ "(pair " + ++ bytesExpr (map (fromIntegral . fromEnum) "tree-calculus.v1") ++ " " -- treeCalculus + ++ "(pair " + ++ bytesExpr (map (fromIntegral . fromEnum) "sha256") ++ " " -- treeHashAlgorithm + ++ "(pair " + ++ bytesExpr (map (fromIntegral . fromEnum) "arboricx.merkle.node.v1") ++ " " -- treeHashDomain + ++ "(pair " + ++ bytesExpr (map (fromIntegral . fromEnum) "arboricx.merkle.payload.v1") ++ " " -- treeNodePayload + ++ "(pair " + ++ bytesExpr (map (fromIntegral . fromEnum) "tree-calculus.v1") ++ " " -- runtimeSemantics + ++ "(pair " + ++ bytesExpr (map (fromIntegral . fromEnum) "normal-order") ++ " " -- runtimeEvaluation + ++ "(pair " + ++ bytesExpr (map (fromIntegral . fromEnum) "arboricx.abi.tree.v1") ++ " " -- runtimeAbi + ++ "(pair " + ++ "[] " -- capabilities + ++ "(pair " + ++ "0 " -- closure + ++ "(pair " + ++ "[(pair " ++ bytesExpr (replicate 32 0) ++ " " + ++ bytesExpr (map (fromIntegral . fromEnum) "default") ++ ")" -- roots (1 root) + ++ "] " + ++ "[(pair " + ++ bytesExpr (map (fromIntegral . fromEnum) "term") ++ " " + ++ "(pair " ++ bytesExpr (replicate 32 0) ++ " " + ++ "(pair " + ++ bytesExpr (map (fromIntegral . fromEnum) "term") ++ " " + ++ bytesExpr (map (fromIntegral . fromEnum) "arboricx.abi.tree.v1") ++ ")))" -- exports (1 export) + ++ "])" + ++ "]" + ++ "]" + ++ "]" + ++ "]" + ++ "]" + ++ "]" + ++ "]" + ++ "]" + ++ "]" + ++ "]" + ++ "]" + ++ "]" + ++ ")" + +-- Build a tricu expression that extracts a specific manifest field from +-- readArboricxBundle result and returns it as a byte-list T value. +-- The Haskell test then uses toString to convert it to a String. +extractManifestField :: ByteString -> String -> String +extractManifestField fixtureBytes fieldName = + "matchResult " + ++ " (errCode rest : errCode) " + ++ " (bundleResult rest : " + ++ " matchPair " + ++ " (validCore metadataWithExtensions : " + ++ " " ++ fieldName ++ " validCore) " + ++ " bundleResult) " + ++ " (readArboricxBundle " ++ bytesExpr (map toInteger $ BS.unpack fixtureBytes) ++ ")" + +manifestReadingTests :: TestTree +manifestReadingTests = testGroup "Manifest Reading Tests" + [ + -- ------------------------------------------------------------------------ + -- Step 1: readManifestMagic + -- ------------------------------------------------------------------------ + testCase "readManifestMagic: accepts correct manifest magic and preserves rest" $ do + let input = "readManifestMagic ((append arboricxManifestMagic) [(1) (2)])" + library <- evaluateFile "./lib/arboricx.tri" + let env = evalTricu library (parseTricu input) + result env @?= okT unitT (bytesT [1,2]) + + , testCase "readManifestMagic: rejects wrong magic" $ do + let input = "readManifestMagic [(65) (83) (66) (77) (78) (70) (83) (84)]" + library <- evaluateFile "./lib/arboricx.tri" + let env = evalTricu library (parseTricu input) + result env @?= errT unexpectedBytesT (bytesT [65,83,66,77,78,70,83,84]) + + , testCase "readManifestMagic: short input returns EOF" $ do + let input = "readManifestMagic [(65) (82) (66) (77)]" + library <- evaluateFile "./lib/arboricx.tri" + let env = evalTricu library (parseTricu input) + result env @?= errT eofT (bytesT [65,82,66,77]) + + -- ------------------------------------------------------------------------ + -- Step 2: readLengthPrefixedString + -- ------------------------------------------------------------------------ + + , testCase "readLengthPrefixedString: reads a 5-byte string" $ do + let input = "readLengthPrefixedString [(0) (0) (0) (5) (104) (101) (108) (108) (111) (99) (111) (110) (116) (101) (114)]" + library <- evaluateFile "./lib/arboricx.tri" + let env = evalTricu library (parseTricu input) + result env @?= okT (bytesT [104,101,108,108,111]) (bytesT [99,111,110,116,101,114]) + + , testCase "readLengthPrefixedString: reads an empty string" $ do + let input = "readLengthPrefixedString [(0) (0) (0) (0) (97) (98)]" + library <- evaluateFile "./lib/arboricx.tri" + let env = evalTricu library (parseTricu input) + result env @?= okT (bytesT []) (bytesT [97,98]) + + , testCase "readLengthPrefixedString: short payload returns EOF" $ do + let input = "readLengthPrefixedString [(0) (0) (0) (5) (104) (101) (108)]" + library <- evaluateFile "./lib/arboricx.tri" + let env = evalTricu library (parseTricu input) + result env @?= errT eofT (bytesT [104,101,108]) + + -- ------------------------------------------------------------------------ + -- Step 3: readManifestCore (construct a minimal valid manifest) + -- ------------------------------------------------------------------------ + + , testCase "readManifestCore: reads a minimal valid manifest core" $ do + let input = "readManifestCore " ++ bytesExpr minimalManifestCoreBytes + library <- evaluateFile "./lib/arboricx.tri" + let env = evalTricu library (parseTricu input) + let actualResult = result env + case actualResult of + (Fork Leaf Leaf) -> assertFailure "should be ok, not t" + (Fork _ (Fork _ rest)) -> return () -- ok case: pair true (pair value rest) + _ -> assertFailure $ "expected ok result, got: " ++ show actualResult + + , testCase "readManifestCore: returns error on wrong magic" $ do + let badMagic = [65,83,66,77,78,70,83,84] ++ (drop 8 minimalManifestCoreBytes) + let input = "readManifestCore " ++ bytesExpr badMagic + library <- evaluateFile "./lib/arboricx.tri" + let env = evalTricu library (parseTricu input) + let actualResult = result env + case actualResult of + (Fork falseT _) -> return () -- err case: pair false (pair code rest) + _ -> assertFailure $ "expected err result, got: " ++ show actualResult + + -- ------------------------------------------------------------------------ + -- Step 4: TLV reader + -- ------------------------------------------------------------------------ + + , testCase "readTLV: reads a metadata TLV entry" $ do + -- tag = u16 1 = [(0)(1)], length = u32 3 = [(0)(0)(0)(3)], value = "foo" = [102,111,111] + let input = "readTLV [(0) (1) (0) (0) (0) (3) (102) (111) (111) (99) (111) (110) (116) (114) (101) (115) (116)]" + library <- evaluateFile "./lib/arboricx.tri" + let env = evalTricu library (parseTricu input) + let actualResult = result env + case actualResult of + (Fork _ (Fork _ rest)) -> do + -- ok case: verify the value pair + let value = case result env of + (Fork _ (Fork val _)) -> case val of + (Fork tagVal _) -> tagVal + _ -> Leaf + return () + _ -> assertFailure $ "expected ok result, got: " ++ show actualResult + + , testCase "readTLV: returns EOF on empty input" $ do + let input = "readTLV []" + library <- evaluateFile "./lib/arboricx.tri" + let env = evalTricu library (parseTricu input) + result env @?= errT eofT (bytesT []) + + , testCase "readTLV: returns EOF on short tag" $ do + let input = "readTLV [(0)]" + library <- evaluateFile "./lib/arboricx.tri" + let env = evalTricu library (parseTricu input) + result env @?= errT eofT (bytesT [0]) + + , testCase "readTLVList: reads zero TLV entries" $ do + let input = "readTLVList 0 [(1) (2) (3)]" + library <- evaluateFile "./lib/arboricx.tri" + let env = evalTricu library (parseTricu input) + result env @?= okT (ofList []) (bytesT [1,2,3]) + + , testCase "readTLVList: reads one TLV entry and preserves rest" $ do + -- tag=1, len=3, value="foo" + let input = "readTLVList 1 [(0) (1) (0) (0) (0) (3) (102) (111) (111) (99) (111) (110) (116) (114) (101) (115) (116)]" + library <- evaluateFile "./lib/arboricx.tri" + let env = evalTricu library (parseTricu input) + let actualResult = result env + case actualResult of + (Fork _ (Fork _ rest)) -> do + -- ok: value is list with one TLV, rest should be [(99)...] + return () + _ -> assertFailure $ "expected ok result, got: " ++ show actualResult + + -- ------------------------------------------------------------------------ + -- Step 5: readManifest (full parser) + -- ------------------------------------------------------------------------ + + , testCase "readManifest: parses a minimal manifest with no metadata" $ do + let input = "readManifest " ++ bytesExpr fullMinimalManifestBytes + library <- evaluateFile "./lib/arboricx.tri" + let env = evalTricu library (parseTricu input) + let actualResult = result env + case actualResult of + (Fork _ (Fork _ _)) -> return () -- ok result + _ -> assertFailure $ "expected ok result, got: " ++ show actualResult + + , testCase "readManifest: preserves trailing extension bytes" $ do + let input = "readManifest (append " ++ bytesExpr fullMinimalManifestBytes ++ " [(99) (111) (110) (116) (101) (110) (116) (101) (114)])" + library <- evaluateFile "./lib/arboricx.tri" + let env = evalTricu library (parseTricu input) + let actualResult = result env + case actualResult of + (Fork trueTag (Fork _ _)) | trueTag == trueT -> return () + _ -> assertFailure $ "expected ok result, got: " ++ show actualResult + + -- ------------------------------------------------------------------------ + -- Step 6: lookupMetadata + -- ------------------------------------------------------------------------ + + , testCase "lookupMetadata: finds metadata by tag" $ do + let tlv1 = makeTLVPair 1 "my-pkg" + let tlv2 = makeTLVPair 2 "1.0" + let input = "lookupMetadata (" ++ tlv1 ++ ") " ++ bytesExpr [(0), (1)] + library <- evaluateFile "./lib/arboricx.tri" + let env = evalTricu library (parseTricu input) + result env @?= justT (bytesT [109,121,45,112,107,103]) + + , testCase "lookupMetadata: returns nothing for unknown tag" $ do + let tlv1 = makeTLVPair 1 "my-pkg" + let input = "lookupMetadata " ++ tlv1 ++ " " ++ bytesExpr [(0), (2)] + library <- evaluateFile "./lib/arboricx.tri" + let env = evalTricu library (parseTricu input) + result env @?= nothingT + + , testCase "lookupMetadata: returns nothing for empty list" $ do + let input = "lookupMetadata [] " ++ bytesExpr [(0), (1)] + library <- evaluateFile "./lib/arboricx.tri" + let env = evalTricu library (parseTricu input) + result env @?= nothingT + + -- ------------------------------------------------------------------------ + -- Step 7: Export selection + -- ------------------------------------------------------------------------ + + -- Build export entry: (pair name (pair rootHash (pair kind abi))) + -- Test: select export by explicit name ("main") + , testCase "selectExport: finds export by explicit name" $ do + let input = "selectExport " ++ multiExportExpr ++ " " ++ bytesExpr (map (fromIntegral . fromEnum) "main") + library <- evaluateFile "./lib/arboricx.tri" + let env = evalTricu library (parseTricu input) + let actualResult = result env + case actualResult of + (Fork _ (Fork _ _)) -> return () -- ok result + _ -> assertFailure $ "expected ok result, got: " ++ show actualResult + + -- Test: selectExport prefers "main" when no explicit name + , testCase "selectExport: selects 'main' when no explicit name and 'main' exists" $ do + let input = "selectExport " ++ multiExportExpr ++ " " ++ bytesExpr [] + library <- evaluateFile "./lib/arboricx.tri" + let env = evalTricu library (parseTricu input) + let actualResult = result env + case actualResult of + (Fork _ (Fork _ _)) -> return () -- ok result + _ -> assertFailure $ "expected ok result, got: " ++ show actualResult + + -- Test: selectExport selects single export when only one exists + , testCase "selectExport: auto-selects single export" $ do + let input = "selectExport " ++ singleExportExpr ++ " " ++ bytesExpr [] + library <- evaluateFile "./lib/arboricx.tri" + let env = evalTricu library (parseTricu input) + let actualResult = result env + case actualResult of + (Fork _ (Fork _ _)) -> return () -- ok result + _ -> assertFailure $ "expected ok result, got: " ++ show actualResult + + -- Test: getExportNames lists all export names + , testCase "getExportNames: returns list of all export names" $ do + let input = "getExportNames " ++ multiExportExpr + library <- evaluateFile "./lib/arboricx.tri" + let env = evalTricu library (parseTricu input) + let actualResult = result env + -- Should return a list of two byte strings + case actualResult of + (Fork (Fork _ _) (Fork (Fork _ _) _)) -> return () -- list with 2 items + _ -> assertFailure $ "expected list of 2 items, got: " ++ show actualResult + + -- Test: selectExport errors when multiple exports but no "main" and no explicit name + , testCase "selectExport: errors with multiple exports but no 'main'" $ do + let multiNoMain = + "[" + ++ exportEntryExpr "validate" (replicate 32 0) "term" "arboricx.abi.tree.v1" + ++ " " + ++ exportEntryExpr "test" (replicate 32 1) "term" "arboricx.abi.tree.v1" + ++ "]" + let input = "selectExport " ++ multiNoMain ++ " " ++ bytesExpr [] + library <- evaluateFile "./lib/arboricx.tri" + let env = evalTricu library (parseTricu input) + let actualResult = result env + case actualResult of + (Fork falseT _) -> return () -- err result + _ -> assertFailure $ "expected err result, got: " ++ show actualResult + + -- Test: selectExportOpt works with Just bytes (explicit name given) + , testCase "selectExportOpt: selects by explicit name when given" $ do + let input = "selectExportOpt " ++ multiExportExpr ++ " " ++ bytesExpr (map (fromIntegral . fromEnum) "validate") + library <- evaluateFile "./lib/arboricx.tri" + let env = evalTricu library (parseTricu input) + let actualResult = result env + case actualResult of + (Fork _ (Fork _ _)) -> return () -- ok result + _ -> assertFailure $ "expected ok result, got: " ++ show actualResult + + -- ------------------------------------------------------------------------ + -- Step 8: validateManifestCore + -- ------------------------------------------------------------------------ + + , testCase "validateManifestCore: passes on valid core" $ do + let input = "matchResult (code rest : err code rest) (core rest : validateManifestCore core " ++ bytesExpr [(1), (2)] ++ ") (readManifestCore " ++ bytesExpr minimalManifestCoreBytes ++ ")" + library <- evaluateFile "./lib/arboricx.tri" + let env = evalTricu library (parseTricu input) + let actualResult = result env + case actualResult of + (Fork trueTag (Fork _ rest)) | trueTag == trueT -> rest @?= bytesT [1,2] + _ -> assertFailure $ "expected ok result, got: " ++ show actualResult + + , testCase "validateManifestCore: fails on wrong schema" $ do + let badCoreBytes = take 16 minimalManifestCoreBytes ++ map (fromIntegral . fromEnum) "z" ++ drop 17 minimalManifestCoreBytes + let input = "matchResult (code rest : err code rest) (core rest : validateManifestCore core " ++ bytesExpr [] ++ ") (readManifestCore " ++ bytesExpr badCoreBytes ++ ")" + library <- evaluateFile "./lib/arboricx.tri" + let env = evalTricu library (parseTricu input) + let actualResult = result env + case actualResult of + (Fork falseTag _) | falseTag == falseT -> return () + _ -> assertFailure $ "expected err result, got: " ++ show actualResult + + -- ------------------------------------------------------------------------ + -- Step 9: readArboricxBundle (end-to-end with real fixture) + -- ------------------------------------------------------------------------ + + , testCase "readArboricxBundle: parses id.arboricx fixture" $ do + fixtureBytes <- BS.readFile "test/fixtures/id.arboricx" + case decodeBundle fixtureBytes of + Left err -> assertFailure $ "decodeBundle failed: " ++ err + Right bundle -> do + let manifestBytes = bundleManifestBytes bundle + -- The manifest section should be parseable + let input = "readManifest " ++ bytesExpr (map toInteger (BS.unpack manifestBytes)) + library <- evaluateFile "./lib/arboricx.tri" + let env = evalTricu library (parseTricu input) + let actualResult = result env + case actualResult of + (Fork trueTag (Fork _ _)) | trueTag == trueT -> return () + _ -> assertFailure $ "readManifest failed on id.arboricx manifest: " ++ show actualResult + + , testCase "readArboricxBundle: end-to-end bundle parse" $ do + fixtureBytes <- BS.readFile "test/fixtures/id.arboricx" + let input = "readArboricxBundle " ++ bytesExpr (map toInteger (BS.unpack fixtureBytes)) + library <- evaluateFile "./lib/arboricx.tri" + let env = evalTricu library (parseTricu input) + let actualResult = result env + case actualResult of + (Fork _ (Fork _ _)) -> return () -- ok: (pair validManifest afterManifest) + _ -> assertFailure $ "readArboricxBundle failed: " ++ show actualResult + + , testCase "readArboricxBundle: rejects bundle with wrong manifest core" $ do + fixtureBytes <- BS.readFile "test/fixtures/id.arboricx" + -- Modify a byte in the manifest section to invalidate it + -- The manifest starts at offset 152 in the bundle (from header dirOffset=32) + -- Section directory: 2 entries * 60 = 120 bytes, starting at offset 32 + -- Manifest entry at directory offset 32: type(4) + version(2) + flags(2) + compression(2) + digestAlg(2) + offset(8) + length(8) + digest(32) = 60 + -- Manifest offset = 32 + 60 = 92 + -- The manifest itself starts at offset 152 (0x98) + -- Change byte at position 152+8 = 160 from 'a' (97) to 'z' (122) to break the schema string + let bs = map toInteger (BS.unpack fixtureBytes) + let modifiedBs = take 160 bs ++ [122] ++ drop 161 bs + let input = "readArboricxBundle " ++ bytesExpr modifiedBs + library <- evaluateFile "./lib/arboricx.tri" + let env = evalTricu library (parseTricu input) + let actualResult = result env + case actualResult of + (Fork falseT _) -> return () -- err result (validation failure) + _ -> assertFailure $ "expected err result, got: " ++ show actualResult + + -- ------------------------------------------------------------------------ + -- Comprehensive end-to-end: extract manifest fields and verify as strings + -- ------------------------------------------------------------------------ + + , testCase "readArboricxBundle: extracts and validates manifest schema" $ do + fixtureBytes <- BS.readFile "test/fixtures/id.arboricx" + let input = extractManifestField fixtureBytes "manifestSchema" + library <- evaluateFile "./lib/arboricx.tri" + let env = evalTricu library (parseTricu input) + let schemaT = result env + toString schemaT @?= Right "arboricx.bundle.manifest.v1" + + , testCase "readArboricxBundle: extracts and validates bundleType" $ do + fixtureBytes <- BS.readFile "test/fixtures/id.arboricx" + let input = extractManifestField fixtureBytes "manifestBundleType" + library <- evaluateFile "./lib/arboricx.tri" + let env = evalTricu library (parseTricu input) + let bundleTypeT = result env + toString bundleTypeT @?= Right "tree-calculus-executable-object" + + , testCase "readArboricxBundle: extracts and validates runtime evaluation" $ do + fixtureBytes <- BS.readFile "test/fixtures/id.arboricx" + let input = extractManifestField fixtureBytes "manifestRuntimeEvaluation" + library <- evaluateFile "./lib/arboricx.tri" + let env = evalTricu library (parseTricu input) + let evalT = result env + toString evalT @?= Right "normal-order" + + , testCase "readArboricxBundle: extracts and validates runtime ABI" $ do + fixtureBytes <- BS.readFile "test/fixtures/id.arboricx" + let input = extractManifestField fixtureBytes "manifestRuntimeAbi" + library <- evaluateFile "./lib/arboricx.tri" + let env = evalTricu library (parseTricu input) + let abiT = result env + toString abiT @?= Right "arboricx.abi.tree.v1" + + , testCase "readArboricxBundle: extracts and validates root names" $ do + fixtureBytes <- BS.readFile "test/fixtures/id.arboricx" + let input = "matchResult " + ++ " (errCode rest : errCode) " + ++ " (bundleResult rest : " + ++ " matchPair " + ++ " (validCore metadataWithExtensions : " + ++ " matchList " + ++ " (err 99 t) " -- empty roots + ++ " (rootEntry rest : " + ++ " matchPair " + ++ " (_ roleField : roleField) " + ++ " rootEntry) " + ++ " (manifestRoots validCore)) " + ++ " bundleResult) " + ++ " (readArboricxBundle " ++ bytesExpr (map toInteger $ BS.unpack fixtureBytes) ++ ")" + library <- evaluateFile "./lib/arboricx.tri" + let env = evalTricu library (parseTricu input) + let rootRoleT = result env + -- Should find at least one root with a role (either "default" or "root") + case toString rootRoleT of + Right role -> assertBool "root role should be 'default' or 'root'" + (role == "default" || role == "root") + Left err -> assertFailure $ "failed to extract root role: " ++ err + + , testCase "readArboricxBundle: extracts and validates closure" $ do + fixtureBytes <- BS.readFile "test/fixtures/id.arboricx" + let input = "matchResult " + ++ " (errCode rest : errCode) " + ++ " (bundleResult rest : " + ++ " matchPair " + ++ " (validCore metadataWithExtensions : " + ++ " matchPair " + ++ " (closure _ : closure) " + ++ " (manifestClosureByte validCore)) " + ++ " bundleResult) " + ++ " (readArboricxBundle " ++ bytesExpr (map toInteger $ BS.unpack fixtureBytes) ++ ")" + library <- evaluateFile "./lib/arboricx.tri" + let env = evalTricu library (parseTricu input) + let closureT = result env + case toNumber closureT of + Right 0 -> return () + Right n -> assertFailure $ "closure should be 0, got " ++ show n + Left err -> assertFailure $ "failed to extract closure: " ++ err + + , testCase "readArboricxBundle: extracts and validates hash algorithm" $ do + fixtureBytes <- BS.readFile "test/fixtures/id.arboricx" + let input = extractManifestField fixtureBytes "manifestTreeHashAlgorithm" + library <- evaluateFile "./lib/arboricx.tri" + let env = evalTricu library (parseTricu input) + let algoT = result env + toString algoT @?= Right "sha256" + ]