A shallow embedding of K definitions into Lean 4

[tothtamas28]

The transformation should be based on definition.kore. However, for ease of exposition, examples will be based on the .k definition.

Prelude

We need a manual Lean 4 implementation of (parts of) domains.md. The implementation should define sorts like Int and Map, functions over them, and provide useful theorems. Stubs for hooked functions, as well as non-hooked function implementations (hopefully) can be auto-generated.

We need to decide if we want to map sorts directly (e.g. K Int to Lean 4 Int), or add an extra layer (KInt.mk : Int -> KInt). In the direct mapping case, abbrev is useful for aliasing Lean 4 types:

abbrev KId := String

The mapping is obvious for some sorts, for others, we might need a custom implementation:

K	Lean 4
Bool	Bool
Int	Int
String	String
Bytes	ByteArray
List	List KItem
Set	custom?
Map	custom?

The sort K with constructors dotk : K and kseq : KItem -> K can either be modeled as List KItem, or as generated from definition.kore.

User defined sorts

syntax AExp ::= AExp "*" AExp
              > AExp "+" AExp

inductive AExp : Type where
    | mul : AExp -> AExp -> AExp
    | add : AExp -> AExp -> AExp
    deriving DecidableEq

Sorts that depend on each other should be put in a mutual block:

syntax Block ::= "{" "}"
               | "{" Stmt "}"

syntax Stmt  ::= Block
               | ...

mutual
    inductive Block : Type where
        | empty : Block
        | single : Stmt -> Block
        deriving DecidableEq

    inductive Stmt : Type where
        | inj_block : Block -> Stmt
        | ...
        deriving DecidableEq
end

It's probably fine to model user lists as List.

syntax Ids ::= List{Id, ","}

abbrev KIds := List KId

Injection

The sort of ad-hoc polymorphism provided by injections can be modeled using type classes.

class Inj (a b : Type) where ...

instance : Inj KInt AExp := ...
instance : Inj AExp KItem := ...
instance : Inj KInt KItem := ...

axiom inj {a b : Type} [Inj a b] (x : a) : b := ...

It is probably possible to define a transitivity instance to reduce the number of explicitly defined instances, but that complicates type class resolution.

Unfortunately, implementing the inj function is not straightforward. To demonstrate the problem, consider

 KItem
  / \
Bar Baz
  \ /
  Foo

Here, we need

inj{Bar,KItem} ∘ inj{Foo,Bar} = inj{Foo,KItem} = inj{Baz,KItem} ∘ inj{Foo,Baz}

Without a deeper embedding, this does not seem directly feasible, but approximations are possible.

Axiomatic approach

class Inj (a b : Type)

instance : Inj KInt AExp := {}
instance : Inj AExp KItem := {}
instance : Inj KInt KItem := {}

axiom inj {a b : Type} [Inj a b] (x : a) : b
axiom inj_tran {a b c : Type} [iab : Inj a b] [ibc : Inj b c] [iac : Inj a c] {x : a} : @inj b c ibc (@inj a b iab x) = @inj a c iac x

noncomputable example : KItem := inj (KInt.mk 0)

Here, we just assert the function and its transitivity. On the downside, all functions calling inj have to be marked noncomputable, so we lose computability.

Constructive approach

syntax AExp  ::= Int | Id
syntax KItem ::= AExp

inductive AExp : Type where
    | inj_int : KInt -> AExp
    | inj_id : KId -> AExp

inductive KItem : Type where
    | inj_int : KInt -> KItem
    | inj_id : KId -> KItem
    | inj_aexp : AExp -> KItem

instance : Inj KInt AExp where
    inj := AExp.inj_int

instance : Inj KId AExp where
    inj := AExp.inj_id

instance : Inj KInt KItem where
    inj := KItem.inj_int

instance : Inj KId KItem where
    inj := KItem.inj_id

instance : Inj AExp KItem where
    inj (x : AExp) :=
        match x with
        | AExp.inj_int n => KItem.inj_int n
        | AExp.inj_id id => KItem.inj_id id
        | _ => KItem.inj_aexp x

Here, as expected,

(inj (inj (KInt.mk 0) : AExp) : KItem) = (inj (KInt.mk 0) : KItem) = KItem.inj_int (KInt.mk 0)

On the downside, the constructors induce spurious terms like KItem.inj_aexp (AExp.inj_int (KInt.mk 0)). Since we never refer to such terms in the transition relation, this is probably acceptable.

Rewrite rules

It seems straightforward to get an overapproximation of the transition relation by neglecting rule priorities and ensures clauses (and probably other finer details we're just not aware yet).

rule <k> int (X , Xs => Xs) ; _ ... </k> <state> STATE => STATE [ X <- 0 ] </state>
  requires notBool (X in keys(STATE))

def config (k : K) (state : Map) : GeneratedTopCell :=
    GeneratedTopCell.mk (TCell.mk (KCell.mk k) (StateCell.mk state))

inductive Rewrites : GeneratedTopCell -> GeneratedTopCell -> Prop where
    | decl_nonempty {rest : K} {state : Map} {s : Stmt} {id : KId} {ids : KIds} :
        not (state.contains (inj id)) ->
        Rewrites
            (config (K.kseq (inj (Pgm.mk (id :: ids) s)) rest) state)
            (config (K.kseq (inj (Pgm.mk ids s)) rest) (state.insert (inj id) (inj (KInt.mk 0))))

Free variables become implicit arguments, requires becomes an antecedent, and the LHS and RHS are mapped directly.

Functions

Ideally, we can map K functions to Lean 4 functions. So far, this seems to be the most challenging part of the transformation. The reason for this is a discrepancy in representation. K function rules have a priority, a requires and a pattern to match. These induce if and match expressions, and the cases for the latter need to be non-overlapping and total.

We need a best effort transformation that handles at least the simple cases (like foo below). We might also be able to rewrite some functions to a form that's better suited for the transformation. For the rest of the cases, we can still generate a signature, and either handle them axiomatically (by generating theorems from simplification rules), or implement them manually.

Totality

The generated Lean 4 functions have to be total. We can handle this by returning Option from non-total functions, then expect a proof of definedness for rewrite rules:

rule foo X => X +Int 1 requires X >=Int 0
rule foo X => X -Int 1 requires X <Int  0

rule [do-foo] <state/> X => foo(X) </state>

def foo (x : KInt) : Option KInt :=
    if KInt.ge x (KInt.mk 0) then
        some (KInt.add x (KInt.mk 1))
    else if KInt.lt x (KInt.mk 0) then
        some (KInt.sub x (KInt.mk 1))
    else
        none

do-foo {x : KInt} : foo x = some y -> Rewrites (StateCell.mk x) (StateCell.mk y)

Here, we implicitly assume the requires clauses are non-overlapping (hopefully K enforces this to some extent).

Note that we could mark foo total in K. In these case, we can auto generate a proof obligation:

theorem foo_total {x : KInt} : exists (y : KInt), foo x = some y := sorry

From this, we can get the witness for taking rewrite step do-foo. An even better solution to generate inline proofs / proof stubs for fallthrough cases:

def foo (x : KInt) : Option KInt :=
    if h0 : KInt.ge x (KInt.mk 0) then
        some (KInt.add x (KInt.mk 1))
    else if h1 : KInt.lt x (KInt.mk 0) then
        some (KInt.sub x (KInt.mk 1))
    else by
        exfalso
        exact foo_total_1 h0 h1

theorem foo_total
    (h0 : not (KInt.ge x (KInt.mk 0)))
    (h1 : not (KInt.lt x (KInt.mk 0)))
: False := sorry

Then the Option wrapper and the extra implication can even be omitted:

do-foo {x : KInt} : Rewrites (StateCell.mk x) (StateCell.mk (foo x))

Code generation

The code generator should be implemented in a way that auto generated vs user supplied code is separated.

Also, code generation should be based on an internal model of the generated Lean 4 program (as opposed to appending strings directly as in ModuleToKore). In one extreme, the model is the Lean 4 abstract syntax, but full generality is not necessary for our purposes. We should check if there's a Python package that implements the Lean 4 AST.

Files representing Lean 4 abstract syntax:

• https://github.com/leanprover/lean4/blob/master/src/Lean/Expr.lean
• https://github.com/leanprover/lean4/blob/master/src/Lean/Declaration.lean

[tothtamas28]

A small script to print the AST for a .lean file:

import Lean

open Lean
open Lean.Parser

def main (args : List String): IO Unit := do
    let env ← mkEmptyEnvironment
    let fname := args.get! 0
    let tsyntax ← testParseFile env fname
    IO.println tsyntax

$ lean --run ParseModule.lean ParseModule.lean

output

(Module.module
 (Module.header [] [(Module.import "import" [] `Lean [])])
 [(Command.open "open" (Command.openSimple [`Lean]))
  (Command.open "open" (Command.openSimple [`Lean.Parser]))
  (Command.declaration
   (Command.declModifiers [] [] [] [] [] [])
   (Command.definition
    "def"
    (Command.declId `main [])
    (Command.optDeclSig
     [(Term.explicitBinder "(" [`args] [":" (Term.app `List [`String])] [] ")")]
     [(Term.typeSpec ":" (Term.app `IO [`Unit]))])
    (Command.declValSimple
     ":="
     (Term.do
      "do"
      (Term.doSeqIndent
       [(Term.doSeqItem (Term.doLetArrow "let" [] (Term.doIdDecl `env [] "←" (Term.doExpr `mkEmptyEnvironment))) [])
        (Term.doSeqItem
         (Term.doLet "let" [] (Term.letDecl (Term.letIdDecl `fname [] [] ":=" (Term.app `args.get! [(num "0")]))))
         [])
        (Term.doSeqItem
         (Term.doLetArrow
          "let"
          []
          (Term.doIdDecl `tsyntax [] "←" (Term.doExpr (Term.app `testParseFile [`env `fname]))))
         [])
        (Term.doSeqItem (Term.doExpr (Term.app `IO.println [`tsyntax])) [])]))
     (Termination.suffix [] [])
     [])
    []))])