Direct u32 fixslice hazmat port from pinned aes 0.9.3. The library supports u32/u64 backends; this implements its concrete u32 software circuit, not a replacement AES specification. Cross-backend equivalence remains a QA obligation.

@[reducible, inline]

abbrev Miri.Interpreter.IntrinsicX86.Aes.State : Type

Rust's fixed [u32; 8], materialized after each assignment. A function-valued state would re-evaluate the predecessor swap circuit on every lane access.

Equations

• Miri.Interpreter.IntrinsicX86.Aes.State = Vector UInt32 8

@[instance_reducible]

instance Miri.Interpreter.IntrinsicX86.Aes.instCoeFunStateForallFinOfNatNatUInt32 : CoeFun State fun (x : State) => Fin 8 → UInt32

Equations

• Miri.Interpreter.IntrinsicX86.Aes.instCoeFunStateForallFinOfNatNatUInt32 = { coe := fun (state : Miri.Interpreter.IntrinsicX86.Aes.State) (index : Fin 8) => state[index] }

def Miri.Interpreter.IntrinsicX86.Aes.subBytes (state : State) : State

Equations

• One or more equations did not get rendered due to their size.

def Miri.Interpreter.IntrinsicX86.Aes.invSubBytes (state : State) : State

Equations

• One or more equations did not get rendered due to their size.

def Miri.Interpreter.IntrinsicX86.Aes.subBytesNots (state : State) : State

Equations

• One or more equations did not get rendered due to their size.

def Miri.Interpreter.IntrinsicX86.Aes.bitsliceSwaps (state : State) : State

Equations

• One or more equations did not get rendered due to their size.

def Miri.Interpreter.IntrinsicX86.Aes.bitslice (block : ABI.U128) : State

Equations

• One or more equations did not get rendered due to their size.

def Miri.Interpreter.IntrinsicX86.Aes.invBitslice (state : State) : ABI.U128

Equations

• One or more equations did not get rendered due to their size.

def Miri.Interpreter.IntrinsicX86.Aes.shiftRows (inverse : Bool) (state : State) : State

Equations

• One or more equations did not get rendered due to their size.

def Miri.Interpreter.IntrinsicX86.Aes.mixColumnsState (state : State) : State

Equations

• One or more equations did not get rendered due to their size.

def Miri.Interpreter.IntrinsicX86.Aes.invMixColumnsState (state : State) : State

Equations

• One or more equations did not get rendered due to their size.

def Miri.Interpreter.IntrinsicX86.Aes.mixColumns (inverse : Bool) (block : ABI.U128) : ABI.U128

Equations

• One or more equations did not get rendered due to their size.

def Miri.Interpreter.IntrinsicX86.Aes.round (inverse : Bool) (block key : ABI.U128) : ABI.U128

Equations

• One or more equations did not get rendered due to their size.