Finite-width polynomial and SHA256 math from pinned intrinsics/math.rs and aarch64.rs. No host cryptographic approximation is used.

structure Miri.Interpreter.IntrinsicCrypto.Quad (A : Type) : Type

• a : A
• b : A
• c : A
• d : A

def Miri.Interpreter.IntrinsicCrypto.instDecidableEqQuad.decEq {A✝ : Type} [DecidableEq A✝] (x✝ x✝¹ : Quad A✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Miri.Interpreter.IntrinsicCrypto.instDecidableEqQuad {A✝ : Type} [DecidableEq A✝] : DecidableEq (Quad A✝)

Equations

• Miri.Interpreter.IntrinsicCrypto.instDecidableEqQuad = Miri.Interpreter.IntrinsicCrypto.instDecidableEqQuad.decEq

@[instance_reducible]

instance Miri.Interpreter.IntrinsicCrypto.instReprQuad {A✝ : Type} [Repr A✝] : Repr (Quad A✝)

Equations

• Miri.Interpreter.IntrinsicCrypto.instReprQuad = { reprPrec := Miri.Interpreter.IntrinsicCrypto.instReprQuad.repr }

def Miri.Interpreter.IntrinsicCrypto.instReprQuad.repr {A✝ : Type} [Repr A✝] : Quad A✝ → Nat → Std.Format

Equations

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

def Miri.Interpreter.IntrinsicCrypto.crc32 (crc : UInt32) (data : UInt64) (bits : Nat) (polynomial : ABI.U128) : Except StepError UInt32

Descending polynomial degrees reproduce the source leading-zero loop.

Equations

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

def Miri.Interpreter.IntrinsicCrypto.carryless64 (left right : UInt64) : ABI.U128

Equations

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

def Miri.Interpreter.IntrinsicCrypto.sigma0 (x : UInt32) : UInt32

Equations

• Miri.Interpreter.IntrinsicCrypto.sigma0 x = Miri.Interpreter.IntrinsicCrypto.rotr✝ x 7 ^^^ Miri.Interpreter.IntrinsicCrypto.rotr✝ x 18 ^^^ x >>> 3

def Miri.Interpreter.IntrinsicCrypto.sigma1 (x : UInt32) : UInt32

Equations

• Miri.Interpreter.IntrinsicCrypto.sigma1 x = Miri.Interpreter.IntrinsicCrypto.rotr✝ x 17 ^^^ Miri.Interpreter.IntrinsicCrypto.rotr✝ x 19 ^^^ x >>> 10

def Miri.Interpreter.IntrinsicCrypto.shaRound (abcd efgh : Quad UInt32) (wk : UInt32) : Quad UInt32 × Quad UInt32

Equations

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

def Miri.Interpreter.IntrinsicCrypto.shaHash (abcd efgh wk : Quad UInt32) : Quad UInt32 × Quad UInt32

Equations

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

def Miri.Interpreter.IntrinsicCrypto.shaSu0 (a b : Quad UInt32) : Quad UInt32

Equations

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

def Miri.Interpreter.IntrinsicCrypto.shaSu1 (a b c : Quad UInt32) : Quad UInt32

Equations

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