diff --git a/Strata/DL/SMT/Denote.lean b/Strata/DL/SMT/Denote.lean index d1b84925d8..a035eeeb61 100644 --- a/Strata/DL/SMT/Denote.lean +++ b/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 diff --git a/Strata/DL/SMT/Translate.lean b/Strata/DL/SMT/Translate.lean index 1b761271b0..24a8d7ea4e 100644 --- a/Strata/DL/SMT/Translate.lean +++ b/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 diff --git a/Strata/MetaVerifier.lean b/Strata/MetaVerifier.lean index c841f4c107..84021e4511 100644 --- a/Strata/MetaVerifier.lean +++ b/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 diff --git a/StrataTest/Languages/Boole/datatype_selector_vcs.lean b/StrataTest/Languages/Boole/datatype_selector_vcs.lean new file mode 100644 index 0000000000..efd0c612fe --- /dev/null +++ b/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)