Arboricx bundle format 1.1
We don't need SHA verification or Merkle dags in our transport bundle. Content stores can handle both bundle and term verification and hashing.
This commit is contained in:
@@ -1,37 +1,21 @@
|
||||
!import "arboricx-common.tri" !Local
|
||||
|
||||
-- Indexed Arboricx node section reader.
|
||||
--
|
||||
-- Node records in the indexed format are just length-prefixed payloads:
|
||||
-- u32 payloadLength || payload
|
||||
-- A payload is one of:
|
||||
-- 0x00
|
||||
-- 0x01 || childIndex:u32be
|
||||
-- 0x02 || leftIndex:u32be || rightIndex:u32be
|
||||
-- Child indices must point strictly backward in the node array.
|
||||
|
||||
readNodeRecord = (bs :
|
||||
bindResult (readBytes 32 bs)
|
||||
(nodeHash afterNodeHash :
|
||||
bindResult (readBytes 4 afterNodeHash)
|
||||
(payloadLength afterPayloadLength :
|
||||
bindResult (readBytes (u32BEBytesToNat payloadLength) afterPayloadLength)
|
||||
(payload afterPayload :
|
||||
ok
|
||||
(pair nodeHash
|
||||
(pair payloadLength payload))
|
||||
afterPayload))))
|
||||
|
||||
nodeRecordHash = (nodeRecord :
|
||||
matchPair
|
||||
(nodeHash _ : nodeHash)
|
||||
nodeRecord)
|
||||
|
||||
nodeRecordPayloadLength = (nodeRecord :
|
||||
matchPair
|
||||
(_ payload :
|
||||
matchPair
|
||||
(payloadLength _ : payloadLength)
|
||||
payload)
|
||||
nodeRecord)
|
||||
|
||||
nodeRecordPayload = (nodeRecord :
|
||||
matchPair
|
||||
(_ payload :
|
||||
matchPair
|
||||
(_ nodePayload : nodePayload)
|
||||
payload)
|
||||
nodeRecord)
|
||||
bindResult (readBytes 4 bs)
|
||||
(payloadLength afterPayloadLength :
|
||||
bindResult (readBytes (u32BEBytesToNat payloadLength) afterPayloadLength)
|
||||
(payload afterPayload :
|
||||
ok payload afterPayload)))
|
||||
|
||||
nodePayloadKind = (nodePayload : bytesHead nodePayload)
|
||||
|
||||
@@ -42,17 +26,18 @@ nodePayloadHasTag? = (tag nodePayload :
|
||||
(_ _ : false)
|
||||
(nodePayloadKind nodePayload))
|
||||
|
||||
nodePayloadLeaf? = (nodePayload : bytesEq? [(0)] nodePayload)
|
||||
nodePayloadLeaf? = (nodePayload :
|
||||
bytesEq? [(0)] nodePayload)
|
||||
|
||||
nodePayloadStem? = (nodePayload :
|
||||
and?
|
||||
(nodePayloadHasTag? nodePayloadStemTag nodePayload)
|
||||
(equal? (bytesLength nodePayload) 33))
|
||||
(equal? (bytesLength nodePayload) 5))
|
||||
|
||||
nodePayloadFork? = (nodePayload :
|
||||
and?
|
||||
(nodePayloadHasTag? nodePayloadForkTag nodePayload)
|
||||
(equal? (bytesLength nodePayload) 65))
|
||||
(equal? (bytesLength nodePayload) 9))
|
||||
|
||||
nodePayloadValid? = (nodePayload :
|
||||
or?
|
||||
@@ -61,96 +46,87 @@ nodePayloadValid? = (nodePayload :
|
||||
(nodePayloadStem? nodePayload)
|
||||
(nodePayloadFork? nodePayload)))
|
||||
|
||||
nodePayloadStemChildHash = (nodePayload : bytesTake 32 (bytesDrop 1 nodePayload))
|
||||
nodePayloadForkLeftHash = (nodePayload : bytesTake 32 (bytesDrop 1 nodePayload))
|
||||
nodePayloadForkRightHash = (nodePayload : bytesTake 32 (bytesDrop 33 nodePayload))
|
||||
nodePayloadStemChildIndex = (nodePayload :
|
||||
u32BEBytesToNat (bytesTake 4 (bytesDrop 1 nodePayload)))
|
||||
|
||||
nodeRecordPayloadValid? = (nodeRecord : nodePayloadValid? (nodeRecordPayload nodeRecord))
|
||||
nodePayloadForkLeftIndex = (nodePayload :
|
||||
u32BEBytesToNat (bytesTake 4 (bytesDrop 1 nodePayload)))
|
||||
|
||||
nodePayloadForkRightIndex = (nodePayload :
|
||||
u32BEBytesToNat (bytesTake 4 (bytesDrop 5 nodePayload)))
|
||||
|
||||
nodeRecordsHaveInvalidPayload? = y (self nodeRecords :
|
||||
matchList
|
||||
false
|
||||
(nodeRecord rest :
|
||||
(nodePayload rest :
|
||||
or?
|
||||
(not? (nodeRecordPayloadValid? nodeRecord))
|
||||
(not? (nodePayloadValid? nodePayload))
|
||||
(self rest))
|
||||
nodeRecords)
|
||||
|
||||
nodeRecordsHaveHash? = y (self nodeRecords nodeHash :
|
||||
matchList
|
||||
false
|
||||
(nodeRecord rest :
|
||||
or?
|
||||
(bytesEq? nodeHash (nodeRecordHash nodeRecord))
|
||||
(self rest nodeHash))
|
||||
nodeRecords)
|
||||
nodePayloadChildIndices = (nodePayload :
|
||||
matchBool
|
||||
t
|
||||
(matchBool
|
||||
(pair (nodePayloadStemChildIndex nodePayload) t)
|
||||
(pair (nodePayloadForkLeftIndex nodePayload)
|
||||
(pair (nodePayloadForkRightIndex nodePayload) t))
|
||||
(nodePayloadStem? nodePayload))
|
||||
(nodePayloadLeaf? nodePayload))
|
||||
|
||||
nodeRecordsHaveDuplicateHashes? = y (self nodeRecords :
|
||||
matchList
|
||||
-- True iff index n names an element before limit in records.
|
||||
-- For topologically sorted indexed bundles, every child of record i must
|
||||
-- satisfy childIndex < i, so searching only the prefix [0, i) validates both
|
||||
-- bounds and acyclicity.
|
||||
nodeIndexInPrefix? = y (self n records i limit :
|
||||
matchBool
|
||||
false
|
||||
(nodeRecord rest :
|
||||
or?
|
||||
(nodeRecordsHaveHash? rest (nodeRecordHash nodeRecord))
|
||||
(self rest))
|
||||
nodeRecords)
|
||||
(matchList
|
||||
false
|
||||
(_ rest :
|
||||
matchBool
|
||||
true
|
||||
(self n rest (succ i) limit)
|
||||
(equal? i n))
|
||||
records)
|
||||
(equal? i limit))
|
||||
|
||||
lookupNodeRecord_ = y (self nodeRecords nodeHash :
|
||||
nodeChildIndicesInPrefix? = y (self childIndices records limit :
|
||||
matchList
|
||||
nothing
|
||||
(nodeRecord rest :
|
||||
true
|
||||
(childIndex rest :
|
||||
matchBool
|
||||
(just nodeRecord)
|
||||
(self rest nodeHash)
|
||||
(bytesEq? nodeHash (nodeRecordHash nodeRecord)))
|
||||
nodeRecords)
|
||||
(self rest records limit)
|
||||
false
|
||||
(nodeIndexInPrefix? childIndex records 0 limit))
|
||||
childIndices)
|
||||
|
||||
lookupNodeRecord = (nodeHash nodeRecords : lookupNodeRecord_ nodeRecords nodeHash)
|
||||
nodePayloadIndicesValid? = (nodePayload i records :
|
||||
nodeChildIndicesInPrefix?
|
||||
(nodePayloadChildIndices nodePayload)
|
||||
records
|
||||
i)
|
||||
|
||||
nodeRecordChildHashes = (nodeRecord :
|
||||
(nodePayload :
|
||||
matchBool
|
||||
t
|
||||
(matchBool
|
||||
(pair (nodePayloadStemChildHash nodePayload) t)
|
||||
(pair (nodePayloadForkLeftHash nodePayload)
|
||||
(pair (nodePayloadForkRightHash nodePayload) t))
|
||||
(nodePayloadStem? nodePayload))
|
||||
(nodePayloadLeaf? nodePayload))
|
||||
(nodeRecordPayload nodeRecord))
|
||||
|
||||
nodeHashPresent? = (nodeHash nodeRecords : nodeRecordsHaveHash? nodeRecords nodeHash)
|
||||
|
||||
nodeChildHashesPresent? = y (self childHashes nodeRecords :
|
||||
nodeRecordsValidIndicesFrom? = y (self allRecords remainingRecords i :
|
||||
matchList
|
||||
true
|
||||
(childHash rest :
|
||||
and?
|
||||
(nodeHashPresent? childHash nodeRecords)
|
||||
(self rest nodeRecords))
|
||||
childHashes)
|
||||
(nodePayload rest :
|
||||
matchBool
|
||||
(self allRecords rest (succ i))
|
||||
false
|
||||
(nodePayloadIndicesValid? nodePayload i allRecords))
|
||||
remainingRecords)
|
||||
|
||||
nodeRecordChildrenPresent? = (nodeRecord nodeRecords :
|
||||
nodeChildHashesPresent? (nodeRecordChildHashes nodeRecord) nodeRecords)
|
||||
|
||||
nodeRecordsClosed? = y (self nodeRecords allNodeRecords :
|
||||
matchList
|
||||
true
|
||||
(nodeRecord rest :
|
||||
and?
|
||||
(nodeRecordChildrenPresent? nodeRecord allNodeRecords)
|
||||
(self rest allNodeRecords))
|
||||
nodeRecords)
|
||||
nodeRecordsValidIndices? = (nodeRecords i :
|
||||
nodeRecordsValidIndicesFrom? nodeRecords nodeRecords i)
|
||||
|
||||
validateNodeRecords = (nodeRecords rest :
|
||||
matchBool
|
||||
(err errInvalidNodePayload rest)
|
||||
(matchBool
|
||||
(err errDuplicateNode rest)
|
||||
(matchBool
|
||||
(ok nodeRecords rest)
|
||||
(err errMissingNode rest)
|
||||
(nodeRecordsClosed? nodeRecords nodeRecords))
|
||||
(nodeRecordsHaveDuplicateHashes? nodeRecords))
|
||||
(ok nodeRecords rest)
|
||||
(err errMissingNode rest)
|
||||
(nodeRecordsValidIndices? nodeRecords 0))
|
||||
(nodeRecordsHaveInvalidPayload? nodeRecords))
|
||||
|
||||
readNodeRecords_ = y (self bs nodeCount i acc :
|
||||
@@ -161,7 +137,8 @@ readNodeRecords_ = y (self bs nodeCount i acc :
|
||||
self afterNodeRecord nodeCount (succ i) (pair nodeRecord acc)))
|
||||
(equal? i nodeCount))
|
||||
|
||||
readNodeRecords = (nodeCount bs : readNodeRecords_ bs nodeCount 0 t)
|
||||
readNodeRecords = (nodeCount bs :
|
||||
readNodeRecords_ bs nodeCount 0 t)
|
||||
|
||||
readNodesSection = (bs :
|
||||
bindResult (readBytes 8 bs)
|
||||
@@ -201,32 +178,31 @@ nodesSectionRecords = (nodesSection :
|
||||
(_ nodeRecords : nodeRecords)
|
||||
nodesSection)
|
||||
|
||||
nodeRecordToTreeWith = (self nodeRecords nodeRecord :
|
||||
nodePayloadToTreeWith = (self nodeRecords nodePayload :
|
||||
matchBool
|
||||
(ok t t)
|
||||
(matchBool
|
||||
(bindResult (self (nodePayloadStemChildIndex nodePayload) nodeRecords)
|
||||
(child _ : ok (t child) t))
|
||||
(bindResult (self (nodePayloadForkLeftIndex nodePayload) nodeRecords)
|
||||
(left _ :
|
||||
bindResult (self (nodePayloadForkRightIndex nodePayload) nodeRecords)
|
||||
(right _ : ok (pair left right) t)))
|
||||
(nodePayloadStem? nodePayload))
|
||||
(nodePayloadLeaf? nodePayload))
|
||||
|
||||
nodeIndexToTree = y (self nodeIndex nodeRecords :
|
||||
(nodePayload :
|
||||
matchBool
|
||||
(ok t t)
|
||||
(matchBool
|
||||
(bindResult (self (nodePayloadStemChildHash nodePayload) nodeRecords)
|
||||
(child _ : ok (t child) t))
|
||||
(bindResult (self (nodePayloadForkLeftHash nodePayload) nodeRecords)
|
||||
(left _ :
|
||||
bindResult (self (nodePayloadForkRightHash nodePayload) nodeRecords)
|
||||
(right _ : ok (pair left right) t)))
|
||||
(nodePayloadStem? nodePayload))
|
||||
(nodePayloadLeaf? nodePayload))
|
||||
(nodeRecordPayload nodeRecord))
|
||||
(nodePayloadToTreeWith self nodeRecords nodePayload)
|
||||
(err errMissingNode t)
|
||||
(not? (equal? nodePayload t)))
|
||||
(nth nodeIndex nodeRecords))
|
||||
|
||||
nodeHashToTree = y (self nodeHash nodeRecords :
|
||||
triage
|
||||
(err errMissingNode t)
|
||||
(nodeRecord : nodeRecordToTreeWith self nodeRecords nodeRecord)
|
||||
(_ _ : err errMissingNode t)
|
||||
(lookupNodeRecord nodeHash nodeRecords))
|
||||
|
||||
readArboricxTreeFromHash = (rootHash bs :
|
||||
readArboricxTreeFromIndex = (rootIndexBytes bs :
|
||||
bindResult (readArboricxNodesSection bs)
|
||||
(nodesSection afterContainer :
|
||||
bindResult (nodeHashToTree rootHash (nodesSectionRecords nodesSection))
|
||||
bindResult (nodeIndexToTree (u32BEBytesToNat rootIndexBytes) (nodesSectionRecords nodesSection))
|
||||
(tree _ : ok tree afterContainer)))
|
||||
|
||||
readArboricxExecutableFromHash = readArboricxTreeFromHash
|
||||
readArboricxExecutableFromIndex = readArboricxTreeFromIndex
|
||||
|
||||
Reference in New Issue
Block a user