tricu

An interpreted language for exploring Tree Calculus
Log | Files | Refs | README | LICENSE

common.tri (8707B)

      1 !import prelude *
      2 !import binary *
      3 !import native_math as N
      4 !export *
      5 
      6 
      7 arboricxMagic = [(65) (82) (66) (79) (82) (73) (67) (88)]
      8 arboricxMajorVersion = [(0) (1)]
      9 arboricxMinorVersion = [(0) (0)]
     10 arboricxManifestSectionId = [(0) (0) (0) (1)]
     11 arboricxNodesSectionId = [(0) (0) (0) (2)]
     12 
     13 -- Manifest magic and version constants
     14 arboricxManifestMagic = [(65) (82) (66) (77) (78) (70) (83) (84)]
     15 arboricxManifestMajorVersion = [(0) (1)]
     16 arboricxManifestMinorVersion = [(0) (1)]
     17 
     18 errMissingSection = 4
     19 errUnsupportedVersion = 5
     20 errDuplicateSection = 6
     21 errDuplicateNode = 7
     22 errInvalidNodePayload = 8
     23 errMissingNode = 9
     24 errInvalidManifestMagic = 10
     25 errUnsupportedManifestVersion = 11
     26 errTrailingManifestBytes = 12
     27 errManifestValidationFailed = 13
     28 
     29 nodePayloadLeafTag = 0
     30 nodePayloadStemTag = 1
     31 nodePayloadForkTag = 2
     32 
     33 readArboricxMagic = (bs : expectBytes arboricxMagic bs)
     34 
     35 readArboricxHeader = (do bindParser
     36   readArboricxMagic
     37   majorVersion <- readBytes 2
     38   minorVersion <- readBytes 2
     39   sectionCount <- readBytes 4
     40   flags <- readBytes 8
     41   dirOffset <- readBytes 8
     42   pureParser (pair majorVersion (pair minorVersion (pair sectionCount (pair flags dirOffset)))))
     43 
     44 readSectionRecord = (do bindParser
     45   sectionId <- readBytes 4
     46   sectionVersion <- readBytes 2
     47   sectionFlags <- readBytes 2
     48   compression <- readBytes 2
     49   reserved1 <- readBytes 2
     50   offset <- readBytes 8
     51   length <- readBytes 8
     52   reserved2 <- readBytes 4
     53   pureParser (pair sectionId (pair sectionVersion (pair sectionFlags (pair compression (pair reserved1 (pair offset (pair length reserved2))))))))
     54 
     55 readSectionDirectory count = repeatParser count readSectionRecord
     56 
     57 sectionRecordId record = case record of
     58   (value, _) = value
     59   _ = t
     60 
     61 sectionRecordVersion record = case record of
     62   (_, (value, _)) = value
     63   _ = t
     64 
     65 sectionRecordFlags record = case record of
     66   (_, (_, (value, _))) = value
     67   _ = t
     68 
     69 sectionRecordCompression record = case record of
     70   (_, (_, (_, (value, _)))) = value
     71   _ = t
     72 
     73 sectionRecordReserved1 record = case record of
     74   (_, (_, (_, (_, (value, _))))) = value
     75   _ = t
     76 
     77 sectionRecordOffset record = case record of
     78   (_, (_, (_, (_, (_, (value, _)))))) = value
     79   _ = t
     80 
     81 sectionRecordLength record = case record of
     82   (_, (_, (_, (_, (_, (_, (value, _))))))) = value
     83   _ = t
     84 
     85 sectionRecordReserved2 record = case record of
     86   (_, (_, (_, (_, (_, (_, (_, value))))))) = value
     87   _ = t
     88 
     89 lookupSectionRecord sectionId directory = find (record : bytesEq? sectionId (sectionRecordId record)) directory
     90 sectionDirectoryHasId? sectionId directory = any? (record : bytesEq? sectionId (sectionRecordId record)) directory
     91 sectionDirectoryHasDuplicateIds? directory = case directory of
     92   [] = false
     93   [record | rest] = or? (sectionDirectoryHasId? (sectionRecordId record) rest) (sectionDirectoryHasDuplicateIds? rest)
     94   _ = true
     95 
     96 errUnsupportedSection = 17
     97 errInvalidSectionRange = 18
     98 sectionRecordSupported? record = (and?
     99   (and? (equal? (sectionRecordVersion record) [0 1])
    100     (or? (equal? (sectionRecordFlags record) [0 0]) (equal? (sectionRecordFlags record) [0 1])))
    101   (and? (equal? (sectionRecordCompression record) [0 0])
    102     (and? (equal? (sectionRecordReserved1 record) [0 0])
    103       (and? (equal? (sectionRecordReserved2 record) [0 0 0 0])
    104         (or? (equal? (sectionRecordFlags record) [0 0])
    105           (or? (equal? (sectionRecordId record) arboricxManifestSectionId)
    106             (equal? (sectionRecordId record) arboricxNodesSectionId)))))))
    107 
    108 validateSectionDirectory directory rest = (lazyBool
    109   (_ : err errDuplicateSection rest)
    110   (_ : lazyBool (_ : ok directory rest) (_ : err errUnsupportedSection rest)
    111     (all? sectionRecordSupported? directory))
    112   (sectionDirectoryHasDuplicateIds? directory))
    113 
    114 -- Section ranges must be wholly after the directory, in bounds and disjoint.
    115 -- Sections are few; pairwise overlap checking is deliberately simple.
    116 validateSectionRanges directory total rest = (let
    117   start = N.add 32 (N.multiply 32 (length directory))
    118   end record = N.add (sectionRecordOffsetNat record) (sectionRecordLengthNat record)
    119   overlaps a b = (and? (not? (N.zero (sectionRecordLengthNat a)))
    120     (and? (not? (N.zero (sectionRecordLengthNat b)))
    121       (and? (N.lt (sectionRecordOffsetNat a) (end b)) (N.lt (sectionRecordOffsetNat b) (end a)))))
    122   in let rec
    123     valid records = (case records of
    124       [] = true
    125       [record | tail] = (and? (N.gte (sectionRecordOffsetNat record) start)
    126         (and? (N.lte (end record) total)
    127           (and? (not? (any? (overlaps record) tail)) (valid tail))))
    128       _ = false)
    129     in lazyBool (_ : ok directory rest) (_ : err errInvalidSectionRange rest) (valid directory))
    130 
    131 byteSlice = (offset length bytes : bytesTake length (bytesDrop offset bytes))
    132 
    133 -- Unchecked canonical-byte fold; readers validate octets before this conversion.
    134 -- Remove the independent broken adder rather than preserving its representation bug.
    135 beBytesToNat bytes = foldl (acc byte : N.add (N.multiply acc 256) byte) 0 bytes
    136 u32BEBytesToNat = beBytesToNat
    137 u64BEBytesToNat = beBytesToNat
    138 
    139 arboricxHeaderMajorVersion record = case record of
    140   (value, _) = value
    141   _ = t
    142 
    143 arboricxHeaderMinorVersion record = case record of
    144   (_, (value, _)) = value
    145   _ = t
    146 
    147 arboricxHeaderSectionCount record = case record of
    148   (_, (_, (value, _))) = value
    149   _ = t
    150 
    151 arboricxHeaderFlags record = case record of
    152   (_, (_, (_, (value, _)))) = value
    153   _ = t
    154 
    155 arboricxHeaderDirOffset record = case record of
    156   (_, (_, (_, (_, value)))) = value
    157   _ = t
    158 
    159 validateArboricxHeader = (header rest :
    160   matchBool
    161     (ok header rest)
    162     (err errUnsupportedVersion rest)
    163     (and?
    164       (bytesEq? arboricxMajorVersion (arboricxHeaderMajorVersion header))
    165       (and? (bytesEq? arboricxMinorVersion (arboricxHeaderMinorVersion header))
    166         (and? (equal? (arboricxHeaderFlags header) [0 0 0 0 0 0 0 0])
    167           (equal? (arboricxHeaderDirOffset header) [0 0 0 0 0 0 0 32])))))
    168 
    169 readArboricxContainerChecked = (bs :
    170   bindResult (readArboricxHeader bs)
    171     (header afterHeader :
    172       bindResult (validateArboricxHeader header afterHeader)
    173         (validHeader afterValidHeader :
    174           bindResult (readSectionDirectory
    175             (u32BEBytesToNat (arboricxHeaderSectionCount validHeader))
    176             (bytesDrop (u64BEBytesToNat (arboricxHeaderDirOffset validHeader)) bs))
    177             (directory afterDirectory :
    178               bindResult (validateSectionDirectory directory afterDirectory)
    179                 (validDirectory afterValidDirectory :
    180                   bindResult (validateSectionRanges validDirectory (length bs) afterValidDirectory)
    181                     (checked rest : ok (pair validHeader checked) rest))))))
    182 
    183 -- This is an in-memory boundary, not an incremental stream parser.
    184 readArboricxContainer bs = (lazyBool
    185   (_ : readArboricxContainerChecked bs)
    186   (_ : err errInvalidBinaryInput bs)
    187   (binaryBytes? bs))
    188 
    189 sectionRecordOffsetNat = (sectionRecord :
    190   u64BEBytesToNat (sectionRecordOffset sectionRecord))
    191 
    192 sectionRecordLengthNat = (sectionRecord :
    193   u64BEBytesToNat (sectionRecordLength sectionRecord))
    194 
    195 extractSectionBytes = (sectionRecord containerBytes :
    196   byteSlice
    197     (sectionRecordOffsetNat sectionRecord)
    198     (sectionRecordLengthNat sectionRecord)
    199     containerBytes)
    200 
    201 extractSectionBytesResult = (sectionRecord containerBytes rest :
    202   (sectionBytes :
    203     matchBool
    204       (ok sectionBytes rest)
    205       (err errUnexpectedEof rest)
    206       (equal? (bytesLength sectionBytes) (sectionRecordLengthNat sectionRecord)))
    207     (extractSectionBytes sectionRecord containerBytes))
    208 
    209 lookupSectionBytes = (sectionId directory containerBytes :
    210   triage
    211     nothing
    212     (sectionRecord : just (extractSectionBytes sectionRecord containerBytes))
    213     (_ _ : nothing)
    214     (lookupSectionRecord sectionId directory))
    215 
    216 sectionBytesOrErr = (sectionId directory containerBytes rest :
    217   triage
    218     (err errMissingSection rest)
    219     (sectionRecord : extractSectionBytesResult sectionRecord containerBytes rest)
    220     (_ _ : err errMissingSection rest)
    221     (lookupSectionRecord sectionId directory))
    222 
    223 readArboricxSectionBytes = (sectionId bs :
    224   bindResult (readArboricxContainer bs)
    225     (container afterContainer :
    226       matchPair
    227         (_ directory : sectionBytesOrErr sectionId directory bs afterContainer)
    228         container))
    229 
    230 readArboricxRequiredSections = (bs :
    231   bindResult (readArboricxContainer bs)
    232     (container afterContainer :
    233       matchPair
    234         (_ directory :
    235           bindResult (sectionBytesOrErr arboricxManifestSectionId directory bs afterContainer)
    236             (manifestBytes _ :
    237               bindResult (sectionBytesOrErr arboricxNodesSectionId directory bs afterContainer)
    238                 (nodesBytes _ :
    239                   ok (pair manifestBytes nodesBytes) afterContainer)))
    240         container))