bend-kit-collections Releases (6): 0.1.4.1 0x2e75a06e0acd57f098569f07516e8aae indexed https://jend.leeeet.dev/files.txt?path=bend-kit-collections@0.1.4.1 0.1.4.0 0x72fb885ca117e27146e7e70059f63236 unindexed https://jend.leeeet.dev/files.txt?path=bend-kit-collections@0.1.4.0 0.1.3.0 0x3247b353c72fc13d6f940252da321399 unindexed https://jend.leeeet.dev/files.txt?path=bend-kit-collections@0.1.3.0 0.1.2.0 0xd2d968d969a26029a632a3347c989456 unindexed https://jend.leeeet.dev/files.txt?path=bend-kit-collections@0.1.2.0 0.1.1.0 0x9d83ddf966d11f828944383c8c9577cc unindexed https://jend.leeeet.dev/files.txt?path=bend-kit-collections@0.1.1.0 0.1.0.0 0x620317aa272e53852c5b5baae68a727b unindexed https://jend.leeeet.dev/files.txt?path=bend-kit-collections@0.1.0.0 Definitions (620, 1 to 100 shown): LAWS.scmp.fin (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=scmp.fin) def scmp.fin(r: (String & String) & Cmp) -> Cmp: LAWS.scmp (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=scmp) def scmp(a: String, b: String) -> Cmp: LAWS.m3 (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=m3) def m3() -> O.OMap: LAWS.m7.go (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=m7.go) def m7.go(n: Nat, +i: U32, m: O.OMap) -> O.OMap: LAWS.m7 (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=m7) def m7() -> O.OMap: LAWS.omap_keys_ascending_puts (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=omap_keys_ascending_puts) law omap_keys_ascending_puts: {O.OMap.keys(U32, U32, m7()) == [1, 2, 3, 4, 5, 6, 7] : List<&2, U32>} LAWS.omap_size_del (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=omap_size_del) law omap_size_del: {O.OMap.size(U32, U32, O.OMap.del(~U32, ~U32, ~U32.cmp, m7(), 4)) == 6 : U32} LAWS.omap_get_after_rotations (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=omap_get_after_rotations) law omap_get_after_rotations: {O.OMap.get(~U32, ~U32, ~U32.cmp, O.OMap.del(~U32, ~U32, ~U32.cmp, m7(), 4), 6) == Some{60} : Maybe<&2, U32>} LAWS.omap_keys_del_root (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=omap_keys_del_root) law omap_keys_del_root: {O.OMap.keys(U32, U32, O.OMap.del(~U32, ~U32, ~U32.cmp, m7(), 4)) == [1, 2, 3, 5, 6, 7] : List<&2, U32>} LAWS.omap_get_put (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=omap_get_put) law omap_get_put: {O.OMap.get(~U32, ~U32, ~U32.cmp, O.OMap.put(~U32, ~U32, ~U32.cmp, m3(), 4, 40), 4) == Some{40} : Maybe<&2, U32>} LAWS.omap_get_put_replace (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=omap_get_put_replace) law omap_get_put_replace: {O.OMap.get(~U32, ~U32, ~U32.cmp, O.OMap.put(~U32, ~U32, ~U32.cmp, m3(), 3, 33), 3) == Some{33} : Maybe<&2, U32>} LAWS.omap_get_put_other (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=omap_get_put_other) law omap_get_put_other: {O.OMap.get(~U32, ~U32, ~U32.cmp, O.OMap.put(~U32, ~U32, ~U32.cmp, m3(), 4, 40), 3) == O.OMap.get(~U32, ~U32, ~U32.cmp, m3(), 3) : Maybe<&2, U32>} LAWS.omap_get_missing (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=omap_get_missing) law omap_get_missing: {O.OMap.get(~U32, ~U32, ~U32.cmp, m3(), 2) == None{} : Maybe<&2, U32>} LAWS.omap_keys_sorted (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=omap_keys_sorted) law omap_keys_sorted: {O.OMap.keys(U32, U32, O.OMap.put(~U32, ~U32, ~U32.cmp, m3(), 4, 40)) == [1, 3, 4, 5] : List<&2, U32>} LAWS.omap_size_replace (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=omap_size_replace) law omap_size_replace: {O.OMap.size(U32, U32, O.OMap.put(~U32, ~U32, ~U32.cmp, m3(), 5, 55)) == 3 : U32} LAWS.omap_get_del (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=omap_get_del) law omap_get_del: {O.OMap.get(~U32, ~U32, ~U32.cmp, O.OMap.del(~U32, ~U32, ~U32.cmp, m3(), 3), 3) == None{} : Maybe<&2, U32>} LAWS.omap_get_del_other (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=omap_get_del_other) law omap_get_del_other: {O.OMap.get(~U32, ~U32, ~U32.cmp, O.OMap.del(~U32, ~U32, ~U32.cmp, m3(), 3), 5) == Some{50} : Maybe<&2, U32>} LAWS.omap_keys_del (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=omap_keys_del) law omap_keys_del: {O.OMap.keys(U32, U32, O.OMap.del(~U32, ~U32, ~U32.cmp, m3(), 5)) == [1, 3] : List<&2, U32>} LAWS.omap_string_keys (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=omap_string_keys) law omap_string_keys: {O.OMap.keys(String, U32, O.OMap.put(~String, ~U32, ~scmp, O.OMap.put(~String, ~U32, ~scmp, O.OMap.new(String, U32), "b", 2), "a", 1)) == ["a", "b"] : List<&2, String>} LAWS.oset_to_list (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=oset_to_list) law oset_to_list: {O.OSet.to_list(U32, O.OSet.add(~U32, ~U32.cmp, O.OSet.add(~U32, ~U32.cmp, O.OSet.add(~U32, ~U32.cmp, O.OSet.new(U32), 3), 1), 3)) == [1, 3] : List<&2, U32>} LAWS.oset_has_del (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=oset_has_del) law oset_has_del: {O.OSet.has(~U32, ~U32.cmp, O.OSet.del(~U32, ~U32.cmp, O.OSet.add(~U32, ~U32.cmp, O.OSet.new(U32), 3), 3), 3) == False{} : Bool} LAWS.flip (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=flip) # The laws below hold for every comparator that is a total order, with EQ # meaning equal keys. def flip(c: Cmp) -> Cmp: LAWS.above (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=above) def above(~K: Data, ~cmp: K -> K -> Cmp, lb: Maybe<&2, K>, +k: K) -> Bool: LAWS.below (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=below) def below(~K: Data, ~cmp: K -> K -> Cmp, ub: Maybe<&2, K>, +k: K) -> Bool: LAWS.bounded (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=bounded) # Every key of m lies strictly between the bounds, in search-tree order. def bounded( ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: O.OMap, +lb: Maybe<&2, K>, +ub: Maybe<&2, K> ) -> Bool: LAWS.searchtree (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=searchtree) def searchtree(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: O.OMap) -> Bool: LAWS.sorted.go (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=sorted.go) def sorted.go(~K: Data, ~cmp: K -> K -> Cmp, xs: List<&2, K>, +prev: K) -> Bool: LAWS.sorted (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=sorted) def sorted(~K: Data, ~cmp: K -> K -> Cmp, xs: List<&2, K>) -> Bool: LAWS.omap_new_searchtree (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=omap_new_searchtree) law omap_new_searchtree: for ~K: Data for ~V: Data for ~cmp: K -> K -> Cmp {searchtree(~K, ~V, ~cmp, O.OMap.new(K, V)) == True{} : Bool} LAWS.omap_put_searchtree (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=omap_put_searchtree) law omap_put_searchtree: for ~K: Data for ~V: Data for ~cmp: K -> K -> Cmp for ~refl: @x: K -> {cmp(x, x) == EQ{} : Cmp} for ~eq: @x: K -> @y: K -> {cmp(x, y) == EQ{} : Cmp} -> {x == y : K} for ~flip: @x: K -> @y: K -> {cmp(y, x) == flip(cmp(x, y)) : Cmp} for ~trans: @x: K -> @y: K -> @z: K -> {cmp(x, y) == LT{} : Cmp} -> {cmp(y, z) == LT{} : Cmp} -> {cmp(x, z) == LT{} : Cmp} for m: O.OMap for tree: {searchtree(~K, ~V, ~cmp, m) == True{} : Bool} for +k: K … LAWS.omap_del_searchtree (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=omap_del_searchtree) law omap_del_searchtree: for ~K: Data for ~V: Data for ~cmp: K -> K -> Cmp for ~refl: @x: K -> {cmp(x, x) == EQ{} : Cmp} for ~eq: @x: K -> @y: K -> {cmp(x, y) == EQ{} : Cmp} -> {x == y : K} for ~flip: @x: K -> @y: K -> {cmp(y, x) == flip(cmp(x, y)) : Cmp} for ~trans: @x: K -> @y: K -> @z: K -> {cmp(x, y) == LT{} : Cmp} -> {cmp(y, z) == LT{} : Cmp} -> {cmp(x, z) == LT{} : Cmp} for m: O.OMap for tree: {searchtree(~K, ~V, ~cmp, m) == True{} : Bool} for +k: K {searchtree(~K, ~V, ~cmp, O.OMap.del(~K, ~V, ~cmp, m, k)) == True{} : Bool} LAWS.omap_searchtree_keys_sorted (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=omap_searchtree_keys_sorted) law omap_searchtree_keys_sorted: for ~K: Data for ~V: Data for ~cmp: K -> K -> Cmp for m: O.OMap for tree: {searchtree(~K, ~V, ~cmp, m) == True{} : Bool} {sorted(~K, ~cmp, O.OMap.keys(K, V, m)) == True{} : Bool} LAWS.omap_get_put_same (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=omap_get_put_same) law omap_get_put_same: for ~K: Data for ~V: Data for ~cmp: K -> K -> Cmp for ~refl: @x: K -> {cmp(x, x) == EQ{} : Cmp} for ~eq: @x: K -> @y: K -> {cmp(x, y) == EQ{} : Cmp} -> {x == y : K} for ~flip: @x: K -> @y: K -> {cmp(y, x) == flip(cmp(x, y)) : Cmp} for ~trans: @x: K -> @y: K -> @z: K -> {cmp(x, y) == LT{} : Cmp} -> {cmp(y, z) == LT{} : Cmp} -> {cmp(x, z) == LT{} : Cmp} for m: O.OMap for tree: {searchtree(~K, ~V, ~cmp, m) == True{} : Bool} for +k: K … LAWS.omap_get_put_other_key (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=omap_get_put_other_key) law omap_get_put_other_key: for ~K: Data for ~V: Data for ~cmp: K -> K -> Cmp for ~refl: @x: K -> {cmp(x, x) == EQ{} : Cmp} for ~eq: @x: K -> @y: K -> {cmp(x, y) == EQ{} : Cmp} -> {x == y : K} for ~flip: @x: K -> @y: K -> {cmp(y, x) == flip(cmp(x, y)) : Cmp} for ~trans: @x: K -> @y: K -> @z: K -> {cmp(x, y) == LT{} : Cmp} -> {cmp(y, z) == LT{} : Cmp} -> {cmp(x, z) == LT{} : Cmp} for m: O.OMap for tree: {searchtree(~K, ~V, ~cmp, m) == True{} : Bool} for +k2: K … LAWS.order_string_refl (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=order_string_refl) # Order.string is a total order with EQ meaning equal strings: it meets the # refl, eq, flip and trans facts that the OMap laws above take. It answers for # every pair, so it is total; flip makes it antisymmetric. law order_string_refl: for x: String {Order.string(x, x) == EQ{} : Cmp} LAWS.order_string_eq (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=order_string_eq) law order_string_eq: for x: String for y: String for e: {Order.string(x, y) == EQ{} : Cmp} {x == y : String} LAWS.order_string_flip (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=order_string_flip) law order_string_flip: for x: String for y: String {Order.string(y, x) == flip(Order.string(x, y)) : Cmp} LAWS.order_string_trans (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=order_string_trans) law order_string_trans: for x: String for y: String for z: String for e1: {Order.string(x, y) == LT{} : Cmp} for e2: {Order.string(y, z) == LT{} : Cmp} {Order.string(x, z) == LT{} : Cmp} LAWS.order_string_fixtures (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=order_string_fixtures) # Lower code points first, and a prefix before its extensions. law order_string_fixtures: {[Order.string("a", "b"), Order.string("ab", "a"), Order.string("", "a"), Order.string("é", "z")] == [LT{}, GT{}, LT{}, GT{}] : List<&2, Cmp>} LAWS.omap_weight (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=omap_weight) # Ghost weight from tree shape: weight = stored size + 1, so OTip has weight 1 and # OBin{lo, hi} has weight w(lo) + w(hi). Balance is Hirai-Yamamoto (delta 3, gamma 2). def omap_weight(-K: Data, -V: Data, m: O.OMap) -> Nat: LAWS.weight_ok (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=weight_ok) def weight_ok(+wl: Nat, +wh: Nat) -> Bool: LAWS.weight_balanced (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=weight_balanced) def weight_balanced(-K: Data, -V: Data, m: O.OMap) -> Bool: LAWS.g_heavy_hi (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=g_heavy_hi) # The ghost map below has the shape of OMap: it builds nodes with the same # OMap.bin and rotations, but it compares Nat weights where OMap compares U32 # sizes. While 3 * (size + 1) stays below 2^32, the U32 tests give the same # answers, so g_put and g_del give the same tree as put and del. The checker # cannot see into U32, so that link is an assumption, checked on fixtures below. def g_heavy_hi(-K: Data, -V: Data, +lo: O.OMap, +hi: O.OMap) -> Bool: LAWS.g_heavy_lo (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=g_heavy_lo) def g_heavy_lo(-K: Data, -V: Data, +lo: O.OMap, +hi: O.OMap) -> Bool: LAWS.g_rot_lo (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=g_rot_lo) def g_rot_lo(-K: Data, -V: Data, k: K, v: V, lo: O.OMap, hi: O.OMap) -> O.OMap: LAWS.g_rot_hi (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=g_rot_hi) def g_rot_hi(-K: Data, -V: Data, k: K, v: V, lo: O.OMap, hi: O.OMap) -> O.OMap: LAWS.g_balance.if (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=g_balance.if) def g_balance.if( -K: Data, -V: Data, heavy_hi: Bool, heavy_lo: Bool, k: K, v: V, lo: O.OMap, hi: O.OMap ) -> O.OMap: LAWS.g_balance (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=g_balance) def g_balance(-K: Data, -V: Data, k: K, v: V, +lo: O.OMap, +hi: O.OMap) -> O.OMap: LAWS.g_put (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=g_put) def g_put( ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: O.OMap, +k: K, +v: V ) -> O.OMap: LAWS.g_pop_min.fin (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=g_pop_min.fin) def g_pop_min.fin( -K: Data, -V: Data, k: K, v: V, hi: O.OMap, r: K & V & O.OMap ) -> K & V & O.OMap: LAWS.g_pop_min (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=g_pop_min) def g_pop_min( -K: Data, -V: Data, lo: O.OMap, k: K, v: V, hi: O.OMap ) -> K & V & O.OMap: LAWS.g_glue.fin (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=g_glue.fin) def g_glue.fin(-K: Data, -V: Data, lo: O.OMap, r: K & V & O.OMap) -> O.OMap: LAWS.g_glue (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=g_glue) def g_glue(-K: Data, -V: Data, lo: O.OMap, hi: O.OMap) -> O.OMap: LAWS.g_del (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=g_del) def g_del( ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, m: O.OMap, +k: K ) -> O.OMap: LAWS.omap_new_weight_balanced (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=omap_new_weight_balanced) law omap_new_weight_balanced: for ~K: Data for ~V: Data {weight_balanced(K, V, O.OMap.new(K, V)) == True{} : Bool} LAWS.omap_g_put_matches (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=omap_g_put_matches) law omap_g_put_matches: {g_put(~U32, ~U32, ~U32.cmp, m7(), 8, 80) == O.OMap.put(~U32, ~U32, ~U32.cmp, m7(), 8, 80) : O.OMap} LAWS.omap_g_del_matches (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=omap_g_del_matches) law omap_g_del_matches: {g_del(~U32, ~U32, ~U32.cmp, m7(), 4) == O.OMap.del(~U32, ~U32, ~U32.cmp, m7(), 4) : O.OMap} LAWS.omap_put_weight_balanced (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=omap_put_weight_balanced) law omap_put_weight_balanced: for ~K: Data for ~V: Data for ~cmp: K -> K -> Cmp for +m: O.OMap for wb: {weight_balanced(K, V, m) == True{} : Bool} for +k: K for +v: V {weight_balanced(K, V, g_put(~K, ~V, ~cmp, m, k, v)) == True{} : Bool} LAWS.omap_del_weight_balanced (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=omap_del_weight_balanced) law omap_del_weight_balanced: for ~K: Data for ~V: Data for ~cmp: K -> K -> Cmp for +m: O.OMap for wb: {weight_balanced(K, V, m) == True{} : Bool} for +k: K {weight_balanced(K, V, g_del(~K, ~V, ~cmp, m, k)) == True{} : Bool} LAWS.vec_from_list (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=vec_from_list) law vec_from_list: {V.Vec.to_list(~U32, V.Vec.from_list(~U32, [1, 2, 3, 4, 5])) == [1, 2, 3, 4, 5] : List<&2, U32>} LAWS.vec_get (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=vec_get) law vec_get: {Pair.snd(V.Vec, Maybe<&2, U32>, V.Vec.get(~U32, V.Vec.from_list(~U32, [1, 2, 3]), 2)) == Some{3} : Maybe<&2, U32>} LAWS.vec_get_past_len (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=vec_get_past_len) law vec_get_past_len: {Pair.snd(V.Vec, Maybe<&2, U32>, V.Vec.get(~U32, V.Vec.from_list(~U32, [1, 2, 3]), 3)) == None{} : Maybe<&2, U32>} LAWS.vec_set (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=vec_set) law vec_set: {V.Vec.to_list(~U32, V.Vec.set(~U32, V.Vec.from_list(~U32, [1, 2, 3]), 1, 9)) == [1, 9, 3] : List<&2, U32>} LAWS.vec_pop (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=vec_pop) law vec_pop: {Pair.snd(V.Vec, Maybe<&2, U32>, V.Vec.pop(~U32, V.Vec.from_list(~U32, [1, 2, 3]))) == Some{3} : Maybe<&2, U32>} LAWS.vec_pop_empty (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=vec_pop_empty) law vec_pop_empty: {Pair.snd(V.Vec, Maybe<&2, U32>, V.Vec.pop(~U32, V.Vec.new(~U32))) == None{} : Maybe<&2, U32>} LAWS.vec_pop_to_list (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=vec_pop_to_list) law vec_pop_to_list: {V.Vec.to_list(~U32, Pair.fst(V.Vec, Maybe<&2, U32>, V.Vec.pop(~U32, V.Vec.from_list(~U32, [1, 2, 3])))) == [1, 2] : List<&2, U32>} LAWS.deque_ends (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=deque_ends) law deque_ends: {D.Deque.to_list(&2, U32, D.Deque.push_front(&2, U32, 0, D.Deque.push_back(&2, U32, 2, D.Deque.push_back(&2, U32, 1, D.Deque.new(&2, U32))))) == [0, 1, 2] : List<&2, U32>} LAWS.heap_sort (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=heap_sort) law heap_sort: {H.Heap.sort(~U32, ~U32.is_le, [3, 1, 4, 1, 5]) == [1, 1, 3, 4, 5] : List<&2, U32>} LAWS.hkey (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=hkey) def hkey(k: U32) -> U32: LAWS.hm (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=hm) def hm() -> M.HMap: LAWS.hmap_get_put (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=hmap_get_put) law hmap_get_put: {M.HMap.get(~U32, ~U32, ~hkey, ~U32.is_eq, M.HMap.put(~U32, ~U32, ~hkey, ~U32.is_eq, hm(), 4, 40), 4) == Some{40} : Maybe<&2, U32>} LAWS.hmap_get_put_other (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=hmap_get_put_other) law hmap_get_put_other: {M.HMap.get(~U32, ~U32, ~hkey, ~U32.is_eq, M.HMap.put(~U32, ~U32, ~hkey, ~U32.is_eq, hm(), 4, 40), 3) == M.HMap.get(~U32, ~U32, ~hkey, ~U32.is_eq, hm(), 3) : Maybe<&2, U32>} LAWS.hmap_collision (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=hmap_collision) law hmap_collision: {M.HMap.get(~U32, ~U32, ~hkey, ~U32.is_eq, M.HMap.put(~U32, ~U32, ~hkey, ~U32.is_eq, hm(), 4, 40), 2) == Some{20} : Maybe<&2, U32>} LAWS.hmap_replace_collision (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=hmap_replace_collision) law hmap_replace_collision: {M.HMap.get(~U32, ~U32, ~hkey, ~U32.is_eq, M.HMap.put(~U32, ~U32, ~hkey, ~U32.is_eq, hm(), 2, 22), 2) == Some{22} : Maybe<&2, U32>} LAWS.full (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=full) def full(k: U32) -> U32: LAWS.hmap_high_bit (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=hmap_high_bit) law hmap_high_bit: {M.HMap.get(~U32, ~U32, ~full, ~U32.is_eq, M.HMap.put(~U32, ~U32, ~full, ~U32.is_eq, M.HMap.put(~U32, ~U32, ~full, ~U32.is_eq, M.HMap.new(U32, U32), 0, 10), 2147483648, 20), 0) == Some{10} : Maybe<&2, U32>} LAWS.hmap_missing_collision (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=hmap_missing_collision) law hmap_missing_collision: {M.HMap.get(~U32, ~U32, ~hkey, ~U32.is_eq, hm(), 4) == None{} : Maybe<&2, U32>} LAWS.hmap_absent (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=hmap_absent) # No entry of xs has a key equal to k. def hmap_absent( ~K: Data, ~V: Data, ~eq: K -> K -> Bool, xs: List<&2, M.Entry>, +k: K ) -> Bool: LAWS.hmap_distinct (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=hmap_distinct) # No two entries of xs have equal keys. def hmap_distinct(~K: Data, ~V: Data, ~eq: K -> K -> Bool, xs: List<&2, M.Entry>) -> Bool: LAWS.hmap_hashed (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=hmap_hashed) # Every key of xs hashes to h. def hmap_hashed( ~K: Data, ~V: Data, ~hash: K -> U32, xs: List<&2, M.Entry>, +h: U32 ) -> Bool: LAWS.hmap_wf.go (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=hmap_wf.go) # A trie with n levels left: buckets hold distinct keys; above the last level, # a bucket's keys hash to its hash; the last level has no branches. def hmap_wf.go( ~K: Data, ~V: Data, ~hash: K -> U32, ~eq: K -> K -> Bool, +n: Nat, m: M.HMap ) -> Bool: LAWS.hmap_wf (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=hmap_wf) def hmap_wf(~K: Data, ~V: Data, ~hash: K -> U32, ~eq: K -> K -> Bool, m: M.HMap) -> Bool: LAWS.hmap_new_wf (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=hmap_new_wf) law hmap_new_wf: for ~K: Data for ~V: Data for ~hash: K -> U32 for ~eq: K -> K -> Bool {hmap_wf(~K, ~V, ~hash, ~eq, M.HMap.new(K, V)) == True{} : Bool} LAWS.hmap_put_wf (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=hmap_put_wf) law hmap_put_wf: for ~K: Data for ~V: Data for ~hash: K -> U32 for ~eq: K -> K -> Bool for ~refl: @x: K -> {eq(x, x) == True{} : Bool} for ~sound: @x: K -> @y: K -> {eq(x, y) == True{} : Bool} -> {x == y : K} for m: M.HMap for wf: {hmap_wf(~K, ~V, ~hash, ~eq, m) == True{} : Bool} for +k: K for +v: V {hmap_wf(~K, ~V, ~hash, ~eq, M.HMap.put(~K, ~V, ~hash, ~eq, m, k, v)) == True{} : Bool} LAWS.hmap_del_wf (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=hmap_del_wf) law hmap_del_wf: for ~K: Data for ~V: Data for ~hash: K -> U32 for ~eq: K -> K -> Bool for m: M.HMap for wf: {hmap_wf(~K, ~V, ~hash, ~eq, m) == True{} : Bool} for +k: K {hmap_wf(~K, ~V, ~hash, ~eq, M.HMap.del(~K, ~V, ~hash, ~eq, m, k)) == True{} : Bool} LAWS.hmap_get_put_same (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=hmap_get_put_same) law hmap_get_put_same: for ~K: Data for ~V: Data for ~hash: K -> U32 for ~eq: K -> K -> Bool for ~refl: @x: K -> {eq(x, x) == True{} : Bool} for m: M.HMap for wf: {hmap_wf(~K, ~V, ~hash, ~eq, m) == True{} : Bool} for +k: K for +v: V {M.HMap.get(~K, ~V, ~hash, ~eq, M.HMap.put(~K, ~V, ~hash, ~eq, m, k, v), k) == Some{v} : Maybe<&2, V>} LAWS.hmap_get_put_other_key (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=hmap_get_put_other_key) law hmap_get_put_other_key: for ~K: Data for ~V: Data for ~hash: K -> U32 for ~eq: K -> K -> Bool for ~sound: @x: K -> @y: K -> {eq(x, y) == True{} : Bool} -> {x == y : K} for m: M.HMap for wf: {hmap_wf(~K, ~V, ~hash, ~eq, m) == True{} : Bool} for +k2: K for +k: K for ne: {k2 != k : K} … LAWS.hmap_get_del_same (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=hmap_get_del_same) law hmap_get_del_same: for ~K: Data for ~V: Data for ~hash: K -> U32 for ~eq: K -> K -> Bool for ~sound: @x: K -> @y: K -> {eq(x, y) == True{} : Bool} -> {x == y : K} for m: M.HMap for wf: {hmap_wf(~K, ~V, ~hash, ~eq, m) == True{} : Bool} for +k: K {M.HMap.get(~K, ~V, ~hash, ~eq, M.HMap.del(~K, ~V, ~hash, ~eq, m, k), k) == None{} : Maybe<&2, V>} LAWS.hmap_get_del_other_key (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=hmap_get_del_other_key) law hmap_get_del_other_key: for ~K: Data for ~V: Data for ~hash: K -> U32 for ~eq: K -> K -> Bool for ~sound: @x: K -> @y: K -> {eq(x, y) == True{} : Bool} -> {x == y : K} for m: M.HMap for +k2: K for +k: K for ne: {k2 != k : K} {M.HMap.get(~K, ~V, ~hash, ~eq, M.HMap.del(~K, ~V, ~hash, ~eq, m, k2), k) == M.HMap.get(~K, ~V, ~hash, ~eq, m, k) : Maybe<&2, V>} LAWS.hmap_size_put_new (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=hmap_size_put_new) law hmap_size_put_new: for ~K: Data for ~V: Data for ~hash: K -> U32 for ~eq: K -> K -> Bool for ~sound: @x: K -> @y: K -> {eq(x, y) == True{} : Bool} -> {x == y : K} for m: M.HMap for wf: {hmap_wf(~K, ~V, ~hash, ~eq, m) == True{} : Bool} for +k: K for +v: V for miss: {M.HMap.get(~K, ~V, ~hash, ~eq, m, k) == None{} : Maybe<&2, V>} … LAWS.hmap_size_put_replace (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=hmap_size_put_replace) law hmap_size_put_replace: for ~K: Data for ~V: Data for ~hash: K -> U32 for ~eq: K -> K -> Bool for m: M.HMap for +k: K for +v: V for -w: V for hit: {M.HMap.get(~K, ~V, ~hash, ~eq, m, k) == Some{w} : Maybe<&2, V>} {M.HMap.size(K, V, M.HMap.put(~K, ~V, ~hash, ~eq, m, k, v)) == M.HMap.size(K, V, m) : Nat} LAWS.hmap_size_del (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=hmap_size_del) law hmap_size_del: for ~K: Data for ~V: Data for ~hash: K -> U32 for ~eq: K -> K -> Bool for m: M.HMap for +k: K for -w: V for hit: {M.HMap.get(~K, ~V, ~hash, ~eq, m, k) == Some{w} : Maybe<&2, V>} {1n+M.HMap.size(K, V, M.HMap.del(~K, ~V, ~hash, ~eq, m, k)) == M.HMap.size(K, V, m) : Nat} LAWS.hmap_size_del_missing (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=hmap_size_del_missing) law hmap_size_del_missing: for ~K: Data for ~V: Data for ~hash: K -> U32 for ~eq: K -> K -> Bool for m: M.HMap for +k: K for miss: {M.HMap.get(~K, ~V, ~hash, ~eq, m, k) == None{} : Maybe<&2, V>} {M.HMap.size(K, V, M.HMap.del(~K, ~V, ~hash, ~eq, m, k)) == M.HMap.size(K, V, m) : Nat} LAWS.hmap_collision_get (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=hmap_collision_get) # Two distinct keys with one hash share a bucket; both stay reachable. law hmap_collision_get: for ~K: Data for ~V: Data for ~hash: K -> U32 for ~eq: K -> K -> Bool for ~refl: @x: K -> {eq(x, x) == True{} : Bool} for ~sound: @x: K -> @y: K -> {eq(x, y) == True{} : Bool} -> {x == y : K} for +m: M.HMap for +wf: {hmap_wf(~K, ~V, ~hash, ~eq, m) == True{} : Bool} for +k1: K … LAWS.hmap_collision_size (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=hmap_collision_size) law hmap_collision_size: for ~K: Data for ~V: Data for ~hash: K -> U32 for ~eq: K -> K -> Bool for ~refl: @x: K -> {eq(x, x) == True{} : Bool} for ~sound: @x: K -> @y: K -> {eq(x, y) == True{} : Bool} -> {x == y : K} for +m: M.HMap for +wf: {hmap_wf(~K, ~V, ~hash, ~eq, m) == True{} : Bool} for +k1: K for +k2: K … PROOF.c4.a (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=c4.a) def c4.a( +a: Bool, +b: Bool, +c: Bool, +d: Bool, e: {Bool.and(Bool.and(Bool.and(a, b), c), d) == True{} : Bool} ) -> {a == True{} : Bool}: PROOF.c4.b (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=c4.b) def c4.b( +a: Bool, +b: Bool, +c: Bool, +d: Bool, e: {Bool.and(Bool.and(Bool.and(a, b), c), d) == True{} : Bool} ) -> {b == True{} : Bool}: PROOF.c4.c (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=c4.c) def c4.c( +a: Bool, +b: Bool, +c: Bool, +d: Bool, e: {Bool.and(Bool.and(Bool.and(a, b), c), d) == True{} : Bool} ) -> {c == True{} : Bool}: PROOF.c4.d (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=c4.d) def c4.d( +a: Bool, +b: Bool, +c: Bool, +d: Bool, e: {Bool.and(Bool.and(Bool.and(a, b), c), d) == True{} : Bool} ) -> {d == True{} : Bool}: PROOF.c4.i (https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=c4.i) def c4.i( +a: Bool, +b: Bool, +c: Bool, +d: Bool, ea: {a == True{} : Bool}, eb: {b == True{} : Bool}, ec: {c == True{} : Bool}, ed: {d == True{} : Bool} ) -> {Bool.and(Bool.and(Bool.and(a, b), c), d) == True{} : Bool}: More: https://jend.leeeet.dev/packages/bend-kit-collections.txt?definitions_offset=100