kdrag.printers.rust

Functions

`compile_rust`(fun_name, fun_code[, dir])
`datatype_sort`(s)
`init_proj`([proj_path])
`mangle_name`(name)	Mangle a name to be a valid Rust identifier >>> mangle_name("my-fun") 'my_KDHYPH_fun' >>> mangle_name("my.fun") 'my_KDDOT_fun'
`of_expr`(e)
`of_sort`(s)
`rust_module_template`(modname, fun_name, fun_code)

Classes

VerusModule(name, datatypes, spec_funs, ...)

class kdrag.printers.rust.VerusModule(name: str, datatypes: list[z3.z3.DatatypeSortRef] = <factory>, spec_funs: dict[str, tuple[list[z3.z3.ExprRef], z3.z3.ExprRef]] = <factory>, proof_funs: dict[str, tuple[list[z3.z3.ExprRef], z3.z3.BoolRef]] = <factory>)

Bases: object

Parameters:

name (str)
datatypes (list[DatatypeSortRef])
spec_funs (dict[str, tuple[list[ExprRef], ExprRef]])
proof_funs (dict[str, tuple[list[ExprRef], BoolRef]])

add_defn(f: FuncDeclRef)

Parameters:: f (FuncDeclRef)

check(filename, verus_binary='verus'): Write module to file and check with Verus >>> m = VerusModule(“testmod”) >>> x = smt.Int(“x”) >>> m.spec_funs[“myabs”] = ([x], smt.If(x >= 0, x, -x)) >>> myabs = smt.Function(“myabs”, smt.IntSort(), smt.IntSort()) >>> m.proof_funs[“myabs_nonneg”] = ([x], myabs(x) >= 0)

datatypes: list[DatatypeSortRef]

name: str

proof_funs: dict[str, tuple[list[ExprRef], BoolRef]]

spec_funs: dict[str, tuple[list[ExprRef], ExprRef]]

to_str()

write(filename): Write module to file

kdrag.printers.rust.compile_rust(fun_name, fun_code, dir='/tmp/kdrag_rust')

kdrag.printers.rust.datatype_sort(s: DatatypeSortRef) → str

>>> datatype_sort(kd.TupleSort(smt.IntSort(), smt.BoolSort()))
'struct Tuple_Int_Bool { _0 : int, _1 : bool }'
>>> datatype_sort(kd.ListSort(smt.IntSort()))
'enum List_Int { Nil {  }, Cons { head : int, tail : List_Int } }'

Parameters:: s (DatatypeSortRef)
Return type:: str

kdrag.printers.rust.init_proj(proj_path='/tmp/kdrag_rust')

kdrag.printers.rust.mangle_name(name: str) → str

Mangle a name to be a valid Rust identifier >>> mangle_name(“my-fun”) ‘my_KDHYPH_fun’ >>> mangle_name(“my.fun”) ‘my_KDDOT_fun’

Parameters:: name (str)
Return type:: str

kdrag.printers.rust.of_expr(e: ExprRef) → str

>>> of_expr(smt.IntVal(5))
'5'
>>> of_expr(smt.BitVecVal(255, 8))
'0xff'
>>> of_expr(smt.Or(smt.BoolVal(True), smt.BoolVal(False)))
'(true || false)'
>>> of_expr(smt.And(smt.BoolVal(True), smt.BoolVal(False)))
'(true && false)'
>>> of_expr(smt.Not(smt.BoolVal(True)))
'(!true)'
>>> of_expr(smt.Int("x"))
'x'
>>> of_expr(smt.If(smt.Int("x") > 0, smt.Int("x"), -smt.Int("x")))
'(if (x > 0) { x } else { (-x) })'

Parameters:: e (ExprRef)
Return type:: str

kdrag.printers.rust.of_sort(s: SortRef) → str

>>> of_sort(smt.SeqSort(smt.BitVecSort(8)))
'Seq<u8>'
>>> of_sort(smt.IntSort())
'int'
>>> of_sort(smt.BoolSort())
'bool'
>>> of_sort(smt.ArraySort(smt.IntSort(), smt.BoolSort()))
'Set<int>'

Parameters:: s (SortRef)
Return type:: str

kdrag.printers.rust.rust_module_template(modname: str, fun_name: str, fun_code: str)

Parameters:

modname (str)
fun_name (str)
fun_code (str)