bend-osdev-hashes Releases (1): 0.1.0.0 0xd04c3185dce130521497bf85ab03f249 indexed https://jend.leeeet.dev/files.txt?path=bend-osdev-hashes@0.1.0.0 Definitions (266, 1 to 100 shown): LAWS.md_streaming (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=md_streaming) # The engine (hashes.bend), for every chaining value type, compression # function and block size: a ++ b is a, then b, from every state law md_streaming: for ~C: Data for ~compress: C -> List<&2, U32> -> C for ~last: U32 for s: Hs.HsMdState for +a: B.Octets for +b: B.Octets {Hs.HsMd.update(~C, ~compress, ~last, s, B.Octets.append(a, b)) == Hs.HsMd.update(~C, ~compress, ~last, Hs.HsMd.update(~C, ~compress, ~last, s, a), b) : Hs.HsMdState} LAWS.md4_streaming (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=md4_streaming) # MD4 (RFC 1320): update over a ++ b is update over a, then b, from every state law md4_streaming: for s: Hs.HsMdState for +a: B.Octets for +b: B.Octets {M4.HsMd4.update(s, B.Octets.append(a, b)) == M4.HsMd4.update(M4.HsMd4.update(s, a), b) : Hs.HsMdState} LAWS.md4_split (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=md4_split) # MD4 (RFC 1320): the digest in two pieces is the one-shot digest, for every split law md4_split: for +a: B.Octets for +b: B.Octets {M4.HsMd4.final(M4.HsMd4.update(M4.HsMd4.update(M4.HsMd4.init(), a), b)) == M4.HsMd4.digest(B.Octets.append(a, b)) : B.Octets} LAWS.md4_split3 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=md4_split3) # MD4 (RFC 1320): and in three pieces law md4_split3: for +a: B.Octets for +b: B.Octets for +c: B.Octets {M4.HsMd4.final(M4.HsMd4.update(M4.HsMd4.update(M4.HsMd4.update(M4.HsMd4.init(), a), b), c)) == M4.HsMd4.digest(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets} LAWS.md4_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=md4_length) # MD4 (RFC 1320): the digest of every state has 16 bytes law md4_length: for +s: Hs.HsMdState {B.Octets.len(M4.HsMd4.final(s)) == 16n : Nat} LAWS.md4_digest_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=md4_digest_length) # MD4 (RFC 1320): the digest of every message has 16 bytes law md4_digest_length: for +m: B.Octets {B.Octets.len(M4.HsMd4.digest(m)) == 16n : Nat} LAWS.md4_rfc1320_1 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=md4_rfc1320_1) # MD4 (RFC 1320): RFC 1320, appendix A.5 (the test suite) law md4_rfc1320_1: {M4.HsMd4.digest(B.Octets.of_string("")) == B.Octets.of_list([49, 214, 207, 224, 209, 106, 233, 49, 183, 60, 89, 215, 224, 192, 137, 192]) : B.Octets} LAWS.md4_rfc1320_2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=md4_rfc1320_2) # MD4 (RFC 1320): RFC 1320, appendix A.5 (the test suite) law md4_rfc1320_2: {M4.HsMd4.digest(B.Octets.of_string("a")) == B.Octets.of_list([189, 229, 44, 179, 29, 227, 62, 70, 36, 94, 5, 251, 219, 214, 251, 36]) : B.Octets} LAWS.md4_rfc1320_3 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=md4_rfc1320_3) # MD4 (RFC 1320): RFC 1320, appendix A.5 (the test suite) law md4_rfc1320_3: {M4.HsMd4.digest(B.Octets.of_string("abc")) == B.Octets.of_list([164, 72, 1, 122, 175, 33, 216, 82, 95, 193, 10, 232, 122, 166, 114, 157]) : B.Octets} LAWS.md4_rfc1320_4 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=md4_rfc1320_4) # MD4 (RFC 1320): RFC 1320, appendix A.5 (the test suite) law md4_rfc1320_4: {M4.HsMd4.digest(B.Octets.of_string("message digest")) == B.Octets.of_list([217, 19, 10, 129, 100, 84, 159, 232, 24, 135, 72, 6, 225, 199, 1, 75]) : B.Octets} LAWS.md4_rfc1320_5 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=md4_rfc1320_5) # MD4 (RFC 1320): RFC 1320, appendix A.5 (the test suite) law md4_rfc1320_5: {M4.HsMd4.digest(B.Octets.of_string("abcdefghijklmnopqrstuvwxyz")) == B.Octets.of_list([215, 158, 28, 48, 138, 165, 187, 205, 238, 168, 237, 99, 223, 65, 45, 169]) : B.Octets} LAWS.md4_rfc1320_6 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=md4_rfc1320_6) # MD4 (RFC 1320): RFC 1320, appendix A.5 (the test suite) law md4_rfc1320_6: {M4.HsMd4.digest(B.Octets.of_string("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789")) == B.Octets.of_list([4, 63, 133, 130, 242, 65, 219, 53, 28, 230, 39, 225, 83, 231, 240, 228]) : B.Octets} LAWS.md4_rfc1320_7 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=md4_rfc1320_7) # MD4 (RFC 1320): RFC 1320, appendix A.5 (the test suite) law md4_rfc1320_7: {M4.HsMd4.digest(B.Octets.of_string("12345678901234567890123456789012345678901234567890123456789012345678901234567890")) == B.Octets.of_list([227, 59, 77, 220, 156, 56, 242, 25, 156, 62, 123, 22, 79, 204, 5, 54]) : B.Octets} LAWS.md5_streaming (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=md5_streaming) # MD5 (RFC 1321): update over a ++ b is update over a, then b, from every state law md5_streaming: for s: Hs.HsMdState for +a: B.Octets for +b: B.Octets {M5.HsMd5.update(s, B.Octets.append(a, b)) == M5.HsMd5.update(M5.HsMd5.update(s, a), b) : Hs.HsMdState} LAWS.md5_split (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=md5_split) # MD5 (RFC 1321): the digest in two pieces is the one-shot digest, for every split law md5_split: for +a: B.Octets for +b: B.Octets {M5.HsMd5.final(M5.HsMd5.update(M5.HsMd5.update(M5.HsMd5.init(), a), b)) == M5.HsMd5.digest(B.Octets.append(a, b)) : B.Octets} LAWS.md5_split3 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=md5_split3) # MD5 (RFC 1321): and in three pieces law md5_split3: for +a: B.Octets for +b: B.Octets for +c: B.Octets {M5.HsMd5.final(M5.HsMd5.update(M5.HsMd5.update(M5.HsMd5.update(M5.HsMd5.init(), a), b), c)) == M5.HsMd5.digest(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets} LAWS.md5_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=md5_length) # MD5 (RFC 1321): the digest of every state has 16 bytes law md5_length: for +s: Hs.HsMdState {B.Octets.len(M5.HsMd5.final(s)) == 16n : Nat} LAWS.md5_digest_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=md5_digest_length) # MD5 (RFC 1321): the digest of every message has 16 bytes law md5_digest_length: for +m: B.Octets {B.Octets.len(M5.HsMd5.digest(m)) == 16n : Nat} LAWS.md5_rfc1321_1 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=md5_rfc1321_1) # MD5 (RFC 1321): RFC 1321, appendix A.5 (the test suite) law md5_rfc1321_1: {M5.HsMd5.digest(B.Octets.of_string("")) == B.Octets.of_list([212, 29, 140, 217, 143, 0, 178, 4, 233, 128, 9, 152, 236, 248, 66, 126]) : B.Octets} LAWS.md5_rfc1321_2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=md5_rfc1321_2) # MD5 (RFC 1321): RFC 1321, appendix A.5 (the test suite) law md5_rfc1321_2: {M5.HsMd5.digest(B.Octets.of_string("a")) == B.Octets.of_list([12, 193, 117, 185, 192, 241, 182, 168, 49, 195, 153, 226, 105, 119, 38, 97]) : B.Octets} LAWS.md5_rfc1321_3 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=md5_rfc1321_3) # MD5 (RFC 1321): RFC 1321, appendix A.5 (the test suite) law md5_rfc1321_3: {M5.HsMd5.digest(B.Octets.of_string("abc")) == B.Octets.of_list([144, 1, 80, 152, 60, 210, 79, 176, 214, 150, 63, 125, 40, 225, 127, 114]) : B.Octets} LAWS.md5_rfc1321_4 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=md5_rfc1321_4) # MD5 (RFC 1321): RFC 1321, appendix A.5 (the test suite) law md5_rfc1321_4: {M5.HsMd5.digest(B.Octets.of_string("message digest")) == B.Octets.of_list([249, 107, 105, 125, 124, 183, 147, 141, 82, 90, 47, 49, 170, 241, 97, 208]) : B.Octets} LAWS.md5_rfc1321_5 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=md5_rfc1321_5) # MD5 (RFC 1321): RFC 1321, appendix A.5 (the test suite) law md5_rfc1321_5: {M5.HsMd5.digest(B.Octets.of_string("abcdefghijklmnopqrstuvwxyz")) == B.Octets.of_list([195, 252, 211, 215, 97, 146, 228, 0, 125, 251, 73, 108, 202, 103, 225, 59]) : B.Octets} LAWS.md5_rfc1321_6 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=md5_rfc1321_6) # MD5 (RFC 1321): RFC 1321, appendix A.5 (the test suite) law md5_rfc1321_6: {M5.HsMd5.digest(B.Octets.of_string("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789")) == B.Octets.of_list([209, 116, 171, 152, 210, 119, 217, 245, 165, 97, 28, 44, 159, 65, 157, 159]) : B.Octets} LAWS.md5_rfc1321_7 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=md5_rfc1321_7) # MD5 (RFC 1321): RFC 1321, appendix A.5 (the test suite) law md5_rfc1321_7: {M5.HsMd5.digest(B.Octets.of_string("12345678901234567890123456789012345678901234567890123456789012345678901234567890")) == B.Octets.of_list([87, 237, 244, 162, 43, 227, 201, 85, 172, 73, 218, 46, 33, 7, 182, 122]) : B.Octets} LAWS.sha1_streaming (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=sha1_streaming) # SHA-1 (FIPS 180-4): update over a ++ b is update over a, then b, from every state law sha1_streaming: for s: Hs.HsMdState for +a: B.Octets for +b: B.Octets {S1.HsSha1.update(s, B.Octets.append(a, b)) == S1.HsSha1.update(S1.HsSha1.update(s, a), b) : Hs.HsMdState} LAWS.sha1_split (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=sha1_split) # SHA-1 (FIPS 180-4): the digest in two pieces is the one-shot digest, for every split law sha1_split: for +a: B.Octets for +b: B.Octets {S1.HsSha1.final(S1.HsSha1.update(S1.HsSha1.update(S1.HsSha1.init(), a), b)) == S1.HsSha1.digest(B.Octets.append(a, b)) : B.Octets} LAWS.sha1_split3 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=sha1_split3) # SHA-1 (FIPS 180-4): and in three pieces law sha1_split3: for +a: B.Octets for +b: B.Octets for +c: B.Octets {S1.HsSha1.final(S1.HsSha1.update(S1.HsSha1.update(S1.HsSha1.update(S1.HsSha1.init(), a), b), c)) == S1.HsSha1.digest(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets} LAWS.sha1_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=sha1_length) # SHA-1 (FIPS 180-4): the digest of every state has 20 bytes law sha1_length: for +s: Hs.HsMdState {B.Octets.len(S1.HsSha1.final(s)) == 20n : Nat} LAWS.sha1_digest_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=sha1_digest_length) # SHA-1 (FIPS 180-4): the digest of every message has 20 bytes law sha1_digest_length: for +m: B.Octets {B.Octets.len(S1.HsSha1.digest(m)) == 20n : Nat} LAWS.sha1_fips_1 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=sha1_fips_1) # SHA-1 (FIPS 180-4): FIPS 180-4's examples (NIST's SHA-1 example values): "abc" and the 448-bit message law sha1_fips_1: {S1.HsSha1.digest(B.Octets.of_string("abc")) == B.Octets.of_list([169, 153, 62, 54, 71, 6, 129, 106, 186, 62, 37, 113, 120, 80, 194, 108, 156, 208, 216, 157]) : B.Octets} LAWS.sha1_fips_2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=sha1_fips_2) # SHA-1 (FIPS 180-4): FIPS 180-4's examples (NIST's SHA-1 example values): "abc" and the 448-bit message law sha1_fips_2: {S1.HsSha1.digest(B.Octets.of_string("abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq")) == B.Octets.of_list([132, 152, 62, 68, 28, 59, 210, 110, 186, 174, 74, 161, 249, 81, 41, 229, 229, 70, 112, 241]) : B.Octets} LAWS.ripemd160_streaming (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=ripemd160_streaming) # RIPEMD-160: update over a ++ b is update over a, then b, from every state law ripemd160_streaming: for s: Hs.HsMdState for +a: B.Octets for +b: B.Octets {RM.HsRipemd160.update(s, B.Octets.append(a, b)) == RM.HsRipemd160.update(RM.HsRipemd160.update(s, a), b) : Hs.HsMdState} LAWS.ripemd160_split (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=ripemd160_split) # RIPEMD-160: the digest in two pieces is the one-shot digest, for every split law ripemd160_split: for +a: B.Octets for +b: B.Octets {RM.HsRipemd160.final(RM.HsRipemd160.update(RM.HsRipemd160.update(RM.HsRipemd160.init(), a), b)) == RM.HsRipemd160.digest(B.Octets.append(a, b)) : B.Octets} LAWS.ripemd160_split3 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=ripemd160_split3) # RIPEMD-160: and in three pieces law ripemd160_split3: for +a: B.Octets for +b: B.Octets for +c: B.Octets {RM.HsRipemd160.final(RM.HsRipemd160.update(RM.HsRipemd160.update(RM.HsRipemd160.update(RM.HsRipemd160.init(), a), b), c)) == RM.HsRipemd160.digest(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets} LAWS.ripemd160_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=ripemd160_length) # RIPEMD-160: the digest of every state has 20 bytes law ripemd160_length: for +s: Hs.HsMdState {B.Octets.len(RM.HsRipemd160.final(s)) == 20n : Nat} LAWS.ripemd160_digest_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=ripemd160_digest_length) # RIPEMD-160: the digest of every message has 20 bytes law ripemd160_digest_length: for +m: B.Octets {B.Octets.len(RM.HsRipemd160.digest(m)) == 20n : Nat} LAWS.ripemd160_paper_1 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=ripemd160_paper_1) # RIPEMD-160: the test values of Dobbertin, Bosselaers and Preneel (the RIPEMD-160 page) law ripemd160_paper_1: {RM.HsRipemd160.digest(B.Octets.of_string("")) == B.Octets.of_list([156, 17, 133, 165, 197, 233, 252, 84, 97, 40, 8, 151, 126, 232, 245, 72, 178, 37, 141, 49]) : B.Octets} LAWS.ripemd160_paper_2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=ripemd160_paper_2) # RIPEMD-160: the test values of Dobbertin, Bosselaers and Preneel (the RIPEMD-160 page) law ripemd160_paper_2: {RM.HsRipemd160.digest(B.Octets.of_string("a")) == B.Octets.of_list([11, 220, 157, 45, 37, 107, 62, 233, 218, 174, 52, 123, 230, 244, 220, 131, 90, 70, 127, 254]) : B.Octets} LAWS.ripemd160_paper_3 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=ripemd160_paper_3) # RIPEMD-160: the test values of Dobbertin, Bosselaers and Preneel (the RIPEMD-160 page) law ripemd160_paper_3: {RM.HsRipemd160.digest(B.Octets.of_string("abc")) == B.Octets.of_list([142, 178, 8, 247, 224, 93, 152, 122, 155, 4, 74, 142, 152, 198, 176, 135, 241, 90, 11, 252]) : B.Octets} LAWS.ripemd160_paper_4 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=ripemd160_paper_4) # RIPEMD-160: the test values of Dobbertin, Bosselaers and Preneel (the RIPEMD-160 page) law ripemd160_paper_4: {RM.HsRipemd160.digest(B.Octets.of_string("message digest")) == B.Octets.of_list([93, 6, 137, 239, 73, 210, 250, 229, 114, 184, 129, 177, 35, 168, 95, 250, 33, 89, 95, 54]) : B.Octets} LAWS.ripemd160_paper_5 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=ripemd160_paper_5) # RIPEMD-160: the test values of Dobbertin, Bosselaers and Preneel (the RIPEMD-160 page) law ripemd160_paper_5: {RM.HsRipemd160.digest(B.Octets.of_string("abcdefghijklmnopqrstuvwxyz")) == B.Octets.of_list([247, 28, 39, 16, 156, 105, 44, 27, 86, 187, 220, 235, 91, 157, 40, 101, 179, 112, 141, 188]) : B.Octets} LAWS.ripemd160_paper_6 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=ripemd160_paper_6) # RIPEMD-160: the test values of Dobbertin, Bosselaers and Preneel (the RIPEMD-160 page) law ripemd160_paper_6: {RM.HsRipemd160.digest(B.Octets.of_string("abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq")) == B.Octets.of_list([18, 160, 83, 56, 74, 156, 12, 136, 228, 5, 160, 108, 39, 220, 244, 154, 218, 98, 235, 43]) : B.Octets} LAWS.ripemd160_paper_7 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=ripemd160_paper_7) # RIPEMD-160: the test values of Dobbertin, Bosselaers and Preneel (the RIPEMD-160 page) law ripemd160_paper_7: {RM.HsRipemd160.digest(B.Octets.of_string("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789")) == B.Octets.of_list([176, 226, 11, 110, 49, 22, 100, 2, 134, 237, 58, 135, 165, 113, 48, 121, 178, 31, 81, 137]) : B.Octets} LAWS.ripemd160_paper_8 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=ripemd160_paper_8) # RIPEMD-160: the test values of Dobbertin, Bosselaers and Preneel (the RIPEMD-160 page) law ripemd160_paper_8: {RM.HsRipemd160.digest(B.Octets.of_string("12345678901234567890123456789012345678901234567890123456789012345678901234567890")) == B.Octets.of_list([155, 117, 46, 69, 87, 61, 75, 57, 244, 219, 211, 50, 60, 171, 130, 191, 99, 50, 107, 251]) : B.Octets} LAWS.sm3_streaming (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=sm3_streaming) # SM3 (GB/T 32905): update over a ++ b is update over a, then b, from every state law sm3_streaming: for s: Hs.HsMdState for +a: B.Octets for +b: B.Octets {SM.HsSm3.update(s, B.Octets.append(a, b)) == SM.HsSm3.update(SM.HsSm3.update(s, a), b) : Hs.HsMdState} LAWS.sm3_split (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=sm3_split) # SM3 (GB/T 32905): the digest in two pieces is the one-shot digest, for every split law sm3_split: for +a: B.Octets for +b: B.Octets {SM.HsSm3.final(SM.HsSm3.update(SM.HsSm3.update(SM.HsSm3.init(), a), b)) == SM.HsSm3.digest(B.Octets.append(a, b)) : B.Octets} LAWS.sm3_split3 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=sm3_split3) # SM3 (GB/T 32905): and in three pieces law sm3_split3: for +a: B.Octets for +b: B.Octets for +c: B.Octets {SM.HsSm3.final(SM.HsSm3.update(SM.HsSm3.update(SM.HsSm3.update(SM.HsSm3.init(), a), b), c)) == SM.HsSm3.digest(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets} LAWS.sm3_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=sm3_length) # SM3 (GB/T 32905): the digest of every state has 32 bytes law sm3_length: for +s: Hs.HsMdState {B.Octets.len(SM.HsSm3.final(s)) == 32n : Nat} LAWS.sm3_digest_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=sm3_digest_length) # SM3 (GB/T 32905): the digest of every message has 32 bytes law sm3_digest_length: for +m: B.Octets {B.Octets.len(SM.HsSm3.digest(m)) == 32n : Nat} LAWS.sm3_example_1 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=sm3_example_1) # SM3 (GB/T 32905): draft-shen-sm3-hash-01, examples 1 and 2 law sm3_example_1: {SM.HsSm3.digest(B.Octets.of_string("abc")) == B.Octets.of_list([102, 199, 240, 244, 98, 238, 237, 217, 209, 242, 212, 107, 220, 16, 228, 226, 65, 103, 196, 135, 92, 242, 247, 162, 41, 125, 160, 43, 143, 75, 168, 224]) : B.Octets} LAWS.sm3_example_2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=sm3_example_2) # SM3 (GB/T 32905): draft-shen-sm3-hash-01, examples 1 and 2 law sm3_example_2: {SM.HsSm3.digest(B.Octets.of_string("abcdabcdabcdabcdabcdabcdabcdabcdabcdabcdabcdabcdabcdabcdabcdabcd")) == B.Octets.of_list([222, 190, 159, 249, 34, 117, 184, 161, 56, 96, 72, 137, 193, 142, 90, 77, 111, 219, 112, 229, 56, 126, 87, 101, 41, 61, 203, 163, 156, 12, 87, 50]) : B.Octets} LAWS.streebog512_streaming (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=streebog512_streaming) # Streebog-512 (RFC 6986): update over a ++ b is update over a, then b, from every state law streebog512_streaming: for s: Hs.HsMdState for +a: B.Octets for +b: B.Octets {ST.HsStreebog.update(s, B.Octets.append(a, b)) == ST.HsStreebog.update(ST.HsStreebog.update(s, a), b) : Hs.HsMdState} LAWS.streebog512_split (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=streebog512_split) # Streebog-512 (RFC 6986): the digest in two pieces is the one-shot digest, for every split law streebog512_split: for +a: B.Octets for +b: B.Octets {ST.HsStreebog.final512(ST.HsStreebog.update(ST.HsStreebog.update(ST.HsStreebog.init512(), a), b)) == ST.HsStreebog.digest512(B.Octets.append(a, b)) : B.Octets} LAWS.streebog512_split3 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=streebog512_split3) # Streebog-512 (RFC 6986): and in three pieces law streebog512_split3: for +a: B.Octets for +b: B.Octets for +c: B.Octets {ST.HsStreebog.final512(ST.HsStreebog.update(ST.HsStreebog.update(ST.HsStreebog.update(ST.HsStreebog.init512(), a), b), c)) == ST.HsStreebog.digest512(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets} LAWS.streebog512_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=streebog512_length) # Streebog-512 (RFC 6986): the digest of every state has 64 bytes law streebog512_length: for +s: Hs.HsMdState {B.Octets.len(ST.HsStreebog.final512(s)) == 64n : Nat} LAWS.streebog512_digest_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=streebog512_digest_length) # Streebog-512 (RFC 6986): the digest of every message has 64 bytes law streebog512_digest_length: for +m: B.Octets {B.Octets.len(ST.HsStreebog.digest512(m)) == 64n : Nat} LAWS.streebog256_streaming (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=streebog256_streaming) # Streebog-256 (RFC 6986): update over a ++ b is update over a, then b, from every state law streebog256_streaming: for s: Hs.HsMdState for +a: B.Octets for +b: B.Octets {ST.HsStreebog.update(s, B.Octets.append(a, b)) == ST.HsStreebog.update(ST.HsStreebog.update(s, a), b) : Hs.HsMdState} LAWS.streebog256_split (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=streebog256_split) # Streebog-256 (RFC 6986): the digest in two pieces is the one-shot digest, for every split law streebog256_split: for +a: B.Octets for +b: B.Octets {ST.HsStreebog.final256(ST.HsStreebog.update(ST.HsStreebog.update(ST.HsStreebog.init256(), a), b)) == ST.HsStreebog.digest256(B.Octets.append(a, b)) : B.Octets} LAWS.streebog256_split3 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=streebog256_split3) # Streebog-256 (RFC 6986): and in three pieces law streebog256_split3: for +a: B.Octets for +b: B.Octets for +c: B.Octets {ST.HsStreebog.final256(ST.HsStreebog.update(ST.HsStreebog.update(ST.HsStreebog.update(ST.HsStreebog.init256(), a), b), c)) == ST.HsStreebog.digest256(B.Octets.append(a, B.Octets.append(b, c))) : B.Octets} LAWS.streebog256_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=streebog256_length) # Streebog-256 (RFC 6986): the digest of every state has 32 bytes law streebog256_length: for +s: Hs.HsMdState {B.Octets.len(ST.HsStreebog.final256(s)) == 32n : Nat} LAWS.streebog256_digest_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=streebog256_digest_length) # Streebog-256 (RFC 6986): the digest of every message has 32 bytes law streebog256_digest_length: for +m: B.Octets {B.Octets.len(ST.HsStreebog.digest256(m)) == 32n : Nat} LAWS.streebog_lps_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=streebog_lps_zero) # Streebog-512, K = LPS(h xor N) = LPS(0^512) (RFC 6986 prints it most significant byte first) law streebog_lps_zero: {ST.HsStreebog.lps(B.Octets.zeros(64n)) == B.Octets.of_list([116, 165, 212, 206, 46, 252, 131, 179, 116, 165, 212, 206, 46, 252, 131, 179, 116, 165, 212, 206, 46, 252, 131, 179, 116, 165, 212, 206, 46, 252, 131, 179, 116, 165, 212, 206, 46, 252, 131, 179, 116, 165, 212, 206, 46, 252, 131, 179, 116, 165, 212, 206, 46, 252, 131, 179, 116, 165, 212, 206, 46, 252, 131, 179]) : B.Octets} LAWS.streebog_g_example1 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=streebog_g_example1) # Streebog-512, the first compression, g_N(h, m) with h = N = 0 and m the padded M1 (RFC 6986 prints it most significant byte first) law streebog_g_example1: {ST.HsStreebog.g(B.Octets.zeros(64n), B.Octets.zeros(64n), B.Octets.of_list([48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 48, 49, 50, 1])) == B.Octets.of_list([226, 218, 59, 107, 115, 228, 254, 5, 217, 245, 177, 63, 121, 53, 65, 149, 92, 129, 80, 44, 82, 15, 237, 211, 197, 186, 187, 140, 144, 246, 84, 39, 189, 142, 115, 51, 219, 138, 72, 38, 166, 169, 90, 68, 65, 102, 168, 23, 56, 79, 57, 33, 175, 52, 234, 145, 17, 203, 44, 129, 248, 44, 16, 253]) : B.Octets} LAWS.streebog_g0_example1 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=streebog_g0_example1) # Streebog-512, g_0(h, N) after it, N = 504 (RFC 6986 prints it most significant byte first) law streebog_g0_example1: {ST.HsStreebog.g(B.Octets.zeros(64n), B.Octets.of_list([226, 218, 59, 107, 115, 228, 254, 5, 217, 245, 177, 63, 121, 53, 65, 149, 92, 129, 80, 44, 82, 15, 237, 211, 197, 186, 187, 140, 144, 246, 84, 39, 189, 142, 115, 51, 219, 138, 72, 38, 166, 169, 90, 68, 65, 102, 168, 23, 56, 79, 57, 33, 175, 52, 234, 145, 17, 203, 44, 129, 248, 44, 16, 253]), B.Octets.of_list([248, 1])) == B.Octets.of_list([124, 29, 119, 231, 93, 26, 144, 168, 1, 69, 211, 98, 214, 225, 55, 144, 127, 110, 166, 25, 79, 161, 71, 33, 98, 148, 55, 109, 157, 182, 45, 61, 82, 151, 213, 212, 103, 112, 187, 170, 235, 22, 23, 11, 42, 111, 2, 66, 182, 20, 13, 194, 254, 228, 194, 150, 241, 92, 105, 36, 217, 31, 136, 92]) : B.Octets} LAWS.michael_streaming (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=michael_streaming) # Michael (IEEE 802.11i): update over a ++ b is update over a, then b, from every state law michael_streaming: for s: Hs.HsMdState for +a: B.Octets for +b: B.Octets {MI.HsMichael.update(s, B.Octets.append(a, b)) == MI.HsMichael.update(MI.HsMichael.update(s, a), b) : Hs.HsMdState} LAWS.michael_split (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=michael_split) # Michael (IEEE 802.11i): the tag in two pieces is the one-call tag, for every key and split law michael_split: for +k: Hs.HsW2 for +a: B.Octets for +b: B.Octets {MI.HsMichael.final(MI.HsMichael.update(MI.HsMichael.update(MI.HsMichael.init(k), a), b)) == MI.HsMichael.mic(k, B.Octets.append(a, b)) : B.Octets} LAWS.michael_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=michael_length) # Michael (IEEE 802.11i): the tag of every state has 8 bytes law michael_length: for +s: Hs.HsMdState {B.Octets.len(MI.HsMichael.final(s)) == 8n : Nat} LAWS.michael_mic_length (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=michael_mic_length) # Michael (IEEE 802.11i): the tag of every message under every key has 8 bytes law michael_mic_length: for +k: Hs.HsW2 for +m: B.Octets {B.Octets.len(MI.HsMichael.mic(k, m)) == 8n : Nat} LAWS.michael_short_key (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=michael_short_key) # Michael (IEEE 802.11i): a key of 7 bytes is refused law michael_short_key: {Result.map(&2, &2, Hs.HsError, Hs.HsW2, Unit, k => Unit{}, MI.HsMichael.key(B.Octets.zeros(7n))) == Fail{Hs.HsBadKeyLength{7n}} : Result<&2, &2, Hs.HsError, Unit>} LAWS.michael_vector_1 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=michael_vector_1) # Michael (IEEE 802.11i): test vector 1 as recalled from IEEE 802.11i's Annex H.2 (each key the previous tag), not checked against a published copy (README.md) law michael_vector_1: {Result.map(&2, &2, Hs.HsError, Hs.HsW2, B.Octets, k => MI.HsMichael.mic(k, B.Octets.of_string("")), MI.HsMichael.key(B.Octets.of_list([0, 0, 0, 0, 0, 0, 0, 0]))) == Done{B.Octets.of_list([130, 146, 92, 28, 161, 209, 48, 184])} : Result<&2, &2, Hs.HsError, B.Octets>} LAWS.michael_vector_2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=michael_vector_2) # Michael (IEEE 802.11i): test vector 2 as recalled from IEEE 802.11i's Annex H.2 (each key the previous tag), not checked against a published copy (README.md) law michael_vector_2: {Result.map(&2, &2, Hs.HsError, Hs.HsW2, B.Octets, k => MI.HsMichael.mic(k, B.Octets.of_string("M")), MI.HsMichael.key(B.Octets.of_list([130, 146, 92, 28, 161, 209, 48, 184]))) == Done{B.Octets.of_list([67, 71, 33, 202, 64, 99, 155, 63])} : Result<&2, &2, Hs.HsError, B.Octets>} LAWS.michael_vector_3 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=michael_vector_3) # Michael (IEEE 802.11i): test vector 3 as recalled from IEEE 802.11i's Annex H.2 (each key the previous tag), not checked against a published copy (README.md) law michael_vector_3: {Result.map(&2, &2, Hs.HsError, Hs.HsW2, B.Octets, k => MI.HsMichael.mic(k, B.Octets.of_string("Mi")), MI.HsMichael.key(B.Octets.of_list([67, 71, 33, 202, 64, 99, 155, 63]))) == Done{B.Octets.of_list([232, 249, 190, 202, 233, 126, 93, 41])} : Result<&2, &2, Hs.HsError, B.Octets>} LAWS.michael_vector_4 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=michael_vector_4) # Michael (IEEE 802.11i): test vector 4 as recalled from IEEE 802.11i's Annex H.2 (each key the previous tag), not checked against a published copy (README.md) law michael_vector_4: {Result.map(&2, &2, Hs.HsError, Hs.HsW2, B.Octets, k => MI.HsMichael.mic(k, B.Octets.of_string("Mic")), MI.HsMichael.key(B.Octets.of_list([232, 249, 190, 202, 233, 126, 93, 41]))) == Done{B.Octets.of_list([144, 3, 143, 198, 207, 19, 193, 219])} : Result<&2, &2, Hs.HsError, B.Octets>} LAWS.michael_vector_5 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=michael_vector_5) # Michael (IEEE 802.11i): test vector 5 as recalled from IEEE 802.11i's Annex H.2 (each key the previous tag), not checked against a published copy (README.md) law michael_vector_5: {Result.map(&2, &2, Hs.HsError, Hs.HsW2, B.Octets, k => MI.HsMichael.mic(k, B.Octets.of_string("Mich")), MI.HsMichael.key(B.Octets.of_list([144, 3, 143, 198, 207, 19, 193, 219]))) == Done{B.Octets.of_list([213, 94, 16, 5, 16, 18, 137, 134])} : Result<&2, &2, Hs.HsError, B.Octets>} LAWS.michael_vector_6 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=michael_vector_6) # Michael (IEEE 802.11i): test vector 6 as recalled from IEEE 802.11i's Annex H.2 (each key the previous tag), not checked against a published copy (README.md) law michael_vector_6: {Result.map(&2, &2, Hs.HsError, Hs.HsW2, B.Octets, k => MI.HsMichael.mic(k, B.Octets.of_string("Michael")), MI.HsMichael.key(B.Octets.of_list([213, 94, 16, 5, 16, 18, 137, 134]))) == Done{B.Octets.of_list([10, 148, 43, 18, 78, 202, 165, 70])} : Result<&2, &2, Hs.HsError, B.Octets>} LAWS.michael_tkip_m63 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/LAWS.bend&name=michael_tkip_m63) # Michael (IEEE 802.11i): IEEE Std 802.11-2012, M.6.3 (the TKIP test vector, as hostap's BSD-licensed wlantest/test_vectors.c reproduces it): the MIC of its MSDU (DA, SA, priority 0 and three zero bytes, then the data) under TK bytes 16 to 23 law michael_tkip_m63: {Result.map(&2, &2, Hs.HsError, Hs.HsW2, B.Octets, k => MI.HsMichael.mic(k, B.Octets.of_list([2, 3, 4, 5, 6, 8, 2, 3, 4, 5, 6, 7, 0, 0, 0, 0, 170, 170, 3, 0, 0, 0, 8, 0, 69, 0, 0, 84, 0, 0, 64, 0, 64, 1, 165, 85, 192, 168, 10, 2, 192, 168, 10, 1, 8, 0, 58, 176, 0, 0, 0, 0, 205, 76, 5, 0, 0, 0, 0, 0, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55])), MI.HsMichael.key(B.Octets.of_list([52, 86, 120, 144, 18, 52, 86, 120]))) == Done{B.Octets.of_list([104, 129, 163, 243, 214, 72, 208, 60])} : Result<&2, &2, Hs.HsError, B.Octets>} PROOF.feed_append (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/PROOF.bend&name=feed_append) # The engine: feeding xs ++ ys is feeding xs, then ys (induction on xs) def feed_append(~C: Data, ~compress: C -> List<&2, U32> -> C, ~last: U32, xs: List<&2, U32>, +ys: List<&2, U32>, s: Hs.HsMdState) -> {Hs.hs.md.feed(~C, ~compress, ~last, B.append(xs, ys), s) == Hs.hs.md.feed(~C, ~compress, ~last, ys, Hs.hs.md.feed(~C, ~compress, ~last, xs, s)) : Hs.HsMdState}: PROOF.mask_len (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/PROOF.bend&name=mask_len) # Lengths: an Octets made from a list has the list's length; the bytes of # a chaining value are a list of fixed shape whatever its words are def mask_len(xs: List<&2, U32>) -> {B.len(B.mask(xs)) == B.len(xs) : Nat}: PROOF.octets_len_of (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/PROOF.bend&name=octets_len_of) def octets_len_of(+xs: List<&2, U32>) -> {B.Octets.len(B.Octets.of_list(xs)) == B.len(xs) : Nat}: PROOF.w2le_len_list (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/PROOF.bend&name=w2le_len_list) def w2le_len_list(a0: U32, a1: U32) -> {B.len(B.append(B.le32(a0), B.le32(a1))) == 8n : Nat}: PROOF.w2le_len (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/PROOF.bend&name=w2le_len) def w2le_len(x: Hs.HsW2) -> {B.Octets.len(Hs.HsW2.le(x)) == 8n : Nat}: PROOF.w4le_len_list (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/PROOF.bend&name=w4le_len_list) def w4le_len_list(a0: U32, a1: U32, a2: U32, a3: U32) -> {B.len(B.append(B.le32(a0), B.append(B.le32(a1), B.append(B.le32(a2), B.le32(a3))))) == 16n : Nat}: PROOF.w4le_len (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/PROOF.bend&name=w4le_len) def w4le_len(x: Hs.HsW4) -> {B.Octets.len(Hs.HsW4.le(x)) == 16n : Nat}: PROOF.w5le_len_list (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/PROOF.bend&name=w5le_len_list) def w5le_len_list(a0: U32, a1: U32, a2: U32, a3: U32, a4: U32) -> {B.len(B.append(B.le32(a0), B.append(B.le32(a1), B.append(B.le32(a2), B.append(B.le32(a3), B.le32(a4)))))) == 20n : Nat}: PROOF.w5le_len (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/PROOF.bend&name=w5le_len) def w5le_len(x: Hs.HsW5) -> {B.Octets.len(Hs.HsW5.le(x)) == 20n : Nat}: PROOF.w5be_len_list (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/PROOF.bend&name=w5be_len_list) def w5be_len_list(a0: U32, a1: U32, a2: U32, a3: U32, a4: U32) -> {B.len(B.append(B.be32(a0), B.append(B.be32(a1), B.append(B.be32(a2), B.append(B.be32(a3), B.be32(a4)))))) == 20n : Nat}: PROOF.w5be_len (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/PROOF.bend&name=w5be_len) def w5be_len(x: Hs.HsW5) -> {B.Octets.len(Hs.HsW5.be(x)) == 20n : Nat}: PROOF.w8be_len_list (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/PROOF.bend&name=w8be_len_list) def w8be_len_list(a0: U32, a1: U32, a2: U32, a3: U32, a4: U32, a5: U32, a6: U32, a7: U32) -> {B.len(B.append(B.be32(a0), B.append(B.be32(a1), B.append(B.be32(a2), B.append(B.be32(a3), B.append(B.be32(a4), B.append(B.be32(a5), B.append(B.be32(a6), B.be32(a7))))))))) == 32n : Nat}: PROOF.w8be_len (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/PROOF.bend&name=w8be_len) def w8be_len(x: Hs.HsW8) -> {B.Octets.len(Hs.HsW8.be(x)) == 32n : Nat}: PROOF.stb512_len_list (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/PROOF.bend&name=stb512_len_list) def stb512_len_list(a0: U32, a1: U32, a2: U32, a3: U32, a4: U32, a5: U32, a6: U32, a7: U32, a8: U32, a9: U32, a10: U32, a11: U32, a12: U32, a13: U32, a14: U32, a15: U32) -> {B.len(B.append(B.le32(a0), B.append(B.le32(a1), B.append(B.le32(a2), B.append(B.le32(a3), B.append(B.le32(a4), B.append(B.le32(a5), B.append(B.le32(a6), B.append(B.le32(a7), B.append(B.le32(a8), B.append(B.le32(a9), B.append(B.le32(a10), B.append(B.le32(a11), B.append(B.le32(a12), B.append(B.le32(a13), B.append(B.le32(a14), B.le32(a15))))))))))))))))) == 64n : Nat}: PROOF.stb512_len (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/PROOF.bend&name=stb512_len) def stb512_len(x: Hs.HsW16) -> {B.Octets.len(ST.hs.stb.out512(x)) == 64n : Nat}: PROOF.stb256_len_list (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/PROOF.bend&name=stb256_len_list) def stb256_len_list(a8: U32, a9: U32, a10: U32, a11: U32, a12: U32, a13: U32, a14: U32, a15: U32) -> {B.len(B.append(B.le32(a8), B.append(B.le32(a9), B.append(B.le32(a10), B.append(B.le32(a11), B.append(B.le32(a12), B.append(B.le32(a13), B.append(B.le32(a14), B.le32(a15))))))))) == 32n : Nat}: PROOF.stb256_len (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/PROOF.bend&name=stb256_len) def stb256_len(x: Hs.HsW16) -> {B.Octets.len(ST.hs.stb.out256(x)) == 32n : Nat}: Check.third (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/check.bend&name=third) # a byte string in three pieces: [0, n/3), [n/3, 2n/3), [2n/3, n) def third(+o: B.Octets) -> Nat: Check.p1 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/check.bend&name=p1) def p1(+o: B.Octets) -> B.Octets: Check.p2 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/check.bend&name=p2) def p2(+o: B.Octets) -> B.Octets: Check.p3 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/check.bend&name=p3) def p3(+o: B.Octets) -> B.Octets: Check.mic.of (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/check.bend&name=mic.of) def mic.of(r: Result<&2, &2, Hs.HsError, Hs.HsW2>, +m: B.Octets) -> String: Check.mic (https://jend.leeeet.dev/definition.txt?path=bend-osdev-hashes@0.1.0.0/check.bend&name=mic) def mic(k: B.Octets, m: B.Octets) -> String: More: https://jend.leeeet.dev/packages/bend-osdev-hashes.txt?definitions_offset=100