padding_proof.bend source
padding_proof.bend on the hub · documented module
import Baseimport ./fips.bend as F# Universal bridge from implementation modular padding to the FIPS piecewise rule.# Every Nat is either one of 0..119 or 120+p. Each branch closes by reduction.law zeros_correct: for r: Nat {Nat.mod(Nat.sub(119n, r), 64n) == F.zero_count(r) : Nat}def zeros_correct(r): match r: case 0n: {==} case 1n: {==} case 2n: {==} case 3n: {==} case 4n: {==} case 5n: {==} case 6n: {==} case 7n: {==} case 8n: {==} case 9n: {==} case 10n: {==} case 11n: {==} case 12n: {==} case 13n: {==} case 14n: {==} case 15n: {==} case 16n: {==} case 17n: {==} case 18n: {==} case 19n: {==} case 20n: {==} case 21n: {==} case 22n: {==} case 23n: {==} case 24n: {==} case 25n: {==} case 26n: {==} case 27n: {==} case 28n: {==} case 29n: {==} case 30n: {==} case 31n: {==} case 32n: {==} case 33n: {==} case 34n: {==} case 35n: {==} case 36n: {==} case 37n: {==} case 38n: {==} case 39n: {==} case 40n: {==} case 41n: {==} case 42n: {==} case 43n: {==} case 44n: {==} case 45n: {==} case 46n: {==} case 47n: {==} case 48n: {==} case 49n: {==} case 50n: {==} case 51n: {==} case 52n: {==} case 53n: {==} case 54n: {==} case 55n: {==} case 56n: {==} case 57n: {==} case 58n: {==} case 59n: {==} case 60n: {==} case 61n: {==} case 62n: {==} case 63n: {==} case 64n: {==} case 65n: {==} case 66n: {==} case 67n: {==} case 68n: {==} case 69n: {==} case 70n: {==} case 71n: {==} case 72n: {==} case 73n: {==} case 74n: {==} case 75n: {==} case 76n: {==} case 77n: {==} case 78n: {==} case 79n: {==} case 80n: {==} case 81n: {==} case 82n: {==} case 83n: {==} case 84n: {==} case 85n: {==} case 86n: {==} case 87n: {==} case 88n: {==} case 89n: {==} case 90n: {==} case 91n: {==} case 92n: {==} case 93n: {==} case 94n: {==} case 95n: {==} case 96n: {==} case 97n: {==} case 98n: {==} case 99n: {==} case 100n: {==} case 101n: {==} case 102n: {==} case 103n: {==} case 104n: {==} case 105n: {==} case 106n: {==} case 107n: {==} case 108n: {==} case 109n: {==} case 110n: {==} case 111n: {==} case 112n: {==} case 113n: {==} case 114n: {==} case 115n: {==} case 116n: {==} case 117n: {==} case 118n: {==} case 119n: {==} case 120n+p: {==}