James Eversole
31bf7094f4
We don't need SHA verification or Merkle dags in our transport bundle. Content stores can handle both bundle and term verification and hashing.
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)
|
|
(reserved1 afterReserved1 :
|
|
bindResult (readBytes 8 afterReserved1)
|
|
(offset afterOffset :
|
|
bindResult (readBytes 8 afterOffset)
|
|
(length afterLength :
|
|
bindResult (readBytes 4 afterLength)
|
|
(reserved2 afterReserved2 :
|
|
ok
|
|
(pair sectionId
|
|
(pair sectionVersion
|
|
(pair sectionFlags
|
|
(pair compression
|
|
(pair reserved1
|
|
(pair offset
|
|
(pair length reserved2)))))))
|
|
afterReserved2)))))))))
|
|
|
|
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)
|
|
|
|
sectionRecordReserved1 = (sectionRecord :
|
|
matchPair
|
|
(_ payload :
|
|
matchPair
|
|
(_ payload2 :
|
|
matchPair
|
|
(_ payload3 :
|
|
matchPair
|
|
(_ payload4 :
|
|
matchPair
|
|
(reserved1 _ : reserved1)
|
|
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)
|
|
|
|
sectionRecordReserved2 = (sectionRecord :
|
|
matchPair
|
|
(_ payload :
|
|
matchPair
|
|
(_ payload2 :
|
|
matchPair
|
|
(_ payload3 :
|
|
matchPair
|
|
(_ payload4 :
|
|
matchPair
|
|
(_ payload5 :
|
|
matchPair
|
|
(_ payload6 :
|
|
matchPair
|
|
(_ reserved2 : reserved2)
|
|
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))
|