def valid_of

bendtorch-core@0.1.0.0 · src/tensor/contracts/binary_build_proof.bend:77

import Base
import bendtorch-core@0.1.0.0/src/storage/api.bend as Api
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

77def valid_of(+n: Nat, +history: List<&2, Api.Effect>, +all: {written(n, history) == True{} : Bool}) -> Api.Valid(n, history):
78  match history:
79    case Nil{}:
80      Unit{}
81    case +effect <> +past:
82      match effect:
83        case Api.Wrote{+i, +w}:
84          (Arith.and_left(Nat.is_lt(U32.to_nat(i), n), written(n, past), all),
85            valid_of(n, past, Arith.and_right(Nat.is_lt(U32.to_nat(i), n), written(n, past), all)))
86        case Api.Kept{+i}:
87          valid_of(n, past, all)
88        case Api.Left{}:
89          valid_of(n, past, all)
90        case Api.Right{}:
91          valid_of(n, past, all)