choose operator in Boole

StrataBoole/StrataBoole/Grammar.lean

@@ -64,11 +64,25 @@ op boole_procedure (name : Ident,
 //     datatype testers) so the DDM never sees a bare dot between identifiers.
 // ─────────────────────────────────────────────────────────────────────────────
 
-// choose assignment: `w := choose z : T :: pred(z);`
+// choose assignment: `w := ε z : T . pred(z);`
 // Lowers to: `assert ∃ z : T . pred(z); havoc w; assume pred[z/w];`
-// Uses `" :: "` (not `" . "`) to avoid the id.id ambiguity above.
+// The `. ` separator is normalized to `::` before parsing (see StrataDDM.Elab).
+// Both forms are accepted; `::` still works as well.
 op choose_assign (lhs : Ident, v : MonoBind, @[scope(v)] pred : bool) : Statement =>
-  lhs " := choose " v " :: " pred ";";
+  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).
+// `@[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)]
+op command_choosefndef (name : Ident,
+                        typeArgs : Option TypeArgs,
+                        @[scope(typeArgs)] b : Bindings,
+                        @[scope(typeArgs)] r : Type,
+                        @[scope(b)] v : MonoBind,
+                        @[scope(v)] pred : bool) : Command =>
+  "function " name typeArgs b " : " r " :=\n  ε " v " :: " pred ";\n";
 
 // Boole keeps the `call lhs := f(args)` syntax for calls with outputs.
 // Unit calls (no outputs) use Core's `call_statement` with `callArgExpr` args.

StrataBoole/StrataBoole/Verify.lean

@@ -998,6 +998,46 @@ def toCoreDecls (cmd : BooleDDM.Command SourceRange) : TranslateM (List Core.Dec
   | .command_fndef m ⟨_, n⟩ ⟨_, targs?⟩ bs ret ⟨_, pres⟩ body ⟨_, inline?⟩ =>
     let tys := match targs? with | none => [] | some ts => typeArgsToList ts
     return [.func (← lowerPureFuncDef m n tys bs ret pres body inline?.isSome) .empty]
+  | .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).
+    -- 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.
+    let tys := match targs? with | none => [] | some ts => typeArgsToList ts
+    withTypeBVars tys do
+      let bsList := bindingsToList bs
+      let inputs ← bsList.mapM toCoreBinding
+      let retTy ← toCoreMonoType ret
+      let (_, vTy) ← toCoreMonoBind v
+      let numParams := bsList.length
+      let funcDecl : Core.Decl :=
+        .func { name := mkIdent n, typeArgs := tys, inputs := inputs, output := retTy,
+                body := none, concreteEval := 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.
+      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)
+      let funcCallBvar : Core.Expression.Expr :=
+        (List.range numParams).foldl (fun acc i =>
+          .app () acc (.bvar () (numParams - i)))
+          (.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
+      let axiomDecl : Core.Decl :=
+        .ax { name := s!"{n}_choose_axiom", e := axiomExpr } .empty
+      return [funcDecl, axiomDecl]
   | .command_recfndefs _ ⟨_, funcs⟩ =>
     -- Mirror the DDM elaborator's @[declareFn] sibling-bvar accumulation:
     -- the i-th function's body sees the i preceding siblings as bvars.

StrataBoole/StrataBooleTest/FeatureRequests/choose_operator.lean

@@ -13,7 +13,7 @@ Near-upstream anchors from `differential_status.md`:
 - `verus-examples:trigger_loops` (`choose_example`, `quantifier_example`)
 - Verus link:
   `trigger_loops`: https://github.com/verus-lang/verus/blob/main/examples/trigger_loops.rs
-- Status: implemented — `w := choose z: T :: pred(z)` desugars to:
+- Status: implemented — `w := ε z: T . pred(z)` desugars to:
     assert ∃ z : T . pred(z);   -- existence obligation (soundness guard)
     havoc w;
     assume pred[z/w];
@@ -33,16 +33,16 @@ spec {
   ensures good(w, x);
 }
 {
-  w := choose z: int :: good(z, x);
+  w := ε z: int . good(z, x);
 };
 #end
 
 /-- info:
-Obligation: choose_2_884_exists
+Obligation: choose_2_879_exists
 Property: assert
 Result: ✅ pass
 
-Obligation: choose_seed_ensures_1_858
+Obligation: choose_seed_ensures_1_853
 Property: assert
 Result: ✅ pass-/
 #guard_msgs in
@@ -64,17 +64,87 @@ spec {
   ensures true;
 }
 {
-  w := choose z: int :: z != z;
+  w := ε z: int . z != z;
 };
 #end
 
 /-- info:
-Obligation: choose_1_1613_exists
+Obligation: choose_1_1603_exists
 Property: assert
 Result: ❌ fail
 
-Obligation: choose_unsat_ensures_0_1593
+Obligation: choose_unsat_ensures_0_1583
 Property: assert
 Result: ✅ pass-/
 #guard_msgs in
 #eval Strata.Boole.verify "cvc5" chooseUnsatSeed (options := .quiet)
+
+/-!
+## choose-function declarations
+
+`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)
+
+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.
+-/
+
+private def chooseFnSeed : StrataDDM.Program :=
+#strata
+program Boole;
+
+function good(z: int, x: int) : bool;
+
+function best(x: int) : int :=
+  ε z : int . good(z, x);
+
+procedure test_choose_fn(x: int) returns (w: int)
+spec {
+  requires ∃ z: int :: good(z, x);
+  ensures good(w, x);
+}
+{
+  w := best(x);
+};
+#end
+
+/-- info:
+Obligation: test_choose_fn_ensures_1_2749
+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.
+private def chooseFnNoPrecondSeed : StrataDDM.Program :=
+#strata
+program Boole;
+
+function good(z: int, x: int) : bool;
+
+function best(x: int) : int :=
+  ε z : int . good(z, x);
+
+procedure test_no_precond(x: int) returns (w: int)
+spec {
+  ensures good(w, x);
+}
+{
+  w := best(x);
+};
+#end
+
+/-- info:
+Obligation: test_no_precond_ensures_0_3444
+Property: assert
+Result: ✅ pass-/
+#guard_msgs in
+#eval Strata.Boole.verify "cvc5" chooseFnNoPrecondSeed (options := .quiet)

StrataDDM/StrataDDM/Elab.lean

@@ -45,9 +45,9 @@ private inductive QuantifierSepState where
 | sawColon
 
 /--
-Canonicalize the legacy dotted Unicode quantifier separator to `::` before DDM
-parsing. This keeps `#strata` generic while accepting both `∀ x . P` and
-`∀ x :: P`.
+Canonicalize dotted binder separators to `::` before DDM parsing.
+Handles Unicode quantifiers (`∀`, `∃`, `ε`): `Q x . P` → `Q x :: P`.
+Both `x . P` and `x :: P` forms remain accepted.
 -/
 private def normalizeUnicodeQuantifierSeparators (src : String) : String :=
   (src.foldl
@@ -56,22 +56,15 @@ private def normalizeUnicodeQuantifierSeparators (src : String) : String :=
       let (acc, qstate) := st
       match qstate with
       | .outside =>
-        if ch == '∀' || ch == '∃' then
-          (acc.push ch, .inBinder)
-        else
-          (acc.push ch, .outside)
+        if ch == '∀' || ch == '∃' || ch == 'ε' then (acc.push ch, .inBinder)
+        else (acc.push ch, .outside)
       | .inBinder =>
-        if ch == '.' then
-          (acc ++ "::", .outside)
-        else if ch == ':' then
-          (acc.push ch, .sawColon)
-        else
-          (acc.push ch, .inBinder)
+        if ch == '.' then (acc ++ "::", .outside)
+        else if ch == ':' then (acc.push ch, .sawColon)
+        else (acc.push ch, .inBinder)
       | .sawColon =>
-        if ch == ':' then
-          (acc.push ch, .outside)
-        else
-          (acc.push ch, .inBinder))).fst
+        if ch == ':' then (acc.push ch, .outside)
+        else (acc.push ch, .inBinder))).fst
 
 private def normalizeInputContext (inputContext : InputContext) : InputContext :=
   let inputString := normalizeUnicodeQuantifierSeparators inputContext.inputString
@@ -80,22 +73,15 @@ private def normalizeInputContext (inputContext : InputContext) : InputContext :
 private def normalizedQuantifierSepStep (state : QuantifierSepState) (ch : Char) : Nat × QuantifierSepState :=
   match state with
   | .outside =>
-    if ch == '∀' || ch == '∃' then
-      (ch.utf8Size, .inBinder)
-    else
-      (ch.utf8Size, .outside)
+    if ch == '∀' || ch == '∃' || ch == 'ε' then (ch.utf8Size, .inBinder)
+    else (ch.utf8Size, .outside)
   | .inBinder =>
-    if ch == '.' then
-      ("::".utf8ByteSize, .outside)
-    else if ch == ':' then
-      (ch.utf8Size, .sawColon)
-    else
-      (ch.utf8Size, .inBinder)
+    if ch == '.' then ("::".utf8ByteSize, .outside)
+    else if ch == ':' then (ch.utf8Size, .sawColon)
+    else (ch.utf8Size, .inBinder)
   | .sawColon =>
-    if ch == ':' then
-      (ch.utf8Size, .outside)
-    else
-      (ch.utf8Size, .inBinder)
+    if ch == ':' then (ch.utf8Size, .outside)
+    else (ch.utf8Size, .inBinder)
 
 /--
 Translate a byte position in the original input to the corresponding byte