kdrag.contrib.cert

Functions

deserialize_proof(st)
serialize_proof(proof)

kdrag.contrib.cert.deserialize_proof(st: str) → Proof

Parameters:

st (str)

Return type:

Proof

kdrag.contrib.cert.serialize_proof(proof: Proof) → str

>>> x = smt.Int("x")
>>> assert "(assert (kd_export (kd_prove (= (+ x 1) (+ 1 x)) true)))" in serialize_proof(kernel.prove(x + 1 == 1 + x))
>>> z = kernel.define("z", [], smt.IntVal(42))
>>> _ = serialize_proof(kernel.prove(z > 0, by=[z.defn]))

Parameters:

proof (Proof)

Return type:

str