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

[kondylidou]

Adds three cross-sort conversion operators to Core, as proposed in #1191.
Split from the original PR per reviewer request — Core layer only.
Boole surface syntax follows in a separate PR.

Operators

Core name	SMT-LIB 2.7	Lean	Direction
Bv{n}.ToUInt	ubv_to_int	BitVec.toNat	bv → int (unsigned)
Bv{n}.ToInt	sbv_to_int	BitVec.toInt	bv → int (signed, two's complement)
Int.ToBv{n}	(_ int_to_bv n)	BitVec.ofInt n	int → bv (mod 2^n)

Supported widths: 1, 8, 16, 32, 64, 128. All three are total — no
preconditions, no Safe variants, no axioms.

Changes

• CoreOp: BvOpKind.ToUInt, BvOpKind.ToInt (unary, cross-sort);
  CoreOp.intToBv n
• Factory: bvToUIntFunc, bvToIntFunc, intToBvFunc + per-width
  instances for all 6 widths; registered in WFFactory
  (factoryOps: 286 → 304)
• SMTEncoder: maps .bv ⟨_, .ToUInt⟩ → ubv_to_int,
  .bv ⟨_, .ToInt⟩ → sbv_to_int, .intToBv n → (_ int_to_bv n)
• DL/SMT/Op: Op.BV.ubv_to_int, Op.BV.sbv_to_int, Op.BV.int_to_bv n
  + mkName entries
• DL/SMT/Denote + Translate: handle ubv_to_int / sbv_to_int / int_to_bv
• Core DDMTransform/Grammar + Translate: bv128 type + literal;
  bv128 → .bitvec 128
• Boole/Verify (minimal): bv128 cases in typeRange,
  toCoreMonoType, bvWidth — required because bv128 enters
  BooleDDM.BooleType via the grammar change above
• Tests: ProgramEvalTests (18 new func entries for all 3 ops × 6
  widths), StatisticsTest (count bump)

[shigoel]

@kondylidou Could we please have some test programs for each new op in Core, all the way down to SMT?

[shigoel]

@kondylidou Could we please have some test programs for each new op in Core, all the way down to SMT?

Thanks for adding tests, @kondylidou! These tests cover SMT encoding correctness and factory registration. But there's no end-to-end verification test: i.e., a Core program with cast operators that runs through verify and produces pass/fail results from the solver.

Good test candidates would exercise properties like:

• Provable: Int.ToBv8(Bv8.ToUInt(x)) == x (unsigned roundtrip)
• Provable: Bv8.ToUInt(bv{8}(255)) == 255
• Failing: Bv8.ToUInt(x) >= 256 (impossible for 8-bit)
• Signed semantics: Bv8.ToInt(bv{8}(255)) == -1

[kondylidou]

@kondylidou Could we please have some test programs for each new op in Core, all the way down to SMT?

Thanks for adding tests, @kondylidou! These tests cover SMT encoding correctness and factory registration. But there's no end-to-end verification test: i.e., a Core program with cast operators that runs through verify and produces pass/fail results from the solver.

Good test candidates would exercise properties like:

• Provable: Int.ToBv8(Bv8.ToUInt(x)) == x (unsigned roundtrip)
• Provable: Bv8.ToUInt(bv{8}(255)) == 255
• Failing: Bv8.ToUInt(x) >= 256 (impossible for 8-bit)
• Signed semantics: Bv8.ToInt(bv{8}(255)) == -1

Thanks for the feedback! Added BvIntCastVerifyTests.lean with end-to-end verification through cvc5. It covers all four cases you suggested:

• Provable — Int.ToBv8(Bv8.ToUInt(x)) == x (unsigned roundtrip)
• Provable — Bv8.ToUInt(bv{8}(255)) == 255 (concrete value)
• Provable — Bv8.ToInt(bv{8}(255)) == -1 (signed two's complement semantics)
• Failing — Bv8.ToUInt(x) >= 256 (impossible for 8-bit, correctly reported as ❌ fail)

One note on the implementation: factory ops like Bv8.ToUInt can't be called from
#strata program Core; text (the elaborator only resolves names declared in the program
itself, and re-declaring a factory op errors with "already in factory"). So the programs
are constructed via the Lean API using bv8ToUIntFunc.opExpr etc., and verified with
Strata.Core.verifyProgram. The test still exercises the full pipeline —
VCG → SMT encoding → cvc5.

[kondylidou]

ci: bump cvc5 default 1.2.1 → 1.3.4

ubv_to_int and sbv_to_int (SMT-LIB 2.7 BV↔Int casts) are not reliably
solved by cvc5 1.2.1; the new cast tests all returned unknown on CI.
I aligned the CI with the version that supports these operators.