First, the background noise:
module Goop.Theroy.BisectableHistory
import Data.Void
import Goop.Theroy.Types
%default total
The history is only for providing a locally bisectable ordering of items. The history does not so much care what the items are , only that they can be refereed to by their cryptographic digest.
public export
record Item (output : Type) (digest_value : output) where
constructor MkItem
{0 a : Type}
{auto impl : Digest output a}
0 item : a
{auto witness : digest_value = digest @{impl} item}
We shall say that if two item's hashes are equal, then they are equal. This will help with "reassociating" items read off of disk with their in-structure counter part.
This is nominally unsound, any collisions in the hash function will break the type system. However, if this implementation's choice of hash, blake3, has collisions found, we will already have bigger issues.
export
itemDigestEq : {d1, d2 : output} -> d1 = d2
-> (item1 : Item output d1) -> (item2 : Item output d2)
-> item1 = item2
itemDigestEq prf item1 item2 = believe_me $ the (1 = 1) Refl
A Set is an object that contains an arbitrarily ordered
collection of unique Item s. The order is important, in that
it is preserved, but is only meaningful in so much as allowing the
client to explicitly represent the actual order items happened
in.
namespace Set
public export
data Set : (output : Type) -> Type
public export
data NotInSet : (output : Type) -> {d : output}
-> (item : Item output d)
-> (set : Set output)
-> Type
export
contains : {auto cmp : (x, y : output) -> Dec (x = y) }
-> Set output -> output -> Bool
data Set : (output : Type) -> Type where
Nil : Set output
(::) : {digest_value : output} -> (x : Item output digest_value)
-> (xs : Set output) -> {auto 0 not_in_rest : NotInSet output x xs}
-> Set output
data NotInSet : (output : Type) -> {d : output}
-> (i : Item output d)
-> (s : Set output)
-> Type where
NotInEmpty : NotInSet output i []
NotHereOrThere : {digest_value : output} -> (x : Item output digest_value)
-> (xs : Set output)
-> {auto cmp : (x, y : output) -> Dec (x = y) }
-> So (Basics.not $ Set.contains xs digest_value)
-> NotInSet output x xs
contains {cmp} [] y = False
contains {cmp} ((::) {digest_value} _ xs) y =
case cmp digest_value y of
Yes _ => True
No _ => contains xs y
Two sets can be merged, appending the new unique elements from the lefthand side onto the start of the left hand side. Under this convention, the right hand side is newer
export
((x, y : output) -> Dec (x = y)) => Semigroup (Set output) where
(<+>) [] y = y
(<+>) ((::) {digest_value} x xs {not_in_rest}) y =
let rest = xs <+> y
in case decSo (not $ contains rest digest_value) of
Yes prf => x :: xs
No contra => rest
A Set can also be changed into a LazyList / iterator of digests
export
contents : Set output -> LazyList output
contents [] = []
contents ((::) {digest_value} x xs) =
digest_value :: contents xs
A Set can be referenced to by the merkle combination of its digests
namespace ErasedSet
public export
record ErasedSet output (merkle_value : output) where
constructor MkErasedSet
0 the_set : Set output
{0 t : Type}
0 digest_impl : Digest output t
witness : merkle_value = merkle @{digest_impl} (contents the_set)
The logic here is going to get a little bit tangled, so we'll need to forward declare most of our types.
A History is a local log of set applications, indexed by its merkle digest
public export
data History : (output : Type) -> (merkle_value : output) -> Type
A HistoryEntry is set application that can be included in a History, indexed by its merkle digest
public export
data HistoryEntry : (output : Type) -> (merkle_value : output) -> Type
Both HistoryEntry s and History s can be
reduced to a Set
export
historyContents : History output merkel_value -> Set output
export
historyEntryContents : HistoryEntry output merkel_value -> Set output
A HistoryEntry can either be the inclusion of a set, or
the inclusion of another history
data HistoryEntry : (output : Type) -> (merkle_value : output) -> Type where
IncludeSet : (merkle_value : output) -> {auto impl : Digest output output}
-> (s : Set output) -> {auto witness : merkel_value = merkle @{impl} (contents s)}
-> HistoryEntry output merkle_value
IncludeHistory : (merkle_value : output) -> (hs : History output merkle_value)
-> HistoryEntry output merkle_value
A History Entry can be reduced to a digest by extraction, and this correctly returns the value in the type signature
export
historyEntryMerkle : HistoryEntry output merkle_value -> output
historyEntryMerkle (IncludeSet merkle_value _) = merkle_value
historyEntryMerkle (IncludeHistory merkle_value _) = merkle_value
export
historyEntryMerkleCorrect : (hs : HistoryEntry o mv) -> mv = (historyEntryMerkle hs)
historyEntryMerkleCorrect (IncludeSet mv s) = Refl
historyEntryMerkleCorrect (IncludeHistory mv hs) = Refl
A History Entry is reduced to a Set by returning the corresponding set for the given kind of history entry
historyEntryContents (IncludeSet _ s) = s
historyEntryContents (IncludeHistory _ hs) = historyContents hs
A History can be reduced to it's digest
export
historyMerkle : History output merkle_value -> output
A History is an ordered collection of HistoryEntries, where the hash of each is the merkle combination of the hash of the head and hash of the tail
data History : (output : Type) -> (merkle_value : output) -> Type where
Nil : {auto impl : Digest output output} -> History output (merkle @{impl} [])
(::) : {auto impl : Digest output output}
-> {mv_x : output} -> (x : HistoryEntry output mv_x)
-> {mv_xs : output} -> (xs : History output mv_xs)
-> History output (merkle @{impl} [mv_x, mv_xs])
A History is reduced to it's digest by extraction, and this correctly returns the value in the type signature
historyMerkle (Nil {impl}) = merkle @{impl} []
historyMerkle ((::) {impl} {mv_x} x {mv_xs} xs) = merkle @{impl} [mv_x, mv_xs]
export
historyMerkleCorrect : (hs : History o mv) -> mv = historyMerkle hs
historyMerkleCorrect [] = Refl
historyMerkleCorrect (x :: xs) = Refl
A History's contents are produced by merging all the containing sets, preserving the releative order by keeping locally-newer entries on the rhs and locally-older ones on the lhs
historyContents [] = Nil
historyContents ((::) {impl} x xs) =
let rest = historyContents xs
head = historyEntryContents x
-- Need to have this to be able to find the semigroup instance
_ = outputDecEq @{impl}
in head <+> rest
We need to be able to describe a range of
HistoryEntry s.
For this we'll need a few things, first, a way to say that a given
digest is the reference for a HistoryEntry in a given
History
public export
data HistoryContains : (output : Type) -> (mv_he : output)
-> {mv_hs : output} -> History output mv_hs
-> Type where
ContainsHere : {auto impl : Digest output output}
-> {0 mv_he : output} -> (he : HistoryEntry output mv_he)
-> HistoryContains output mv_he (he :: hs)
ContainsThere : {auto impl : Digest output output}
-> {rest : HistoryContains output mv_he hs}
-> HistoryContains output mv_he (he :: hs)
The corresponding history entry can be extracted from this proof
export
entry : HistoryContains output mv_he hs -> HistoryEntry output mv_he
entry (ContainsHere he) = he
entry (ContainsThere {rest}) = entry rest
We will need to know that the empty history is uninhabited
export
Digest output output => Uninhabited (HistoryContains output mv_he []) where
uninhabited ( ContainsHere he) impossible
uninhabited ContainsThere impossible
We also need to be able to query this fact
export
decContains : (mv_he : output) -> (hs : History output mv_hs)
-> Dec (HistoryContains output mv_he hs)
decContains mv_he (Nil @{i}) = No (\x => absurd x)
decContains mv_he ((::) @{i} {mv_x} x xs) =
case outputDecEq @{i} mv_he mv_x of
Yes Refl => Yes $ ContainsHere x
No not_here =>
case decContains mv_he xs of
Yes rest => Yes $ ContainsThere {rest}
No not_there => No $ neitherHereNorThere not_here not_there
where
neitherHereNorThere : (mv_he = mv_x -> Void)
-> (HistoryContains output mv_he xs -> Void)
-> HistoryContains output mv_he (x :: xs)
-> Void
neitherHereNorThere f g x =
case x of
ContainsHere _ => f Refl
ContainsThere {rest} => g rest
We will rely upon a function to return the history at the point of occurance of the given hash
export
historyAt : (hs : History o mv_hs)
-> HistoryContains o mv_he hs
-> (mv : o \*\* History o mv)
historyAt [] x = absurd x
historyAt (x :: xs) y =
case y of
(ContainsHere x) => (_ \*\* (x :: xs) )
ContainsThere {rest} => historyAt xs rest
And another to produce the index of the occurance
export
index : {hs : History o mv_hs}
-> HistoryContains o mv_he hs
-> Nat
index (ContainsHere he) = 0
index (ContainsThere {rest}) = S (index rest)
We need a way to be able to say that a specific entry comes after another entry already included in the range
public export
data HistoryContainsAfter : (output : Type) -> (mv_start, mv_end : output)
-> {mv_hs : output} -> (hs : History output mv_hs)
-> (start : HistoryContains output mv_start hs)
-> Type where
AfterHere : {auto impl : Digest output output}
-> {mv_end : output}
-> (he_end : HistoryEntry output mv_end)
-> {auto start : HistoryContains output mv_start hs}
-> HistoryContainsAfter output mv_start mv_end (he_end :: hs)
(ContainsThere {rest = start} {he = he_end})
AfterThere : {auto impl : Digest output output}
-> {auto rest : HistoryContainsAfter output mv_start mv_end hs start}
-> HistoryContainsAfter output mv_start mv_end (h :: hs)
(ContainsThere {rest = start} {hs} {he = h})
We also need to be able to query this fact
export
decContainsAfter : (hs : History output mv_hs)
-> (start : HistoryContains output mv_start hs)
-> (mv_end : output)
-> Dec (HistoryContainsAfter output mv_start mv_end hs start)
decContainsAfter [] start mv_end = absurd start
decContainsAfter ((::) {impl} {mv_x} x xs) start mv_end =
case start of
ContainsHere x => No $ \oops =>
case oops of
AfterHere he_end impossible
AfterThere impossible
ContainsThere {rest} =>
case outputDecEq @{impl} mv_end mv_x of
Yes Refl => Yes $ AfterHere x
No not_here =>
case decContainsAfter xs rest mv_end of
Yes prf => Yes $ AfterThere {rest = prf}
No not_there => No $ \oops =>
case oops of
AfterHere x => not_here Refl
AfterThere {rest = rest'} => not_there rest'
And a convenience function to query for an entire range at once
export
decRange' : (mv_start, mv_end : output) -> (hs : History output mv_hs)
-> Dec (start : HistoryContains output mv_start hs \*\* HistoryContainsAfter output mv_start mv_end hs start)
decRange' mv_start mv_end hs =
case decContains mv_start hs of
Yes start =>
case decContainsAfter hs start mv_end of
Yes end => Yes (start \*\* end )
-- TODO: Figure out how to prove this? Probably need a smarter return data structure
No contra => No $ \(_ \*\* oops) => contra (believe_me oops)
No contra => No $ \ (oops \*\* _ ) => contra oops
We also need a way to find the state of a history history at the start and end of a range
export
start : {hs : History o mv_hs}
-> {st : HistoryContains o mv_s hs}
-> HistoryContainsAfter o mv_s mv_e hs st
-> (mv : o \*\* History o mv)
start x = historyAt hs st
export
end : {hs : History o mv_hs}
-> {0 st : HistoryContains o mv_s hs}
-> HistoryContainsAfter o mv_s mv_e hs st
-> (mv : o \*\* History o mv)
end {hs = []} x = absurdity st
end {hs = (x :: xs)} y =
case y of
(AfterHere x) => (_ \*\* x :: xs )
AfterThere {rest} => end {hs = xs} rest
And another to return the length of a range
export
length : {hs : History o mv_hs}
-> {st : HistoryContains o mv_s hs}
-> HistoryContainsAfter o mv_s mv_e hs st
-> Nat
length (AfterHere he_end) = 1 + index st
length (AfterThere {rest}) = length rest
We also want to be able to wrap this all up in a type to avoid type signature hell
public export
record HistoryRange output where
constructor MkRange
{rmv_hs, rmv_start, rmv_end : output}
range_hs : History output rmv_hs
range_start : HistoryContains output rmv_start range_hs
range_end : HistoryContainsAfter output rmv_start rmv_end range_hs range_start
export
maybeRange : {mv_hs : _} -> (mv_start, mv_end : output) -> (hs : History output mv_hs)
-> Maybe (HistoryRange output)
maybeRange mv_start mv_end hs =
case decRange' mv_start mv_end hs of
Yes (start \*\* end ) => Just $ MkRange hs start end
No _ => Nothing