Goop's Bisectable History

First, the background noise:

module  Goop.Theroy.BisectableHistory

import  Goop.Theroy.Types

%default  total

Defining What a History is

Items, the atomic elements of history

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.

Warning

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

Grouping items into Sets

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

((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 History Proper

The Type Sketch

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

public  export
data  History  :  (output  :  Type)  ->  Type

A HistoryEntry is set application that can be included in a History

public  export
data  HistoryEntry  :  (output  :  Type)  ->  Type

Both HistoryEntry s and History s can be reduced to a Set export
historyContents  :  History  output  ->  Set  output

export
historyEntryContents  :  HistoryEntry  output  ->  Set  output

Both HistoryEntry s and History s can be reduced to a list of digests of their components export
historyComponents  :  History  output  ->  LazyList  output

export
historyEntryComponents  :  HistoryEntry  output  ->  LazyList  output

Both HistoryEntry and History can be referenced by their digests namespace  HistoryRef
  public  export
  record  HistoryRef  output  (merkle_value  :  output)  where  
    constructor  MkHistoryRef
    0  the_history  :  History  output
    {0  t  :  Type}
    0  digest_impl  :  Digest  output  t
    witnesss  :  merkle_value  =  merkle  @{digest_impl}  (historyComponents  the_history)

namespace  HistoryEntryRef
  public  export
  record  HistoryEntryRef  output  (merkle_value  :  output)  where  
    constructor  MkHistoryEntryRef
    0  the_history_entry  :  HistoryEntry  output
    {0  t  :  Type}
    0  digest_impl  :  Digest  output  t
    witnesss  :  merkle_value  =  merkle  @{digest_impl}  (historyEntryComponents  the_history_entry)

The Implementations