def ceil_ok

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/kdf/okm.bend:93

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/hkdf.bend as Spec

93def ceil_ok(len: Nat) -> {Nat.is_le(len, Nat.mul(Spec.block_count(len), 32n)) == True{} : Bool}:
94  match len:
95    case 0n:
96      {==}
97    case 1n:
98      {==}
99    case 2n:
100      {==}
101    case 3n:
102      {==}
103    case 4n:
104      {==}
105    case 5n:
106      {==}
107    case 6n:
108      {==}
109    case 7n:
110      {==}
111    case 8n:
112      {==}
113    case 9n:
114      {==}
115    case 10n:
116      {==}
117    case 11n:
118      {==}
119    case 12n:
120      {==}
121    case 13n:
122      {==}
123    case 14n:
124      {==}
125    case 15n:
126      {==}
127    case 16n:
128      {==}
129    case 17n:
130      {==}
131    case 18n:
132      {==}
133    case 19n:
134      {==}
135    case 20n:
136      {==}
137    case 21n:
138      {==}
139    case 22n:
140      {==}
141    case 23n:
142      {==}
143    case 24n:
144      {==}
145    case 25n:
146      {==}
147    case 26n:
148      {==}
149    case 27n:
150      {==}
151    case 28n:
152      {==}
153    case 29n:
154      {==}
155    case 30n:
156      {==}
157    case 31n:
158      {==}
159    case 32n+ +q:
160      %Equal.sym(Nat, Nat.div(Nat.add(32n+q, 31n), 32n), 1n+Nat.div(Nat.add(q, 31n), 32n), div_step(q)) : {Nat.is_le(32n+q, Nat.mul(_, 32n)) == True{} : Bool}
161      ceil_ok(q)