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