proofs/crypto/aes/inverse.bend checks

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

import Base
import ../../../spec/crypto/aes/aes.bend as S
import ../../lib/logic.bend as L

Laws

@+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 -> @+h:{U32.is_eq(U32.and(255, 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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}), 0) == False{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.mul(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.inverse(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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}})) == 1 : U32}

@+x:U32 -> @+h:{U32.is_eq(U32.and(255, x), 0) == False{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.mul(x, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.inverse(x)) == 1 : U32}

{0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.inverse(0) == 0 : U32}