prop idea. casting. emt tactics. pcode proof state

Author: philzook58

src/kdrag/cast.py

@@ -0,0 +1,51 @@
+import kdrag.smt as smt
+
+cast_table = {}
+
+
+def cast(s: smt.SortRef, e: object) -> smt.ExprRef:
+    if isinstance(e, smt.ExprRef):
+        s1 = e.sort()
+        if s1.eq(s):
+            return e
+        else:
+            key = (s, e.sort())
+    else:
+        key = (s, type(e))
+    coerce = cast_table.get(key)
+    if coerce is not None:
+        return coerce(e)
+    else:
+        # if isinstance(e, smt.SeqRef):
+        # elif isinstance(e, smt.ArraySortRef):
+        return s.cast(e)
+
+
+def cast_dt(dt: smt.DatatypeSortRef, e: smt.DatatypeRef) -> smt.DatatypeRef:
+    """
+    Simple field name based downcasting between two struct-like datatypes
+
+    """
+    dt1 = e.sort()
+    assert dt1.num_constructors() == 1 and dt.num_constructors() == 1
+    constr, constr1 = dt.constructor(0), dt1.constructor(0)
+    assert constr.arity() <= constr1.arity()
+    args = []
+    for i in range(constr.arity()):
+        acc = dt.accessor(0, i)
+        args.append(getattr(e, acc.name()))  # TODO:  consider extra cast here
+    return constr(*args)
+
+
+"""
+def coerce_exprs(a, b):
+    return smt._coerce_exprs(a, b)
+
+
+def coerce_expr_merge(s: smt.SortRef, a: smt.ExprRef):
+    return smt._coerce_expr_merge(s, a)
+"""
+
+
+def subsort(s: smt.SortRef, t: smt.SortRef) -> bool:
+    return s.subsort(t)

src/kdrag/contrib/pcode/__init__.py

@@ -460,6 +460,13 @@ def __init__(self, filename=None, langid="x86:LE:64:default"):
         self.definitions.extend(
             [bv.store_concats(self.bits, size, le=le) for size in [16, 32, 64]]
         )
+        # Helpers
+        self.select16 = bv.select_concats(self.bits, 16, le=le)
+        self.select32 = bv.select_concats(self.bits, 32, le=le)
+        self.select64 = bv.select_concats(self.bits, 64, le=le)
+        self.store16 = bv.store_concats(self.bits, 16, le=le)
+        self.store32 = bv.store_concats(self.bits, 32, le=le)
+        self.store64 = bv.store_concats(self.bits, 64, le=le)
         if filename is not None:
             self.load(filename)
 

src/kdrag/contrib/pcode/asmspec.py

@@ -605,10 +605,16 @@ def run_all_paths(
 
 
 class VCProofState(kd.tactics.ProofState):
-    def __init__(self, vc: VerificationCondition, ctx: pcode.BinaryContext):
+    def __init__(
+        self, vc: VerificationCondition, ctx: pcode.BinaryContext, _parent=None
+    ):
         self.vc = vc
         self.binctx = ctx
-        super().__init__(kd.tactics.Goal(sig=[], ctx=[], goal=vc.vc(ctx)))
+        super().__init__(
+            kd.tactics.Goal(sig=[], ctx=[], goal=vc.vc(ctx)), _parent=_parent
+        )
+        # self.intros()
+        # self.split(at=0)
 
     def auto(self, **kwargs):
         try:
@@ -623,21 +629,61 @@ def auto(self, **kwargs):
                 self.vc.countermodel(self.binctx, countermodel),
             )
 
+    def __repr__(self):
+        return super().__repr__() + f"\n\nfrom VC: {self.vc}"
+
+
+class AsmProofState:
+    def __init__(self, ctx: pcode.BinaryContext, spec: AsmSpec):
+        self.ctx = ctx
+        self.spec = spec
+        # self._spec = spec.copy() # TODO copy
+        mem = self.ctx.init_mem()
+        tracestates, vcs = init_trace_states(self.ctx, mem, self.spec)
+        while tracestates:
+            tracestate = tracestates.pop()
+            new_tracestates, new_vcs = execute_spec_and_insn(
+                tracestate, self.spec, self.ctx
+            )
+            vcs.extend(new_vcs)
+            tracestates.extend(new_tracestates)
+        self.vcs = tuple(vcs)
+        self.pfs = []
+
+    def auto(self, n, **kwargs):
+        vc = self.vcs[n]
+        self.pfs.append(vc.verify(self.ctx, **kwargs))
+
+    def lemma(self, n) -> VCProofState:
+        return VCProofState(self.vcs[n], self.ctx, _parent=self)
+
+    def exact(self, pf: kd.Proof):
+        # it's goofy, but this is the current ProofState api
+        self.pfs.append(pf)
+
+    def qed(self):
+        assert len(self.vcs) == len(self.pfs)
+        assert all(
+            isinstance(pf, kd.Proof) and pf.thm.eq(vc.vc(self.ctx))
+            for vc, pf in zip(self.vcs, self.pfs)
+        )
+
 
 class Debug:
     def __init__(
-        self, ctx: pcode.BinaryContext, spec: Optional[AsmSpec] = None, verbose=True
+        self,
+        ctx: pcode.BinaryContext,
+        spec: AsmSpec = AsmSpec(),
+        verbose=True,
     ):
         self.ctx = ctx
-        if spec is None:
-            self.spec = AsmSpec()
-        else:
-            self.spec: AsmSpec = spec
+        self.spec: AsmSpec = spec
         self.tracestates: list[TraceState] = []
         self.vcs: list[VerificationCondition] = []
         self.breakpoints = set()
         self.verbose = verbose
         self._cur_model = None
+        self.pfs = []
 
     def spec_file(self, filename: str):
         self.spec = AsmSpec.of_file(filename, self.ctx)
@@ -723,16 +769,15 @@ def pop_run(self):
 
     def pop_verify(self, **kwargs):
         vc = self.vcs.pop()
-        vc.verify(self.ctx, **kwargs)
+        self.pfs.append((vc, vc.verify(self.ctx, **kwargs)))
 
     def verify(self, **kwargs):
         if not self.vcs:
             raise Exception("No verification conditions to verify")
         if self.tracestates:
             raise Exception("There are still trace states to execute")
         while self.vcs:
-            vc = self.vcs.pop(0)
-            vc.verify(self.ctx, **kwargs)
+            self.pop_verify(**kwargs)
 
     def pop_lemma(self) -> kd.tactics.ProofState:
         vc = self.vcs.pop()

src/kdrag/smt.py

@@ -468,7 +468,10 @@ def DeclareSort(name):
         return sort_registry[tid]
 
 
+# Implicit tags for properties
 ExprRef.assumes = None
+ExprRef.prop = None
+FuncDeclRef.prop = None
 
 
 type FuncRef = ArrayRef | QuantifierRef

src/kdrag/tactics.py

@@ -14,6 +14,7 @@
 from dataclasses import dataclass
 import kdrag.parsers.microlean as microlean
 import kdrag.reflect as reflect
+import kdrag.solvers.egraph as egraph
 
 
 def FreshVar(name: str, sort: smt.SortRef, assume=None) -> smt.ExprRef:
@@ -717,6 +718,35 @@ def simp(self, at=None, unfold=False, path=None) -> "ProofState":
             )
         return self
 
+    def emt(self):
+        """
+        Use egraph based equality modulo theories to simplify the goal.
+        >>> x, y, z, w = smt.Ints("x y z w")
+        >>> l = Lemma(smt.Implies(x + y + 1 == z, x + y + 1 == w))
+        >>> l.intros()
+        [x + y + 1 == z] ?|= x + y + 1 == w
+        >>> l.emt()
+        [x + y + 1 == z] ?|= z == w
+
+        """
+        goalctx = self.top_goal()
+        ctx, goal = goalctx.ctx, goalctx.goal
+        E = egraph.EGraph()
+        E.solver.add(ctx)
+        E.add_term(goal)
+        for c in ctx:
+            E.add_term(c)
+        E.rebuild()
+        newgoal = E.extract(goal)
+        if newgoal.eq(goal):
+            raise ValueError("EMT failed. Goal is already in simplest form.", goal)
+        else:
+            self.add_lemma(
+                kd.kernel.prove(smt.Implies(smt.And(ctx), smt.Eq(goal, newgoal)))
+            )
+            self.goals[-1] = goalctx._replace(goal=newgoal)
+            return self
+
     def cases(self, t):
         """
         `cases` let's us consider an object by cases.

src/kdrag/tele.py

@@ -1,8 +1,16 @@
+"""
+Refinement subtyping
+
+- https://www.philipzucker.com/refinement_kdrag1/ Semantic Refinement/Dependent Typing for Knuckledragger/SMTLIB Pt 1
+- https://belle.sourceforge.net/doc/subtypes.pdf Predicate Subtyping with Predicate Sets - Joe Hurd
+
+"""
+
 import kdrag.smt as smt
 import kdrag as kd
 import functools
 
-type SubSort = smt.QuantifierRef | smt.ArrayRef
+type SubSort = smt.FuncRef
 type Type = SubSort
 # User telescope
 """