lawful-arrays Releases (1): 0.1.0.0 0x13527df86b638e4649c15a58682c998e indexed https://jend.leeeet.dev/files.txt?path=lawful-arrays@0.1.0.0 Definitions (159, 1 to 100 shown): LAWS.new_full (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/LAWS.bend&name=new_full) law new_full: for -T: Data for d: Nat for v: T {D.full(T, Array.new(T, d, v), d) == True{} : Bool} LAWS.new_view (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/LAWS.bend&name=new_view) law new_view: for -T: Data for d: Nat for v: T {D.view(T, Array.new(T, d, v)) == List.replicate(T, Nat.pow(2n, d), v) : List<&2, T>} LAWS.view_length (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/LAWS.bend&name=view_length) law view_length: for -T: Data for a: Array for d: Nat for hf: {D.full(T, a, d) == True{} : Bool} {List.length(&2, T, D.view(T, a)) == Nat.pow(2n, d) : Nat} LAWS.size_count (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/LAWS.bend&name=size_count) # Array.size doubles 1 once per level of the left spine: for a perfect tree of # depth d below 32 that is the number of leaves, 2^d. law size_count: for -T: Data for a: Array for d: Nat for hf: {D.full(T, a, d) == True{} : Bool} for hd: {Nat.is_lt(d, 32n) == True{} : Bool} {U32.to_nat(Pair.snd(Array, U32, Array.size(T, a))) == Nat.pow(2n, d) : Nat} LAWS.size_kept (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/LAWS.bend&name=size_kept) law size_kept: for -T: Data for a: Array {Pair.fst(Array, U32, Array.size(T, a)) == a : Array} LAWS.get_view (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/LAWS.bend&name=get_view) # Array.get reads leaf i (modulo the size). law get_view: for -T: Data for a: Array for d: Nat for i: U32 for hf: {D.full(T, a, d) == True{} : Bool} for hd: {Nat.is_lt(d, 32n) == True{} : Bool} {Some{Pair.snd(Array, T, Array.get(T, a, i))} == List.get(&2, T, D.view(T, a), D.slot(i, d)) : Maybe<&2, T>} LAWS.get_kept (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/LAWS.bend&name=get_kept) # Array.get hands back the same array. law get_kept: for -T: Data for a: Array for i: U32 {Pair.fst(Array, T, Array.get(T, a, i)) == a : Array} LAWS.set_view (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/LAWS.bend&name=set_view) # Array.set replaces leaf i (modulo the size) and nothing else. law set_view: for -T: Data for a: Array for d: Nat for i: U32 for v: T for hf: {D.full(T, a, d) == True{} : Bool} for hd: {Nat.is_lt(d, 32n) == True{} : Bool} {D.view(T, Array.set(T, a, i, v)) == List.set(&2, T, D.view(T, a), D.slot(i, d), v) : List<&2, T>} LAWS.set_full (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/LAWS.bend&name=set_full) law set_full: for -T: Data for a: Array for d: Nat for i: U32 for v: T for hf: {D.full(T, a, d) == True{} : Bool} {D.full(T, Array.set(T, a, i, v), d) == True{} : Bool} LAWS.get_set_same (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/LAWS.bend&name=get_set_same) # Reading what was just written gives it back. # (This holds for every tree: set and get take the same path.) law get_set_same: for -T: Data for a: Array for i: U32 for v: T {Pair.snd(Array, T, Array.get(T, Array.set(T, a, i, v), i)) == v : T} LAWS.get_set_other (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/LAWS.bend&name=get_set_other) # Writing leaf i does not change leaf j (j a different leaf modulo the size). law get_set_other: for -T: Data for a: Array for d: Nat for i: U32 for j: U32 for v: T for hf: {D.full(T, a, d) == True{} : Bool} for hd: {Nat.is_lt(d, 32n) == True{} : Bool} for hij: {Nat.is_eq(D.slot(i, d), D.slot(j, d)) == False{} : Bool} {Pair.snd(Array, T, Array.get(T, Array.set(T, a, i, v), j)) == Pair.snd(Array, T, Array.get(T, a, j)) : T} LAWS.swap_view (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/LAWS.bend&name=swap_view) law swap_view: for -T: Data for a: Array for d: Nat for i: U32 for v: T for hf: {D.full(T, a, d) == True{} : Bool} for hd: {Nat.is_lt(d, 32n) == True{} : Bool} {D.view(T, Pair.fst(Array, T, Array.swap(T, a, i, v))) == List.set(&2, T, D.view(T, a), D.slot(i, d), v) : List<&2, T>} LAWS.swap_old (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/LAWS.bend&name=swap_old) law swap_old: for -T: Data for a: Array for d: Nat for i: U32 for v: T for hf: {D.full(T, a, d) == True{} : Bool} for hd: {Nat.is_lt(d, 32n) == True{} : Bool} {Some{Pair.snd(Array, T, Array.swap(T, a, i, v))} == List.get(&2, T, D.view(T, a), D.slot(i, d)) : Maybe<&2, T>} LAWS.swap_full (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/LAWS.bend&name=swap_full) law swap_full: for -T: Type for a: Array for d: Nat for i: U32 for v: T for hf: {D.full(T, a, d) == True{} : Bool} {D.full(T, Pair.fst(Array, T, Array.swap(T, a, i, v)), d) == True{} : Bool} LAWS.view_inj (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/LAWS.bend&name=view_inj) # Two perfect trees of the same depth with the same leaves are the same array. law view_inj: for -T: Data for a: Array for b: Array for d: Nat for ha: {D.full(T, a, d) == True{} : Bool} for hb: {D.full(T, b, d) == True{} : Bool} for h: {D.view(T, a) == D.view(T, b) : List<&2, T>} {a == b : Array} LAWS.get_pair (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/LAWS.bend&name=get_pair) # Array.get as a literal pair (so code that destructures it can be rewritten). law get_pair: for -T: Data for a: Array for i: U32 {Array.get(T, a, i) == (a, Pair.snd(Array, T, Array.get(T, a, i))) : Array & T} LAWS.size_pair (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/LAWS.bend&name=size_pair) law size_pair: for -T: Data for a: Array for d: Nat for hf: {D.full(T, a, d) == True{} : Bool} {Array.size(T, a) == (a, U32.shln(1, d)) : Array & U32} LAWS.get_new (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/LAWS.bend&name=get_new) # A new array reads as its initial value everywhere (every depth, every index). law get_new: for -T: Data for d: Nat for v: T for i: U32 {Pair.snd(Array, T, Array.get(T, Array.new(T, d, v), i)) == v : T} LAWS.slot_lt (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/LAWS.bend&name=slot_lt) law slot_lt: for i: U32 for d: Nat {Nat.is_lt(D.slot(i, d), Nat.pow(2n, d)) == True{} : Bool} LAWS.slot_small (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/LAWS.bend&name=slot_small) law slot_small: for i: U32 for d: Nat for h: {Nat.is_lt(U32.to_nat(i), Nat.pow(2n, d)) == True{} : Bool} {D.slot(i, d) == U32.to_nat(i) : Nat} LAWS.clone_pair (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/LAWS.bend&name=clone_pair) # Array.clone gives two arrays equal to the original. law clone_pair: for -T: Data for a: Array {Array.clone(T, a) == (a, a) : Array & Array} PROOF.full_t (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/PROOF.bend&name=full_t) # Rewrites a fact about a into the same fact about the mirror. def full_t(-T: Data, -a: Array, -t: P.Tree, +d: Nat, e: {P.fromT(T, t) == a : Array}, hf: {D.full(T, a, d) == True{} : Bool}) -> {D.full(T, P.fromT(T, t), d) == True{} : Bool}: PROOF.view_length.go (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/PROOF.bend&name=view_length.go) def view_length.go(-T: Data, -a: Array, +d: Nat, hf: {D.full(T, a, d) == True{} : Bool}, m: P.Mirror(T, a)) -> {List.length(&2, T, D.view(T, a)) == Nat.pow(2n, d) : Nat}: PROOF.size_count.go (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/PROOF.bend&name=size_count.go) def size_count.go(-T: Data, -a: Array, +d: Nat, hf: {D.full(T, a, d) == True{} : Bool}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, m: P.Mirror(T, a)) -> {U32.to_nat(Pair.snd(Array, U32, Array.size(T, a))) == Nat.pow(2n, d) : Nat}: PROOF.size_pair.go (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/PROOF.bend&name=size_pair.go) def size_pair.go(-T: Data, -a: Array, +d: Nat, hf: {D.full(T, a, d) == True{} : Bool}, m: P.Mirror(T, a)) -> {Array.size(T, a) == (a, U32.shln(1, d)) : Array & U32}: PROOF.get_view.go (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/PROOF.bend&name=get_view.go) def get_view.go(-T: Data, -a: Array, +d: Nat, +i: U32, hf: {D.full(T, a, d) == True{} : Bool}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, m: P.Mirror(T, a)) -> {Some{Pair.snd(Array, T, Array.get(T, a, i))} == List.get(&2, T, D.view(T, a), D.slot(i, d)) : Maybe<&2, T>}: PROOF.get_pair.go (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/PROOF.bend&name=get_pair.go) def get_pair.go(-T: Data, -a: Array, +i: U32, m: P.Mirror(T, a)) -> {Array.get(T, a, i) == (a, Pair.snd(Array, T, Array.get(T, a, i))) : Array & T}: PROOF.get_kept.go (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/PROOF.bend&name=get_kept.go) def get_kept.go(-T: Data, -a: Array, +i: U32, m: P.Mirror(T, a)) -> {Pair.fst(Array, T, Array.get(T, a, i)) == a : Array}: PROOF.set_view.go (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/PROOF.bend&name=set_view.go) def set_view.go(-T: Data, -a: Array, +d: Nat, +i: U32, +v: T, hf: {D.full(T, a, d) == True{} : Bool}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, m: P.Mirror(T, a)) -> {D.view(T, Array.set(T, a, i, v)) == List.set(&2, T, D.view(T, a), D.slot(i, d), v) : List<&2, T>}: PROOF.get_set_same.go (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/PROOF.bend&name=get_set_same.go) def get_set_same.go(-T: Data, -a: Array, +i: U32, +v: T, m: P.Mirror(T, a)) -> {Pair.snd(Array, T, Array.get(T, Array.set(T, a, i, v), i)) == v : T}: PROOF.get_set_other.go (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/PROOF.bend&name=get_set_other.go) def get_set_other.go(-T: Data, -a: Array, +d: Nat, +i: U32, +j: U32, +v: T, hf: {D.full(T, a, d) == True{} : Bool}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hij: {Nat.is_eq(D.slot(i, d), D.slot(j, d)) == False{} : Bool}, m: P.Mirror(T, a)) -> {Pair.snd(Array, T, Array.get(T, Array.set(T, a, i, v), j)) == Pair.snd(Array, T, Array.get(T, a, j)) : T}: PROOF.swap_view.go (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/PROOF.bend&name=swap_view.go) def swap_view.go(-T: Data, -a: Array, +d: Nat, +i: U32, +v: T, hf: {D.full(T, a, d) == True{} : Bool}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, m: P.Mirror(T, a)) -> {D.view(T, Pair.fst(Array, T, Array.swap(T, a, i, v))) == List.set(&2, T, D.view(T, a), D.slot(i, d), v) : List<&2, T>}: PROOF.swap_old.go (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/PROOF.bend&name=swap_old.go) def swap_old.go(-T: Data, -a: Array, +d: Nat, +i: U32, +v: T, hf: {D.full(T, a, d) == True{} : Bool}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, m: P.Mirror(T, a)) -> {Some{Pair.snd(Array, T, Array.swap(T, a, i, v))} == List.get(&2, T, D.view(T, a), D.slot(i, d)) : Maybe<&2, T>}: PROOF.view_inj.go (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/PROOF.bend&name=view_inj.go) def view_inj.go(-T: Data, -a: Array, -b: Array, +d: Nat, ha: {D.full(T, a, d) == True{} : Bool}, hb: {D.full(T, b, d) == True{} : Bool}, h: {D.view(T, a) == D.view(T, b) : List<&2, T>}, ma: P.Mirror(T, a), mb: P.Mirror(T, b)) -> {a == b : Array}: Defs.full (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/defs.bend&name=full) # a is a perfect tree of depth d: 2^d leaves, every one at depth d. Arrays # made by Array.new are; Array.set and Array.get keep it so. def full(-T: Type, a: Array, +d: Nat) -> Bool: Defs.view (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/defs.bend&name=view) # The leaves of a, left to right (the same list as Base's Array.to_list, which # is a template and cannot appear in a law). Elements must be Data. def view(-T: Data, a: Array) -> List<&2, T>: Defs.slot (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/defs.bend&name=slot) # The leaf an access at index i reaches in a perfect tree of depth d < 32: # i modulo 2^d. (From depth 32 up, Base's Array.size wraps to 0 and every # access reaches the last leaf; the laws exclude that.) def slot(i: U32, d: Nat) -> Nat: ProofBase.subst (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=subst) # Transport along an equation. def subst(-A: Type, -P: A -> Type, -x: A, -y: A, e: {x == y : A}, p: P(x)) -> P(y): ProofBase.Bool.disc_ft (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=Bool.disc_ft) def Bool.disc_ft(b: Bool) -> Type: ProofBase.false_ne_true (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=false_ne_true) law false_ne_true: for e: {False{} == True{} : Bool} Empty ProofBase.true_ne_false (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=true_ne_false) law true_ne_false: for e: {True{} == False{} : Bool} Empty ProofBase.and_true_l (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=and_true_l) law and_true_l: for +a: Bool for +b: Bool for e: {Bool.and(a, b) == True{} : Bool} {a == True{} : Bool} ProofBase.and_true_r (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=and_true_r) law and_true_r: for +a: Bool for +b: Bool for e: {Bool.and(a, b) == True{} : Bool} {b == True{} : Bool} ProofBase.Nat.disc_z (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=Nat.disc_z) def Nat.disc_z(n: Nat) -> Type: ProofBase.succ_ne_zero (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=succ_ne_zero) law succ_ne_zero: for -n: Nat for e: {1n+n == 0n : Nat} Empty ProofBase.pred (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=pred) def pred(n: Nat) -> Nat: ProofBase.succ_inj (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=succ_inj) law succ_inj: for -a: Nat for -b: Nat for e: {1n+a == 1n+b : Nat} {a == b : Nat} ProofBase.add_zero (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=add_zero) law add_zero: for +n: Nat {Nat.add(n, 0n) == n : Nat} ProofBase.add_succ (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=add_succ) law add_succ: for +a: Nat for +b: Nat {Nat.add(a, 1n+b) == 1n+Nat.add(a, b) : Nat} ProofBase.sub_zero (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=sub_zero) law sub_zero: for +i: Nat {Nat.sub(i, 0n) == i : Nat} ProofBase.lt_zero (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=lt_zero) law lt_zero: for +i: Nat {Nat.is_lt(i, 0n) == False{} : Bool} ProofBase.lt_zero_absurd (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=lt_zero_absurd) law lt_zero_absurd: for +i: Nat for e: {Nat.is_lt(i, 0n) == True{} : Bool} Empty ProofBase.lt_one (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=lt_one) # Below 1 is 0. law lt_one: for +k: Nat for e: {Nat.is_lt(k, 1n) == True{} : Bool} {k == 0n : Nat} ProofBase.not_lt_le (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=not_lt_le) law not_lt_le: for +a: Nat for +b: Nat for e: {Nat.is_lt(a, b) == False{} : Bool} {Nat.is_le(b, a) == True{} : Bool} ProofBase.lt_sub (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=lt_sub) # k is at least m and below m + m2, so k - m is below m2. law lt_sub: for +m: Nat for +k: Nat for +m2: Nat for h1: {Nat.is_lt(k, m) == False{} : Bool} for h2: {Nat.is_lt(k, Nat.add(m, m2)) == True{} : Bool} {Nat.is_lt(Nat.sub(k, m), m2) == True{} : Bool} ProofBase.lt0_add (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=lt0_add) law lt0_add: for +a: Nat for +b: Nat for e: {Nat.is_lt(0n, a) == True{} : Bool} {Nat.is_lt(0n, Nat.add(a, b)) == True{} : Bool} ProofBase.pow_pos (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=pow_pos) law pow_pos: for +d: Nat {Nat.is_lt(0n, Nat.pow(2n, d)) == True{} : Bool} ProofBase.pow_succ (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=pow_succ) # 2^(1+p) unfolds to p' + (p' + 0); this is p' + p'. law pow_succ: for +p: Nat {Nat.pow(2n, 1n+p) == Nat.add(Nat.pow(2n, p), Nat.pow(2n, p)) : Nat} ProofBase.lt_dbl (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=lt_dbl) law lt_dbl: for +a: Nat for +b: Nat for e: {Nat.is_lt(a, b) == True{} : Bool} {Nat.is_lt(Nat.add(a, a), Nat.add(b, b)) == True{} : Bool} ProofBase.lt_one_dbl (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=lt_one_dbl) law lt_one_dbl: for +b: Nat for e: {Nat.is_lt(0n, b) == True{} : Bool} {Nat.is_lt(1n, Nat.add(b, b)) == True{} : Bool} ProofBase.pow_lt (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=pow_lt) law pow_lt: for +d: Nat for +e: Nat for h: {Nat.is_lt(d, e) == True{} : Bool} {Nat.is_lt(Nat.pow(2n, d), Nat.pow(2n, e)) == True{} : Bool} ProofBase.length_append (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=length_append) law length_append: for -A: Data for +xs: List<&2, A> for +ys: List<&2, A> {List.length(&2, A, List.append(&2, A, xs, ys)) == Nat.add(List.length(&2, A, xs), List.length(&2, A, ys)) : Nat} ProofBase.get_append_l (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=get_append_l) # Before index length(xs), xs ++ ys reads like xs. law get_append_l: for -A: Data for +xs: List<&2, A> for +ys: List<&2, A> for +i: Nat for e: {Nat.is_lt(i, List.length(&2, A, xs)) == True{} : Bool} {List.get(&2, A, List.append(&2, A, xs, ys), i) == List.get(&2, A, xs, i) : Maybe<&2, A>} ProofBase.get_append_r (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=get_append_r) # From index length(xs) on, xs ++ ys reads like ys. law get_append_r: for -A: Data for +xs: List<&2, A> for +ys: List<&2, A> for +i: Nat for e: {Nat.is_lt(i, List.length(&2, A, xs)) == False{} : Bool} {List.get(&2, A, List.append(&2, A, xs, ys), i) == List.get(&2, A, ys, Nat.sub(i, List.length(&2, A, xs))) : Maybe<&2, A>} ProofBase.set_append_l (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=set_append_l) law set_append_l: for -A: Data for +xs: List<&2, A> for +ys: List<&2, A> for +i: Nat for +v: A for e: {Nat.is_lt(i, List.length(&2, A, xs)) == True{} : Bool} {List.set(&2, A, List.append(&2, A, xs, ys), i, v) == List.append(&2, A, List.set(&2, A, xs, i, v), ys) : List<&2, A>} ProofBase.set_append_r (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=set_append_r) law set_append_r: for -A: Data for +xs: List<&2, A> for +ys: List<&2, A> for +i: Nat for +v: A for e: {Nat.is_lt(i, List.length(&2, A, xs)) == False{} : Bool} {List.set(&2, A, List.append(&2, A, xs, ys), i, v) == List.append(&2, A, xs, List.set(&2, A, ys, Nat.sub(i, List.length(&2, A, xs)), v)) : List<&2, A>} ProofBase.replicate_add (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=replicate_add) law replicate_add: for -A: Data for +m: Nat for +n: Nat for +v: A {List.replicate(A, Nat.add(m, n), v) == List.append(&2, A, List.replicate(A, m, v), List.replicate(A, n, v)) : List<&2, A>} ProofBase.get_set_ne (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=get_set_ne) # Writing index i does not change index j != i. law get_set_ne: for -A: Data for +xs: List<&2, A> for +i: Nat for +j: Nat for +v: A for e: {Nat.is_eq(i, j) == False{} : Bool} {List.get(&2, A, List.set(&2, A, xs, i, v), j) == List.get(&2, A, xs, j) : Maybe<&2, A>} ProofBase.head_or (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=head_or) def head_or(-A: Data, +d: A, xs: List<&2, A>) -> A: ProofBase.tail (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=tail) def tail(-A: Data, xs: List<&2, A>) -> List<&2, A>: ProofBase.cons_inj_h (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=cons_inj_h) law cons_inj_h: for -A: Data for -x: A for -y: A for -xs: List<&2, A> for -ys: List<&2, A> for e: {x <> xs == y <> ys : List<&2, A>} {x == y : A} ProofBase.cons_inj_t (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=cons_inj_t) law cons_inj_t: for -A: Data for -x: A for -y: A for -xs: List<&2, A> for -ys: List<&2, A> for e: {x <> xs == y <> ys : List<&2, A>} {xs == ys : List<&2, A>} ProofBase.append_inj_l (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=append_inj_l) # Two appends with equally long first parts: the first parts are equal... law append_inj_l: for -A: Data for +x1: List<&2, A> for +x2: List<&2, A> for -y1: List<&2, A> for -y2: List<&2, A> for hl: {List.length(&2, A, x1) == List.length(&2, A, x2) : Nat} for +e: {List.append(&2, A, x1, y1) == List.append(&2, A, x2, y2) : List<&2, A>} {x1 == x2 : List<&2, A>} ProofBase.append_cancel_l (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=append_cancel_l) # ...and so are the second parts. law append_cancel_l: for -A: Data for +xs: List<&2, A> for -y1: List<&2, A> for -y2: List<&2, A> for e: {List.append(&2, A, xs, y1) == List.append(&2, A, xs, y2) : List<&2, A>} {y1 == y2 : List<&2, A>} ProofIndex.n_half (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_index.bend&name=n_half) law n_half: for +p: Nat {Nat.div(Nat.pow(2n, 1n+p), 2n) == Nat.pow(2n, p) : Nat} ProofIndex.half (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_index.bend&name=half) law half: for +n: U32 for +p: Nat for +hn: {U32.to_nat(n) == Nat.pow(2n, 1n+p) : Nat} {U32.to_nat(U32.shr(n)) == Nat.pow(2n, p) : Nat} ProofIndex.lo_idx (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_index.bend&name=lo_idx) law lo_idx: for +n: U32 for +i: U32 for +p: Nat for +hn: {U32.to_nat(n) == Nat.pow(2n, 1n+p) : Nat} for +hz: {U32.is_lt(i, U32.shr(n)) == True{} : Bool} {Nat.is_lt(U32.to_nat(i), Nat.pow(2n, p)) == True{} : Bool} ProofIndex.hi_nlt (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_index.bend&name=hi_nlt) law hi_nlt: for +n: U32 for +i: U32 for +p: Nat for +hn: {U32.to_nat(n) == Nat.pow(2n, 1n+p) : Nat} for +hz: {U32.is_lt(i, U32.shr(n)) == False{} : Bool} {Nat.is_lt(U32.to_nat(i), Nat.pow(2n, p)) == False{} : Bool} ProofIndex.le_shr (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_index.bend&name=le_shr) law le_shr: for +n: U32 for +i: U32 for +p: Nat for +hn: {U32.to_nat(n) == Nat.pow(2n, 1n+p) : Nat} for +hz: {U32.is_lt(i, U32.shr(n)) == False{} : Bool} {U32.is_le(U32.shr(n), i) == True{} : Bool} ProofIndex.hi_sub (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_index.bend&name=hi_sub) law hi_sub: for +n: U32 for +i: U32 for +p: Nat for +hn: {U32.to_nat(n) == Nat.pow(2n, 1n+p) : Nat} for +hz: {U32.is_lt(i, U32.shr(n)) == False{} : Bool} {U32.to_nat(U32.sub(i, U32.shr(n))) == Nat.sub(U32.to_nat(i), Nat.pow(2n, p)) : Nat} ProofIndex.hi_idx (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_index.bend&name=hi_idx) law hi_idx: for +n: U32 for +i: U32 for +p: Nat for +hn: {U32.to_nat(n) == Nat.pow(2n, 1n+p) : Nat} for +hi: {Nat.is_lt(U32.to_nat(i), Nat.pow(2n, 1n+p)) == True{} : Bool} for +hz: {U32.is_lt(i, U32.shr(n)) == False{} : Bool} {Nat.is_lt(U32.to_nat(U32.sub(i, U32.shr(n))), Nat.pow(2n, p)) == True{} : Bool} ProofIndex.gg (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_index.bend&name=gg) law gg: for -T: Data for +d: Nat for +t: P.Tree for +n: U32 for +i: U32 for +z: Bool for +hf: {D.full(T, P.fromT(T, t), d) == True{} : Bool} for +hn: {U32.to_nat(n) == Nat.pow(2n, d) : Nat} for +hi: {Nat.is_lt(U32.to_nat(i), Nat.pow(2n, d)) == True{} : Bool} for +hz: {U32.is_lt(i, U32.shr(n)) == z : Bool} … ProofIndex.gso (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_index.bend&name=gso) # What a swap hands back is the leaf it replaced. law gso: for -T: Data for +d: Nat for +t: P.Tree for +n: U32 for +i: U32 for +v: T for +z: Bool for +hf: {D.full(T, P.fromT(T, t), d) == True{} : Bool} for +hn: {U32.to_nat(n) == Nat.pow(2n, d) : Nat} … ProofIndex.gsv (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_index.bend&name=gsv) # A swap writes leaf i of the list of leaves. law gsv: for -T: Data for +d: Nat for +t: P.Tree for +n: U32 for +i: U32 for +v: T for +z: Bool for +hf: {D.full(T, P.fromT(T, t), d) == True{} : Bool} for +hn: {U32.to_nat(n) == Nat.pow(2n, d) : Nat} … ProofIndex.one_mul (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_index.bend&name=one_mul) law one_mul: for +x: Nat {Nat.mul(U32.to_nat(1), x) == x : Nat} ProofIndex.size_n (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_index.bend&name=size_n) law size_n: for +d: Nat for +hd: {Nat.is_lt(d, 32n) == True{} : Bool} {U32.to_nat(U32.shln(1, d)) == Nat.pow(2n, d) : Nat} ProofIndex.le0 (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_index.bend&name=le0) law le0: for +y: Nat {Nat.is_le(0n, y) == True{} : Bool} ProofIndex.le1_pow (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_index.bend&name=le1_pow) law le1_pow: for +d: Nat {Nat.is_le(1n, Nat.pow(2n, d)) == True{} : Bool} ProofIndex.le1_pow.go (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_index.bend&name=le1_pow.go) def le1_pow.go(+x: Nat, h: {Nat.is_lt(0n, x) == True{} : Bool}) -> {Nat.is_le(1n, x) == True{} : Bool}: ProofIndex.le1 (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_index.bend&name=le1) law le1: for +d: Nat for +hd: {Nat.is_lt(d, 32n) == True{} : Bool} {U32.is_le(1, U32.shln(1, d)) == True{} : Bool} ProofIndex.mask_n (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_index.bend&name=mask_n) law mask_n: for +d: Nat for +hd: {Nat.is_lt(d, 32n) == True{} : Bool} {U32.to_nat(U32.sub(U32.shln(1, d), 1)) == Nat.sub(Nat.pow(2n, d), 1n) : Nat} ProofIndex.slot_n (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_index.bend&name=slot_n) law slot_n: for +i: U32 for +d: Nat for +hd: {Nat.is_lt(d, 32n) == True{} : Bool} {U32.to_nat(U32.and(i, U32.sub(U32.shln(1, d), 1))) == D.slot(i, d) : Nat} ProofIndex.slot_lt_t (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_index.bend&name=slot_lt_t) law slot_lt_t: for +i: U32 for +d: Nat {Nat.is_lt(D.slot(i, d), Nat.pow(2n, d)) == True{} : Bool} ProofIndex.slot_small_t (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_index.bend&name=slot_small_t) law slot_small_t: for +i: U32 for +d: Nat for +h: {Nat.is_lt(U32.to_nat(i), Nat.pow(2n, d)) == True{} : Bool} {D.slot(i, d) == U32.to_nat(i) : Nat} ProofIndex.jlt (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_index.bend&name=jlt) law jlt: for +i: U32 for +d: Nat for +hd: {Nat.is_lt(d, 32n) == True{} : Bool} {Nat.is_lt(U32.to_nat(U32.and(i, U32.sub(U32.shln(1, d), 1))), Nat.pow(2n, d)) == True{} : Bool} ProofIndex.size_count_t (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_index.bend&name=size_count_t) law size_count_t: for -T: Data for +t: P.Tree for +d: Nat for +hf: {D.full(T, P.fromT(T, t), d) == True{} : Bool} for +hd: {Nat.is_lt(d, 32n) == True{} : Bool} {U32.to_nat(Pair.snd(Array, U32, Array.size(T, P.fromT(T, t)))) == Nat.pow(2n, d) : Nat} ProofIndex.get_view_t (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_index.bend&name=get_view_t) law get_view_t: for -T: Data for +t: P.Tree for +d: Nat for +i: U32 for +hf: {D.full(T, P.fromT(T, t), d) == True{} : Bool} for +hd: {Nat.is_lt(d, 32n) == True{} : Bool} {Some{Pair.snd(Array, T, Array.get(T, P.fromT(T, t), i))} == List.get(&2, T, D.view(T, P.fromT(T, t)), D.slot(i, d)) : Maybe<&2, T>} ProofIndex.swap_old_t (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_index.bend&name=swap_old_t) law swap_old_t: for -T: Data for +t: P.Tree for +d: Nat for +i: U32 for +v: T for +hf: {D.full(T, P.fromT(T, t), d) == True{} : Bool} for +hd: {Nat.is_lt(d, 32n) == True{} : Bool} {Some{Pair.snd(Array, T, Array.swap(T, P.fromT(T, t), i, v))} == List.get(&2, T, D.view(T, P.fromT(T, t)), D.slot(i, d)) : Maybe<&2, T>} ProofIndex.swap_view_t (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_index.bend&name=swap_view_t) law swap_view_t: for -T: Data for +t: P.Tree for +d: Nat for +i: U32 for +v: T for +hf: {D.full(T, P.fromT(T, t), d) == True{} : Bool} for +hd: {Nat.is_lt(d, 32n) == True{} : Bool} {D.view(T, Pair.fst(Array, T, Array.swap(T, P.fromT(T, t), i, v))) == List.set(&2, T, D.view(T, P.fromT(T, t)), D.slot(i, d), v) : List<&2, T>} ProofIndex.set_view_t (https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_index.bend&name=set_view_t) law set_view_t: for -T: Data for +t: P.Tree for +d: Nat for +i: U32 for +v: T for +hf: {D.full(T, P.fromT(T, t), d) == True{} : Bool} for +hd: {Nat.is_lt(d, 32n) == True{} : Bool} {D.view(T, Array.set(T, P.fromT(T, t), i, v)) == List.set(&2, T, D.view(T, P.fromT(T, t)), D.slot(i, d), v) : List<&2, T>} More: https://jend.leeeet.dev/packages/lawful-arrays.txt?definitions_offset=100