def bsel.go

lawful-words@0.1.0.0 · proof_bytes.bend:1025

import Base
import lawful-words@0.1.0.0/defs.bend as D
import lawful-words@0.1.0.0/proof_nat.bend as N

1025# Bit k of byte J of b << 8X, for b < 256 and k < 8: bit k of b when J = X.
1026def bsel.go(+b: U32, +x: Nat, +j: Nat, +k: Nat, +hb: {Nat.is_lt(U32.to_nat(b), Nat.pow(2n, 8n)) == True{} : Bool},
1027  +hk: {Nat.is_lt(k, 8n) == True{} : Bool}, c: Cmp, +ec: {Nat.cmp(j, x) == c : Cmp}) ->
1028  {Bool.and(Nat.is_le(Nat.mul(8n, x), Nat.add(Nat.mul(8n, j), k)), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, j), k), 32n),
1029     D.bit(b, Nat.sub(Nat.add(Nat.mul(8n, j), k), Nat.mul(8n, x)))))
1030   == Bool.and(Nat.is_eq(j, x), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, j), k), 32n), D.bit(b, k))) : Bool}:
1031  match c:
1032    case LT{}:
1033      +p = Nat.add(Nat.mul(8n, j), k)
1034      +ii = Nat.is_lt(p, 32n)
1035      +hlt = {%Equal.sym(Cmp, Nat.cmp(j, x), LT{}, ec) : {Cmp.is_lt(_) == True{} : Bool}; {==} : {Nat.is_lt(j, x) == True{} : Bool}}
1036      %Equal.sym(Bool, Nat.is_le(Nat.mul(8n, x), p), False{}, lt_not_le(p, Nat.mul(8n, x), N.lt_le_trans(p, Nat.mul(8n, 1n+j), Nat.mul(8n, x), lt_mul8(j, k, hk),
1037          N.le_mul_l(8n, 1n+j, x, %Equal.sym(Bool, Nat.is_le(1n+j, x), Nat.is_lt(j, x), N.le_succ_lt(j, x)) : {_ == True{} : Bool}; hlt)))) :
1038        {Bool.and(_, Bool.and(ii, D.bit(b, Nat.sub(p, Nat.mul(8n, x))))) == Bool.and(Nat.is_eq(j, x), Bool.and(ii, D.bit(b, k))) : Bool}
1039      %Equal.sym(Cmp, Nat.cmp(j, x), LT{}, ec) : {False{} == Bool.and(Cmp.is_eq(_), Bool.and(ii, D.bit(b, k))) : Bool}
1040      {==}
1041    case EQ{}:
1042      +hjx = N.eq_sound(j, x, %Equal.sym(Cmp, Nat.cmp(j, x), EQ{}, ec) : {Cmp.is_eq(_) == True{} : Bool}; {==})
1043      +p = Nat.add(Nat.mul(8n, j), k)
1044      +ii = Nat.is_lt(p, 32n)
1045      %hjx : {Bool.and(Nat.is_le(Nat.mul(8n, _), p), Bool.and(ii, D.bit(b, Nat.sub(p, Nat.mul(8n, _))))) == Bool.and(Nat.is_eq(j, _), Bool.and(ii, D.bit(b, k))) : Bool}
1046      %Equal.sym(Bool, Nat.is_le(Nat.mul(8n, j), p), True{}, N.le_add_r(Nat.mul(8n, j), k)) :
1047        {Bool.and(_, Bool.and(ii, D.bit(b, Nat.sub(p, Nat.mul(8n, j))))) == Bool.and(Nat.is_eq(j, j), Bool.and(ii, D.bit(b, k))) : Bool}
1048      %Equal.sym(Nat, Nat.sub(p, Nat.mul(8n, j)), k, N.sub_add_l(Nat.mul(8n, j), k)) :
1049        {Bool.and(True{}, Bool.and(ii, D.bit(b, _))) == Bool.and(Nat.is_eq(j, j), Bool.and(ii, D.bit(b, k))) : Bool}
1050      %Equal.sym(Bool, Nat.is_eq(j, j), True{}, N.eq_refl(j)) :
1051        {Bool.and(True{}, Bool.and(ii, D.bit(b, k))) == Bool.and(_, Bool.and(ii, D.bit(b, k))) : Bool}
1052      {==}
1053    case GT{}:
1054      +p = Nat.add(Nat.mul(8n, j), k)
1055      +ii = Nat.is_lt(p, 32n)
1056      +hxj = gt_flip(j, x, ec)
1057      +hle = N.lt_to_le(x, j, hxj)
1058      +q = Nat.add(Nat.mul(8n, Nat.sub(j, x)), k)
1059      %Equal.sym(Bool, Nat.is_le(Nat.mul(8n, x), p), True{}, N.le_trans(Nat.mul(8n, x), Nat.mul(8n, j), p, N.le_mul_l(8n, x, j, hle), N.le_add_r(Nat.mul(8n, j), k))) :
1060        {Bool.and(_, Bool.and(ii, D.bit(b, Nat.sub(p, Nat.mul(8n, x))))) == Bool.and(Nat.is_eq(j, x), Bool.and(ii, D.bit(b, k))) : Bool}
1061      %Equal.sym(Nat, Nat.sub(p, Nat.mul(8n, x)), q, idx_sub(x, j, k, hle)) :
1062        {Bool.and(True{}, Bool.and(ii, D.bit(b, _))) == Bool.and(Nat.is_eq(j, x), Bool.and(ii, D.bit(b, k))) : Bool}
1063      %Equal.sym(Bool, D.bit(b, q), False{}, bit_lt_pow(b, 8n, q, hb,
1064          N.le_trans(8n, Nat.mul(8n, Nat.sub(j, x)), q,
1065            N.le_mul_l(8n, 1n, Nat.sub(j, x), %Equal.sym(Bool, Nat.is_le(1n, Nat.sub(j, x)), Nat.is_lt(0n, Nat.sub(j, x)), N.le_succ_lt(0n, Nat.sub(j, x))) : {_ == True{} : Bool};
1066              lt_sub(0n, x, j, hxj)),
1067            N.le_add_r(Nat.mul(8n, Nat.sub(j, x)), k)))) :
1068        {Bool.and(True{}, Bool.and(ii, _)) == Bool.and(Nat.is_eq(j, x), Bool.and(ii, D.bit(b, k))) : Bool}
1069      %Equal.sym(Cmp, Nat.cmp(j, x), GT{}, ec) : {Bool.and(ii, False{}) == Bool.and(Cmp.is_eq(_), Bool.and(ii, D.bit(b, k))) : Bool}
1070      N.and_false_r(ii)