~/bend-docscommunity

proofs/crypto/aes/sbox.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/sbox.bend as Sbox

3 imports
import Base
import ../../../src/crypto/aes/sbox.bend as B
import ../../../spec/crypto/aes/aes.bend as S

Laws

law sbox_byte_bits provedsource · line 8 · raw

@+b0:Bool -> @+b1:Bool -> @+b2:Bool -> @+b3:Bool -> @+b4:Bool -> @+b5:Bool -> @+b6:Bool -> @+b7:Bool -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/sbox.sbox(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.sbox(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WCon{False{}, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}) : U32}

law sbox_bits provedsource · line 534 · raw

@+b0:Bool -> @+b1:Bool -> @+b2:Bool -> @+b3:Bool -> @+b4:Bool -> @+b5:Bool -> @+b6:Bool -> @+b7:Bool -> @+b8:Bool -> @+b9:Bool -> @+b10:Bool -> @+b11:Bool -> @+b12:Bool -> @+b13:Bool -> @+b14:Bool -> @+b15:Bool -> @+b16:Bool -> @+b17:Bool -> @+b18:Bool -> @+b19:Bool -> @+b20:Bool -> @+b21:Bool -> @+b22:Bool -> @+b23:Bool -> @+b24:Bool -> @+b25:Bool -> @+b26:Bool -> @+b27:Bool -> @+b28:Bool -> @+b29:Bool -> @+b30:Bool -> @+b31:Bool -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/sbox.sbox(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.sbox(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}) : U32}

law sbox_ok provedsource · line 573 · raw

@+x:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/sbox.sbox(x) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.sbox(x) : U32}

law xtime_bits provedsource · line 582 · raw

@b0:Bool -> @b1:Bool -> @b2:Bool -> @b3:Bool -> @b4:Bool -> @b5:Bool -> @b6:Bool -> @b7:Bool -> @b8:Bool -> @b9:Bool -> @b10:Bool -> @b11:Bool -> @b12:Bool -> @b13:Bool -> @b14:Bool -> @b15:Bool -> @b16:Bool -> @b17:Bool -> @b18:Bool -> @b19:Bool -> @b20:Bool -> @b21:Bool -> @b22:Bool -> @b23:Bool -> @b24:Bool -> @b25:Bool -> @b26:Bool -> @b27:Bool -> @b28:Bool -> @b29:Bool -> @b30:Bool -> @b31:Bool -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/sbox.xtime(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.mul(2, U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}) : U32}

law xtime_ok provedsource · line 1132 · raw

@+x:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/sbox.xtime(x) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.mul(2, x) : U32}

law mul3_bits provedsource · line 1141 · raw

@b0:Bool -> @b1:Bool -> @b2:Bool -> @b3:Bool -> @b4:Bool -> @b5:Bool -> @b6:Bool -> @b7:Bool -> @b8:Bool -> @b9:Bool -> @b10:Bool -> @b11:Bool -> @b12:Bool -> @b13:Bool -> @b14:Bool -> @b15:Bool -> @b16:Bool -> @b17:Bool -> @b18:Bool -> @b19:Bool -> @b20:Bool -> @b21:Bool -> @b22:Bool -> @b23:Bool -> @b24:Bool -> @b25:Bool -> @b26:Bool -> @b27:Bool -> @b28:Bool -> @b29:Bool -> @b30:Bool -> @b31:Bool -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/sbox.mul3(U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.mul(3, U32{WCon{b0, WCon{b1, WCon{b2, WCon{b3, WCon{b4, WCon{b5, WCon{b6, WCon{b7, WCon{b8, WCon{b9, WCon{b10, WCon{b11, WCon{b12, WCon{b13, WCon{b14, WCon{b15, WCon{b16, WCon{b17, WCon{b18, WCon{b19, WCon{b20, WCon{b21, WCon{b22, WCon{b23, WCon{b24, WCon{b25, WCon{b26, WCon{b27, WCon{b28, WCon{b29, WCon{b30, WCon{b31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}) : U32}

law mul3_ok provedsource · line 1691 · raw

@+x:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/sbox.mul3(x) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.mul(3, x) : U32}