diff --git a/ergotree-ir/src/mir/val_def.rs b/ergotree-ir/src/mir/val_def.rs
index 38e56da96..b9768dbd0 100644
--- a/ergotree-ir/src/mir/val_def.rs
+++ b/ergotree-ir/src/mir/val_def.rs
@@ -21,7 +21,13 @@ use proptest_derive::Arbitrary;
 /// Variable id
 #[derive(PartialEq, Eq, Hash, Debug, Clone, Copy, From, Display, Ord, PartialOrd)]
 #[cfg_attr(feature = "arbitrary", derive(Arbitrary))]
-pub struct ValId(pub u32);
+pub struct ValId(
+    // Valid variable ids fit in a signed `Int` (`ValDef.id` is read with
+    // `getUIntExact`); keep the generator in range so `ValDef` round-trips
+    // through the bounded parse. `ValUse` accepts the wider wire range but its
+    // ids reference a `ValDef`, so in-range generation stays representative.
+    #[cfg_attr(feature = "arbitrary", proptest(strategy = "0u32..=(i32::MAX as u32)"))] pub u32,
+);
 
 impl ValId {
     pub(crate) fn sigma_serialize<W: SigmaByteWrite>(&self, w: &mut W) -> core2::io::Result<()> {
@@ -32,6 +38,24 @@ impl ValId {
         let id = r.get_u32()?;
         Ok(ValId(id))
     }
+
+    /// Parse a `ValId` with the `getUIntExact` bound the JVM `ValDefSerializer`
+    /// applies to `ValDef.id`: the unsigned VLQ must fit in a signed `Int`
+    /// (`<= 0x7fffffff`), else deserialization fails (JVM `toIntExact` throws
+    /// `ArithmeticException`, before any eval). `ValUse`/`FuncValue` ids use the
+    /// wrapping `getUInt().toInt` and deliberately stay on the plain
+    /// `sigma_parse` — bounding them would over-reject.
+    pub(crate) fn sigma_parse_exact<R: SigmaByteRead>(
+        r: &mut R,
+    ) -> Result<Self, SigmaParsingError> {
+        let id = r.get_u32()?;
+        if id > i32::MAX as u32 {
+            return Err(SigmaParsingError::Misc(alloc::format!(
+                "ValDef id {id} exceeds Int.MaxValue (getUIntExact)"
+            )));
+        }
+        Ok(ValId(id))
+    }
 }
 
 /** IR node for let-bound expressions `let x = rhs` which is ValDef.
@@ -65,7 +89,7 @@ impl SigmaSerializable for ValDef {
     }
 
     fn sigma_parse<R: SigmaByteRead>(r: &mut R) -> Result<Self, SigmaParsingError> {
-        let id = ValId::sigma_parse(r)?;
+        let id = ValId::sigma_parse_exact(r)?;
         let rhs = Expr::sigma_parse(r)?;
         r.val_def_type_store().insert(id, rhs.tpe());
         Ok(ValDef {
@@ -95,4 +119,25 @@ mod tests {
             prop_assert_eq![sigma_serialize_roundtrip(&e), e];
         }
     }
+
+    #[test]
+    #[allow(clippy::unwrap_used)]
+    fn valdef_id_getuintexact_bound() {
+        // JVM `ValDefSerializer` reads `ValDef.id` with `getUIntExact`, so an id
+        // VLQ above Int.MaxValue is rejected at deserialize. The inclusive max
+        // 0x7fffffff (`ffffffff07`) binds; 0x80000000 (`8080808008`) errors.
+        // ValUse keeps the wrapping `getUInt().toInt` read and still accepts it.
+        use crate::serialization::sigma_byte_reader::from_bytes;
+        let accept = [0xffu8, 0xff, 0xff, 0xff, 0x07];
+        let reject = [0x80u8, 0x80, 0x80, 0x80, 0x08];
+        assert_eq!(
+            ValId::sigma_parse_exact(&mut from_bytes(&accept[..])).unwrap(),
+            ValId(0x7fff_ffff)
+        );
+        assert!(ValId::sigma_parse_exact(&mut from_bytes(&reject[..])).is_err());
+        assert_eq!(
+            ValId::sigma_parse(&mut from_bytes(&reject[..])).unwrap(),
+            ValId(0x8000_0000)
+        );
+    }
 }
diff --git a/ergotree-ir/src/serialization/property_call.rs b/ergotree-ir/src/serialization/property_call.rs
index 9f1f3429d..c9521ae09 100644
--- a/ergotree-ir/src/serialization/property_call.rs
+++ b/ergotree-ir/src/serialization/property_call.rs
@@ -26,6 +26,18 @@ impl SigmaSerializable for PropertyCall {
         let obj = Expr::sigma_parse(r)?;
         let method =
             SMethod::from_ids(type_id, method_id)?.specialize_for(obj.tpe(), Vec::new())?;
+        // Reject a method whose required ErgoTree version exceeds the tree's, at
+        // DESERIALIZE — the JVM gates this in `SMethod.fromIds`, so it fires
+        // structurally over the whole tree (a dead `if` branch is still parsed,
+        // not lazily skipped). `MethodCall` already does this; `PropertyCall`
+        // (e.g. `Global.none[T]`) was missing it, so a v6 property in a pre-v3
+        // tree was accepted.
+        if r.tree_version() < method.method_raw.min_version {
+            return Err(SigmaParsingError::UnknownMethodId(
+                method_id,
+                type_id.value(),
+            ));
+        }
         Ok(PropertyCall::new(obj, method)?)
     }
 }
@@ -34,10 +46,15 @@ impl SigmaSerializable for PropertyCall {
 #[cfg(feature = "arbitrary")]
 #[allow(clippy::unwrap_used)]
 mod tests {
+    use crate::ergo_tree::ErgoTreeVersion;
     use crate::mir::expr::Expr;
     use crate::mir::property_call::PropertyCall;
+    use crate::serialization::roundtrip_new_feature;
     use crate::serialization::sigma_serialize_roundtrip;
     use crate::types::scontext;
+    use crate::types::sglobal;
+    use crate::types::stype::SType;
+    use alloc::vec;
 
     #[test]
     fn ser_roundtrip_property() {
@@ -45,4 +62,22 @@ mod tests {
         let expr = Expr::PropertyCall(mc.into());
         assert_eq![sigma_serialize_roundtrip(&expr), expr];
     }
+
+    #[test]
+    fn versioned_roundtrip() {
+        // `Global.none` is a v6 (V3) property; a pre-V3 ErgoTree must reject it
+        // at parse, mirroring MethodCall's version gate. (SANTA v6 audit: the
+        // dead-branch `Global.none[UnsignedBigInt]` over-acceptance,
+        // V6-PROPERTY-TYPEARG-GATE-01.)
+        let pc: Expr = PropertyCall::new(
+            Expr::Global,
+            sglobal::NONE_METHOD
+                .clone()
+                .specialize_for(SType::SGlobal, vec![])
+                .unwrap(),
+        )
+        .unwrap()
+        .into();
+        roundtrip_new_feature(&pc, ErgoTreeVersion::V3);
+    }
 }