feat(Core): add Bv{n}.ToUInt, Bv{n}.ToInt, Int.ToBv{n} cast operators

Add three cross-sort conversion operators to Core:
- Bv{n}.ToUInt : Bv{n} → Int  (SMT-LIB ubv_to_int)
- Bv{n}.ToInt  : Bv{n} → Int  (SMT-LIB sbv_to_int)
- Int.ToBv{n}  : Int → Bv{n}  (SMT-LIB int_to_bv n)

Supported widths: 1, 8, 16, 32, 64, 128. All three are total.

Changes:
- Core DDMTransform/Grammar: as_uint, as_sint, as_bv{1..128} built-in funcs
- Core DDMTransform/Translate: dispatch for the new grammar functions
- DL/SMT/Translate: handle bv2nat / sbv2int / int_to_bv
- editors/vscode: regenerated syntax highlighting
- BvIntCastVerifyTests.lean: rewritten using new function syntax

Split from #1218.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: 2 people

Strata/DL/SMT/Translate.lean

@@ -534,11 +534,13 @@ def translateTerm (t : SMT.Term) : TranslateM (Expr × Expr) := do
     let w ← getBitVecWidth α
     return (mkBitVec (w + i), mkApp3 (.const ``BitVec.zeroExtend []) (toExpr w) (toExpr (w + i)) x)
   | .app .ubv_to_int [x] _ =>
-    let (_, x) ← translateTerm x
-    return (mkInt, mkApp (.const ``Int.ofNat []) (mkApp (.const ``BitVec.toNat []) x))
+    let (α, x) ← translateTerm x
+    let w ← getBitVecWidth α
+    return (mkInt, mkApp (.const ``Int.ofNat []) (mkApp2 (.const ``BitVec.toNat []) (toExpr w) x))
   | .app .sbv_to_int [x] _ =>
-    let (_, x) ← translateTerm x
-    return (mkInt, mkApp (.const ``BitVec.toInt []) x)
+    let (α, x) ← translateTerm x
+    let w ← getBitVecWidth α
+    return (mkInt, mkApp2 (.const ``BitVec.toInt []) (toExpr w) x)
   | .app (.int_to_bv n) [x] _ =>
     let (_, x) ← translateTerm x
     return (mkBitVec n, mkApp2 (.const ``BitVec.ofInt []) (toExpr n) x)

Strata/Languages/Core/DDMTransform/Grammar.lean

@@ -93,6 +93,15 @@ fn bv16Lit (n : Num) : bv16 => "bv{16}" "(" n ")";
 fn bv32Lit (n : Num) : bv32 => "bv{32}" "(" n ")";
 fn bv64Lit (n : Num) : bv64 => "bv{64}" "(" n ")";
 fn bv128Lit (n : Num) : bv128 => "bv{128}" "(" n ")";
+
+fn as_uint  (T : Type, e : T) : int  => "as_uint"  "(" e ")";
+fn as_sint  (T : Type, e : T) : int  => "as_sint"  "(" e ")";
+fn as_bv1   (e : int) : bv1   => "as_bv1"   "(" e ")";
+fn as_bv8   (e : int) : bv8   => "as_bv8"   "(" e ")";
+fn as_bv16  (e : int) : bv16  => "as_bv16"  "(" e ")";
+fn as_bv32  (e : int) : bv32  => "as_bv32"  "(" e ")";
+fn as_bv64  (e : int) : bv64  => "as_bv64"  "(" e ")";
+fn as_bv128 (e : int) : bv128 => "as_bv128" "(" e ")";
 fn strLit (s : Str) : string => s;
 fn realLit (d : Decimal) : real => d;
 

Strata/Languages/Core/DDMTransform/Translate.lean

@@ -715,6 +715,9 @@ def translateFn (ty? : Option LMonoTy) (q : QualifiedIdent) : TransM Core.Expres
   | .some .bv64, q`Core.bv_usub_overflow => return Core.bv64USubOverflowOp
   | .some .bv64, q`Core.bv_umul_overflow => return Core.bv64UMulOverflowOp
 
+  | .some (.bitvec n), q`Core.as_uint => return .op () ⟨s!"Bv{n}.ToUInt", ()⟩ (.some (.arrow (.bitvec n) .int))
+  | .some (.bitvec n), q`Core.as_sint => return .op () ⟨s!"Bv{n}.ToInt",  ()⟩ (.some (.arrow (.bitvec n) .int))
+
   | _, q`Core.str_len      => return Core.strLengthOp
   | _, q`Core.str_concat   => return Core.strConcatOp
   | _, q`Core.str_substr   => return Core.strSubstrOp
@@ -878,6 +881,24 @@ partial def translateExpr (p : Program) (bindings : TransBindings) (arg : Arg) :
     let fn : LExpr Core.CoreLParams.mono ←
       translateFn (.some tp) q`Core.bvnot
     return (.app () fn x)
+  -- Bv → Int casts
+  | .fn _ q`Core.as_uint, [tpa, xa] =>
+    let tp ← translateLMonoTy bindings (dealiasTypeArg p tpa)
+    let x ← translateExpr p bindings xa
+    let fn ← translateFn (.some tp) q`Core.as_uint
+    return .app () fn x
+  | .fn _ q`Core.as_sint, [tpa, xa] =>
+    let tp ← translateLMonoTy bindings (dealiasTypeArg p tpa)
+    let x ← translateExpr p bindings xa
+    let fn ← translateFn (.some tp) q`Core.as_sint
+    return .app () fn x
+  -- Int → Bv casts
+  | .fn _ q`Core.as_bv1,   [xa] => return .app () (.op () ⟨"Int.ToBv1",   ()⟩ (.some (.arrow .int (.bitvec 1))))   (← translateExpr p bindings xa)
+  | .fn _ q`Core.as_bv8,   [xa] => return .app () (.op () ⟨"Int.ToBv8",   ()⟩ (.some (.arrow .int (.bitvec 8))))   (← translateExpr p bindings xa)
+  | .fn _ q`Core.as_bv16,  [xa] => return .app () (.op () ⟨"Int.ToBv16",  ()⟩ (.some (.arrow .int (.bitvec 16))))  (← translateExpr p bindings xa)
+  | .fn _ q`Core.as_bv32,  [xa] => return .app () (.op () ⟨"Int.ToBv32",  ()⟩ (.some (.arrow .int (.bitvec 32))))  (← translateExpr p bindings xa)
+  | .fn _ q`Core.as_bv64,  [xa] => return .app () (.op () ⟨"Int.ToBv64",  ()⟩ (.some (.arrow .int (.bitvec 64))))  (← translateExpr p bindings xa)
+  | .fn _ q`Core.as_bv128, [xa] => return .app () (.op () ⟨"Int.ToBv128", ()⟩ (.some (.arrow .int (.bitvec 128)))) (← translateExpr p bindings xa)
   -- If-then-else expression
   | .fn _ q`Core.if, [_tpa, ca, ta, fa] =>
     let c ← translateExpr p bindings ca

StrataTest/Languages/Core/Tests/BvIntCastVerifyTests.lean

@@ -3,40 +3,71 @@
 
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
+module
 
-import Strata.Languages.Core.Verifier
-import Strata.Languages.Core.Factory
-import Strata.SimpleAPI
+meta import Strata.Languages.Core
+import StrataDDM.Integration.Lean.HashCommands
 
 /-!
-End-to-end verification tests for the three Bv↔Int cast operators,
-exercised all the way through the SMT pipeline via `Strata.Core.verifyProgram`.
+End-to-end verification tests for the three Bv↔Int cast built-in functions,
+exercised all the way through the SMT pipeline via `Core.verify`.
 
-Factory ops (`Bv{n}.ToUInt`, `Bv{n}.ToInt`, `Int.ToBv{n}`) cannot be called
-from `#strata program Core;` text, so programs are constructed programmatically
-using the Lean API.
-
-- `Bv{n}.ToUInt` ≙ SMT-LIB 2.7 `ubv_to_int`  — unsigned bv → Int
-- `Bv{n}.ToInt`  ≙ SMT-LIB 2.7 `sbv_to_int`  — signed bv → Int
-- `Int.ToBv{n}`  ≙ SMT-LIB 2.7 `(_ int_to_bv n)` — Int → bv
+- `as_uint(e)` ≙ SMT-LIB 2.7 `ubv_to_int`  — unsigned bv → Int
+- `as_sint(e)` ≙ SMT-LIB 2.7 `sbv_to_int`  — signed bv → Int
+- `as_bv8(e)`  ≙ SMT-LIB 2.7 `(_ int_to_bv 8)` — Int → bv8
 -/
 
-namespace Core.BvIntCastVerify
-
-open Lambda Core
-
-private def xBv8   : Expression.Expr := .fvar () ⟨"x", ()⟩ (.some (.bitvec 8))
-private def bv8255 : Expression.Expr := .bitvecConst () 8 (255 : BitVec 8)
-
-private def zero   : Expression.Expr := .intConst () 0
-private def i255   : Expression.Expr := .intConst () 255
-private def i256   : Expression.Expr := .intConst () 256
-private def negOne : Expression.Expr := .intConst () (-1)
-
-private def applyGe (l r : Expression.Expr) : Expression.Expr :=
-  .app () (.app () intGeOp l) r
-
-private def mkProc (name : String) (postcond : Expression.Expr) : Decl :=
+meta section
+open Strata
+open StrataDDM (Program)
+
+private def bvIntCastProgram : Program :=
+#strata
+program Core;
+
+procedure test_ubv_nonneg(x : bv8)
+spec {
+  ensures as_uint(x) >= 0;
+}
+{
+  assume true;
+};
+
+procedure test_ubv_concrete()
+spec {
+  ensures as_uint(bv{8}(255)) == 255;
+}
+{
+  assume true;
+};
+
+procedure test_ubv_roundtrip(x : bv8)
+spec {
+  ensures as_bv8(as_uint(x)) == x;
+}
+{
+  assume true;
+};
+
+procedure test_sbv_concrete()
+spec {
+  ensures as_sint(bv{8}(255)) == -1;
+}
+{
+  assume true;
+};
+
+procedure test_ubv_impossible(x : bv8)
+spec {
+  ensures as_uint(x) >= 256;
+}
+{
+  assume true;
+};
+
+#end
+
+private def mkProc (name : String) (postcond : Core.Expression.Expr) : Core.Decl :=
   .proc {
     header := {
       name     := ⟨name, ()⟩
@@ -51,25 +82,6 @@ private def mkProc (name : String) (postcond : Expression.Expr) : Decl :=
     body := .structured [.assume "body" (.true ()) #[]]
   } #[]
 
-private def castVerifyProg : Core.Program :=
-  { decls := [
-      -- Provable: Bv8.ToUInt is always nonneg
-      mkProc "test_ubv_nonneg"
-        (applyGe (.app () bv8ToUIntFunc.opExpr xBv8) zero),
-      -- Provable: concrete value bv{8}(255) as unsigned == 255
-      mkProc "test_ubv_concrete"
-        (.eq () (.app () bv8ToUIntFunc.opExpr bv8255) i255),
-      -- Provable: unsigned round-trip Int.ToBv8(Bv8.ToUInt(x)) == x
-      mkProc "test_ubv_roundtrip"
-        (.eq () (.app () int8ToBvFunc.opExpr (.app () bv8ToUIntFunc.opExpr xBv8)) xBv8),
-      -- Provable: signed semantics bv{8}(255) as signed == -1
-      mkProc "test_sbv_concrete"
-        (.eq () (.app () bv8ToIntFunc.opExpr bv8255) negOne),
-      -- Failing: Bv8.ToUInt(x) >= 256 is impossible for 8-bit
-      mkProc "test_ubv_impossible"
-        (applyGe (.app () bv8ToUIntFunc.opExpr xBv8) i256),
-    ] }
-
 /--
 info:
 Obligation: test_ubv_nonneg_ensures_0
@@ -93,9 +105,4 @@ Property: assert
 Result: ❌ fail
 -/
 #guard_msgs in
-#eval show IO Unit from do
-  let results ← EIO.toIO (fun e => IO.Error.userError e)
-    (Strata.Core.verifyProgram castVerifyProg Core.VerifyOptions.quiet)
-  IO.println (toString results)
-
-end Core.BvIntCastVerify
+#eval Strata.Core.verify bvIntCastProgram (options := .quiet)

editors/vscode/syntaxes/core-st.tmLanguage.json

@@ -79,7 +79,7 @@
         },
         {
           "name": "keyword.operator.symbol.core-st",
-          "match": "(safe_neg|safe-|safe\\+|safe\\*|<==>|>=s|==>|>>s|<=s|/t|\\|\\||>=|%t|<<|>>|&&|<=|==|!=|<s|>s|>|\\^|\\+|\\*|/|%|!|-|~|&|<|\\|)"
+          "match": "(safe_neg|as_bv128|as_bv32|as_bv64|as_sint|as_bv16|as_uint|as_bv1|as_bv8|safe-|safe\\+|safe\\*|<==>|>=s|==>|>>s|<=s|!=|/t|%t|<<|>>|&&|\\|\\||==|<s|<=|>=|>s|!|\\^|-|\\+|\\*|/|%|<|>|~|&|\\|)"
         }
       ]
     },