proofs/crypto/argon2/words.bend

bend-collections-laws-crypto@1.0.0.0 · 41 lines · 8 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
4import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as U
5import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/u32.bend as U32P
6import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW
7
8# The U32 value model the Argon2 proofs use (from proofs/math/typed/u32laws.bend
9# and w64sh.bend, restated here so the package does not import their
10# neighbours: Bend 2.0.34 checks every imported definition, and one of them
11# expands 2^13 to a unary Nat, too deep for its stack next to this package).
12# Width 32 stays symbolic inside the proofs.
13
14def v(+x: U32) -> Nat:
15  U32.to_nat(x)
16
17def vb_k(+k: Nat, +hk: {k == 32n : Nat}, +x: U32) -> {C.fits(k, v(x)) == True{} : Bool}:
18  %Equal.sym(Bool, C.fits(k, v(x)), Nat.is_lt(v(x), C.pow2(k)), WW.fits_lt(k, v(x))) : {_ == True{} : Bool}
19  U32P.val_lt(1n, {==}, k, hk, x)
20
21# every U32 value fits 32 bits
22def vb(+x: U32) -> {C.fits(32n, v(x)) == True{} : Bool}:
23  vb_k(32n, {==}, x)
24
25def lt_k(+k: Nat, +n: Nat, +h: {C.fits(k, n) == True{} : Bool}) -> {Nat.is_lt(n, C.pow2(k)) == True{} : Bool}:
26  %WW.fits_lt(k, n) : {_ == True{} : Bool}
27  h
28
29def vo_k(+k: Nat, +hk: {k == 32n : Nat}, +n: Nat, +h: {C.fits(k, n) == True{} : Bool}) -> {v(U32.from_nat(n)) == n : Nat}:
30  U.to_nat_from_nat(n, k, U32P.le_k(k, hk), lt_k(k, n, h))
31
32# a value that fits is the value of its U32
33def vo(+n: Nat, +h: {C.fits(32n, n) == True{} : Bool}) -> {v(U32.from_nat(n)) == n : Nat}:
34  vo_k(32n, {==}, n, h)
35
36def rt(+x: U32) -> {U32.from_nat(v(x)) == x : U32}:
37  U32P.round_trip(x)
38
39# the high part of a value of t + s bits has s bits
40def fits_high(+t: Nat, +s: Nat, +x: Nat, +h: {C.fits(Nat.add(t, s), x) == True{} : Bool}) -> {C.fits(s, C.high(t, x)) == True{} : Bool}:
41  L.subst(Nat, z => {Nat.is_eq(z, 0n) == True{} : Bool}, C.high(Nat.add(t, s), x), C.high(s, C.high(t, x)), WW.high_comp(s, t, x), h)