From 2d45c42ca50884aabdfb94aec52f06f3de563fcf Mon Sep 17 00:00:00 2001 From: Lydia Kondylidou <33327056+kondylidou@users.noreply.github.com> Date: Wed, 8 Jul 2026 13:22:24 +0200 Subject: [PATCH] fix(Core): complete bv128 literal support in FormatCore and Translate MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit FormatCore's bitvec catch-all arm discarded the actual constant value and emitted bv64(128) for any 128-bit literal — wrong type and wrong value. Translate had no bv128Lit case, causing Core→DDM translation to fail for programs with 128-bit literals. Add explicit bv128 arms to both, mirroring the existing bv64 pattern. Co-Authored-By: Claude Sonnet 4.6 --- Strata/Languages/Core/DDMTransform/FormatCore.lean | 1 + Strata/Languages/Core/DDMTransform/Translate.lean | 3 +++ 2 files changed, 4 insertions(+) diff --git a/Strata/Languages/Core/DDMTransform/FormatCore.lean b/Strata/Languages/Core/DDMTransform/FormatCore.lean index 6015bb1832..d4c54ea6c9 100644 --- a/Strata/Languages/Core/DDMTransform/FormatCore.lean +++ b/Strata/Languages/Core/DDMTransform/FormatCore.lean @@ -281,6 +281,7 @@ def lconstToExpr {M} [Inhabited M] (c : Lambda.LConst) : | .bitvecConst 16 n => pure (.bv16Lit default ⟨default, n.toNat⟩) | .bitvecConst 32 n => pure (.bv32Lit default ⟨default, n.toNat⟩) | .bitvecConst 64 n => pure (.bv64Lit default ⟨default, n.toNat⟩) + | .bitvecConst 128 n => pure (.bv128Lit default ⟨default, n.toNat⟩) | .bitvecConst w _ => do ToCSTM.logError "lconstToExpr" "unsupported bitvec width" (toString w) pure (.bv64Lit default ⟨default, w⟩) diff --git a/Strata/Languages/Core/DDMTransform/Translate.lean b/Strata/Languages/Core/DDMTransform/Translate.lean index f46dd95cc3..1f8ddc798d 100644 --- a/Strata/Languages/Core/DDMTransform/Translate.lean +++ b/Strata/Languages/Core/DDMTransform/Translate.lean @@ -860,6 +860,9 @@ partial def translateExpr (p : Program) (bindings : TransBindings) (arg : Arg) : | .fn _ q`Core.bv64Lit, [xa] => let n ← translateBitVec 64 xa return .bitvecConst () 64 n + | .fn _ q`Core.bv128Lit, [xa] => + let n ← translateBitVec 128 xa + return .bitvecConst () 128 n | .fn _ q`Core.strLit, [xa] => let x ← translateStr xa return .strConst () x