Guard choose axioms and support sequence extensional equality

StrataBoole/Grammar.lean

@@ -92,7 +92,8 @@ op choose_assign (lhs : Ident, v : MonoBind, @[scope(v)] pred : bool) : Statemen
   lhs " := ε " v " :: " pred ";";
 
 // choose function declaration: `function f(params) : R := ε z . pred(z, params);`
-// Lowers to: uninterpreted function f + axiom ∀ params, ∀ z, z = f(params) → pred(z, params).
+// Lowers to: uninterpreted f + axiom ∀ params, (∃ z, pred(z, params)) →
+// (∀ z, z = f(params) → pred(z, params)). Without a witness, the result is unconstrained.
 // `@[scope(b)] v` makes b's parameter names available in v's type and (via the scope chain
 // @[scope(v)]) in pred, so pred can reference both z (bvar 0) and all params (bvars 1..n).
 @[declareFn(name, b, r)]

StrataBoole/Verify.lean

@@ -348,8 +348,21 @@ private def toCoreExtensionalEq
       let rhs := mkCoreApp Core.mapSelectOp [b, idx]
       let trigger := lhs
       return .quant () .all "" (some keyTy') trigger (.eq () lhs rhs)
+  | .Sequence _ _ =>
+      let lenEq := .eq () (mkCoreApp Core.seqLengthOp [a]) (mkCoreApp Core.seqLengthOp [b])
+      let idx : Core.Expression.Expr := .bvar () 0
+      let a := Lambda.LExpr.liftBVars 1 a
+      let b := Lambda.LExpr.liftBVars 1 b
+      let lhs := mkCoreApp Core.seqSelectUnsafeOp [a, idx]
+      let rhs := mkCoreApp Core.seqSelectUnsafeOp [b, idx]
+      let inBounds := mkCoreApp Core.boolAndOp [
+        mkCoreApp Core.intLeOp [.intConst () 0, idx],
+        mkCoreApp Core.intLtOp [idx, mkCoreApp Core.seqLengthOp [a]]]
+      let body := mkCoreApp Core.boolImpliesOp [inBounds, .eq () lhs rhs]
+      let trigger := lhs
+      return mkCoreApp Core.boolAndOp [lenEq, .quant () .all "" (some .int) trigger body]
   | _ =>
-      throwAt m s!"Extensional equality is currently only supported for Map types, got: {repr ty}"
+      throwAt m s!"Extensional equality is currently only supported for Map and Sequence types, got: {repr ty}"
 
 private def oldifyExpr (inoutNames : List String) : Core.Expression.Expr → Core.Expression.Expr
   | .fvar m ident ty =>
@@ -1062,14 +1075,12 @@ private def toCoreDecls (cmd : BooleDDM.Command SourceRange) : TranslateM (List
   | .command_choosefndef _ ⟨_, n⟩ ⟨_, targs?⟩ bs ret v pred =>
     -- `function f(params) : R := ε z :: pred(z, params)`
     -- Emits: uninterpreted function declaration + axiom
-    --   ∀ p1:T1,...,pn:Tn, ∀ z:Tz, (z = f(p1,...,pn)) → pred(z, p1,...,pn)
-    -- Note: unlike `w := ε z . pred` (which guards soundness by asserting ∃ z . pred(z)
-    -- before havocing), this form emits the axiom unconditionally. The axiom is sound only
-    -- when pred is satisfiable for all parameter values; callers must supply that guarantee
-    -- (e.g. via a `requires ∃ z . pred(z, params)` precondition).
+    --   ∀ params, (∃ z, pred(z, params)) → (∀ z, z = f(params) → pred(z, params))
+    -- The function is total; its result satisfies pred only when a witness exists.
+    -- An unsatisfiable predicate imposes no guarantee on the result.
     -- De Bruijn context for pred (from @[scope(b)] v + @[scope(v)] pred):
     --   bvar 0 = z, bvar 1 = pn (innermost param), ..., bvar n = p1 (outermost param)
-    -- This matches the 3-forall wrapping (z innermost, params outer) exactly.
+    -- Both the existential and universal bind z innermost, with params outermost.
     let tys := match targs? with | none => [] | some ts => typeArgsToList ts
     withTypeBVars tys do
       let bsList := bindingsToList bs
@@ -1082,7 +1093,7 @@ private def toCoreDecls (cmd : BooleDDM.Command SourceRange) : TranslateM (List
                 body := none, attr := #[], axioms := [] } .empty
       -- Push n+1 passthrough bvar entries (for z=bvar0, pn=bvar1, ..., p1=bvar n) so that
       -- getBVarExpr doesn't throw. Passthrough entries return the original index unchanged,
-      -- so pred's natural de Bruijn indices are preserved exactly as needed by the 3-forall.
+      -- so pred's natural de Bruijn indices are preserved in both branches of the guard.
       let bvarPassthroughs := Array.range (numParams + 1) |>.map (.bvar () ·)
       let predCore ← withBVarExprs bvarPassthroughs (toCoreExpr pred)
       -- f(p1,...,pn): p1 = bvar n (outermost), p2 = bvar n-1, ..., pn = bvar 1 (innermost param)
@@ -1092,10 +1103,14 @@ private def toCoreDecls (cmd : BooleDDM.Command SourceRange) : TranslateM (List
           (.op () (mkIdent n) none)
       let zEqF : Core.Expression.Expr := .eq () (.bvar () 0) funcCallBvar
       let axiomInner := mkCoreApp Core.boolImpliesOp [zEqF, predCore]
-      -- Wrap ∀ p1:T1,...,∀ pn:Tn, ∀ z:Tz using foldr (z innermost = processed first by foldr)
-      let allTys := (inputs.map Prod.snd) ++ [vTy]
-      let axiomExpr := allTys.foldr (fun ty acc =>
-        .quant () .all "" (some ty) (.bvar () 0) acc) axiomInner
+      -- Both branches bind their own z; parameter indices stay unchanged.
+      let existsExpr : Core.Expression.Expr :=
+        .quant () .exist "" (some vTy) (.bvar () 0) predCore
+      let choiceExpr : Core.Expression.Expr :=
+        .quant () .all "" (some vTy) (.bvar () 0) axiomInner
+      let guardedChoice := mkCoreApp Core.boolImpliesOp [existsExpr, choiceExpr]
+      let axiomExpr := (inputs.map Prod.snd).foldr (fun ty acc =>
+        .quant () .all "" (some ty) (.bvar () 0) acc) guardedChoice
       let axiomDecl : Core.Decl :=
         .ax { name := s!"{n}_choose_axiom", e := axiomExpr } .empty
       return [funcDecl, axiomDecl]

StrataBooleTest/FeatureRequests/choose_operator.lean

@@ -84,15 +84,13 @@ Result: ✅ pass-/
 
 `function f(params) : R := ε z . pred(z, params);` declares an uninterpreted
 function `f` together with the axiom:
-  ∀ params, ∀ z, z = f(params) → pred(z, params)
+  ∀ params, (∃ z, pred(z, params)) → (∀ z, z = f(params) → pred(z, params))
 
 This lets a specification define a function by its property rather than its
 implementation — similar to Verus choose-based spec functions.
 
-Note: unlike `w := ε z . pred(z)` (which guards soundness with an existence
-assertion), the function form emits the axiom unconditionally. The user must
-ensure `pred` is satisfiable for all inputs (e.g. via a precondition) to avoid
-an unsound axiom.
+The function is total even when no witness exists. To conclude that its result
+satisfies `pred`, establish existence, for example with a precondition.
 -/
 
 private def chooseFnSeed : StrataDDM.Program :=
@@ -115,15 +113,14 @@ spec {
 #end
 
 /-- info:
-Obligation: test_choose_fn_ensures_1_2749
+Obligation: test_choose_fn_ensures_1_2680
 Property: assert
 Result: ✅ pass-/
 #guard_msgs in
 #eval Strata.Boole.verify "cvc5" chooseFnSeed (options := .quiet)
 
--- Without the ∃ precondition the ensures still passes, because the axiom
--- `∀ z, z = best(x) → good(z, x)` unconditionally asserts good(best(x), x).
--- This demonstrates that soundness relies on the caller supplying the witness.
+-- Without the ∃ precondition, the guarded axiom does not establish good(best(x), x).
+-- The solver must not report a pass without an existence fact.
 private def chooseFnNoPrecondSeed : StrataDDM.Program :=
 #strata
 program Boole;
@@ -143,8 +140,75 @@ spec {
 #end
 
 /-- info:
-Obligation: test_no_precond_ensures_0_3444
+Obligation: test_no_precond_ensures_0_3290
 Property: assert
-Result: ✅ pass-/
+Result: ❓ unknown-/
 #guard_msgs in
 #eval Strata.Boole.verify "cvc5" chooseFnNoPrecondSeed (options := .quiet)
+
+/-!
+The guarded choice law holds for an arbitrary predicate.
+-/
+private def chooseGuardedAxiomSpec : StrataDDM.Program :=
+#strata
+program Boole;
+
+type R;
+type P;
+
+function pred(z: R, params: P) : bool;
+
+function f(params: P) : R :=
+  ε z: R . pred(z, params);
+
+procedure choice_guarded_axiom() returns ()
+spec {
+  ensures ∀ params: P .
+    ((∃ z: R . pred(z, params)) ==>
+     (∀ z: R . z == f(params) ==> pred(z, params)));
+}
+{
+};
+#end
+
+/-- info:
+Obligation: choice_guarded_axiom_ensures_0_3837
+Property: assert
+Result: ✅ pass-/
+#guard_msgs in
+#eval Strata.Boole.verify "cvc5" chooseGuardedAxiomSpec
+  (options := .quiet)
+
+/-!
+The old unconditional choice law admits a countermodel.
+
+The constant-false predicate supplies the witness, on abstract types.
+The cover checks that the exact negation of the old law is satisfiable
+under the generated axioms. An inconsistent axiom cannot pass it.
+-/
+private def chooseOldAxiomCountermodelSpec : StrataDDM.Program :=
+#strata
+program Boole;
+
+type R;
+type P;
+
+function unsat_pred(z: R, params: P) : bool { false }
+
+function f(params: P) : R :=
+  ε z: R . unsat_pred(z, params);
+
+procedure choice_old_axiom_has_countermodel() returns ()
+{
+  cover !(∀ params: P . ∀ z: R .
+    z == f(params) ==> unsat_pred(z, params));
+};
+#end
+
+/-- info:
+Obligation: cover_0_4714
+Property: cover
+Result: ✅ pass-/
+#guard_msgs in
+#eval Strata.Boole.verify "cvc5" chooseOldAxiomCountermodelSpec
+  (options := .quiet)

StrataBooleTest/FeatureRequests/map_extensionality.lean

@@ -18,7 +18,7 @@ Near-upstream anchors from `differential_status.md`:
 - Original gap: extensional equality lowered to ordinary equality
 - Current status: implemented for direct `Map` types via Boole `=~=`
 - Lowering: `a =~= b` becomes `∀ i . a[i] == b[i]`
-- Remaining gap: named map synonyms and non-map extensional equality
+- Remaining gap: named map synonyms and higher-order extensional equality
 -/
 
 private def mapExtensionalitySeed : StrataDDM.Program :=
@@ -39,11 +39,11 @@ spec {
 #end
 
 /-- info:
-Obligation: assert_2_983
+Obligation: assert_2_988
 Property: assert
 Result: ✅ pass
 
-Obligation: map_extensionality_seed_ensures_1_960
+Obligation: map_extensionality_seed_ensures_1_965
 Property: assert
 Result: ✅ pass-/
 #guard_msgs in
@@ -116,3 +116,30 @@ private def expectedQuantifiedMapExtensionalityCapture : Core.Expression.Expr :=
       (.quant () .all "" (some .int) lhs (.eq () lhs rhs)))
 
 #guard loweredQuantifiedMapExtensionalityCapture? == some expectedQuantifiedMapExtensionalityCapture
+
+/-
+For any element type `T` and any sequences `a` and `b`, `a =~= b` exactly when
+they have equal length and in-bounds pointwise equality via `Sequence.select!`.
+-/
+
+private def seqExtensionalitySeed : StrataDDM.Program :=
+#strata
+program Boole;
+
+procedure seq_ext_spec<T>(a: Sequence T, b: Sequence T) returns ()
+spec {
+  ensures (a =~= b) <==>
+    (Sequence.length(a) == Sequence.length(b) &&
+     (∀ i: int . 0 <= i && i < Sequence.length(a) ==>
+        Sequence.select!(a, i) == Sequence.select!(b, i)));
+}
+{
+};
+#end
+
+/-- info:
+Obligation: seq_ext_spec_ensures_0_4004
+Property: assert
+Result: ✅ pass-/
+#guard_msgs in
+#eval Strata.Boole.verify "cvc5" seqExtensionalitySeed (options := .quiet)