From 27f805b29acf11f2f3c0c52537d6355aa6fb0f27 Mon Sep 17 00:00:00 2001
From: Lydia Kondylidou <33327056+kondylidou@users.noreply.github.com>
Date: Thu, 1 Oct 2026 14:08:45 +0200
Subject: [PATCH] Encode a checked sequence operation as its total twin

`Sequence.select!`, `update!`, `take!` and `drop!` are the total variants
of `Sequence.select`, `update`, `take` and `drop`: the same function without
the bounds precondition. The SMT encoder emitted each pair as two unrelated
uninterpreted functions, so the solver could not conclude that they agree,
even for an index in bounds:

    assume Sequence.length(g) == 2;
    assert Sequence.select(g, 0) == Sequence.select!(g, 0);   // unknown

A program therefore could not use both forms on one sequence: a fact stated
with one did not apply to the other.

The encoder now emits the symbol of the total twin for both. The bounds
precondition is discharged as a separate obligation before encoding, so it is
unaffected. No axiom is added; the mirrored axiom copies become identical
terms and are deduplicated by the encoder's axiom set.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
---
 Strata/Languages/Core/SMTEncoder.lean       | 28 ++++++++++-
 StrataTest/Languages/Core/Examples/Seq.lean | 56 +++++++++++++++++++++
 2 files changed, 83 insertions(+), 1 deletion(-)

diff --git a/Strata/Languages/Core/SMTEncoder.lean b/Strata/Languages/Core/SMTEncoder.lean
index bb45ccf3ba..dae3a0841f 100644
--- a/Strata/Languages/Core/SMTEncoder.lean
+++ b/Strata/Languages/Core/SMTEncoder.lean
@@ -217,6 +217,32 @@ def lMonoTyToTermType (useArrayTheory : Bool := false) (ty : LMonoTy) : TermType
       .constr name (args.map $ lMonoTyToTermType useArrayTheory)
   | .ftvar tv => .constr tv []
 
+/-- The total twin of a checked sequence operation. -/
+private def seqTotalTwin? : String → Option String
+  | "Sequence.select" => some "Sequence.select!"
+  | "Sequence.update" => some "Sequence.update!"
+  | "Sequence.take" => some "Sequence.take!"
+  | "Sequence.drop" => some "Sequence.drop!"
+  | _ => none
+
+/--
+The solver symbol for the function named `name`.
+
+A checked sequence operation and its total twin denote the same function: they
+differ only in the bounds precondition, which is discharged as a separate
+obligation before encoding. Both are therefore encoded as one symbol, that of
+the total twin, so that a fact stated with either form applies to the other.
+-/
+private def seqSymbol (name : String) : String :=
+  match Core.NameMangling.demangleFuncName name with
+  | some (base, tys) =>
+    match seqTotalTwin? base with
+    | some twin =>
+      let stem := Core.NameMangling.monoPrefix ++ Core.NameMangling.monoDelim ++ twin
+      if tys.isEmpty then stem else stem ++ Core.NameMangling.monoDelim ++ tys
+    | none => name
+  | none => (seqTotalTwin? name).getD name
+
 /-- Convert a datatype's constructors to typed SMT constructors. -/
 private def datatypeConstructorsToSMT (d : LDatatype CoreLParams.IDMeta) (useArrayTheory : Bool := false): List SMTConstructor :=
   d.constrs.map fun c =>
@@ -627,7 +653,7 @@ def toSMTOp (factory : @Lambda.Factory CoreLParams) (fn : CoreIdent) (fnty : LMo
         let bvs := formalStrs.zip smt_intys
         let outty := tys.getLast (by exact @LMonoTy.destructArrow_non_empty fnty)
         let (smt_outty, ctx) ← LMonoTy.toSMTType outty ctx
-        let uf : UF := { id := (toString $ format fn), args := smt_intys, out := smt_outty }
+        let uf : UF := { id := seqSymbol (toString $ format fn), args := smt_intys, out := smt_outty }
         let arrowParams := func.inputs.toList.filter (fun (_, ty) => ty.containsArrow)
         if !arrowParams.isEmpty then
           let names := arrowParams.map (fun (n, _) => toString (format n))
diff --git a/StrataTest/Languages/Core/Examples/Seq.lean b/StrataTest/Languages/Core/Examples/Seq.lean
index eebc5f146f..8e546fd06c 100644
--- a/StrataTest/Languages/Core/Examples/Seq.lean
+++ b/StrataTest/Languages/Core/Examples/Seq.lean
@@ -748,5 +748,61 @@ Result: ✅ pass
 #guard_msgs in
 #eval Strata.Core.verify seqSelectBangBuildPgm
 
+-- A checked sequence operation and its total twin denote the same function, so
+-- in bounds the two agree. They are encoded as one solver symbol.
+
+private def seqCheckedTotalPgm :=
+#strata
+program Core;
+
+const g : Sequence int;
+
+procedure P()
+{
+  assume [g_len]: Sequence.length(g) == 2;
+  assert [select_pair]: Sequence.select(g, 0) == Sequence.select!(g, 0);
+  assert [update_pair]: Sequence.update(g, 0, 7) == Sequence.update!(g, 0, 7);
+  assert [take_pair]: Sequence.take(g, 1) == Sequence.take!(g, 1);
+  assert [drop_pair]: Sequence.drop(g, 1) == Sequence.drop!(g, 1);
+};
+#end
+
+/--
+info:
+Obligation: assert_select_pair_calls_Sequence.select_0
+Property: out-of-bounds access check
+Result: ✅ pass
+
+Obligation: select_pair
+Property: assert
+Result: ✅ pass
+
+Obligation: assert_update_pair_calls_Sequence.update_0
+Property: out-of-bounds access check
+Result: ✅ pass
+
+Obligation: update_pair
+Property: assert
+Result: ✅ pass
+
+Obligation: assert_take_pair_calls_Sequence.take_0
+Property: out-of-bounds access check
+Result: ✅ pass
+
+Obligation: take_pair
+Property: assert
+Result: ✅ pass
+
+Obligation: assert_drop_pair_calls_Sequence.drop_0
+Property: out-of-bounds access check
+Result: ✅ pass
+
+Obligation: drop_pair
+Property: assert
+Result: ✅ pass
+-/
+#guard_msgs in
+#eval Strata.Core.verify seqCheckedTotalPgm (options := .quiet)
+
 end
 ----------------------------------------------------------------------