datatype support for smtvcs

Strata/DL/SMT/Denote.lean

@@ -612,6 +612,31 @@ and semantics when successful.
       | none => none
     else
       none
+  -- Datatype function application: constructors/selectors/testers are lifted
+  -- into UFs during sanitization; look up by name instead of full-struct equality.
+  | .app (.datatype_op _ name) as _ =>
+    match ctx.tctx.ufs.find? (fun u => u.id == name) with
+    | none => none
+    | some uf =>
+      if hTys : (denoteFunSort ctx.sctx uf.args uf.out).isSome then
+        match h : ctx.tctx.ufs.findIdx? (· == uf) with
+        | some i =>
+          let as ← denoteTerms ctx as
+          if hufas : argTypesAlign as uf.args then
+            have hi := (List.findIdx?_eq_some_iff_findIdx_eq.mp h).left
+            have hiuf := of_decide_eq_true (List.getElem_of_findIdx?_eq_some h)
+            let ft (tdi : TermDenoteInput ctx) :=
+              have _ : i < tdi.tΓ.ufs.length := tdi.htΓ.huf.h ▸ hi
+              have hufΓ : denoteFunSort ctx.sctx uf.args uf.out = denoteFunSort ctx.sctx tdi.tΓ.ufs[i].uf.args tdi.tΓ.ufs[i].uf.out :=
+                hiuf.symm ▸ tdi.htΓ.huf.ha i hi ▸ rfl
+              @applyUF ctx uf.args uf.out hTys tdi
+                (Option.get_congr hufΓ ▸ tdi.tΓ.ufs[i].ufΓ) as hufas
+            return ⟨uf.out, denoteSortOut_isSome_of_denoteFunSort_isSome hTys, ft⟩
+          else
+            none
+        | none => none
+      else
+        none
   -- Quantifiers
   | .quant .all vs _ t =>
     if hTys : (denoteFunSort ctx.sctx vs (.prim .bool)).isSome then

Strata/DL/SMT/Translate.lean

@@ -314,6 +314,17 @@ def translateTerm (t : SMT.Term) : TranslateM (Expr × Expr) := do
     let (_, f) ← findVar (.uf uf)
     let as ← as.mapM (translateTerm · >>= pure ∘ Prod.snd)
     return (← translateSort ty, mkAppN f as.toArray)
+  | .app (.datatype_op _ name) as ty =>
+    -- Datatype functions (constructors/selectors/testers) are lifted into ufs
+    -- during sanitization, so we look them up by name.
+    let state ← get
+    let found := state.bvars.toArray.find? fun (v, _) =>
+      match v with | .uf uf => uf.id == name | _ => false
+    let (_, f) ← match found with
+      | some (.uf uf, _) => findVar (.uf uf)
+      | _ => throw m!"Error: datatype function '{name}' not found in context"
+    let as ← as.mapM (translateTerm · >>= pure ∘ Prod.snd)
+    return (← translateSort ty, mkAppN f as.toArray)
   | .quant q ns _ b =>
     let state ← get
     let translateBinder := fun v => do

Strata/MetaVerifier.lean

@@ -31,8 +31,34 @@ structure SanitizedContext where
   tySubst : Map String TermType := []
 deriving Repr, Inhabited, DecidableEq
 
+-- Convert datatypes seen during SMT encoding into sorts + UF entries so that
+-- the translate/denote paths can handle them without the full datatype machinery.
+private def datatypeUFs (ctx : Core.SMT.Context) : Array UF :=
+  ctx.typeFactory.toList.flatten.foldl (init := #[]) fun acc d =>
+    if !ctx.seenDatatypes.contains d.name then acc
+    else
+      let dtTy : TermType := .constr d.name []
+      let dtVar : TermVar := { id := "self", ty := dtTy }
+      d.constrs.foldl (init := acc) fun acc c =>
+        -- constructor: field types → datatype
+        let fieldVars := c.args.map fun (n, ty) =>
+          (TermVar.mk (d.name ++ ".." ++ n.name) (Core.lMonoTyToTermType (ty := ty)) : TermVar)
+        let constrUF : UF := { id := c.name.name, args := fieldVars, out := dtTy }
+        -- tester: datatype → bool
+        let testerUF : UF := { id := c.testerName, args := [dtVar], out := .bool }
+        -- selectors: datatype → field type (one per field)
+        let selectorUFs := c.args.map fun (n, ty) =>
+          (UF.mk (d.name ++ ".." ++ n.name) [dtVar] (Core.lMonoTyToTermType (ty := ty)) : UF)
+        acc.push constrUF |>.push testerUF |> (· ++ selectorUFs.toArray)
+
 def SanitizedContext.ofCore (ctx : Core.SMT.Context) : SanitizedContext :=
-  { sorts := ctx.sorts, ufs := ctx.ufs, ifs := ctx.ifs, axms := ctx.axms, tySubst := ctx.tySubst }
+  let dtSorts := ctx.seenDatatypes.toArray.map fun name =>
+    (Core.SMT.Sort.mk name 0 : Core.SMT.Sort)
+  { sorts := ctx.sorts ++ dtSorts
+    ufs   := ctx.ufs ++ datatypeUFs ctx
+    ifs   := ctx.ifs
+    axms  := ctx.axms
+    tySubst := ctx.tySubst }
 
 def SanitizedContext.toCore (ctx : SanitizedContext) : Core.SMT.Context :=
   { sorts := ctx.sorts

StrataTest/Languages/Boole/datatype_selector_vcs.lean

@@ -0,0 +1,65 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+
+  Regression test for `smtVCsCorrect` support for programs with user-defined
+  datatypes whose selectors appear in verification conditions.
+
+  This file tests all three fixes using a minimal program with a single-field
+  datatype `Box` whose selector `Box..val` appears both in preconditions and
+  in the postcondition.
+-/
+
+import Strata.MetaVerifier
+
+open Strata
+
+private def boxSelectorSeed : Strata.Program :=
+#strata
+program Boole;
+
+datatype Box {
+  Box_mk(val : int)
+};
+
+procedure inc_val(b : Box) returns (result : int)
+spec {
+  requires Box..val(b) >= 0;
+  ensures result == Box..val(b) + 1;
+}
+{
+  result := Box..val(b) + 1;
+  exit inc_val;
+};
+#end
+
+-- Fix 1 (SanitizedContext.ofCore) + Fix 2 (translateTerm datatype_op):
+-- `Boole.verify` via cvc5 must succeed, and `gen_smt_vcs` must not throw
+-- "datatype function not found in context".
+/-- info:
+Obligation: inc_val_pre_inc_val_requires_0_617_calls_Box..val_0
+Property: assert
+Result: ✅ pass
+
+Obligation: inc_val_post_inc_val_ensures_1_646_calls_Box..val_0
+Property: assert
+Result: ✅ pass
+
+Obligation: set_result_calls_Box..val_0
+Property: assert
+Result: ✅ pass
+
+Obligation: inc_val_ensures_1_646
+Property: assert
+Result: ✅ pass
+-/
+#guard_msgs in
+#eval Strata.Boole.verify "cvc5" boxSelectorSeed (options := .quiet)
+
+-- Fix 3 (denoteTerm datatype_op):
+-- `smtVCsCorrect` must not reduce to `False`; all 4 VCs must be provable
+-- with `gen_smt_vcs`.
+example : Strata.smtVCsCorrect boxSelectorSeed := by
+  gen_smt_vcs
+  all_goals (try grind)