feat(Boole): SMT-LIB 2.7 cast operators (as_int, as_sint, as_bv{n})

[kondylidou]

Summary

Implements all three SMT-LIB 2.7 cast operators end-to-end in the Boole language,
covering the full pipeline from grammar syntax to SMT-LIB 2 serialization.

New operators

Boole syntax	Semantics	Core op	SMT-LIB 2.7
e as_int	unsigned bv → Int	Bv{n}.ToUInt	ubv_to_int
e as_sint	signed bv → Int (two's complement)	Bv{n}.ToInt	sbv_to_int
e as_bv{n}	Int → bv (truncating mod 2^n)	Int.ToBv{n}	(_ int_to_bv n)

Supported widths: 1, 8, 16, 32, 64, 128.

Implementation layers touched

• Grammar (Boole/Grammar.lean): 9 new grammar rules with @[prec(80)] so casts bind tighter than comparisons.
• Lowering (Boole/Verify.lean): bvWidth helper dispatches to Bv{n}.ToUInt / Bv{n}.ToInt; Int.ToBv{n} for the reverse direction. Type errors (as_sint on int, as_int on Map, etc.) produce descriptive messages.
• Core ops (Core/CoreOp.lean): ToUInt and ToInt added to BvOpKind; intToBv (n : Nat) added as a top-level CoreOp (source type is Int, not BitVec).
• Factory (Core/Factory.lean): bvToUIntFunc, bvToIntFunc, intToBvFunc registered for all 6 widths (18 new entries, factory count 292 → 304).
• SMT encoding (Core/SMTEncoder.lean): maps Core ops to Op.ubv_to_int, Op.sbv_to_int, Op.int_to_bv.
• SMT-LIB serialization (DL/SMT/DDMTransform/Translate.lean): int_to_bv uses iden_indexed pattern (_ int_to_bv n), matching zero_extend.
• Lean kernel (DL/SMT/Translate.lean, Denote.lean): denotations use BitVec.toNat (unsigned), BitVec.toInt (signed), BitVec.ofInt n (int→bv).

Naming

BvOpKind.ToUInt (unsigned bv → Int) and BvOpKind.ToInt (signed bv → Int) follow
the SMT-LIB ubv_to_int / sbv_to_int naming convention and are symmetric with each other.

Tests

• cast_all_directions.lean: 7 obligations covering all 3 cast directions, round-trip, and sign-agreement.
• cast_errors.lean: 3 #guard tests verifying descriptive error messages for invalid cast sources.
• cast_expr.lean, widening_casts.lean: updated obligation IDs and ToNat→ToUInt comment fixes.
• ProgramEvalTests.lean, StatisticsTest.lean: updated for renamed ops and new factory entries.

Closes

Gap 6 in BooleFeatureRequests.md.

[joscoh]

Maybe subsumed by the discussion at the meeting, but this axiomatization is unsound even without mixed nat-int constructors:

private def minimalGlobalUnsound : Strata.Program :=
#strata
program Boole;

type nat := int;

datatype NatBox { MkBox(value: nat) };

procedure minus_one_is_nonneg(n: int) returns ()
spec {
  requires n == -1;
  ensures false;
} {
  exit minus_one_is_nonneg;
};
#end

/-- info: Obligation: minus_one_is_nonneg_ensures_1_837
Property: assert
Result: ✅ pass-/
#guard_msgs in
#eval Strata.Boole.verify "cvc5" minimalGlobalUnsound (options := .quiet)