1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/nat.bend as N 4 import ../../lib/list.bend as LL 5 import ../../../spec/lib/common.bend as SC 6 import ../../../src/containers/bitset.bend as B 7 import ../../../src/containers/bitlist.bend as BLI 8 import ../../../src/containers/dynamic_array.bend as D 9 import ../../../src/containers/types/dynamic_array.bend as DE 10 import ../../../spec/containers/dynamic_array.bend as DS 11 import ../dynamic_array/state.bend as DAS 12 import ../dynamic_array/steps.bend as DSP 13 import ../dynamic_array/trace.bend as DTR 14 import ../bitset/listx.bend as LX 15 import ../bitset/model.bend as MD 16 import ../bitset/walk.bend as WK 17 import ../bitset/state.bend as ST 18 import ../bitset/fastcount.bend as FC 19 import ./da.bend as DI 20 import ./bits.bend as BT 21 22 # The two whole-array walks of src/containers/bitlist.bend: count sums the 23 # populations of the words upward, to_list emits the first n bits from the 24 # last word down. Each word read goes through the dynamic array's contract, 25 # which hands back a new good shadow with the same words, so the loop 26 # invariant carries "a good shadow whose words are xs". 27 # (source: proofs/containers/bitlist/loops.src) 28 29 30 # a read of word q: the new shadow keeps the words; the value is word q 31 def read_same(+s: DAS.Shadow, +gs: {DAS.good(U32, s) == True{} : Bool}, +xs: List<&2, U32>, +c: Nat, +es: {DI.ws(s) == xs : List<&2, U32>}, +ec: {DI.lim(s) == c : Nat}, +q: Nat) -> {DAS.good(U32, DI.gsh(s, gs, q)) == True{} : Bool} & ({DI.ws(DI.gsh(s, gs, q)) == xs : List<&2, U32>} & {DI.lim(DI.gsh(s, gs, q)) == c : Nat}): 32 (DI.get_good(s, gs, q), (Equal.trans(List<&2, U32>, DI.ws(DI.gsh(s, gs, q)), DI.ws(s), xs, DI.get_ws(s, gs, q), es), Equal.trans(Nat, DI.lim(DI.gsh(s, gs, q)), DI.lim(s), c, DI.get_lim(s, gs, q), ec))) 33 34 35 def read_eq(+s: DAS.Shadow, +gs: {DAS.good(U32, s) == True{} : Bool}, +xs: List<&2, U32>, +c: Nat, +es: {DI.ws(s) == xs : List<&2, U32>}, +ec: {DI.lim(s) == c : Nat}, +q: Nat) -> {D.get(U32, DAS.real(U32, s), q) == (DAS.real(U32, DI.gsh(s, gs, q)), DS.item_result(U32, SC.nth(U32, xs, q))) : D.DynArray<&2, U32> & Result<&2, &2, DE.Error, U32>}: 36 %Equal.sym(D.DynArray<&2, U32> & Result<&2, &2, DE.Error, U32>, D.get(U32, DAS.real(U32, s), q), (DAS.real(U32, DI.gsh(s, gs, q)), DI.unitem(DTR.so_obs(U32, s, DE.Get{q}, DSP.step_ok(U32, s, DE.Get{q}, gs)))), DI.get_eq(s, gs, q)) : {_ == (DAS.real(U32, DI.gsh(s, gs, q)), DS.item_result(U32, SC.nth(U32, xs, q))) : D.DynArray<&2, U32> & Result<&2, &2, DE.Error, U32>} 37 %Equal.sym(Result<&2, &2, DE.Error, U32>, DI.unitem(DTR.so_obs(U32, s, DE.Get{q}, DSP.step_ok(U32, s, DE.Get{q}, gs))), DS.item_result(U32, SC.nth(U32, DI.ws(s), q)), DI.get_val(s, gs, q)) : {(DAS.real(U32, DI.gsh(s, gs, q)), _) == (DAS.real(U32, DI.gsh(s, gs, q)), DS.item_result(U32, SC.nth(U32, xs, q))) : D.DynArray<&2, U32> & Result<&2, &2, DE.Error, U32>} 38 %Equal.sym(List<&2, U32>, DI.ws(s), xs, es) : {(DAS.real(U32, DI.gsh(s, gs, q)), DS.item_result(U32, SC.nth(U32, _, q))) == (DAS.real(U32, DI.gsh(s, gs, q)), DS.item_result(U32, SC.nth(U32, xs, q))) : D.DynArray<&2, U32> & Result<&2, &2, DE.Error, U32>} 39 {==} 40 41 # ---- count ---- 42 43 44 def CountOK(k: Nat, s: DAS.Shadow, acc: Nat, q: Nat, xs: List<&2, U32>, c: Nat) -> Type: 45 Sigma<&1, &1, DAS.Shadow, s_2 => {BLI.count_go(k, (DAS.real(U32, s), acc), q) == (DAS.real(U32, s_2), Nat.add(acc, MD.count_words(SC.take(U32, SC.drop(U32, xs, q), k)))) : D.DynArray<&2, U32> & Nat} & {DAS.good(U32, s_2) == True{} : Bool} & ({DI.ws(s_2) == xs : List<&2, U32>} & {DI.lim(s_2) == c : Nat})> 46 47 def drop_none(-A: Data, +xs: List<&2, A>, +q: Nat, +h: {SC.nth(A, xs, q) == None{} : Maybe<&2, A>}) -> {SC.drop(A, xs, q) == Nil{} : List<&2, A>}: 48 match xs q: 49 case Nil{} 0n: 50 {==} 51 case Nil{} 1n+p: 52 {==} 53 case Con{x, t} 0n: 54 Empty.absurd({SC.drop(A, Con{x, t}, 0n) == Nil{} : List<&2, A>}, L.none_some(A, x, Equal.sym(Maybe<&2, A>, Some{x}, None{}, h))) 55 case Con{+x, +t} 1n+ +p: 56 drop_none(A, t, p, h) 57 58 def nth_none_succ(-A: Data, +xs: List<&2, A>, +q: Nat, +h: {SC.nth(A, xs, q) == None{} : Maybe<&2, A>}) -> {SC.nth(A, xs, 1n+q) == None{} : Maybe<&2, A>}: 59 match xs q: 60 case Nil{} 0n: 61 {==} 62 case Nil{} 1n+p: 63 {==} 64 case Con{x, t} 0n: 65 Empty.absurd({SC.nth(A, Con{x, t}, 1n) == None{} : Maybe<&2, A>}, L.none_some(A, x, Equal.sym(Maybe<&2, A>, Some{x}, None{}, h))) 66 case Con{+x, +t} 1n+ +p: 67 nth_none_succ(A, t, p, h) 68 69 def cw_none(+xs: List<&2, U32>, +k: Nat, +q: Nat, +h: {SC.nth(U32, xs, q) == None{} : Maybe<&2, U32>}) -> {MD.count_words(SC.take(U32, SC.drop(U32, xs, q), 1n+k)) == MD.count_words(SC.take(U32, SC.drop(U32, xs, 1n+q), k)) : Nat}: 70 %Equal.sym(List<&2, U32>, SC.drop(U32, xs, q), Nil{}, drop_none(U32, xs, q, h)) : {MD.count_words(SC.take(U32, _, 1n+k)) == MD.count_words(SC.take(U32, SC.drop(U32, xs, 1n+q), k)) : Nat} 71 %Equal.sym(List<&2, U32>, SC.drop(U32, xs, 1n+q), Nil{}, drop_none(U32, xs, 1n+q, nth_none_succ(U32, xs, q, h))) : {MD.count_words(SC.take(U32, Nil{}, 1n+k)) == MD.count_words(SC.take(U32, _, k)) : Nat} 72 {==} 73 74 def cw_some(+xs: List<&2, U32>, +k: Nat, +q: Nat, +x: U32, +h: {SC.nth(U32, xs, q) == Some{x} : Maybe<&2, U32>}) -> {MD.count_words(SC.take(U32, SC.drop(U32, xs, q), 1n+k)) == Nat.add(B.word_count(32n, x), MD.count_words(SC.take(U32, SC.drop(U32, xs, 1n+q), k))) : Nat}: 75 %Equal.sym(List<&2, U32>, SC.drop(U32, xs, q), Con{x, SC.drop(U32, xs, 1n+q)}, LX.drop_cons(U32, xs, q, x, h)) : {MD.count_words(SC.take(U32, _, 1n+k)) == Nat.add(B.word_count(32n, x), MD.count_words(SC.take(U32, SC.drop(U32, xs, 1n+q), k))) : Nat} 76 {==} 77 78 79 def count_lift(+r: Nat, s: DAS.Shadow, +acc: Nat, +q: Nat, +xs: List<&2, U32>, +c: Nat, s1: DAS.Shadow, +acc1: Nat, +e_step: {BLI.count_go(1n+r, (DAS.real(U32, s), acc), q) == BLI.count_go(r, (DAS.real(U32, s1), acc1), 1n+q) : D.DynArray<&2, U32> & Nat}, +e_sum: {Nat.add(acc1, MD.count_words(SC.take(U32, SC.drop(U32, xs, 1n+q), r))) == Nat.add(acc, MD.count_words(SC.take(U32, SC.drop(U32, xs, q), 1n+r))) : Nat}, ih: CountOK(r, s1, acc1, 1n+q, xs, c)) -> CountOK(1n+r, s, acc, q, xs, c): 80 match ih: 81 case Tuple{s2, Tuple{e2, same}}: 82 (s2, (Equal.trans(D.DynArray<&2, U32> & Nat, BLI.count_go(1n+r, (DAS.real(U32, s), acc), q), BLI.count_go(r, (DAS.real(U32, s1), acc1), 1n+q), (DAS.real(U32, s2), Nat.add(acc, MD.count_words(SC.take(U32, SC.drop(U32, xs, q), 1n+r)))), e_step, 83 Equal.trans(D.DynArray<&2, U32> & Nat, BLI.count_go(r, (DAS.real(U32, s1), acc1), 1n+q), (DAS.real(U32, s2), Nat.add(acc1, MD.count_words(SC.take(U32, SC.drop(U32, xs, 1n+q), r)))), (DAS.real(U32, s2), Nat.add(acc, MD.count_words(SC.take(U32, SC.drop(U32, xs, q), 1n+r)))), e2, 84 Equal.cong(Nat, D.DynArray<&2, U32> & Nat, z => (DAS.real(U32, s2), z), Nat.add(acc1, MD.count_words(SC.take(U32, SC.drop(U32, xs, 1n+q), r))), Nat.add(acc, MD.count_words(SC.take(U32, SC.drop(U32, xs, q), 1n+r))), e_sum))), same)) 85 86 87 def count_rd(+r: Nat, +s: DAS.Shadow, +gs: {DAS.good(U32, s) == True{} : Bool}, +xs: List<&2, U32>, +c: Nat, +es: {DI.ws(s) == xs : List<&2, U32>}, +ec: {DI.lim(s) == c : Nat}, +acc: Nat, +q: Nat, +y: Maybe<&2, U32>, +hy: {SC.nth(U32, xs, q) == y : Maybe<&2, U32>}) -> {BLI.count_go(1n+r, (DAS.real(U32, s), acc), q) == BLI.count_go(r, BLI.count_add((DAS.real(U32, DI.gsh(s, gs, q)), DS.item_result(U32, y)), acc), 1n+q) : D.DynArray<&2, U32> & Nat}: 88 %Equal.sym(D.DynArray<&2, U32> & Result<&2, &2, DE.Error, U32>, D.get(U32, DAS.real(U32, s), q), (DAS.real(U32, DI.gsh(s, gs, q)), DS.item_result(U32, SC.nth(U32, xs, q))), read_eq(s, gs, xs, c, es, ec, q)) : {BLI.count_go(r, BLI.count_add(_, acc), 1n+q) == BLI.count_go(r, BLI.count_add((DAS.real(U32, DI.gsh(s, gs, q)), DS.item_result(U32, y)), acc), 1n+q) : D.DynArray<&2, U32> & Nat} 89 %Equal.sym(Maybe<&2, U32>, SC.nth(U32, xs, q), y, hy) : {BLI.count_go(r, BLI.count_add((DAS.real(U32, DI.gsh(s, gs, q)), DS.item_result(U32, _)), acc), 1n+q) == BLI.count_go(r, BLI.count_add((DAS.real(U32, DI.gsh(s, gs, q)), DS.item_result(U32, y)), acc), 1n+q) : D.DynArray<&2, U32> & Nat} 90 {==} 91 92 93 94 def count_sum(+acc: Nat, +r: Nat, +q: Nat, +xs: List<&2, U32>, +x: U32, +hy: {SC.nth(U32, xs, q) == Some{x} : Maybe<&2, U32>}) -> {Nat.add(B.count_word(x, acc, U32.is_eq(x, 0)), MD.count_words(SC.take(U32, SC.drop(U32, xs, 1n+q), r))) == Nat.add(acc, MD.count_words(SC.take(U32, SC.drop(U32, xs, q), 1n+r))) : Nat}: 95 %Equal.sym(Nat, B.count_word(x, acc, U32.is_eq(x, 0)), Nat.add(acc, B.word_count(32n, x)), FC.count_word_ok(x, acc, U32.is_eq(x, 0), {==})) : {Nat.add(_, MD.count_words(SC.take(U32, SC.drop(U32, xs, 1n+q), r))) == Nat.add(acc, MD.count_words(SC.take(U32, SC.drop(U32, xs, q), 1n+r))) : Nat} 96 %Equal.sym(Nat, MD.count_words(SC.take(U32, SC.drop(U32, xs, q), 1n+r)), Nat.add(B.word_count(32n, x), MD.count_words(SC.take(U32, SC.drop(U32, xs, 1n+q), r))), cw_some(xs, r, q, x, hy)) : {Nat.add(Nat.add(acc, B.word_count(32n, x)), MD.count_words(SC.take(U32, SC.drop(U32, xs, 1n+q), r))) == Nat.add(acc, _) : Nat} 97 N.add_assoc(acc, B.word_count(32n, x), MD.count_words(SC.take(U32, SC.drop(U32, xs, 1n+q), r))) 98 99 def count_y(+r: Nat, +s: DAS.Shadow, +gs: {DAS.good(U32, s) == True{} : Bool}, +xs: List<&2, U32>, +c: Nat, +es: {DI.ws(s) == xs : List<&2, U32>}, +ec: {DI.lim(s) == c : Nat}, +acc: Nat, +q: Nat, +y: Maybe<&2, U32>, +hy: {SC.nth(U32, xs, q) == y : Maybe<&2, U32>}, +e_rd: {BLI.count_go(1n+r, (DAS.real(U32, s), acc), q) == BLI.count_go(r, BLI.count_add((DAS.real(U32, DI.gsh(s, gs, q)), DS.item_result(U32, y)), acc), 1n+q) : D.DynArray<&2, U32> & Nat}, rec: @+a2: Nat -> @+q2: Nat -> @+s2: DAS.Shadow -> @+g2: {DAS.good(U32, s2) == True{} : Bool} -> @+e2: {DI.ws(s2) == xs : List<&2, U32>} -> @+f2: {DI.lim(s2) == c : Nat} -> CountOK(r, s2, a2, q2, xs, c)) -> CountOK(1n+r, s, acc, q, xs, c): 100 match y: 101 case None{}: 102 +gs1 = DI.get_good(s, gs, q) 103 +es1 = Equal.trans(List<&2, U32>, DI.ws(DI.gsh(s, gs, q)), DI.ws(s), xs, DI.get_ws(s, gs, q), es) 104 +ec1 = Equal.trans(Nat, DI.lim(DI.gsh(s, gs, q)), DI.lim(s), c, DI.get_lim(s, gs, q), ec) 105 +e_sum = Equal.cong(Nat, Nat, z => Nat.add(acc, z), MD.count_words(SC.take(U32, SC.drop(U32, xs, 1n+q), r)), MD.count_words(SC.take(U32, SC.drop(U32, xs, q), 1n+r)), Equal.sym(Nat, MD.count_words(SC.take(U32, SC.drop(U32, xs, q), 1n+r)), MD.count_words(SC.take(U32, SC.drop(U32, xs, 1n+q), r)), cw_none(xs, r, q, hy))) 106 count_lift(r, s, acc, q, xs, c, DI.gsh(s, gs, q), acc, e_rd, e_sum, rec(acc, 1n+q, DI.gsh(s, gs, q), gs1, es1, ec1)) 107 case Some{+x}: 108 +gs1 = DI.get_good(s, gs, q) 109 +es1 = Equal.trans(List<&2, U32>, DI.ws(DI.gsh(s, gs, q)), DI.ws(s), xs, DI.get_ws(s, gs, q), es) 110 +ec1 = Equal.trans(Nat, DI.lim(DI.gsh(s, gs, q)), DI.lim(s), c, DI.get_lim(s, gs, q), ec) 111 count_lift(r, s, acc, q, xs, c, DI.gsh(s, gs, q), B.count_word(x, acc, U32.is_eq(x, 0)), e_rd, count_sum(acc, r, q, xs, x, hy), rec(B.count_word(x, acc, U32.is_eq(x, 0)), 1n+q, DI.gsh(s, gs, q), gs1, es1, ec1)) 112 113 def count_loop(k: Nat, +s: DAS.Shadow, +gs: {DAS.good(U32, s) == True{} : Bool}, +xs: List<&2, U32>, +c: Nat, +es: {DI.ws(s) == xs : List<&2, U32>}, +ec: {DI.lim(s) == c : Nat}, +acc: Nat, +q: Nat) -> CountOK(k, s, acc, q, xs, c): 114 match k: 115 case 0n: 116 (s, (%Equal.sym(List<&2, U32>, SC.take(U32, SC.drop(U32, xs, q), 0n), Nil{}, LX.take_zero(U32, SC.drop(U32, xs, q))) : {(DAS.real(U32, s), acc) == (DAS.real(U32, s), Nat.add(acc, MD.count_words(_))) : D.DynArray<&2, U32> & Nat} 117 %Equal.sym(Nat, Nat.add(acc, 0n), acc, N.add_zero(acc)) : {(DAS.real(U32, s), acc) == (DAS.real(U32, s), _) : D.DynArray<&2, U32> & Nat} 118 {==}, (gs, (es, ec)))) 119 case 1n+ +r: 120 count_y(r, s, gs, xs, c, es, ec, acc, q, SC.nth(U32, xs, q), {==}, count_rd(r, s, gs, xs, c, es, ec, acc, q, SC.nth(U32, xs, q), {==}), (a2 => q2 => s2 => g2 => e2 => f2 => count_loop(r, s2, g2, xs, c, e2, f2, a2, q2))) 121 122 # ---- to_list ---- 123 124 125 def BitsOK(k: Nat, s: DAS.Shadow, n: Nat, xs: List<&2, U32>, c: Nat) -> Type: 126 Sigma<&1, &1, DAS.Shadow, s_2 => {BLI.bits_go(k, (DAS.real(U32, s), SC.take(Bool, ST.flat(SC.drop(U32, xs, k)), Nat.sub(n, Nat.mul(k, 32n)))), n) == (DAS.real(U32, s_2), SC.take(Bool, ST.flat(SC.drop(U32, xs, 0n)), Nat.sub(n, Nat.mul(0n, 32n)))) : D.DynArray<&2, U32> & List<&2, Bool>} & {DAS.good(U32, s_2) == True{} : Bool} & ({DI.ws(s_2) == xs : List<&2, U32>} & {DI.lim(s_2) == c : Nat})> 127 128 def bits_lift(+q: Nat, s: DAS.Shadow, +n: Nat, +xs: List<&2, U32>, +c: Nat, s1: DAS.Shadow, +e_step: {BLI.bits_go(1n+q, (DAS.real(U32, s), SC.take(Bool, ST.flat(SC.drop(U32, xs, 1n+q)), Nat.sub(n, Nat.mul(1n+q, 32n)))), n) == BLI.bits_go(q, (DAS.real(U32, s1), SC.take(Bool, ST.flat(SC.drop(U32, xs, q)), Nat.sub(n, Nat.mul(q, 32n)))), n) : D.DynArray<&2, U32> & List<&2, Bool>}, ih: BitsOK(q, s1, n, xs, c)) -> BitsOK(1n+q, s, n, xs, c): 129 match ih: 130 case Tuple{s2, Tuple{e2, same}}: 131 (s2, (Equal.trans(D.DynArray<&2, U32> & List<&2, Bool>, BLI.bits_go(1n+q, (DAS.real(U32, s), SC.take(Bool, ST.flat(SC.drop(U32, xs, 1n+q)), Nat.sub(n, Nat.mul(1n+q, 32n)))), n), BLI.bits_go(q, (DAS.real(U32, s1), SC.take(Bool, ST.flat(SC.drop(U32, xs, q)), Nat.sub(n, Nat.mul(q, 32n)))), n), (DAS.real(U32, s2), SC.take(Bool, ST.flat(SC.drop(U32, xs, 0n)), Nat.sub(n, Nat.mul(0n, 32n)))), e_step, e2), same)) 132 133 134 def bits_rd(+s: DAS.Shadow, +gs: {DAS.good(U32, s) == True{} : Bool}, +xs: List<&2, U32>, +c: Nat, +es: {DI.ws(s) == xs : List<&2, U32>}, +ec: {DI.lim(s) == c : Nat}, +n: Nat, +q: Nat, +hq: {Nat.is_lt(q, SC.length(U32, xs)) == True{} : Bool}) -> {BLI.bits_go(1n+q, (DAS.real(U32, s), SC.take(Bool, ST.flat(SC.drop(U32, xs, 1n+q)), Nat.sub(n, Nat.mul(1n+q, 32n)))), n) == BLI.bits_go(q, (DAS.real(U32, DI.gsh(s, gs, q)), SC.take(Bool, ST.flat(SC.drop(U32, xs, q)), Nat.sub(n, Nat.mul(q, 32n)))), n) : D.DynArray<&2, U32> & List<&2, Bool>}: 135 +hx = WK.nthw_nth(xs, q, hq) 136 %Equal.sym(D.DynArray<&2, U32> & Result<&2, &2, DE.Error, U32>, D.get(U32, DAS.real(U32, s), q), (DAS.real(U32, DI.gsh(s, gs, q)), DS.item_result(U32, SC.nth(U32, xs, q))), read_eq(s, gs, xs, c, es, ec, q)) : {BLI.bits_go(q, BLI.bits_add(Nat.min(32n, Nat.sub(n, Nat.mul(q, 32n))), SC.take(Bool, ST.flat(SC.drop(U32, xs, 1n+q)), Nat.sub(n, Nat.mul(1n+q, 32n))), _), n) == BLI.bits_go(q, (DAS.real(U32, DI.gsh(s, gs, q)), SC.take(Bool, ST.flat(SC.drop(U32, xs, q)), Nat.sub(n, Nat.mul(q, 32n)))), n) : D.DynArray<&2, U32> & List<&2, Bool>} 137 %Equal.sym(Maybe<&2, U32>, SC.nth(U32, xs, q), Some{WK.nthw(xs, q)}, hx) : {BLI.bits_go(q, BLI.bits_add(Nat.min(32n, Nat.sub(n, Nat.mul(q, 32n))), SC.take(Bool, ST.flat(SC.drop(U32, xs, 1n+q)), Nat.sub(n, Nat.mul(1n+q, 32n))), (DAS.real(U32, DI.gsh(s, gs, q)), DS.item_result(U32, _))), n) == BLI.bits_go(q, (DAS.real(U32, DI.gsh(s, gs, q)), SC.take(Bool, ST.flat(SC.drop(U32, xs, q)), Nat.sub(n, Nat.mul(q, 32n)))), n) : D.DynArray<&2, U32> & List<&2, Bool>} 138 %Equal.sym(List<&2, Bool>, BLI.word_bits(Nat.min(32n, Nat.sub(n, Nat.mul(q, 32n))), WK.nthw(xs, q), SC.take(Bool, ST.flat(SC.drop(U32, xs, 1n+q)), Nat.sub(n, Nat.mul(1n+q, 32n)))), SC.take(Bool, ST.flat(SC.drop(U32, xs, q)), Nat.sub(n, Nat.mul(q, 32n))), Equal.sym(List<&2, Bool>, SC.take(Bool, ST.flat(SC.drop(U32, xs, q)), Nat.sub(n, Nat.mul(q, 32n))), BLI.word_bits(Nat.min(32n, Nat.sub(n, Nat.mul(q, 32n))), WK.nthw(xs, q), SC.take(Bool, ST.flat(SC.drop(U32, xs, 1n+q)), Nat.sub(n, Nat.mul(1n+q, 32n)))), BT.bits_step(xs, n, q, WK.nthw(xs, q), hx))) : {BLI.bits_go(q, (DAS.real(U32, DI.gsh(s, gs, q)), _), n) == BLI.bits_go(q, (DAS.real(U32, DI.gsh(s, gs, q)), SC.take(Bool, ST.flat(SC.drop(U32, xs, q)), Nat.sub(n, Nat.mul(q, 32n)))), n) : D.DynArray<&2, U32> & List<&2, Bool>} 139 {==} 140 141 def bits_loop(k: Nat, +s: DAS.Shadow, +gs: {DAS.good(U32, s) == True{} : Bool}, +xs: List<&2, U32>, +c: Nat, +es: {DI.ws(s) == xs : List<&2, U32>}, +ec: {DI.lim(s) == c : Nat}, +n: Nat, +hk: {Nat.is_le(k, SC.length(U32, xs)) == True{} : Bool}) -> BitsOK(k, s, n, xs, c): 142 match k: 143 case 0n: 144 (s, ({==}, (gs, (es, ec)))) 145 case 1n+ +q: 146 +hq = N.succ_le_lt(q, SC.length(U32, xs), hk) 147 +gs1 = DI.get_good(s, gs, q) 148 +es1 = Equal.trans(List<&2, U32>, DI.ws(DI.gsh(s, gs, q)), DI.ws(s), xs, DI.get_ws(s, gs, q), es) 149 +ec1 = Equal.trans(Nat, DI.lim(DI.gsh(s, gs, q)), DI.lim(s), c, DI.get_lim(s, gs, q), ec) 150 bits_lift(q, s, n, xs, c, DI.gsh(s, gs, q), bits_rd(s, gs, xs, c, es, ec, n, q, hq), bits_loop(q, DI.gsh(s, gs, q), gs1, xs, c, es1, ec1, n, N.lt_le(q, SC.length(U32, xs), hq)))