433 lines
12 KiB
Plaintext
433 lines
12 KiB
Plaintext
!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))
|