Rename bvumod to bvurem, matching the smt-lib function (#890) (#897)

katherine-hough · john-h-kastner-aws · web-flow · commit c92b6bc0a579 · 2026-03-05T11:31:38.000-05:00
Signed-off-by: John Kastner &lt;jkastner@amazon.com&gt;
Signed-off-by: Katherine Hough &lt;kmhough@amazon.com&gt;
Co-authored-by: John Kastner &lt;130772734+john-h-kastner-aws@users.noreply.github.com&gt;
diff --git a/cedar-lean-ffi/protobuf_schema/Messages.proto b/cedar-lean-ffi/protobuf_schema/Messages.proto
@@ -145,7 +145,7 @@ message Op {
         Bvudiv = 10;
         Bvsrem = 11;
         Bvsmod = 12;
-        Bvumod = 13;
+        Bvurem = 13;
         Bvshl = 14;
         Bvlshr = 15;
         Bvslt = 16;
diff --git a/cedar-lean-ffi/src/datatypes.rs b/cedar-lean-ffi/src/datatypes.rs
@@ -283,7 +283,7 @@ pub enum Op {
     Bvudiv,
     Bvsrem,
     Bvsmod,
-    Bvumod,
+    Bvurem,
     Bvshl,
     Bvlshr,
     Bvslt,
@@ -611,7 +611,7 @@ impl TryFrom<Op> for cedar_policy_symcc::op::Op {
             Op::Bvudiv => Self::Bvudiv,
             Op::Bvsrem => Self::Bvsrem,
             Op::Bvsmod => Self::Bvsmod,
-            Op::Bvumod => Self::Bvumod,
+            Op::Bvurem => Self::Bvurem,
             Op::Bvshl => Self::Bvshl,
             Op::Bvlshr => Self::Bvlshr,
             Op::Bvslt => Self::Bvslt,
@@ -941,7 +941,7 @@ impl From<cedar_policy_symcc::op::Op> for Op {
             cedar_policy_symcc::op::Op::Bvudiv => Self::Bvudiv,
             cedar_policy_symcc::op::Op::Bvule => Self::Bvule,
             cedar_policy_symcc::op::Op::Bvult => Self::Bvult,
-            cedar_policy_symcc::op::Op::Bvumod => Self::Bvumod,
+            cedar_policy_symcc::op::Op::Bvurem => Self::Bvurem,
             cedar_policy_symcc::op::Op::Uuf(uuf) => Self::Uuf(Arc::unwrap_or_clone(uuf).into()),
             cedar_policy_symcc::op::Op::OptionGet => Self::OptionGet,
             cedar_policy_symcc::op::Op::RecordGet(a) => Self::RecordGet(a),
diff --git a/cedar-lean-ffi/src/messages.rs b/cedar-lean-ffi/src/messages.rs
@@ -311,7 +311,7 @@ impl proto::op::BaseOp {
             datatypes::Op::Bvudiv => proto::op::BaseOp::Bvudiv,
             datatypes::Op::Bvsrem => proto::op::BaseOp::Bvsrem,
             datatypes::Op::Bvsmod => proto::op::BaseOp::Bvsmod,
-            datatypes::Op::Bvumod => proto::op::BaseOp::Bvumod,
+            datatypes::Op::Bvurem => proto::op::BaseOp::Bvurem,
             datatypes::Op::Bvshl => proto::op::BaseOp::Bvshl,
             datatypes::Op::Bvlshr => proto::op::BaseOp::Bvlshr,
             datatypes::Op::Bvslt => proto::op::BaseOp::Bvslt,
diff --git a/cedar-lean/Cedar/SymCC/Factory.lean b/cedar-lean/Cedar/SymCC/Factory.lean
@@ -167,7 +167,7 @@ def bvsdiv := bvapp .bvsdiv BitVec.smtSDiv
 def bvudiv := bvapp .bvudiv BitVec.smtUDiv
 def bvsrem := bvapp .bvsrem BitVec.srem
 def bvsmod := bvapp .bvsmod BitVec.smod
-def bvumod := bvapp .bvumod BitVec.umod
+def bvurem := bvapp .bvurem BitVec.umod
 
 def bvshl  := bvapp .bvshl (λ b₁ b₂ => b₁ <<< b₂)
 def bvlshr := bvapp .bvlshr (λ b₁ b₂ => b₁ >>> b₂)
diff --git a/cedar-lean/Cedar/SymCC/Interpretation.lean b/cedar-lean/Cedar/SymCC/Interpretation.lean
@@ -108,7 +108,7 @@ def Op.interpret (I : Interpretation) (op : Op) (ts : List Term) (ty : TermType)
   | .bvsdiv, [t₁, t₂]     => Factory.bvsdiv t₁ t₂
   | .bvsrem, [t₁, t₂]     => Factory.bvsrem t₁ t₂
   | .bvsmod, [t₁, t₂]     => Factory.bvsmod t₁ t₂
-  | .bvumod, [t₁, t₂]     => Factory.bvumod t₁ t₂
+  | .bvurem, [t₁, t₂]     => Factory.bvurem t₁ t₂
   | .bvudiv, [t₁, t₂]     => Factory.bvudiv t₁ t₂
   | .bvshl, [t₁, t₂]      => Factory.bvshl t₁ t₂
   | .bvlshr, [t₁, t₂]     => Factory.bvlshr t₁ t₂
diff --git a/cedar-lean/Cedar/SymCC/Op.lean b/cedar-lean/Cedar/SymCC/Op.lean
@@ -74,7 +74,7 @@ inductive Op : Type where
   | bvudiv  -- unsigned bit-vector division
   | bvsrem  -- signed remainder (remainder of division rounded towards zero) (copies sign from dividend)
   | bvsmod  -- signed modulus (remainder of division rounded towards negative infinity) (copies sign from divisor)
-  | bvumod  -- unsigned modulus
+  | bvurem  -- unsigned modulus
   | bvshl
   | bvlshr
   | bvslt
@@ -148,7 +148,7 @@ def Op.mkName : Op → String
   | .bvudiv        => "bvudiv"
   | .bvsrem        => "bvsrem"
   | .bvsmod        => "bvsmod"
-  | .bvumod        => "bvurem"
+  | .bvurem        => "bvurem"
   | .bvshl         => "bvshl"
   | .bvlshr        => "bvlshr"
   | .bvslt         => "bvslt"
diff --git a/cedar-lean/Cedar/Thm/SymCC/Data/Basic.lean b/cedar-lean/Cedar/Thm/SymCC/Data/Basic.lean
@@ -392,10 +392,10 @@ inductive Op.WellTyped (εs : SymEntities) : Op → List Term → TermType → P
     (h₁ : t₁.typeOf = .bitvec n)
     (h₂ : t₂.typeOf = .bitvec n) :
     WellTyped εs .bvsmod [t₁, t₂] (.bitvec n)
-  | bvumod_wt {t₁ t₂ : Term} {n : Nat}
+  | bvurem_wt {t₁ t₂ : Term} {n : Nat}
     (h₁ : t₁.typeOf = .bitvec n)
     (h₂ : t₂.typeOf = .bitvec n) :
-    WellTyped εs .bvumod [t₁, t₂] (.bitvec n)
+    WellTyped εs .bvurem [t₁, t₂] (.bitvec n)
   | bvshl_wt {t₁ t₂ : Term} {n : Nat}
     (h₁ : t₁.typeOf = .bitvec n)
     (h₂ : t₂.typeOf = .bitvec n) :
diff --git a/cedar-lean/Cedar/Thm/SymCC/Env/WF.lean b/cedar-lean/Cedar/Thm/SymCC/Env/WF.lean
@@ -420,7 +420,7 @@ theorem wt_op_same_domain {εs₁ εs₂ : SymEntities} {op : Op} {ts : List Ter
   case bvudiv_wt h h'     => exact Op.WellTyped.bvudiv_wt h h'
   case bvsrem_wt h h'     => exact Op.WellTyped.bvsrem_wt h h'
   case bvsmod_wt h h'     => exact Op.WellTyped.bvsmod_wt h h'
-  case bvumod_wt h h'     => exact Op.WellTyped.bvumod_wt h h'
+  case bvurem_wt h h'     => exact Op.WellTyped.bvurem_wt h h'
   case bvshl_wt h h'      => exact Op.WellTyped.bvshl_wt h h'
   case bvlshr_wt h h'     => exact Op.WellTyped.bvlshr_wt h h'
   case bvsaddo_wt h h'    => exact Op.WellTyped.bvsaddo_wt h h'
diff --git a/cedar-lean/Cedar/Thm/SymCC/Term/Interpret/Basic.lean b/cedar-lean/Cedar/Thm/SymCC/Term/Interpret/Basic.lean
@@ -149,9 +149,9 @@ theorem interpret_term_app_bvsmod {I : Interpretation} {t₁ t₂ : Term} {ty :
   Factory.bvsmod (t₁.interpret I) (t₂.interpret I)
 := by simp_interpret_term_app
 
-theorem interpret_term_app_bvumod {I : Interpretation} {t₁ t₂ : Term} {ty : TermType} :
-  (Term.app .bvumod [t₁, t₂] ty).interpret I =
-  Factory.bvumod (t₁.interpret I) (t₂.interpret I)
+theorem interpret_term_app_bvurem {I : Interpretation} {t₁ t₂ : Term} {ty : TermType} :
+  (Term.app .bvurem [t₁, t₂] ty).interpret I =
+  Factory.bvurem (t₁.interpret I) (t₂.interpret I)
 := by simp_interpret_term_app
 
 theorem interpret_term_app_bvshl {I : Interpretation} {t₁ t₂ : Term} {ty : TermType} :
diff --git a/cedar-lean/Cedar/Thm/SymCC/Term/Interpret/Factory.lean b/cedar-lean/Cedar/Thm/SymCC/Term/Interpret/Factory.lean
@@ -723,9 +723,9 @@ theorem interpret_bvsmod {I : Interpretation} {t₁ t₂ : Term} :
   (Factory.bvsmod t₁ t₂).interpret I = Factory.bvsmod (t₁.interpret I) (t₂.interpret I)
 := by show_interpret_bvop bvsmod bvapp interpret_term_app_bvsmod
 
-theorem interpret_bvumod {I : Interpretation} {t₁ t₂ : Term} :
-  (Factory.bvumod t₁ t₂).interpret I = Factory.bvumod (t₁.interpret I) (t₂.interpret I)
-:= by show_interpret_bvop bvumod bvapp interpret_term_app_bvumod
+theorem interpret_bvurem {I : Interpretation} {t₁ t₂ : Term} :
+  (Factory.bvurem t₁ t₂).interpret I = Factory.bvurem (t₁.interpret I) (t₂.interpret I)
+:= by show_interpret_bvop bvurem bvapp interpret_term_app_bvurem
 
 theorem interpret_bvshl {I : Interpretation} {t₁ t₂ : Term} :
   (Factory.bvshl t₁ t₂).interpret I = Factory.bvshl (t₁.interpret I) (t₂.interpret I)
diff --git a/cedar-lean/Cedar/Thm/SymCC/Term/Interpret/Lit.lean b/cedar-lean/Cedar/Thm/SymCC/Term/Interpret/Lit.lean
@@ -250,8 +250,8 @@ private theorem interpret_term_app_lit {εs : SymEntities} {I : Interpretation}
     show_interpret_term_app_binary_lit t₁ t₂ hI hwf h₁ h₂ ih interpret_term_app_bvsrem pe_bvsrem_wfl
   case bvsmod_wt t₁ t₂ _ h₁ h₂ =>
     show_interpret_term_app_binary_lit t₁ t₂ hI hwf h₁ h₂ ih interpret_term_app_bvsmod pe_bvsmod_wfl
-  case bvumod_wt t₁ t₂ _ h₁ h₂ =>
-    show_interpret_term_app_binary_lit t₁ t₂ hI hwf h₁ h₂ ih interpret_term_app_bvumod pe_bvumod_wfl
+  case bvurem_wt t₁ t₂ _ h₁ h₂ =>
+    show_interpret_term_app_binary_lit t₁ t₂ hI hwf h₁ h₂ ih interpret_term_app_bvurem pe_bvurem_wfl
   case bvshl_wt t₁ t₂ _ h₁ h₂ =>
     show_interpret_term_app_binary_lit t₁ t₂ hI hwf h₁ h₂ ih interpret_term_app_bvshl pe_bvshl_wfl
   case bvlshr_wt t₁ t₂ _ h₁ h₂ =>
diff --git a/cedar-lean/Cedar/Thm/SymCC/Term/Interpret/WF.lean b/cedar-lean/Cedar/Thm/SymCC/Term/Interpret/WF.lean
@@ -371,11 +371,11 @@ private theorem interpret_term_app_wf_bvsmod {εs : SymEntities} {I : Interpreta
   InterpretTermWF εs I (Term.app .bvsmod ts ty)
 := by show_interpret_term_app_wf_binary h₁ ih interpret_term_app_bvsmod wf_term_app_bvsmod wf_bvsmod
 
-private theorem interpret_term_app_wf_bvumod {εs : SymEntities} {I : Interpretation} {ts : List Term} {ty : TermType}
-  (h₁ : Term.WellFormed εs (Term.app .bvumod ts ty))
+private theorem interpret_term_app_wf_bvurem {εs : SymEntities} {I : Interpretation} {ts : List Term} {ty : TermType}
+  (h₁ : Term.WellFormed εs (Term.app .bvurem ts ty))
   (ih : ∀ (t : Term), t ∈ ts → InterpretTermWF εs I t) :
-  InterpretTermWF εs I (Term.app .bvumod ts ty)
-:= by show_interpret_term_app_wf_binary h₁ ih interpret_term_app_bvumod wf_term_app_bvumod wf_bvumod
+  InterpretTermWF εs I (Term.app .bvurem ts ty)
+:= by show_interpret_term_app_wf_binary h₁ ih interpret_term_app_bvurem wf_term_app_bvurem wf_bvurem
 
 private theorem interpret_term_app_wf_bvshl {εs : SymEntities} {I : Interpretation} {ts : List Term} {ty : TermType}
   (h₁ : Term.WellFormed εs (Term.app .bvshl ts ty))
@@ -508,7 +508,7 @@ theorem interpret_term_app_wf {εs : SymEntities} {I : Interpretation} {op : Op}
   | .bvudiv            => exact interpret_term_app_wf_bvudiv h₁ ih
   | .bvsrem            => exact interpret_term_app_wf_bvsrem h₁ ih
   | .bvsmod            => exact interpret_term_app_wf_bvsmod h₁ ih
-  | .bvumod            => exact interpret_term_app_wf_bvumod h₁ ih
+  | .bvurem            => exact interpret_term_app_wf_bvurem h₁ ih
   | .bvshl             => exact interpret_term_app_wf_bvshl h₁ ih
   | .bvlshr            => exact interpret_term_app_wf_bvlshr h₁ ih
   | .bvsaddo           => exact interpret_term_app_wf_bvsaddo h₁ ih
diff --git a/cedar-lean/Cedar/Thm/SymCC/Term/PE.lean b/cedar-lean/Cedar/Thm/SymCC/Term/PE.lean
@@ -638,11 +638,11 @@ theorem pe_bvsmod_wfl {εs : SymEntities} {t₁ t₂ : Term} {n : Nat} :
   Term.isLiteral (Factory.bvsmod t₁ t₂) = true
 := by show_pe_binary_wfl bvsmod bvapp wfl_of_type_bitvec_is_bitvec
 
-theorem pe_bvumod_wfl {εs : SymEntities} {t₁ t₂ : Term} {n : Nat} :
+theorem pe_bvurem_wfl {εs : SymEntities} {t₁ t₂ : Term} {n : Nat} :
   Term.WellFormedLiteral εs t₁ → Term.typeOf t₁ = TermType.bitvec n →
   Term.WellFormedLiteral εs t₂ → Term.typeOf t₂ = TermType.bitvec n →
-  Term.isLiteral (Factory.bvumod t₁ t₂) = true
-:= by show_pe_binary_wfl bvumod bvapp wfl_of_type_bitvec_is_bitvec
+  Term.isLiteral (Factory.bvurem t₁ t₂) = true
+:= by show_pe_binary_wfl bvurem bvapp wfl_of_type_bitvec_is_bitvec
 
 theorem pe_bvshl_wfl {εs : SymEntities} {t₁ t₂ : Term} {n : Nat} :
   Term.WellFormedLiteral εs t₁ → Term.typeOf t₁ = TermType.bitvec n →
@@ -747,12 +747,12 @@ theorem pe_bvsmod {n : Nat} {bv₁ bv₂ : BitVec n} :
   Term.prim (TermPrim.bitvec (BitVec.smod bv₁ bv₂))
 := by simp only [bvsmod, bvapp, BitVec.ofNat_toNat, BitVec.setWidth_eq]
 
-theorem pe_bvumod {n : Nat} {bv₁ bv₂ : BitVec n} :
-  Factory.bvumod
+theorem pe_bvurem {n : Nat} {bv₁ bv₂ : BitVec n} :
+  Factory.bvurem
     (Term.prim (TermPrim.bitvec bv₁))
     (Term.prim (TermPrim.bitvec bv₂)) =
   Term.prim (TermPrim.bitvec (BitVec.umod bv₁ bv₂))
-:= by simp only [bvumod, bvapp, BitVec.ofNat_toNat, BitVec.setWidth_eq]
+:= by simp only [bvurem, bvapp, BitVec.ofNat_toNat, BitVec.setWidth_eq]
 
 theorem pe_bvlshr {n : Nat} {bv₁ bv₂ : BitVec n} :
   Factory.bvlshr
diff --git a/cedar-lean/Cedar/Thm/SymCC/Term/WF.lean b/cedar-lean/Cedar/Thm/SymCC/Term/WF.lean
@@ -459,8 +459,8 @@ theorem wf_term_app_bvsmod {εs : SymEntities} {ts : List Term} {ty : TermType}
   ∃ n, ty = .bitvec n ∧ WFBinary εs ts ty
 := by invert_wf_term_app_param_binary h₁
 
-theorem wf_term_app_bvumod {εs : SymEntities} {ts : List Term} {ty : TermType}
-  (h₁ : (Term.app .bvumod ts ty).WellFormed εs) :
+theorem wf_term_app_bvurem {εs : SymEntities} {ts : List Term} {ty : TermType}
+  (h₁ : (Term.app .bvurem ts ty).WellFormed εs) :
   ∃ n, ty = .bitvec n ∧ WFBinary εs ts ty
 := by invert_wf_term_app_param_binary h₁
 
@@ -940,13 +940,13 @@ theorem wf_bvsmod {εs : SymEntities} {t₁ t₂ : Term} {n : Nat}
   (bvsmod t₁ t₂).WellFormed εs ∧ (bvsmod t₁ t₂).typeOf = .bitvec n
 := by simp_wf_bv_arith h₁ h₂ h₃ h₄ Factory.bvsmod Op.WellTyped.bvsmod_wt
 
-theorem wf_bvumod {εs : SymEntities} {t₁ t₂ : Term} {n : Nat}
+theorem wf_bvurem {εs : SymEntities} {t₁ t₂ : Term} {n : Nat}
   (h₁ : t₁.WellFormed εs)
   (h₂ : t₂.WellFormed εs)
   (h₃ : t₁.typeOf = .bitvec n)
   (h₄ : t₂.typeOf = .bitvec n) :
-  (bvumod t₁ t₂).WellFormed εs ∧ (bvumod t₁ t₂).typeOf = .bitvec n
-:= by simp_wf_bv_arith h₁ h₂ h₃ h₄ Factory.bvumod Op.WellTyped.bvumod_wt
+  (bvurem t₁ t₂).WellFormed εs ∧ (bvurem t₁ t₂).typeOf = .bitvec n
+:= by simp_wf_bv_arith h₁ h₂ h₃ h₄ Factory.bvurem Op.WellTyped.bvurem_wt
 
 theorem wf_bvshl {εs : SymEntities} {t₁ t₂ : Term} {n : Nat}
   (h₁ : t₁.WellFormed εs)
diff --git a/cedar-lean/CedarFFI/ToJson.lean b/cedar-lean/CedarFFI/ToJson.lean
@@ -85,7 +85,7 @@ instance : Lean.ToJson Op where
   | .bvudiv => Lean.Json.str "bvudiv"
   | .bvsrem => Lean.Json.str "bvsrem"
   | .bvsmod => Lean.Json.str "bvsmod"
-  | .bvumod => Lean.Json.str "bvumod"
+  | .bvurem => Lean.Json.str "bvurem"
   | .bvshl => Lean.Json.str "bvshl"
   | .bvlshr => Lean.Json.str "bvlshr"
   | .bvslt => Lean.Json.str "bvslt"
diff --git a/cedar-lean/CedarProto/Term.lean b/cedar-lean/CedarProto/Term.lean
@@ -119,7 +119,7 @@ inductive BaseOp where
   | bvudiv
   | bvsrem
   | bvsmod
-  | bvumod
+  | bvurem
   | bvshl
   | bvlshr
   | bvslt
@@ -153,7 +153,7 @@ namespace BaseOp
     | 10 => .ok .bvudiv
     | 11 => .ok .bvsrem
     | 12 => .ok .bvsmod
-    | 13 => .ok .bvumod
+    | 13 => .ok .bvurem
     | 14 => .ok .bvshl
     | 15 => .ok .bvlshr
     | 16 => .ok .bvslt
@@ -191,7 +191,7 @@ namespace BaseOp
     | .bvudiv => .bvudiv
     | .bvsrem => .bvsrem
     | .bvsmod => .bvsmod
-    | .bvumod => .bvumod
+    | .bvurem => .bvurem
     | .bvshl => .bvshl
     | .bvlshr => .bvlshr
     | .bvslt => .bvslt
