K Prelude in Lean 4

Functions with the hook attribute need to have a manual implementation in the backends. This file contains the Lean 4 definitions of the hooked functions in domains.md.

Currently we translate hooked functions as uninterpreted functions together with axioms asserting their behavior. The current definition can be put into three levels:

1. Signature Level: The signature of the hooks, this includes aliases for Sorts and function symbols for hooked functions.

2. Rule Level: The behavior of the uninterpreted symbols can be asserted through axioms or theorems. Inconsistencies can arise from them, so it falls under the user to make sure axioms are consistent and/or theorems provable.

3. Simplification Level: With the theory defined through function rules, simplifications can be stated as theorems. These theorems should be provable directly from the function rules and the semantics of the Sorts.

Basic K types

Abbreviations

@[reducible, inline]

abbrev SortBool : Type

Equations

• SortBool = Bool

@[reducible, inline]

abbrev SortBytes : Type

Equations

• SortBytes = ByteArray

@[reducible, inline]

abbrev SortId : Type

Equations

• SortId = String

@[reducible, inline]

abbrev SortInt : Type

Equations

• SortInt = Int

@[reducible, inline]

abbrev SortString : Type

Equations

• SortString = String

@[reducible, inline]

abbrev SortStringBuffer : Type

Equations

• SortStringBuffer = String

Inductives

inductive SortEndianness : Type

• bigEndianBytes : SortEndianness
• littleEndianBytes : SortEndianness

instance instBEqSortEndianness : BEq SortEndianness

Equations

• instBEqSortEndianness = { beq := beqSortEndianness✝ }

instance instDecidableEqSortEndianness : DecidableEq SortEndianness

Equations

• instDecidableEqSortEndianness x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

inductive SortSignedness : Type

• signedBytes : SortSignedness
• unsignedBytes : SortSignedness

instance instBEqSortSignedness : BEq SortSignedness

Equations

• instBEqSortSignedness = { beq := beqSortSignedness✝ }

instance instDecidableEqSortSignedness : DecidableEq SortSignedness

Equations

• instDecidableEqSortSignedness x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

structure MapHookSig (K V : Type) : Type

• unit : List (K × V)
• cons : K → V → List (K × V) → List (K × V)
• lookup : List (K × V) → K → Option V
• lookup? : List (K × V) → K → V
• update : K → V → List (K × V) → List (K × V)
• delete : List (K × V) → K → List (K × V)
• concat : List (K × V) → List (K × V) → Option (List (K × V))
• difference : List (K × V) → List (K × V) → List (K × V)
• updateMap : List (K × V) → List (K × V) → List (K × V)
• removeAll : List (K × V) → List K → List (K × V)
• keys : List (K × V) → List K
• in_keys : List (K × V) → K → Bool
• values : List (K × V) → List V
• size : List (K × V) → Nat
• includes : List (K × V) → List (K × V) → Bool
• choice : List (K × V) → K
• split : List (K × V) → List K → Option (List V × List (K × V))

axiom MapHookDef.unitAx (K V : Type) : List (K × V)

axiom MapHookDef.consAx (K V : Type) : K → V → List (K × V) → List (K × V)

axiom MapHookDef.lookupAx (K V : Type) : List (K × V) → K → Option V

axiom MapHookDef.lookupAx? (K V : Type) : List (K × V) → K → V

axiom MapHookDef.updateAx (K V : Type) : K → V → List (K × V) → List (K × V)

axiom MapHookDef.deleteAx (K V : Type) : List (K × V) → K → List (K × V)

axiom MapHookDef.concatAx (K V : Type) : List (K × V) → List (K × V) → Option (List (K × V))

axiom MapHookDef.differenceAx (K V : Type) : List (K × V) → List (K × V) → List (K × V)

axiom MapHookDef.updateMapAx (K V : Type) : List (K × V) → List (K × V) → List (K × V)

axiom MapHookDef.removeAllAx (K V : Type) : List (K × V) → List K → List (K × V)

axiom MapHookDef.keysAx (K V : Type) : List (K × V) → List K

axiom MapHookDef.in_keysAx (K V : Type) : List (K × V) → K → Bool

axiom MapHookDef.valuesAx (K V : Type) : List (K × V) → List V

axiom MapHookDef.sizeAx (K V : Type) : List (K × V) → Nat

axiom MapHookDef.includesAx (K V : Type) : List (K × V) → List (K × V) → Bool

axiom MapHookDef.choiceAx (K V : Type) : List (K × V) → K

axiom MapHookDef.splitAx (K V : Type) : List (K × V) → List K → Option (List V × List (K × V))

noncomputable def MapHook (K V : Type) : MapHookSig K V

Equations

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

structure SetHookSig (T : Type) : Type

• unit : List T
• concat : List T → List T → Option (List T)
• element : T → List T
• union : List T → List T → List T
• intersection : List T → List T → List T
• difference : List T → List T → List T
• inSet : T → List T → Bool
• inclusion : List T → List T → Bool
• size : List T → Int
• choice : List T → T
• split : List T → List T → Option (List T)

axiom SetHookDef.unitAx (T : Type) : List T

axiom SetHookDef.concatAx (T : Type) : List T → List T → Option (List T)

axiom SetHookDef.elementAx (T : Type) : T → List T

axiom SetHookDef.unionAx (T : Type) : List T → List T → List T

axiom SetHookDef.intersectionAx (T : Type) : List T → List T → List T

axiom SetHookDef.differenceAx (T : Type) : List T → List T → List T

axiom SetHookDef.inSetAx (T : Type) : T → List T → Bool

axiom SetHookDef.inclusionAx (T : Type) : List T → List T → Bool

axiom SetHookDef.sizeAx (T : Type) : List T → Int

axiom SetHookDef.choiceAx (T : Type) : List T → T

axiom SetHookDef.splitAx (T : Type) : List T → List T → Option (List T)

noncomputable def SetHook (T : Type) : SetHookSig T

Equations

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

structure listHookSig (T : Type) : Type

• unit : List T
• concat : List T → List T → Option (List T)
• element : T → List T
• push : T → List T → List T
• get : Int → List T → Option T
• updte : Int → T → List T → Option (List T)
• make : Int → T → Option (List T)
• updateAll : List T → Int → List T → Option (List T)
• fill : List T → Int → T → Option (List T)
• range : List T → Int → Int → Option (List T)
• inList : T → List T → Bool
• size : List T → Int
• split : List T → Nat → Nat → Option (List T × List T × List T)

axiom ListHookDef.unitAx (T : Type) : List T

axiom ListHookDef.concatAx (T : Type) : List T → List T → Option (List T)

axiom ListHookDef.elementAx (T : Type) : T → List T

axiom ListHookDef.pushAx (T : Type) : T → List T → List T

axiom ListHookDef.getAx (T : Type) : Int → List T → Option T

axiom ListHookDef.updteAx (T : Type) : Int → T → List T → Option (List T)

axiom ListHookDef.makeAx (T : Type) : Int → T → Option (List T)

axiom ListHookDef.updateAllAx (T : Type) : List T → Int → List T → Option (List T)

axiom ListHookDef.fillAx (T : Type) : List T → Int → T → Option (List T)

axiom ListHookDef.rangeAx (T : Type) : List T → Int → Int → Option (List T)

axiom ListHookDef.inListAx (T : Type) : T → List T → Bool

axiom ListHookDef.sizeAx (T : Type) : List T → Int

axiom ListHookDef.splitAx (T : Type) : List T → Nat → Nat → Option (List T × List T × List T)

noncomputable def ListHook (T : Type) : listHookSig T

Equations

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

Inj class

class Inj (From To : Type) : Type

• inj (x : From) : To
• retr (x : To) : Option From

def inj {From To : Type} [inst : Inj From To] (x : From) : To

Equations

• inj = Inj.inj

def retr {From To : Type} [inst : Inj From To] (x : To) : Option From

Equations

• retr = Inj.retr

Instances

Unrelated to the Inj class

instance instBEqUInt8_evmEquivalence : BEq UInt8

Equations

• instBEqUInt8_evmEquivalence = { beq := fun (a b : UInt8) => decide (a = b) }

instance instBEqSortBytes : BEq SortBytes

Equations

• instBEqSortBytes = { beq := fun (a b : SortBytes) => ByteArray.toList a == ByteArray.toList b }

def ByteArray.decEq (a b : ByteArray) : Decidable (a = b)

Equations

• { data := { toList := al } }.decEq { data := { toList := bl } } = match al.hasDecEq bl with | isTrue t => isTrue ⋯ | isFalse f => isFalse ⋯

instance instDecidableEqSortBytes : DecidableEq SortBytes

Equations

• instDecidableEqSortBytes = ByteArray.decEq

Function Implementations

SortInt

Operations

def «maxInt(_,_)_INT-COMMON_Int_Int_Int» (x0 x1 : SortInt) : Option SortInt

Equations

• «maxInt(_,_)_INT-COMMON_Int_Int_Int» x0 x1 = some (if x0 < x1 then x1 else x0)

def «log2Int(_)_INT-COMMON_Int_Int» (x0 : SortInt) : Option SortInt

Equations

• «log2Int(_)_INT-COMMON_Int_Int» x0 = if 0 < x0 then some ↑(Int.toNat x0).log2 else none

def «~Int_» (x0 : SortInt) : Option SortInt

Equations

• «~Int_» x0 = some (Int.not x0)

Comparisons

SortBytes

def «.Bytes_BYTES-HOOKED_Bytes» : Option SortBytes

Equations

• «.Bytes_BYTES-HOOKED_Bytes» = some ByteArray.empty

Int to Bytes conversion

def «Int2Bytes(_,_,_)_BYTES-HOOKED_Bytes_Int_Int_Endianness» (x0 x1 : SortInt) (x2 : SortEndianness) : Option SortBytes

Adapted from https://github.com/runtimeverification/haskell-backend/blob/362dab30d6435ec117862fea722be67373572034/kore/src/Kore/Builtin/InternalBytes.hs#L496-L511

Equations

• «Int2Bytes(_,_,_)_BYTES-HOOKED_Bytes_Int_Int_Endianness» x0 x1 SortEndianness.littleEndianBytes = some («Int2Bytes(_,_,_)_BYTES-HOOKED_Bytes_Int_Int_Endianness».littleEndian x0 x1).toByteArray
• «Int2Bytes(_,_,_)_BYTES-HOOKED_Bytes_Int_Int_Endianness» x0 x1 SortEndianness.bigEndianBytes = some («Int2Bytes(_,_,_)_BYTES-HOOKED_Bytes_Int_Int_Endianness».littleEndian x0 x1).reverse.toByteArray

def «Int2Bytes(_,_,_)_BYTES-HOOKED_Bytes_Int_Int_Endianness».littleEndian (x0 x1 : SortInt) : List UInt8

Equations

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

def «Int2Bytes(_,_,_)_BYTES-HOOKED_Bytes_Int_Int_Endianness».littleEndian.bytes (pad : UInt8) (len : Nat) (n : Int) : List UInt8

Equations

• One or more equations did not get rendered due to their size.
• «Int2Bytes(_,_,_)_BYTES-HOOKED_Bytes_Int_Int_Endianness».littleEndian.bytes pad 0 n = []
• «Int2Bytes(_,_,_)_BYTES-HOOKED_Bytes_Int_Int_Endianness».littleEndian.bytes pad l.succ 0 = pad :: «Int2Bytes(_,_,_)_BYTES-HOOKED_Bytes_Int_Int_Endianness».littleEndian.bytes pad l 0

def «Bytes2Int(_,_,_)_BYTES-HOOKED_Int_Bytes_Endianness_Signedness» (bytes : SortBytes) (endian : SortEndianness) (sign : SortSignedness) : Option SortInt

Adapted from https://github.com/runtimeverification/haskell-backend/blob/362dab30d6435ec117862fea722be67373572034/kore/src/Kore/Builtin/InternalBytes.hs#L527-L543 Note that we use List.foldl and not ByteArray.foldl for ease of reasoning

Equations

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

def «Bytes2Int(_,_,_)_BYTES-HOOKED_Int_Bytes_Endianness_Signedness».modulus (bytes : SortBytes) (endian : SortEndianness) : Nat

Equations

• «Bytes2Int(_,_,_)_BYTES-HOOKED_Int_Bytes_Endianness_Signedness».modulus bytes endian = («Bytes2Int(_,_,_)_BYTES-HOOKED_Int_Bytes_Endianness_Signedness».res bytes endian).fst

def «Bytes2Int(_,_,_)_BYTES-HOOKED_Int_Bytes_Endianness_Signedness».unsigned (bytes : SortBytes) (endian : SortEndianness) : Nat

Equations

• «Bytes2Int(_,_,_)_BYTES-HOOKED_Int_Bytes_Endianness_Signedness».unsigned bytes endian = («Bytes2Int(_,_,_)_BYTES-HOOKED_Int_Bytes_Endianness_Signedness».res bytes endian).snd

def «Bytes2Int(_,_,_)_BYTES-HOOKED_Int_Bytes_Endianness_Signedness».res (bytes : SortBytes) (endian : SortEndianness) : Nat × Nat

Equations

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

Bytes manipulation

def «padRightBytes(_,_,_)_BYTES-HOOKED_Bytes_Bytes_Int_Int» (b : SortBytes) (len val : SortInt) : Option SortBytes

Pads to the right len - b.length bytes with specified val value

Equations

• «padRightBytes(_,_,_)_BYTES-HOOKED_Bytes_Bytes_Int_Int» b len val = if val < 0 ∨ 255 < val then none else some { data := Array.rightpad (Int.toNat len) { toBitVec := ↑(Int.toNat val) } b.data }

def «padLeftBytes(_,_,_)_BYTES-HOOKED_Bytes_Bytes_Int_Int» (b : SortBytes) (len val : SortInt) : Option SortBytes

Pads to the left len - b.length bytes with specified val value

Equations

• «padLeftBytes(_,_,_)_BYTES-HOOKED_Bytes_Bytes_Int_Int» b len val = if val < 0 ∨ 255 < val then none else some { data := Array.leftpad (Int.toNat len) { toBitVec := ↑(Int.toNat val) } b.data }

def «lengthBytes(_)_BYTES-HOOKED_Int_Bytes» (x0 : SortBytes) : Option SortInt

Equations

• «lengthBytes(_)_BYTES-HOOKED_Int_Bytes» x0 = some (Int.ofNat (ByteArray.size x0))

def «replaceAtBytes(_,_,_)_BYTES-HOOKED_Bytes_Bytes_Int_Bytes» (dest : SortBytes) (index : SortInt) (src : SortBytes) : Option SortBytes

Replaces the contents of dest from index index with the contents of src If dest.size < index + src.size the result is none

Equations

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

def «substrBytes(_,_,_)_BYTES-HOOKED_Bytes_Bytes_Int_Int» (b : SortBytes) (startIndex endIndex : SortInt) : Option SortBytes

Get a new Bytes object containing a range of bytes from the input Bytes

Equations

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