You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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:
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
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
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))
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 foototal 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:
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.
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
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 likeInt
andMap
, 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 4Int
), or add an extra layer (KInt.mk : Int -> KInt
). In the direct mapping case,abbrev
is useful for aliasing Lean 4 types:The mapping is obvious for some sorts, for others, we might need a custom implementation:
Bool
Bool
Int
Int
String
String
Bytes
ByteArray
List
List KItem
Set
Map
The sort
K
with constructorsdotk : K
andkseq : KItem -> K
can either be modeled asList KItem
, or as generated fromdefinition.kore
.User defined sorts
Sorts that depend on each other should be put in a
mutual
block:It's probably fine to model user lists as
List
.Injection
The sort of ad-hoc polymorphism provided by injections can be modeled using type classes.
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, considerHere, we need
Without a deeper embedding, this does not seem directly feasible, but approximations are possible.
Axiomatic approach
Here, we just assert the function and its transitivity. On the downside, all functions calling
inj
have to be markednoncomputable
, so we lose computability.Constructive approach
Here, as expected,
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).
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 induceif
andmatch
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 fromsimplification
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: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: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:Then the
Option
wrapper and the extra implication can even be omitted: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:
The text was updated successfully, but these errors were encountered: