0 | module Goop.Theroy.BisectableHistory

  2 | import Data.Vect

  3 | import Data.Void

  5 | import Goop.Theroy.Types

  7 | %default total

 17 | namespace Item

 18 |   ||| An item is any ol' object branded with its digest, bundled with a proof that the brand is the

 20 |   public export

 21 |   record Item (a : Type) (output : Type) (item_digest : output) where

 22 |     constructor MkItem

 23 |     {auto 0 impl : Digest output a}

 24 |     item : a

 25 |     {auto witness : item_digest = digest @{impl} item}

 31 | namespace Item

 32 |   ||| We shall assume that if `Item`'s digests are equal, then the values contained in the two items

 38 |   export

 39 |   digestEq : {d1, d2 : output} -> d1 = d2

 40 |     -> (item1 : Item a output d1) -> (item2 : Item a output d2)

 41 |     -> item1 = item2

 42 |   digestEq prf item1 item2 = believe_me $ the (1 = 1) Refl

 53 | namespace Set

 54 |   ||| A Set is an arbitrairly ordered collection of unique items, refered to by their digests

 57 |   public export

 58 |   data Set : (output : Type) -> (n : Nat) -> (a : Type) -> Type

 60 |   ||| An item is not in a set if it is not present in every slot in the set

 63 |   public export

 64 |   data NotInSet : (item : Item a output d)

 65 |     -> (set : Set output n a)

 66 |     -> Type

 68 |   ||| A Set contains an item if that item's digest is equal to any of the digest's in the set

 69 |   export

 70 |   contains : {auto cmp : (x, y : output) -> Dec (x = y)}

 71 |     -> Set output n a -> output -> Bool

 77 | namespace Set

 78 |   -- The `Set` itself is a list like structure, externally containing the digest the corresponds to

 79 |   -- each Item, and using a freshlist like approach where each head contains an erased witness that

 80 |   -- it's digest is not contained in the corresponding tail

 81 |   --

 82 |   -- By convention, going towards the tail (the end of the 'list') is going backwards in time

 83 |   data Set : (output : Type) -> (n : Nat) -> (a : Type) -> Type where

 84 |     Nil : Set output 0 a

 85 |     (::) : {digest_value : output} -> (x : Item a output digest_value)

 86 |       -> (xs : Set output n a) -> {auto 0 not_in_rest : NotInSet x xs}

 87 |       -> Set output (S n) a

 89 |   -- The NotInSet proof is a simple witness that calling `contains xs x` returned false

 90 |   data NotInSet : (item : Item a output d)

 91 |     -> (set : Set output n a)

 92 |     -> Type where

 93 |     NotInHere : {digest_value : output} -> (x : Item a output digest_value)

 94 |       -> (xs : Set output n a)

 95 |       -> {auto cmp : (x, y : output) -> Dec (x = y)}

 96 |       -> So (Basics.not $ Set.contains xs digest_value)

 97 |       -> NotInSet x xs

 99 |   -- Simple tail recursive implementation of contains

100 |   contains {cmp} [] y = False

101 |   contains {cmp} ((::) {digest_value} x xs) y =

102 |     case cmp digest_value y of

103 |       Yes _ => True

104 |       No _ => contains xs y

110 | namespace SetMonoid

111 |   export infixr 7 ++

112 |   ||| Concatenation over sets. This is nominally just set union, but preserves our conventional

116 |   export

117 |   (++) : Digest output a => {m, n : Nat}

118 |     -> (lhs : Set output n a) -> (rhs : Set output m a)

119 |     -> (n' : Nat ** Set output n' a)

120 |   (++) [] rhs = (_ ** rhs)

121 |   (++) @{impl} ((::) {digest_value} x xs) rhs =

122 |     let (n' ** rest) = xs ++ rhs

123 |         _ = outputDecEq @{impl}

124 |     in case choose $ contains rest digest_value of

125 |       Left _ => (n' ** rest)

126 |       Right _ =>

127 |         let _ = NotInHere x rest

128 |         in (_ ** x :: rest)

130 |   ||| For the monoid implementation to work, we need to be able to wrap a set up in a way that removes

132 |   public export

133 |   record AnySet (output : Type) (a : Type) where

134 |     constructor MkAnySet

135 |     {inner_n : Nat}

136 |     inner : Set output inner_n a

138 |   ||| The semigroup implementation is just (++) over AnySet

139 |   export

140 |   Digest output a => Semigroup (AnySet output a) where

141 |     x <+> y =

142 |       let (_ ** res) = x.inner ++ y.inner

143 |       in MkAnySet res

145 |   ||| The Neutral element for the AnySet monoid is the empty Set

146 |   export

147 |   Semigroup (AnySet output a) => Monoid (AnySet output a) where

148 |     neutral = MkAnySet Nil

154 | namespace Set

155 |   ||| A Set can be reduced to a LazyList of its digets

156 |   export

157 |   contents : Set output n a -> LazyList output

158 |   contents [] = []

159 |   contents ((::) {digest_value} x xs) =

160 |     digest_value :: contents xs

162 |   ||| A Set has a size, which is its number of elements

163 |   export

164 |   size : Set output n a -> Nat

165 |   size [] = 0

166 |   size (x :: xs) = S (size xs)

168 |   ||| The length is the type parameter

169 |   export

170 |   sizeCorrect : (xs : Set output n a) -> size xs = n

171 |   sizeCorrect [] = Refl

172 |   sizeCorrect (x :: xs) = rewrite sizeCorrect xs in Refl

174 |   ||| The merkle value of a given Set is the merkle combination of its contents

175 |   export

176 |   merkleValue : Digest output a => Set output n a -> output

177 |   merkleValue @{impl} x = merkle @{impl} (contents x)

179 |   ||| If two Sets' merkelValues are the same, they are assumed to be equal

180 |   export

181 |   merkleValueEq : Digest output a => (x, y : Set output n a)

182 |     -> (merkleValue x = merkleValue y)

183 |     -> x = y

184 |   merkleValueEq x y prf = believe_me $ the (1 = 1) Refl

195 | namespace History

196 |   ||| A History describes an ordered joining of sets, tagged by the merkle sum of its head and tail

202 |   public export

203 |   data History : (output : Type) -> (merkle_val : output) -> (n : Nat) -> (a : Type) -> Type

205 |   ||| A History can be reduced to a list of sets that it contains

206 |   export

207 |   contents : History output mv n a -> LazyList (AnySet output a)

209 |   ||| A History can be reduced to the fully applied set of changes it represents

210 |   export

211 |   set : Digest output a => History output mv n a -> AnySet output a

213 | namespace Entry

214 |   ||| Any entry in the history can either be the inclusion of a set, or the inclusion of a whole

219 |   public export

220 |   data Entry : (output : Type) -> (digest_value : output) -> (a : Type) -> Type

222 |   ||| A History Entry can be reduced to the set that it contains

223 |   export

224 |   set : Digest output a => Entry output dv a -> AnySet output a

230 | namespace History

231 |   -- The history is a basic, list-like collection that ensures the proper branding with the merkle

232 |   -- signature at the type level

233 |   data History : (output : Type) -> (merkle_val : output) -> (n : Nat) -> (a : Type) -> Type where

234 |     Nil : {auto i : Digest output a} -> History output (merkle @{i} []) 0 a

235 |     (::) : {auto i : Digest output a}

236 |       -> {digest_x : output} -> (x : Entry output digest_x a)

237 |       -> {merkle_xs : output} -> (xs : History output merkle_xs n a)

238 |       -> History output (merkle @{i} [digest_x, merkle_xs]) (S n) a

240 |   -- The contents are formed by a simple walking of the history

241 |   contents [] = []

242 |   contents (x :: xs) =

243 |     set x :: contents xs

245 |   -- The set is produced by folding the contents under AnySet's moniod definition

246 |   set hs =

247 |     foldr (<+>) neutral (contents hs)

249 |   ||| A History has its own merkleValue

250 |   public export

251 |   merkleValue : (hs : History output mv n a) -> output

252 |   merkleValue (Nil {i}) = merkle @{i} []

253 |   merkleValue ((::) {i} {digest_x} x {merkle_xs} xs) = merkle @{i} [digest_x, merkle_xs]

255 |   ||| That merkleValue is the same as the one in the type signature

256 |   export

257 |   merkleValueCorrect : (hs : History output mv n a) -> merkleValue hs = mv

258 |   merkleValueCorrect [] = Refl

259 |   merkleValueCorrect (x :: xs) = Refl

261 |   ||| Two histories are assumed to be equal if their merkle values are equal

262 |   export

263 |   merkleValueEq : mv1 = mv2

264 |     -> (x : History output mv1 n a)

265 |     -> (y : History output mv2 n a)

266 |     -> x = y

267 |   merkleValueEq prf x y = believe_me $ the (1 = 1) Refl

269 |   ||| A history can be turned into a list of the digests idenifying its heads

270 |   export

271 |   heads : (hs : History output mv n a) -> Vect n output

272 |   heads [] = []

273 |   heads orig@(x :: xs) = merkleValue orig :: heads xs

275 | namespace Entry

276 |   -- Wrap a set by provably pairing it up with its merkleValue, wrap a history by wrapping it up

277 |   -- with its merkle_value

278 |   data Entry : (output : Type) -> (digest_value : output) -> (a : Type) -> Type where

279 |     IncludeSet : {auto i : Digest output a}

280 |       -> {merkle_value : output} -> {n : Nat} -> (x : Set output n a)

281 |       -> {auto witness : merkle_value = merkleValue x}

282 |       -> Entry output merkle_value a

283 |     IncludeHistory : {merkle_value : _} -> {n : Nat} -> (hs : History output merkle_value n a)

284 |       -> Entry output merkle_value a

286 |   -- The set is formed by either returning the inner set, or the set corresponding to the included

287 |   -- history, as appropriate

288 |   set (IncludeSet x) = MkAnySet x

289 |   set (IncludeHistory hs) = set hs

291 |   ||| An Entry has its own digest value

292 |   export

293 |   digestValue : (e : Entry output digest_value a) -> output

294 |   digestValue (IncludeSet x) = digest_value

295 |   digestValue (IncludeHistory hs) = digest_value

297 |   ||| That digest value is the same as the one in the type signature

298 |   export

299 |   digestValueCorrect : (e : Entry output digest_value a) -> digestValue e = digest_value

300 |   digestValueCorrect (IncludeSet x) = Refl

301 |   digestValueCorrect (IncludeHistory hs) = Refl

303 |   ||| Two Entries are assumed to be equal if their digest values are equal

304 |   export

305 |   digestValueEq : mv1 = mv2

306 |     -> (x : Entry output mv1 a)

307 |     -> (y : Entry output mv2 a)

308 |     -> x = y

309 |   digestValueEq prf x y = believe_me $ the (1 = 1) Refl

315 | namespace Contains

316 |   ||| A proof that a given history contains a head with a given merkel value

321 |   public export

322 |   data Contains : (mv_target : output) -> (n : Nat) -> (hs : History output mv_head m a)

323 |     -> Type where

324 |     Here : {auto i : Digest output a}

325 |       -> (head : Entry output dv_head a)

326 |       -> (0 tail : History output mv_tail m a)

327 |       -> Contains (merkleValue (head :: tail)) 0 (head :: tail)

328 |     There : {auto i : Digest output a}

329 |       -> (0 head : Entry output dv_head a)

330 |       -> (0 tail : History output mv_tail m a)

331 |       -> (rest : Contains mv_target n tail)

332 |       -> Contains mv_target (S n) (head :: tail)

334 |   ||| An empty history can not possibly contain anything

335 |   export

336 |   Digest output a => Uninhabited (Contains mv_target n (the (History output _ _ a) [])) where

337 |     uninhabited (Here head tail) impossible

338 |     uninhabited (There head tail rest) impossible

340 |   ||| Decide if a history contains a given head or not

341 |   export

342 |   decContains : (mv_target : output) -> (hs : History output mv_head m a)

343 |     -> Dec (n : Nat ** Contains mv_target n hs)

344 |   decContains mv_target [] = No $ \(_ ** oops) => uninhabited oops

345 |   decContains mv_target ((::) @{i} x xs) =

346 |     case outputDecEq @{i} mv_target (merkleValue (x :: xs)) of

347 |       Yes prf => Yes (0 ** rewrite prf in Here x xs)

348 |       No not_here =>

349 |         case decContains mv_target xs of

350 |           Yes (n' ** rest) =>

351 |             Yes (S n' ** There x xs rest)

352 |           No not_there => No $ \(n' ** oops) =>

353 |             case oops of

354 |               (Here x xs) => not_here Refl

355 |               (There x xs rest) => not_there (_ ** rest)

357 |   ||| A Contains proof has a length, which is the number of elements before the target value

358 |   export

359 |   length : Contains mv_target n hs -> Nat

360 |   length (Here head tail) = 0

361 |   length (There head tail rest) = S (length rest)

363 |   ||| That length is the n index in the type signature

364 |   export

365 |   lengthCorrect : (c : Contains mv_target n hs) -> length c = n

366 |   lengthCorrect (Here head tail) = Refl

367 |   lengthCorrect (There head tail rest) = rewrite lengthCorrect rest in Refl

369 |   ||| A History and an inclusion proof can be combined to 'seek' the history to the point described

371 |   export

372 |   seek : (hs : History output mv_head m a) -> Contains mv_target n hs

373 |     -> History output mv_target (m `minus` n) a

374 |   seek [] c = absurd c

375 |   seek (x :: xs) c =

376 |     case c of

377 |       Here _ _ => x :: xs

378 |       There _ _ rest => seek xs rest