packed_array_proof.bend checks

raw source on the hub · import 0xda83506fb9f059ead7afcfa2f498df5f/packed_array_proof.bend as Packed_array_proof

1 import

import Base

Laws

law reify provedsource · line 14 · raw

@a:Array<U32> -> Sigma<&2, &1, Tree, t => {a == thaw(t) : Array<U32>}>

Consume any linear array once, retaining a proof of its exact representation.

law reify_node provedsource · line 18 · raw

@-l:Array<U32> -> @-r:Array<U32> -> @left:Sigma<&2, &1, Tree, t => {l == thaw(t) : Array<U32>}> -> @right:Sigma<&2, &1, Tree, t => {r == thaw(t) : Array<U32>}> -> Sigma<&2, &1, Tree, t => {ANode{l, r} == thaw(t) : Array<U32>}>

Types

type Tree source · line 4 · raw

Data

A duplicable proof-only description of an array. Never used by the hash.

Leaf
```
@value:U32 -> Tree
```
Node
```
@left:Tree -> @right:Tree -> Tree
```

Definitions

def thaw source · line 8 · raw

@t:Tree -> Array<U32>