86fe4cfaf4adb3f897d87265ff2ee6c6b21eabea1fb0724b161164c6c026aa66.tri (11441B)
1 !import prelude * 2 !import binary * 3 !import arboricx_common * 4 !import arboricx_nodes * 5 !export * 6 7 readManifestMagic = (bs : 8 expectBytes arboricxManifestMagic bs) 9 10 -- Read a u32 BE length, then that many raw bytes. 11 -- Returns the payload bytes and remaining input. 12 readLengthPrefixedString = (do bindParser 13 lengthBytes <- readBytes 4 14 payload <- readBytes (u32BEBytesToNat lengthBytes) 15 pureParser payload) 16 17 -- Helper: read a single capability string (length-prefixed string) 18 readCapability = (bs : 19 readLengthPrefixedString bs) 20 21 -- Helper worker: read N capability strings (counts up from 0) 22 readCapabilities_ bs count i acc = (matchBool 23 (ok (reverse acc) bs) 24 (bindResult (readCapability bs) 25 (cap afterCap : 26 readCapabilities_ afterCap count (succ i) (pair cap acc))) 27 (equal? i count)) 28 29 -- Helper: read N capabilities 30 readCapabilities = (count bs : 31 readCapabilities_ bs count 0 t) 32 33 -- Helper: read a single root entry (4-byte u32 BE index + length-prefixed role) 34 readRootEntry = (do bindParser 35 indexRaw <- readBytes 4 36 role <- readLengthPrefixedString 37 pureParser (pair indexRaw role)) 38 39 -- Helper worker: read N root entries (counts up from 0) 40 readRoots_ bs count i acc = (matchBool 41 (ok (reverse acc) bs) 42 (bindResult (readRootEntry bs) 43 (root afterRoot : 44 readRoots_ afterRoot count (succ i) (pair root acc))) 45 (equal? i count)) 46 47 -- Helper: read N roots 48 readRoots = (count bs : 49 readRoots_ bs count 0 t) 50 51 -- Helper: read a single export entry 52 readExportEntry = (do bindParser 53 name <- readLengthPrefixedString 54 rootIndexRaw <- readBytes 4 55 kind <- readLengthPrefixedString 56 abi <- readLengthPrefixedString 57 pureParser (pair name (pair rootIndexRaw (pair kind abi)))) 58 59 -- Helper worker: read N export entries (counts up from 0) 60 readExports_ bs count i acc = (matchBool 61 (ok (reverse acc) bs) 62 (bindResult (readExportEntry bs) 63 (exp afterExp : 64 readExports_ afterExp count (succ i) (pair exp acc))) 65 (equal? i count)) 66 67 -- Helper: read N exports 68 readExports = (count bs : 69 readExports_ bs count 0 t) 70 71 -- Main core manifest parser. 72 -- Reads: magic, version, core strings, capabilities, closure, roots, exports. 73 readManifestCore = (do bindParser 74 readManifestMagic 75 readBytes 2 76 readBytes 2 77 schema <- readLengthPrefixedString 78 bundleType <- readLengthPrefixedString 79 treeCalculus <- readLengthPrefixedString 80 treeHashAlgorithm <- readLengthPrefixedString 81 treeHashDomain <- readLengthPrefixedString 82 treeNodePayload <- readLengthPrefixedString 83 runtimeSemantics <- readLengthPrefixedString 84 runtimeEvaluation <- readLengthPrefixedString 85 runtimeAbi <- readLengthPrefixedString 86 capCountRaw <- readBytes 4 87 capabilities <- readCapabilities (u32BEBytesToNat capCountRaw) 88 closureByte <- readBytes 1 89 rootCountRaw <- readBytes 4 90 roots <- readRoots (u32BEBytesToNat rootCountRaw) 91 exportCountRaw <- readBytes 4 92 exports <- readExports (u32BEBytesToNat exportCountRaw) 93 pureParser (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))))))))))))) 94 95 -- Metadata tag constants (u16 values) 96 tagPackage = [(0) (1)] 97 tagVersion = [(0) (2)] 98 tagDescription = [(0) (3)] 99 tagLicense = [(0) (4)] 100 tagCreatedBy = [(0) (5)] 101 102 -- Read a single TLV entry: u16 tag + u32 length + value bytes. 103 -- Returns the pair (tag, value) and remaining input. 104 readTLV = (do bindParser 105 tag <- readBytes 2 106 tlvLenRaw <- readBytes 4 107 tlvValue <- readBytes (u32BEBytesToNat tlvLenRaw) 108 pureParser (pair tag tlvValue)) 109 110 -- Worker: read N TLV entries (counts up from 0) 111 readTLVs_ bs count i acc = (matchBool 112 (ok (reverse acc) bs) 113 (bindResult (readTLV bs) 114 (tlv afterTlv : 115 readTLVs_ afterTlv count (succ i) (pair tlv acc))) 116 (equal? i count)) 117 118 -- Read a count followed by that many TLV entries. 119 readTLVList = (count bs : 120 readTLVs_ bs count 0 t) 121 122 -- Skip N extension TLV entries (counts up from 0) 123 skipTLVs_ bs count i = (matchBool 124 (ok unit bs) 125 (bindResult (readTLV bs) 126 (_ afterTlv : 127 skipTLVs_ afterTlv count (succ i))) 128 (equal? i count)) 129 130 -- Full manifest parser: core fields + metadata TLV list + extension TLV list. 131 -- Historical boundary: the extension value and success remainder below are 132 -- unit, not the suffix returned by skipTLVs_. Preserve that behavior here; 133 -- unlike the field readers, this entrypoint discards a successful suffix. 134 readManifest = (bs : 135 bindResult (readManifestCore bs) 136 (coreManifest afterCore : 137 bindResult (readBytes 4 afterCore) 138 (metaCountRaw afterMetaCountRaw : 139 bindResult (readTLVList (u32BEBytesToNat metaCountRaw) afterMetaCountRaw) 140 (metadataFields afterMetadataFields : 141 bindResult (readBytes 4 afterMetadataFields) 142 (extCountRaw afterExtCountRaw : 143 bindResult (skipTLVs_ afterExtCountRaw (u32BEBytesToNat extCountRaw) 0) 144 (afterExtensions _ : 145 ok 146 (pair coreManifest (pair metadataFields afterExtensions)) 147 afterExtensions)))))) 148 149 -- Lookup a metadata value by tag from a TLV list. 150 -- Returns nothing if not found, just value if found. 151 lookupMetadata_ tlvs tag = (matchList 152 nothing 153 (tlv rest : 154 matchBool 155 (just (matchPair (_ value : value) tlv)) 156 (lookupMetadata_ rest tag) 157 (bytesEq? (matchPair (tlvTag _ : tlvTag) tlv) tag)) 158 tlvs) 159 160 lookupMetadata = (tlvs tag : 161 lookupMetadata_ tlvs tag) 162 163 -- Get export name from an export entry (pair name (pair rootIndex (pair kind abi))) 164 exportName = (exp : 165 matchPair 166 (name _ : name) 167 exp) 168 169 exportRoot = (exp : 170 matchPair 171 (_ payload : 172 matchPair 173 (root _ : root) 174 payload) 175 exp) 176 177 -- Check if an export name matches a given byte string. 178 exportNameEq? = (nameBytes exp : 179 bytesEq? nameBytes (exportName exp)) 180 181 -- Find first export matching a name, or nothing. 182 findExportByName_ exports name = (matchList 183 nothing 184 (exp rest : 185 matchBool 186 (just exp) 187 (findExportByName_ rest name) 188 (exportNameEq? name exp)) 189 exports) 190 191 findExportByName = (exports name : 192 findExportByName_ exports name) 193 194 -- Get list of all export names from a list of exports. 195 getExportNames_ acc exports = (matchList 196 (reverse acc) 197 (exp rest : 198 getExportNames_ (pair (exportName exp) acc) rest) 199 exports) 200 201 getExportNames = (exports : 202 getExportNames_ t exports) 203 204 mainExportName = "main" 205 206 maybeExportToResult = (maybeExport : 207 triage 208 (err errMissingSection t) 209 (export : ok export t) 210 (_ _ : err errMissingSection t) 211 maybeExport) 212 213 selectSingleExport = (exports : 214 matchList 215 (err errMissingSection t) 216 (export rest : 217 matchBool 218 (ok export t) 219 (err errMissingSection t) 220 (emptyList? rest)) 221 exports) 222 223 selectDefaultExport = (exports : 224 triage 225 (selectSingleExport exports) 226 (export : ok export t) 227 (_ _ : err errMissingSection t) 228 (findExportByName exports mainExportName)) 229 230 -- Select an export: explicit name if provided, otherwise "main", otherwise 231 -- the sole export if the bundle has exactly one export. 232 selectExport = (exports nameBytes : 233 matchBool 234 (selectDefaultExport exports) 235 (maybeExportToResult (findExportByName exports nameBytes)) 236 (emptyList? nameBytes)) 237 238 selectExportOpt = (exports optNameBytes : 239 selectExport exports optNameBytes) 240 241 -- Expected core string values (raw UTF-8 bytes, not decoded to Unicode characters). 242 expectedSchema = "arboricx.bundle.manifest.v1" 243 expectedBundleType = "tree-calculus-executable-object" 244 expectedTreeCalculus = "tree-calculus.v1" 245 expectedTreeHashAlgorithm = "indexed" 246 expectedTreeHashDomain = "arboricx.indexed.node.v1" 247 expectedTreeNodePayload = "arboricx.indexed.payload.v1" 248 expectedRuntimeSemantics = "tree-calculus.v1" 249 expectedRuntimeEvaluation = "normal-order" 250 expectedRuntimeAbi = "arboricx.abi.tree.v1" 251 252 -- Manifest core field accessors. 253 -- readManifestCore returns: (pair schema (pair bundleType (... (pair closureByte (pair roots exports))))) 254 pairFirst = (p : matchPair (a _ : a) p) 255 pairSecond = (p : matchPair (_ b : b) p) 256 257 manifestSchema = (core : pairFirst core) 258 manifestBundleType = (core : pairFirst (pairSecond core)) 259 manifestTreeCalculus = (core : pairFirst (pairSecond (pairSecond core))) 260 manifestTreeHashAlgorithm = (core : pairFirst (pairSecond (pairSecond (pairSecond core)))) 261 manifestTreeHashDomain = (core : pairFirst (pairSecond (pairSecond (pairSecond (pairSecond core))))) 262 manifestTreeNodePayload = (core : pairFirst (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond core)))))) 263 manifestRuntimeSemantics = (core : pairFirst (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond core))))))) 264 manifestRuntimeEvaluation = (core : pairFirst (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond core)))))))) 265 manifestRuntimeAbi = (core : pairFirst (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond core))))))))) 266 manifestCapabilities = (core : pairFirst (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond core)))))))))) 267 manifestClosureByte = (core : pairFirst (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond core))))))))))) 268 manifestRoots = (core : pairFirst (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond core)))))))))))) 269 manifestExports = (core : pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond (pairSecond core)))))))))))) 270 271 -- Helper: compare a manifest field against an expected byte string. 272 manifestFieldMatch? = (actual expected : bytesEq? actual expected) 273 274 -- Validate core manifest fields against expected values. 275 validateManifestCore = (core rest : 276 matchBool 277 (ok core rest) 278 (err errManifestValidationFailed rest) 279 (and? 280 (manifestFieldMatch? (manifestSchema core) expectedSchema) 281 (and? 282 (manifestFieldMatch? (manifestBundleType core) expectedBundleType) 283 (and? 284 (manifestFieldMatch? (manifestTreeCalculus core) expectedTreeCalculus) 285 (and? 286 (manifestFieldMatch? (manifestTreeHashAlgorithm core) expectedTreeHashAlgorithm) 287 (and? 288 (manifestFieldMatch? (manifestTreeHashDomain core) expectedTreeHashDomain) 289 (and? 290 (manifestFieldMatch? (manifestTreeNodePayload core) expectedTreeNodePayload) 291 (and? 292 (manifestFieldMatch? (manifestRuntimeSemantics core) expectedRuntimeSemantics) 293 (and? 294 (manifestFieldMatch? (manifestRuntimeEvaluation core) expectedRuntimeEvaluation) 295 (and? 296 (manifestFieldMatch? (manifestRuntimeAbi core) expectedRuntimeAbi) 297 (and? 298 (bytesEq? (manifestClosureByte core) [(0)]) 299 (and? 300 (not? (emptyList? (manifestRoots core))) 301 (not? (emptyList? (manifestExports core)))))))))))))))