0 | module Goop.Theroy.BisectableHistory

  2 | import Data.Nat

  3 | import Data.Nat.Views

  4 | import Data.Vect

  5 | import Data.Void

  7 | import Goop.Theroy.Types

  9 | %default total

 19 | namespace Item

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

 22 |   public export

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

 24 |     constructor MkItem

 25 |     {auto 0 impl : Digest output a}

 26 |     item : a

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

 33 | namespace Item

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

 40 |   export

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

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

 43 |     -> item1 = item2

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

 45 |   

 57 | namespace Set

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

 61 |   public export

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

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

 67 |   public export

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

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

 70 |     -> Type

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

 73 |   export

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

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

 81 | namespace Set

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

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

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

 85 |   --

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

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

 88 |     Nil : Set output 0 a

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

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

 91 |       -> Set output (S n) a

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

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

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

 96 |     -> Type where

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

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

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

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

101 |       -> NotInSet x xs

103 |   -- Simple tail recursive implementation of contains

104 |   contains {cmp} [] y = False

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

106 |     case cmp digest_value y of

107 |       Yes _ => True

108 |       No _ => contains xs y

114 | namespace SetMonoid

115 |   export infixr 7 ++

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

120 |   export

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

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

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

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

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

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

127 |         _ = outputDecEq @{impl}

128 |     in case choose $ contains rest digest_value of

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

130 |       Right _ =>

131 |         let _ = NotInHere x rest

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

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

136 |   public export

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

138 |     constructor MkAnySet

139 |     {inner_n : Nat}

140 |     inner : Set output inner_n a

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

143 |   export

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

145 |     x <+> y =

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

147 |       in MkAnySet res

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

150 |   export

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

152 |     neutral = MkAnySet Nil

158 | namespace Set

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

160 |   export

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

162 |   contents [] = []

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

164 |     digest_value :: contents xs

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

167 |   export

168 |   size : Set output n a -> Nat

169 |   size [] = 0

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

172 |   ||| The length is the type parameter

173 |   export

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

175 |   sizeCorrect [] = Refl

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

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

179 |   export

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

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

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

184 |   export

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

186 |     -> (merkleValue x = merkleValue y)

187 |     -> x = y

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

201 | namespace History

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

208 |   public export

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

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

212 |   export

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

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

216 |   export

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

219 | namespace Entry

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

225 |   public export

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

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

229 |   export

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

236 | namespace History

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

238 |   -- signature at the type level

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

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

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

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

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

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

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

247 |   contents [] = []

248 |   contents (x :: xs) =

249 |     set x :: contents xs

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

252 |   set hs =

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

255 |   ||| A History has its own merkleValue

256 |   public export

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

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

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

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

262 |   export

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

264 |   merkleValueCorrect [] = Refl

265 |   merkleValueCorrect (x :: xs) = Refl

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

268 |   export

269 |   merkleValueEq : mv1 = mv2

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

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

272 |     -> x = y

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

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

276 |   export

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

278 |   heads [] = []

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

285 | namespace Entry

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

287 |   -- with its merkle_value

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

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

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

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

292 |       -> Entry output merkle_value a

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

294 |       -> Entry output merkle_value a

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

297 |   -- history, as appropriate

298 |   set (IncludeSet x) = MkAnySet x

299 |   set (IncludeHistory hs) = set hs

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

302 |   export

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

304 |   digestValue (IncludeSet x) = digest_value

305 |   digestValue (IncludeHistory hs) = digest_value

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

308 |   export

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

310 |   digestValueCorrect (IncludeSet x) = Refl

311 |   digestValueCorrect (IncludeHistory hs) = Refl

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

314 |   export

315 |   digestValueEq : mv1 = mv2

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

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

318 |     -> x = y

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

325 | namespace Contains

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

331 |   public export

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

333 |     -> Type where

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

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

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

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

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

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

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

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

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

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

345 |   export

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

347 |     uninhabited (Here head tail) impossible

348 |     uninhabited (There head tail rest) impossible

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

351 |   export

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

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

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

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

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

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

358 |       No not_here =>

359 |         case decContains mv_target xs of

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

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

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

363 |             case oops of

364 |               (Here x xs) => not_here Refl

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

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

368 |   export

369 |   length : Contains mv_target n hs -> Nat

370 |   length (Here head tail) = 0

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

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

374 |   export

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

376 |   lengthCorrect (Here head tail) = Refl

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

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

381 |   export

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

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

384 |   seek [] c = absurd c

385 |   seek (x :: xs) c =

386 |     case c of

387 |       Here _ _ => x :: xs

388 |       There _ _ rest => seek xs rest

389 |   

390 |   ||| Return a new Contains proof pointing to the element _after_ the previous one

391 |   export

392 |   dropLast : (hs : History output mv_head m a) -> Contains mv_target (S n) hs

393 |     -> (new_target ** Contains new_target n hs)

394 |   dropLast [] x = absurd x

395 |   dropLast ((::) {i} x  xs) c = 

396 |     case c of 

397 |       There x xs rest => 

398 |         case rest of 

399 |           Here head tail => (_ ** Here {i} x xs)

400 |           There head tail y => 

401 |             let (new_target ** rest') = dropLast xs rest

402 |             in (new_target ** There {i} _ _ rest')

403 |   

404 |   ||| A Non-Empty History Contains its head

405 |   export

406 |   containsHead : (hs : History output mv_head (S m) a) -> Contains mv_head 0 hs

407 |   containsHead (x :: xs) = Here x xs

408 |   

409 |   ||| A History that contains something is Non-Empty

410 |   export

411 |   containsNonEmpty : (hs : History output mv_head m a) -> Contains mv_target m' hs -> IsSucc m

412 |   containsNonEmpty [] c = absurd c

413 |   containsNonEmpty (x :: xs) c = ItIsSucc

423 | namespace Range

424 |   ||| A Range is defined by the heads at it's start and end points, as well as the number of heads

429 |   public export

430 |   record Range (output : Type) (n : Nat) (a : Type) where

431 |     constructor MkRange

432 |     {m : Nat}

433 |     {mv_start, mv_end : output}

434 |     end : History output mv_end m a

435 |     contains_start : Contains mv_start n end

441 | namespace Range

442 |   ||| Try to extract a range defined by the given start and end points from a history

443 |   export

444 |   maybeRange : {n : _} -> (mv_start, mv_end : output) -> (hs : History output mv_head n a)

445 |     -> Maybe (n' : Nat ** Range output n' a)

446 |   maybeRange mv_start mv_end hs = 

447 |     -- Attempt to extract the end of the range

448 |     case decContains mv_end hs of 

449 |       Yes (n_end ** contains_end) => 

450 |         -- Rewind the history to the end of the range

451 |         let hs' = seek hs contains_end

452 |         -- Attempt to find the start of the range

453 |         in case decContains mv_start hs' of

454 |           Yes (n_start ** contains_start) => 

455 |             -- Glue the start and end together into a range

456 |             Just (_ ** MkRange hs' contains_start)

457 |           No _ => Nothing

458 |       No _ => Nothing

459 |   

460 |   ||| The History at the starting head can be extracted from a range

461 |   export

462 |   (.start) : (x : Range output n a) -> History output x.mv_start (x.m `minus` n) a

463 |   (.start) (MkRange end contains_start) = seek end contains_start

469 | namespace Range

470 |   ||| Reduce a range to just its last/end element

471 |   export

472 |   truncate : Range output n a -> Range output 0 a

473 |   truncate (MkRange {m} end contains_start) with (containsNonEmpty end contains_start)

474 |     truncate (MkRange {m = (S m')} end contains_start) | ItIsSucc = 

475 |       MkRange end (containsHead end)

476 |   

477 |   ||| Slide the last element off the end of a range, moving the start one step closer to the end,

479 |   export

480 |   dropLast : Range output (S n) a -> Range output n a

481 |   dropLast (MkRange end contains_start) = 

482 |     let (_ ** contains_start') = dropLast end contains_start

483 |     in MkRange end contains_start'

484 |   

485 |   ||| Slide the first element off the end of a range, moving the end one step closer to the start,

487 |   export

488 |   dropFirst : Range output (S n) a -> Range output n a

489 |   dropFirst (MkRange [] contains_start) = absurd contains_start

490 |   dropFirst (MkRange (x :: xs) contains_start) = 

491 |     case contains_start of

492 |       There x xs rest => MkRange xs rest

493 |   

494 |   ||| Take a specific number of elements from the head of a range, dropping older elements and

496 |   export

497 |   take : {m : _} -> (n : Nat) -> Range output (m + n) a -> Range output n a

498 |   take {m = 0} n x = x

499 |   take {m = (S k)} n x = 

500 |     let rest = dropLast x

501 |     in take n rest

502 |   

503 |   ||| Drop a specific number of elements from the head of a range, dropping newer elements, and

505 |   export

506 |   drop : (n : Nat) -> n `LTE` n' => Range output n' a -> Range output (n' `minus` n) a

507 |   drop 0 @{LTEZero} x = rewrite minusZeroRight n' in x

508 |   drop (S left) @{(LTESucc y)} x = 

509 |     let x' = dropFirst x

510 |     in drop left x'

511 |   

512 |   -- Bisecting a range in a total way is a little bit tricky, since we need special handling for the

513 |   -- cases with 0 or 1 intermediate elements. We'll handle that by providing multiple variants of

514 |   -- our bisection function, and then wrapping them up in a "blind" composite version that indicates

515 |   -- the case taken

516 |   

517 |   namespace BisectMulti

518 |     ||| Type describing the result of bisecting a range

519 |     public export

520 |     record BisectedRange (output : Type) (n : Nat) (a : Type) where

521 |       constructor MkBisectedRange

522 |       {x, y : Nat}

523 |       end_half : Range output x a

524 |       start_half : Range output y a

525 |       {auto witness : x + y = n}

527 |     ||| Bisect a range containing more than 1 intermediate element (ranges with only 1 intermediate

529 |     export

530 |     bisect : {n : Nat} -> n `GT` 1 => Range output n a -> BisectedRange output n a

531 |     bisect {n} x with (half n)

532 |       bisect {n = (S (k + k))} x | (HalfOdd k) = 

533 |         let end_half = take k {m = S k} x

534 |             start_half = drop k @{ltePlusPlus _} x

535 |         in rewrite plusSuccRightSucc k k in

536 |           MkBisectedRange {x = k} {y = (S k)} end_half $

537 |           rewrite sym $ minusPrf k in start_half

538 |       where

539 |         ltePlusPlus : (j : Nat) -> LTE j (S (plus j j))

540 |         ltePlusPlus 0 = LTEZero

541 |         ltePlusPlus (S j) = LTESucc $

542 |           lteSuccRight $ 

543 |           rewrite sym $ plusSuccRightSucc j j in

544 |           ltePlusPlus j

545 |         minusPrf : (j : Nat) -> minus (S (plus j j)) j = S j

546 |         minusPrf j = 

547 |           rewrite plusSuccRightSucc j j in

548 |           rewrite minusPlus j {n = (S j)} in

549 |           Refl

550 |       bisect {n = (k + k)} x | (HalfEven k) = 

551 |         let end_half = take k x

552 |             start_half = drop k @{ltePlusPlus _} x

553 |         in MkBisectedRange {x = k} {y = k} end_half $

554 |           rewrite sym $ minusPlus k {n = k} in start_half

555 |         where

556 |           ltePlusPlus : (j : Nat) -> LTE j (plus j j)

557 |           ltePlusPlus 0 = LTEZero

558 |           ltePlusPlus (S j) = LTESucc $

559 |             rewrite sym $ plusSuccRightSucc j j in 

560 |             lteSuccRight $ ltePlusPlus j

561 |   

562 |   namespace BisectSingle

563 |     ||| Split a range with one intermediate element into its final two ranges

564 |     export

565 |     bisect : Range output 1 a -> (Range output 0 a, Range output 0 a)

566 |     bisect x = (take {m = 1} 0 x, drop 1 x)

567 |   

568 |   ||| The possible results of attempting to bisect a range

569 |   public export

570 |   data BisectResult : (output : Type) -> (n : Nat) -> (a : Type) -> Type where

571 |     ||| Had enough intermediate elements to split in half

572 |     Multi : n `GT` 1 => BisectedRange output n a -> BisectResult output n a

573 |     ||| Had a single intermediate elements, split into its start and end heads exactly

574 |     Single : (x, y : Range output 0 a) -> BisectResult output 1 a

575 |     ||| Had no intermediate elements, returning verbatim

576 |     None : Range output 0 a -> BisectResult output 0 a

577 |    

578 |   ||| Attempt to bisect a range in a total manner 

579 |   bisect : {n : _} -> Range output n a -> BisectResult output n a

580 |   bisect {n = 0} x = None x

581 |   bisect {n = (S 0)} x = 

582 |     let (x, y) = BisectSingle.bisect x

583 |     in Single x y

584 |   bisect {n = (S (S k))} x = Multi $ BisectMulti.bisect x

586 |   

587 |