trace.bend checks

raw source on the hub · import 0xd684886d10b431b9dce6c3b2d1ef1980/trace.bend as Trace

3 imports

import Base
import ./main.bend as V
import ./model.bend as M

Types

type Snapshot source · line 54 · raw

Data

Snapshot

@xs:List<&2, U32> -> @len:U32 -> @cap:U32 -> @max:U32 -> Snapshot

Definitions

def err source · line 5 · raw

@e:0xd684886d10b431b9dce6c3b2d1ef1980/main.Error -> 0xd684886d10b431b9dce6c3b2d1ef1980/model.Observation

def unit_result source · line 12 · raw

@r:Result<&1, &1, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Error, Unit> -> 0xd684886d10b431b9dce6c3b2d1ef1980/model.Observation

def value_result source · line 17 · raw

@r:Result<&1, &1, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Error, U32> -> 0xd684886d10b431b9dce6c3b2d1ef1980/model.Observation

def data_list source · line 22 · raw

@xs:List<&1, U32> -> List<&2, U32>

def list_result source · line 27 · raw

@r:Result<&1, &1, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Error, List<&1, U32>> -> 0xd684886d10b431b9dce6c3b2d1ef1980/model.Observation

def unit_pair source · line 32 · raw

@pair:Pair(0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec<U32>, Result<&1, &1, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Error, Unit>) -> Pair(0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec<U32>, 0xd684886d10b431b9dce6c3b2d1ef1980/model.Observation)

def value_pair source · line 36 · raw

@pair:Pair(0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec<U32>, Result<&1, &1, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Error, U32>) -> Pair(0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec<U32>, 0xd684886d10b431b9dce6c3b2d1ef1980/model.Observation)

def list_pair source · line 40 · raw

@pair:Pair(0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec<U32>, Result<&1, &1, 0xd684886d10b431b9dce6c3b2d1ef1980/main.Error, List<&1, U32>>) -> Pair(0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec<U32>, 0xd684886d10b431b9dce6c3b2d1ef1980/model.Observation)

def step source · line 44 · raw

@v:0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec<U32> -> @op:0xd684886d10b431b9dce6c3b2d1ef1980/model.Op -> Pair(0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec<U32>, 0xd684886d10b431b9dce6c3b2d1ef1980/model.Observation)

def snapshot_limit source · line 57 · raw

@xs:List<&2, U32> -> @n:U32 -> @c:U32 -> @pair:Pair(0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec<U32>, U32) -> Pair(0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec<U32>, Snapshot)

def snapshot_cap source · line 61 · raw

@xs:List<&2, U32> -> @n:U32 -> @pair:Pair(0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec<U32>, U32) -> Pair(0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec<U32>, Snapshot)

def snapshot_len source · line 65 · raw

@xs:List<&2, U32> -> @pair:Pair(0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec<U32>, U32) -> Pair(0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec<U32>, Snapshot)

def snapshot_list source · line 69 · raw

@pair:Pair(0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec<U32>, List<&1, U32>) -> Pair(0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec<U32>, Snapshot)

def snapshot source · line 73 · raw

@v:0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec<U32> -> Pair(0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec<U32>, Snapshot)

def state_eq source · line 76 · raw

@state:0xd684886d10b431b9dce6c3b2d1ef1980/model.State -> @snap:Snapshot -> Bool

def capacity_ok source · line 87 · raw

@old:U32 -> @+now:U32 -> @+need:U32 -> @grew:Bool -> Bool

Capacity is tested independently from the list oracle. Exact minimum power is characterized by need <= cap and, when cap grows, cap/2 < need.

def capacity_need source · line 94 · raw

@+old:U32 -> @+now:U32 -> @+need:U32 -> Bool

def capacity_op source · line 97 · raw

@+old:U32 -> @+now:U32 -> @n:U32 -> @op:0xd684886d10b431b9dce6c3b2d1ef1980/model.Op -> @observation:0xd684886d10b431b9dce6c3b2d1ef1980/model.Observation -> Bool

def compare_step source · line 109 · raw

@old:U32 -> @op:0xd684886d10b431b9dce6c3b2d1ef1980/model.Op -> @+actual:0xd684886d10b431b9dce6c3b2d1ef1980/model.Observation -> @expected:0xd684886d10b431b9dce6c3b2d1ef1980/model.Observation -> @+state:0xd684886d10b431b9dce6c3b2d1ef1980/model.State -> @pair:Pair(0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec<U32>, Snapshot) -> Pair(Pair(0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec<U32>, 0xd684886d10b431b9dce6c3b2d1ef1980/model.State), Bool)

def run_step source · line 116 · raw

@old:U32 -> @op:0xd684886d10b431b9dce6c3b2d1ef1980/model.Op -> @impl:Pair(0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec<U32>, 0xd684886d10b431b9dce6c3b2d1ef1980/model.Observation) -> @model:Pair(0xd684886d10b431b9dce6c3b2d1ef1980/model.State, 0xd684886d10b431b9dce6c3b2d1ef1980/model.Observation) -> Pair(Pair(0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec<U32>, 0xd684886d10b431b9dce6c3b2d1ef1980/model.State), Bool)

def from_snapshot source · line 122 · raw

@+op:0xd684886d10b431b9dce6c3b2d1ef1980/model.Op -> @state:0xd684886d10b431b9dce6c3b2d1ef1980/model.State -> @pair:Pair(0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec<U32>, Snapshot) -> Pair(Pair(0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec<U32>, 0xd684886d10b431b9dce6c3b2d1ef1980/model.State), Bool)

def run source · line 128 · raw

@ops:List<&2, 0xd684886d10b431b9dce6c3b2d1ef1980/model.Op> -> @state:Pair(Pair(0xd684886d10b431b9dce6c3b2d1ef1980/main.Vec<U32>, 0xd684886d10b431b9dce6c3b2d1ef1980/model.State), Bool) -> Bool

def trace source · line 137 · raw

@+limit:U32 -> @ops:List<&2, 0xd684886d10b431b9dce6c3b2d1ef1980/model.Op> -> Bool