~/bend-docscommunity

proofs/containers/bitset/proof.bend source

proofs/containers/bitset/proof.bend on the hub · documented module

import Baseimport ../../lib/array.bend as Aimport ../../../spec/lib/common.bend as SCimport ../../../spec/containers/bitset.bend as Simport ../../../src/containers/bitset.bend as Bimport ../../../src/containers/types/bitset.bend as Eimport ./lists.bend as BLimport ./word.bend as Wimport ./index.bend as IXimport ./depth.bend as DPimport ./arr.bend as ARimport ./state.bend as STimport ./steps.bend as BSimport ./trace.bend as BTimport ../../lib/logic.bend as Limport ../../lib/nat.bend as Nimport ../../lib/list.bend as LL# Packed bitset: public proof entry point.#   abstraction  ST.abs(n, t)  (first n bits of the stored U32 words)#   invariant    ST.rep(n, d, t)  (the depth is the one `depth_for` picks, the#                word array is a perfect tree of that depth, n <= stored bits,#                every stored bit at a position >= n is zero)#   shadow       ST.Sh / ST.real / ST.good / ST.model  (Base.Array is linear,#                so every law is about the array built from a Data mirror#                tree, exactly as in proofs/dynamic_array)#   word facts   W.*     (U32 and/or/xor/not/shifts from Base's Word defs)#   index facts  IX.*    (i / 32 and i % 32 peel 32 bits at a time)#   array facts  AR.*    (Base.Array get/set against the slot list)#   operations   BS.step_ok (every op; IndexOutOfRange / LengthMismatch keep#                the state)#   traces       trace_new (arbitrary op lists from B.new(n))## `capacity(n)` is the documented capacity condition of the packed# representation: 2^31 words = 2^36 bits (see src/bitset.bend). It is a# premise only of the laws about `new`; every other law holds at every state# satisfying the invariant, and the invariant itself implies it# (ST.rep_fits).def capacity(+n: Nat) -> Type:  {Nat.is_le(n, Nat.mul(SC.pow2(B.depth_for(n)), 32n)) == True{} : Bool}def new_abs(+n: Nat, +h: {Nat.is_le(n, Nat.mul(SC.pow2(B.depth_for(n)), 32n)) == True{} : Bool}) -> {ST.model(BT.initial(n)) == S.new(n) : List<&2, Bool>}:  BT.new_model(n, h)def new_inv(+n: Nat, +h: {Nat.is_le(n, Nat.mul(SC.pow2(B.depth_for(n)), 32n)) == True{} : Bool}) -> {ST.good(BT.initial(n)) == True{} : Bool}:  BT.new_good(n, h)def new_real(+n: Nat) -> {B.new(n) == ST.real(BT.initial(n)) : B.Bitset}:  BT.new_real(n)def from_bools(+ys: List<&2, Bool>, +hf: {Nat.is_le(B.bool_count(ys), Nat.mul(SC.pow2(B.depth_for(B.bool_count(ys))), 32n)) == True{} : Bool}) -> BS.FromOK(ys):  BS.from_ok(ys, hf)def step_ok(sh: ST.Sh, op: E.Op, +g: {ST.good(sh) == True{} : Bool}) -> BS.StepOK(sh, op):  BS.step_ok(sh, op, g)# A runtime bitset determines its shadow, so "the operation lands on the array# of THIS shadow, whose model is the spec's" pins the abstract state: the laws# above cannot be satisfied by naming a different shadow.def shadow_unique(+a: ST.Sh, +b: ST.Sh, +e: {ST.real(a) == ST.real(b) : B.Bitset}) -> {a == b : ST.Sh}:  ST.real_inj(a, b, e)# Arbitrary finite operation traces from the real constructor.def trace_new(+n: Nat, +ops: List<&2, E.Op>, +h: {Nat.is_le(n, Nat.mul(SC.pow2(B.depth_for(n)), 32n)) == True{} : Bool}) -> BT.TraceOK(ops, BT.initial(n)):  BT.trace_from(ops, BT.initial(n), BT.new_good(n, h))# ==== the contract of bitset (stated in spec/containers/bitset.bend) ====================# ---- the implementation ----def Impl(sh: ST.Sh, op: E.Op, Post: (List<&2, Bool> & E.Obs) -> Type) -> Type:  Sigma<&1, &1, ST.Sh, sh2 => Sigma<&1, &1, E.Obs, o => {B.step(ST.real(sh), op) == (ST.real(sh2), o) : B.Bitset & E.Obs} & ({ST.good(sh2) == True{} : Bool} & Post((ST.model(sh2), o)))>>def impl_of(-sh: ST.Sh, -op: E.Op, -Post: (List<&2, Bool> & E.Obs) -> Type, k: BS.StepOK(sh, op), pf: Post(S.step(ST.model(sh), op))) -> Impl(sh, op, Post):  match k:    case Tuple{sh2, Tuple{o, Tuple{e1, Tuple{g2, e2}}}}:      (sh2, (o, (e1, (g2, L.subst(List<&2, Bool> & E.Obs, Post, S.step(ST.model(sh), op), (ST.model(sh2), o), Equal.sym(List<&2, Bool> & E.Obs, (ST.model(sh2), o), S.step(ST.model(sh), op), e2), pf)))))def impl(sh: ST.Sh, op: E.Op, +g: {ST.good(sh) == True{} : Bool}, -Post: (List<&2, Bool> & E.Obs) -> Type, pf: Post(S.step(ST.model(sh), op))) -> Impl(sh, op, Post):  impl_of(sh, op, Post, step_ok(sh, op, g), pf)# ---- arithmetic and Boolean facts ----def succ_ne_zero(+a: Nat, +e: {1n+a == 0n : Nat}) -> Empty:  L.false_true(Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), 1n+a, 0n, e))def zero_ne_succ(+a: Nat, +e: {0n == 1n+a : Nat}) -> Empty:  L.true_false(Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), 0n, 1n+a, e))def succ_pick(+b: Bool, +x: Nat, +y: Nat) -> {1n+Bool.pick(Nat, b, x, y) == Bool.pick(Nat, b, 1n+x, 1n+y) : Nat}:  match b:    case True{}:      {==}    case False{}:      {==}def zero_add(+n: Nat) -> {Nat.add(0n, n) == n : Nat}:  Equal.trans(Nat, Nat.add(0n, n), Nat.add(n, 0n), n, N.add_comm(0n, n), N.add_zero(n))def succ_add(+a: Nat, +b: Nat) -> {Nat.add(1n+a, b) == Nat.add(a, 1n+b) : Nat}:  Equal.trans(Nat, Nat.add(1n+a, b), Nat.add(b, 1n+a), Nat.add(a, 1n+b), N.add_comm(1n+a, b),    Equal.trans(Nat, Nat.add(b, 1n+a), 1n+Nat.add(b, a), Nat.add(a, 1n+b), N.add_succ(b, a),      Equal.trans(Nat, 1n+Nat.add(b, a), 1n+Nat.add(a, b), Nat.add(a, 1n+b), N.succ_cong(Nat.add(b, a), Nat.add(a, b), N.add_comm(b, a)), Equal.sym(Nat, Nat.add(a, 1n+b), 1n+Nat.add(a, b), N.add_succ(a, b)))))# ---- Contains ----def inset_nth(+xs: List<&2, Bool>, +k: Nat, +b: Bool, +h: {SC.nth(Bool, xs, k) == Some{b} : Maybe<&2, Bool>}) -> {S.inset(xs, k) == b : Bool}:  %Equal.sym(Maybe<&2, Bool>, SC.nth(Bool, xs, k), Some{b}, h) : {S.ins(_) == b : Bool}  {==}def gr_y(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}, +y: Maybe<&2, Bool>, +hy: {SC.nth(Bool, xs, i) == y : Maybe<&2, Bool>}) -> {S.ob(xs, E.Get{i}) == E.OBit{Done{S.inset(xs, i)}} : E.Obs}:  match y:    case None{}:      Empty.absurd({S.ob(xs, E.Get{i}) == E.OBit{Done{S.inset(xs, i)}} : E.Obs}, LL.sc_nth_some(Bool, xs, i, h, hy))    case Some{+b}:      %Equal.sym(Maybe<&2, Bool>, SC.nth(Bool, xs, i), Some{b}, hy) : {E.OBit{S.bit(_)} == E.OBit{Done{S.ins(_)}} : E.Obs}      {==}def get_result(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> S.Contains.get_result(xs, i, h):  gr_y(xs, i, h, SC.nth(Bool, xs, i), {==})def get_frame(+xs: List<&2, Bool>, +i: Nat) -> S.Contains.get_frame(xs, i):  {==}def get_outside(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_le(SC.length(Bool, xs), i) == True{} : Bool}) -> S.Contains.get_outside(xs, i, h):  %Equal.sym(Maybe<&2, Bool>, SC.nth(Bool, xs, i), None{}, LL.nth_none(Bool, xs, i, h)) : {E.OBit{S.bit(_)} == E.OBit{Fail{E.IndexOutOfRange{}}} : E.Obs}  {==}# ---- Length (the member count), Capacity (the universe) ----def count_result(+xs: List<&2, Bool>) -> S.Length.count_result(xs):  {==}def count_frame(+xs: List<&2, Bool>) -> S.Length.count_frame(xs):  {==}def length_result(+xs: List<&2, Bool>) -> S.Capacity.length_result(xs):  {==}def length_frame(+xs: List<&2, Bool>) -> S.Capacity.length_frame(xs):  {==}# ---- Empty_Set: no member, Length 0, over the universe [0, n) ----def new_contains(+n: Nat, +k: Nat) -> S.Empty_Set.new_contains(n, k):  match n k:    case 0n _:      {==}    case 1n+m 0n:      {==}    case 1n+ +m 1n+ +j:      new_contains(m, j)def new_count(+n: Nat) -> S.Empty_Set.new_count(n):  match n:    case 0n:      {==}    case 1n+ +m:      new_count(m)def new_length(+n: Nat) -> S.Empty_Set.new_length(n):  LL.length_replicate(Bool, n, False{})# ---- the update of one bit ----def assign_is(+xs: List<&2, Bool>, +i: Nat, +v: Bool, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}, +y: Maybe<&2, Bool>, +hy: {SC.nth(Bool, xs, i) == y : Maybe<&2, Bool>}) -> {S.assign(xs, i, v) == (SC.update(Bool, xs, i, v), E.OUnit{Done{Unit{}}}) : List<&2, Bool> & E.Obs}:  match y:    case None{}:      Empty.absurd({S.assign(xs, i, v) == (SC.update(Bool, xs, i, v), E.OUnit{Done{Unit{}}}) : List<&2, Bool> & E.Obs}, LL.sc_nth_some(Bool, xs, i, h, hy))    case Some{b}:      %Equal.sym(Maybe<&2, Bool>, SC.nth(Bool, xs, i), Some{b}, hy) : {S.assign_at(_, xs, i, v) == (SC.update(Bool, xs, i, v), E.OUnit{Done{Unit{}}}) : List<&2, Bool> & E.Obs}      {==}def inset_update_same(+xs: List<&2, Bool>, +i: Nat, +v: Bool, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> {S.inset(SC.update(Bool, xs, i, v), i) == v : Bool}:  inset_nth(SC.update(Bool, xs, i, v), i, v, LL.nth_update_same(Bool, xs, i, v, h))def inset_update_other(+xs: List<&2, Bool>, +i: Nat, +j: Nat, +v: Bool, +ne: {Nat.is_eq(i, j) == False{} : Bool}) -> {S.inset(SC.update(Bool, xs, i, v), j) == S.inset(xs, j) : Bool}:  Equal.cong(Maybe<&2, Bool>, Bool, z => S.ins(z), SC.nth(Bool, SC.update(Bool, xs, i, v), j), SC.nth(Bool, xs, j), LL.nth_update_other(Bool, xs, i, j, v, ne))# count after setting a bit: one more unless it was setdef cu_set(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> {S.count(SC.update(Bool, xs, i, True{})) == Bool.pick(Nat, S.inset(xs, i), S.count(xs), 1n+S.count(xs)) : Nat}:  match xs i:    case Nil{} _:      Empty.absurd({S.count(SC.update(Bool, Nil{}, i, True{})) == Bool.pick(Nat, S.inset(Nil{}, i), S.count(Nil{}), 1n+S.count(Nil{})) : Nat}, N.lt_zero_absurd(i, h))    case Con{True{}, t} 0n:      {==}    case Con{False{}, t} 0n:      {==}    case Con{True{}, +t} 1n+ +p:      %Equal.sym(Nat, S.count(SC.update(Bool, t, p, True{})), Bool.pick(Nat, S.inset(t, p), S.count(t), 1n+S.count(t)), cu_set(t, p, h)) : {1n+_ == Bool.pick(Nat, S.inset(t, p), 1n+S.count(t), 1n+(1n+S.count(t))) : Nat}      succ_pick(S.inset(t, p), S.count(t), 1n+S.count(t))    case Con{False{}, +t} 1n+ +p:      cu_set(t, p, h)# count after clearing a bit: one less if it was setdef cu_clear(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> {S.count(xs) == Bool.pick(Nat, S.inset(xs, i), 1n+S.count(SC.update(Bool, xs, i, False{})), S.count(SC.update(Bool, xs, i, False{}))) : Nat}:  match xs i:    case Nil{} _:      Empty.absurd({S.count(Nil{}) == Bool.pick(Nat, S.inset(Nil{}, i), 1n+S.count(SC.update(Bool, Nil{}, i, False{})), S.count(SC.update(Bool, Nil{}, i, False{}))) : Nat}, N.lt_zero_absurd(i, h))    case Con{True{}, t} 0n:      {==}    case Con{False{}, t} 0n:      {==}    case Con{True{}, +t} 1n+ +p:      %Equal.sym(Nat, S.count(t), Bool.pick(Nat, S.inset(t, p), 1n+S.count(SC.update(Bool, t, p, False{})), S.count(SC.update(Bool, t, p, False{}))), cu_clear(t, p, h)) : {1n+_ == Bool.pick(Nat, S.inset(t, p), 1n+(1n+S.count(SC.update(Bool, t, p, False{}))), 1n+S.count(SC.update(Bool, t, p, False{}))) : Nat}      succ_pick(S.inset(t, p), 1n+S.count(SC.update(Bool, t, p, False{})), S.count(SC.update(Bool, t, p, False{})))    case Con{False{}, +t} 1n+ +p:      cu_clear(t, p, h)# ---- Include / Insert (set) ----def set_model(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> {S.nx(xs, E.Set{i}) == SC.update(Bool, xs, i, True{}) : List<&2, Bool>}:  %Equal.sym(List<&2, Bool> & E.Obs, S.assign(xs, i, True{}), (SC.update(Bool, xs, i, True{}), E.OUnit{Done{Unit{}}}), assign_is(xs, i, True{}, h, SC.nth(Bool, xs, i), {==})) : {Pair.fst(List<&2, Bool>, E.Obs, _) == SC.update(Bool, xs, i, True{}) : List<&2, Bool>}  {==}def set_contains(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> S.Include.set_contains(xs, i, h):  %Equal.sym(List<&2, Bool>, S.nx(xs, E.Set{i}), SC.update(Bool, xs, i, True{}), set_model(xs, i, h)) : {S.inset(_, i) == True{} : Bool}  inset_update_same(xs, i, True{}, h)def set_others(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}, +j: Nat, +ne: {Nat.is_eq(i, j) == False{} : Bool}) -> S.Include.set_others(xs, i, h, j, ne):  %Equal.sym(List<&2, Bool>, S.nx(xs, E.Set{i}), SC.update(Bool, xs, i, True{}), set_model(xs, i, h)) : {S.inset(_, j) == S.inset(xs, j) : Bool}  inset_update_other(xs, i, j, True{}, ne)def set_universe(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> S.Include.set_universe(xs, i, h):  %Equal.sym(List<&2, Bool>, S.nx(xs, E.Set{i}), SC.update(Bool, xs, i, True{}), set_model(xs, i, h)) : {SC.length(Bool, _) == SC.length(Bool, xs) : Nat}  LL.length_update(Bool, xs, i, True{})def set_outside(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_le(SC.length(Bool, xs), i) == True{} : Bool}) -> S.Include.set_outside(xs, i, h):  %Equal.sym(Maybe<&2, Bool>, SC.nth(Bool, xs, i), None{}, LL.nth_none(Bool, xs, i, h)) : {S.assign_at(_, xs, i, True{}) == (xs, E.OUnit{Fail{E.IndexOutOfRange{}}}) : List<&2, Bool> & E.Obs}  {==}# ---- Exclude / Delete (clear) ----def clear_model(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> {S.nx(xs, E.Clear{i}) == SC.update(Bool, xs, i, False{}) : List<&2, Bool>}:  %Equal.sym(List<&2, Bool> & E.Obs, S.assign(xs, i, False{}), (SC.update(Bool, xs, i, False{}), E.OUnit{Done{Unit{}}}), assign_is(xs, i, False{}, h, SC.nth(Bool, xs, i), {==})) : {Pair.fst(List<&2, Bool>, E.Obs, _) == SC.update(Bool, xs, i, False{}) : List<&2, Bool>}  {==}def clear_contains(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> S.Exclude.clear_contains(xs, i, h):  %Equal.sym(List<&2, Bool>, S.nx(xs, E.Clear{i}), SC.update(Bool, xs, i, False{}), clear_model(xs, i, h)) : {S.inset(_, i) == False{} : Bool}  inset_update_same(xs, i, False{}, h)def clear_others(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}, +j: Nat, +ne: {Nat.is_eq(i, j) == False{} : Bool}) -> S.Exclude.clear_others(xs, i, h, j, ne):  %Equal.sym(List<&2, Bool>, S.nx(xs, E.Clear{i}), SC.update(Bool, xs, i, False{}), clear_model(xs, i, h)) : {S.inset(_, j) == S.inset(xs, j) : Bool}  inset_update_other(xs, i, j, False{}, ne)def clear_universe(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> S.Exclude.clear_universe(xs, i, h):  %Equal.sym(List<&2, Bool>, S.nx(xs, E.Clear{i}), SC.update(Bool, xs, i, False{}), clear_model(xs, i, h)) : {SC.length(Bool, _) == SC.length(Bool, xs) : Nat}  LL.length_update(Bool, xs, i, False{})def clear_outside(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_le(SC.length(Bool, xs), i) == True{} : Bool}) -> S.Exclude.clear_outside(xs, i, h):  %Equal.sym(Maybe<&2, Bool>, SC.nth(Bool, xs, i), None{}, LL.nth_none(Bool, xs, i, h)) : {S.assign_at(_, xs, i, False{}) == (xs, E.OUnit{Fail{E.IndexOutOfRange{}}}) : List<&2, Bool> & E.Obs}  {==}# Include: one more member unless it was one (Insert's Pre: it was not)def set_count(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> S.Include.set_count(xs, i, h):  %Equal.sym(List<&2, Bool>, S.nx(xs, E.Set{i}), SC.update(Bool, xs, i, True{}), set_model(xs, i, h)) : {S.count(_) == Bool.pick(Nat, S.inset(xs, i), S.count(xs), 1n+S.count(xs)) : Nat}  cu_set(xs, i, h)# Exclude: one member less if it was one (Delete's Pre: it was)def clear_count(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> S.Exclude.clear_count(xs, i, h):  %Equal.sym(List<&2, Bool>, S.nx(xs, E.Clear{i}), SC.update(Bool, xs, i, False{}), clear_model(xs, i, h)) : {S.count(xs) == Bool.pick(Nat, S.inset(xs, i), 1n+S.count(_), S.count(_)) : Nat}  cu_clear(xs, i, h)# ---- Union (1180) ----def union_pt(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +k: Nat, +h: {SC.length(Bool, xs) == SC.length(Bool, ys) : Nat}) -> {S.inset(S.zip_or(xs, ys), k) == Bool.or(S.inset(xs, k), S.inset(ys, k)) : Bool}:  match xs ys k:    case Nil{} Nil{} _:      {==}    case Nil{} Con{b, t} _:      Empty.absurd({S.inset(S.zip_or(Nil{}, Con{b, t}), k) == Bool.or(S.inset(Nil{}, k), S.inset(Con{b, t}, k)) : Bool}, zero_ne_succ(SC.length(Bool, t), h))    case Con{a, s} Nil{} _:      Empty.absurd({S.inset(S.zip_or(Con{a, s}, Nil{}), k) == Bool.or(S.inset(Con{a, s}, k), S.inset(Nil{}, k)) : Bool}, succ_ne_zero(SC.length(Bool, s), h))    case Con{a, s} Con{b, t} 0n:      {==}    case Con{a, +s} Con{b, +t} 1n+ +p:      union_pt(s, t, p, N.succ_inj(SC.length(Bool, s), SC.length(Bool, t), h))def union_contains(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +k: Nat, +h: {SC.length(Bool, xs) == SC.length(Bool, ys) : Nat}) -> S.Union.union_contains(xs, ys, k, h):  %h : {S.inset(Pair.fst(List<&2, Bool>, E.Obs, S.combine_if(Nat.is_eq(SC.length(Bool, xs), _), xs, S.zip_or(xs, ys))), k) == Bool.or(S.inset(xs, k), S.inset(ys, k)) : Bool}  %Equal.sym(Bool, Nat.is_eq(SC.length(Bool, xs), SC.length(Bool, xs)), True{}, N.is_eq_refl(SC.length(Bool, xs))) : {S.inset(Pair.fst(List<&2, Bool>, E.Obs, S.combine_if(_, xs, S.zip_or(xs, ys))), k) == Bool.or(S.inset(xs, k), S.inset(ys, k)) : Bool}  union_pt(xs, ys, k, h)def union_mismatch(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +h: {Nat.is_eq(SC.length(Bool, xs), SC.length(Bool, ys)) == False{} : Bool}) -> S.Union.union_mismatch(xs, ys, h):  %Equal.sym(Bool, Nat.is_eq(SC.length(Bool, xs), SC.length(Bool, ys)), False{}, h) : {S.combine_if(_, xs, S.zip_or(xs, ys)) == (xs, E.OUnit{Fail{E.LengthMismatch{}}}) : List<&2, Bool> & E.Obs}  {==}# ---- Intersection (1279) ----def intersection_pt(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +k: Nat, +h: {SC.length(Bool, xs) == SC.length(Bool, ys) : Nat}) -> {S.inset(S.zip_and(xs, ys), k) == Bool.and(S.inset(xs, k), S.inset(ys, k)) : Bool}:  match xs ys k:    case Nil{} Nil{} _:      {==}    case Nil{} Con{b, t} _:      Empty.absurd({S.inset(S.zip_and(Nil{}, Con{b, t}), k) == Bool.and(S.inset(Nil{}, k), S.inset(Con{b, t}, k)) : Bool}, zero_ne_succ(SC.length(Bool, t), h))    case Con{a, s} Nil{} _:      Empty.absurd({S.inset(S.zip_and(Con{a, s}, Nil{}), k) == Bool.and(S.inset(Con{a, s}, k), S.inset(Nil{}, k)) : Bool}, succ_ne_zero(SC.length(Bool, s), h))    case Con{a, s} Con{b, t} 0n:      {==}    case Con{a, +s} Con{b, +t} 1n+ +p:      intersection_pt(s, t, p, N.succ_inj(SC.length(Bool, s), SC.length(Bool, t), h))def intersection_contains(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +k: Nat, +h: {SC.length(Bool, xs) == SC.length(Bool, ys) : Nat}) -> S.Intersection.intersection_contains(xs, ys, k, h):  %h : {S.inset(Pair.fst(List<&2, Bool>, E.Obs, S.combine_if(Nat.is_eq(SC.length(Bool, xs), _), xs, S.zip_and(xs, ys))), k) == Bool.and(S.inset(xs, k), S.inset(ys, k)) : Bool}  %Equal.sym(Bool, Nat.is_eq(SC.length(Bool, xs), SC.length(Bool, xs)), True{}, N.is_eq_refl(SC.length(Bool, xs))) : {S.inset(Pair.fst(List<&2, Bool>, E.Obs, S.combine_if(_, xs, S.zip_and(xs, ys))), k) == Bool.and(S.inset(xs, k), S.inset(ys, k)) : Bool}  intersection_pt(xs, ys, k, h)def intersection_mismatch(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +h: {Nat.is_eq(SC.length(Bool, xs), SC.length(Bool, ys)) == False{} : Bool}) -> S.Intersection.intersection_mismatch(xs, ys, h):  %Equal.sym(Bool, Nat.is_eq(SC.length(Bool, xs), SC.length(Bool, ys)), False{}, h) : {S.combine_if(_, xs, S.zip_and(xs, ys)) == (xs, E.OUnit{Fail{E.LengthMismatch{}}}) : List<&2, Bool> & E.Obs}  {==}# ---- Difference (1340) ----def difference_pt(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +k: Nat, +h: {SC.length(Bool, xs) == SC.length(Bool, ys) : Nat}) -> {S.inset(S.zip_diff(xs, ys), k) == Bool.and(S.inset(xs, k), Bool.not(S.inset(ys, k))) : Bool}:  match xs ys k:    case Nil{} Nil{} _:      {==}    case Nil{} Con{b, t} _:      Empty.absurd({S.inset(S.zip_diff(Nil{}, Con{b, t}), k) == Bool.and(S.inset(Nil{}, k), Bool.not(S.inset(Con{b, t}, k))) : Bool}, zero_ne_succ(SC.length(Bool, t), h))    case Con{a, s} Nil{} _:      Empty.absurd({S.inset(S.zip_diff(Con{a, s}, Nil{}), k) == Bool.and(S.inset(Con{a, s}, k), Bool.not(S.inset(Nil{}, k))) : Bool}, succ_ne_zero(SC.length(Bool, s), h))    case Con{a, s} Con{b, t} 0n:      {==}    case Con{a, +s} Con{b, +t} 1n+ +p:      difference_pt(s, t, p, N.succ_inj(SC.length(Bool, s), SC.length(Bool, t), h))def difference_contains(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +k: Nat, +h: {SC.length(Bool, xs) == SC.length(Bool, ys) : Nat}) -> S.Difference.difference_contains(xs, ys, k, h):  %h : {S.inset(Pair.fst(List<&2, Bool>, E.Obs, S.combine_if(Nat.is_eq(SC.length(Bool, xs), _), xs, S.zip_diff(xs, ys))), k) == Bool.and(S.inset(xs, k), Bool.not(S.inset(ys, k))) : Bool}  %Equal.sym(Bool, Nat.is_eq(SC.length(Bool, xs), SC.length(Bool, xs)), True{}, N.is_eq_refl(SC.length(Bool, xs))) : {S.inset(Pair.fst(List<&2, Bool>, E.Obs, S.combine_if(_, xs, S.zip_diff(xs, ys))), k) == Bool.and(S.inset(xs, k), Bool.not(S.inset(ys, k))) : Bool}  difference_pt(xs, ys, k, h)def difference_mismatch(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +h: {Nat.is_eq(SC.length(Bool, xs), SC.length(Bool, ys)) == False{} : Bool}) -> S.Difference.difference_mismatch(xs, ys, h):  %Equal.sym(Bool, Nat.is_eq(SC.length(Bool, xs), SC.length(Bool, ys)), False{}, h) : {S.combine_if(_, xs, S.zip_diff(xs, ys)) == (xs, E.OUnit{Fail{E.LengthMismatch{}}}) : List<&2, Bool> & E.Obs}  {==}# ---- Symmetric_Difference (1404) ----def symmetric_difference_pt(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +k: Nat, +h: {SC.length(Bool, xs) == SC.length(Bool, ys) : Nat}) -> {S.inset(S.zip_xor(xs, ys), k) == Bool.xor(S.inset(xs, k), S.inset(ys, k)) : Bool}:  match xs ys k:    case Nil{} Nil{} _:      {==}    case Nil{} Con{b, t} _:      Empty.absurd({S.inset(S.zip_xor(Nil{}, Con{b, t}), k) == Bool.xor(S.inset(Nil{}, k), S.inset(Con{b, t}, k)) : Bool}, zero_ne_succ(SC.length(Bool, t), h))    case Con{a, s} Nil{} _:      Empty.absurd({S.inset(S.zip_xor(Con{a, s}, Nil{}), k) == Bool.xor(S.inset(Con{a, s}, k), S.inset(Nil{}, k)) : Bool}, succ_ne_zero(SC.length(Bool, s), h))    case Con{a, s} Con{b, t} 0n:      {==}    case Con{a, +s} Con{b, +t} 1n+ +p:      symmetric_difference_pt(s, t, p, N.succ_inj(SC.length(Bool, s), SC.length(Bool, t), h))def symmetric_difference_contains(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +k: Nat, +h: {SC.length(Bool, xs) == SC.length(Bool, ys) : Nat}) -> S.Symmetric_Difference.symmetric_difference_contains(xs, ys, k, h):  %h : {S.inset(Pair.fst(List<&2, Bool>, E.Obs, S.combine_if(Nat.is_eq(SC.length(Bool, xs), _), xs, S.zip_xor(xs, ys))), k) == Bool.xor(S.inset(xs, k), S.inset(ys, k)) : Bool}  %Equal.sym(Bool, Nat.is_eq(SC.length(Bool, xs), SC.length(Bool, xs)), True{}, N.is_eq_refl(SC.length(Bool, xs))) : {S.inset(Pair.fst(List<&2, Bool>, E.Obs, S.combine_if(_, xs, S.zip_xor(xs, ys))), k) == Bool.xor(S.inset(xs, k), S.inset(ys, k)) : Bool}  symmetric_difference_pt(xs, ys, k, h)def xor_mismatch(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +h: {Nat.is_eq(SC.length(Bool, xs), SC.length(Bool, ys)) == False{} : Bool}) -> S.Symmetric_Difference.xor_mismatch(xs, ys, h):  %Equal.sym(Bool, Nat.is_eq(SC.length(Bool, xs), SC.length(Bool, ys)), False{}, h) : {S.combine_if(_, xs, S.zip_xor(xs, ys)) == (xs, E.OUnit{Fail{E.LengthMismatch{}}}) : List<&2, Bool> & E.Obs}  {==}def to_list_result(+xs: List<&2, Bool>) -> S.Elements.to_list_result(xs):  {==}def to_list_frame(+xs: List<&2, Bool>) -> S.Elements.to_list_frame(xs):  {==}# no member below the offsetdef members_above(+xs: List<&2, Bool>, +off: Nat, +j: Nat, +h: {Nat.is_lt(j, off) == True{} : Bool}) -> {S.nmem(j, S.members(xs, off)) == False{} : Bool}:  match xs:    case Nil{}:      {==}    case Con{False{}, +t}:      members_above(t, 1n+off, j, N.lt_trans(j, off, 1n+off, h, N.lt_succ(off)))    case Con{True{}, +t}:      %Equal.sym(Bool, Nat.is_eq(off, j), False{}, N.is_eq_sym_false(j, off, N.is_eq_lt(j, off, h))) : {Bool.or(_, S.nmem(j, S.members(t, 1n+off))) == False{} : Bool}      members_above(t, 1n+off, j, N.lt_trans(j, off, 1n+off, h, N.lt_succ(off)))def rel_add(+off: Nat, +p: Nat) -> {Nat.add(1n+off, p) == Nat.add(1n+p, off) : Nat}:  Equal.trans(Nat, Nat.add(1n+off, p), Nat.add(off, 1n+p), Nat.add(1n+p, off), succ_add(off, p), N.add_comm(off, 1n+p))def ne_add_succ(+off: Nat, +p: Nat) -> {Nat.is_eq(off, Nat.add(1n+p, off)) == False{} : Bool}:  N.is_eq_lt(off, Nat.add(1n+p, off), N.lt_le_trans(off, 1n+off, Nat.add(1n+p, off), N.lt_succ(off), L.subst(Nat, z => {Nat.is_le(1n+off, z) == True{} : Bool}, Nat.add(1n+off, p), Nat.add(1n+p, off), rel_add(off, p), N.le_add_right(1n+off, p))))# the member at relative index k is there exactly when bit k is setdef members_pt(+xs: List<&2, Bool>, +k: Nat, +off: Nat) -> {S.nmem(Nat.add(k, off), S.members(xs, off)) == S.inset(xs, k) : Bool}:  match xs k:    case Nil{} _:      {==}    case Con{False{}, +t} 0n:      %Equal.sym(Nat, Nat.add(0n, off), off, zero_add(off)) : {S.nmem(_, S.members(t, 1n+off)) == False{} : Bool}      members_above(t, 1n+off, off, N.lt_succ(off))    case Con{True{}, +t} 0n:      %Equal.sym(Nat, Nat.add(0n, off), off, zero_add(off)) : {Bool.or(Nat.is_eq(off, _), S.nmem(_, S.members(t, 1n+off))) == True{} : Bool}      %Equal.sym(Bool, Nat.is_eq(off, off), True{}, N.is_eq_refl(off)) : {Bool.or(_, S.nmem(off, S.members(t, 1n+off))) == True{} : Bool}      {==}    case Con{False{}, +t} 1n+ +p:      %Equal.sym(Nat, Nat.add(1n+p, off), Nat.add(p, 1n+off), succ_add(p, off)) : {S.nmem(_, S.members(t, 1n+off)) == S.inset(t, p) : Bool}      members_pt(t, p, 1n+off)    case Con{True{}, +t} 1n+ +p:      %Equal.sym(Bool, Nat.is_eq(off, Nat.add(1n+p, off)), False{}, ne_add_succ(off, p)) : {Bool.or(_, S.nmem(Nat.add(1n+p, off), S.members(t, 1n+off))) == S.inset(t, p) : Bool}      %Equal.sym(Nat, Nat.add(1n+p, off), Nat.add(p, 1n+off), succ_add(p, off)) : {Bool.or(False{}, S.nmem(_, S.members(t, 1n+off))) == S.inset(t, p) : Bool}      members_pt(t, p, 1n+off)def elements_contains(+xs: List<&2, Bool>, +k: Nat) -> S.Elements.elements_contains(xs, k):  %N.add_zero(k) : {S.nmem(_, S.members(xs, 0n)) == S.inset(xs, k) : Bool}  members_pt(xs, k, 0n)# as many elements as members (SPARK: Length (Elements) = Length (Container))def elements_length(+xs: List<&2, Bool>, +off: Nat) -> S.Elements.elements_length(xs, off):  match xs:    case Nil{}:      {==}    case Con{False{}, +t}:      elements_length(t, 1n+off)    case Con{True{}, +t}:      N.succ_cong(SC.length(Nat, S.members(t, 1n+off)), S.count(t), elements_length(t, 1n+off))