Added helper functions for toInt/toNat that check for _ characters. (#881)

Signed-off-by: Liana Hadarean <hadarean@amazon.com>

Author: lianah

cedar-lean/Cedar/Spec/Ext/Datetime.lean

@@ -15,6 +15,7 @@
 -/
 
 import Cedar.Data.Int64
+import Cedar.Spec.Ext.Util
 import Std.Time
 import Std.Time.Format
 
@@ -227,7 +228,7 @@ def parseUnit? (isNegative : Bool) (str : String) (suffix : String) : Option (In
     if digits.isEmpty
     then none
     else do
-      let nUnsignedUnits ← String.toNat? (String.ofList digits)
+      let nUnsignedUnits ← toNat?' (String.ofList digits)
       let units ← if isNegative
         then durationUnits? (Int.negOfNat nUnsignedUnits) suffix
         else durationUnits? (Int.ofNat nUnsignedUnits) suffix

cedar-lean/Cedar/Spec/Ext/Decimal.lean

@@ -15,6 +15,7 @@
 -/
 
 import Cedar.Data.Int64
+import Cedar.Spec.Ext.Util
 
 /-! This file defines Cedar decimal values and functions. -/
 
@@ -48,11 +49,7 @@ def parse (str : String) : Option Decimal :=
     let rlen := right.length
     if 0 < rlen ∧ rlen ≤ DECIMAL_DIGITS
     then
-      -- String.toInt? has undocumented behavior (well, undocumented as of this writing)
-      -- that it allows `_` characters in certain positions in the representation of an
-      -- integer. We want to disallow strings with `_` characters per the Cedar spec.
-      if left.contains '_' ∨ right.contains '_' then .none else
-      match String.toInt? left, String.toNat? right with
+      match toInt?' left, toNat?' right with
       | .some l, .some r =>
         let l' := l * (Int.pow 10 DECIMAL_DIGITS)
         let r' := r * (Int.pow 10 (DECIMAL_DIGITS - rlen))

cedar-lean/Cedar/Spec/Ext/IPAddr.lean

@@ -14,6 +14,8 @@
  limitations under the License.
 -/
 
+import Cedar.Spec.Ext.Util
+
 /-! This file defines Cedar IpAddr values and functions. -/
 
 namespace Cedar.Spec.Ext
@@ -136,15 +138,15 @@ private def parsePrefixNat (str : String) (digits : Nat) (size : Nat) : Option (
   let len := str.length
   if 0 < len && len ≤ digits && (str.startsWith "0" → str = "0")
   then do
-    let n ← str.toNat?
+    let n ← toNat?' str
     if n ≤ size then .some (Fin.ofNat (size+1) n) else .none
   else .none
 
 private def parseNumV4 (str : String) : Option (BitVec 8) :=
   let len := str.length
   if 0 < len && len ≤ 3 && (str.startsWith "0" → str = "0")
   then do
-    let n ← str.toNat?
+    let n ← toNat?' str
     if n ≤ 0xff then .some n else .none
   else .none
 

cedar-lean/Cedar/Spec/Ext/Util.lean

@@ -0,0 +1,17 @@
+namespace Cedar.Spec.Ext
+
+----- Helper Functions -----
+
+/--
+Helper function that wraps String.toInt? but returns .none if the string contains '_'.
+This prevents the undocumented behavior where String.toInt? allows '_' characters.
+-/
+def toInt?' (str : String) : Option Int :=
+  if str.contains '_' then .none else String.toInt? str
+
+/--
+Helper function that wraps String.toNat? but returns .none if the string contains '_'.
+This prevents the undocumented behavior where String.toNat? allows '_' characters.
+-/
+def toNat?' (str : String) : Option Nat :=
+  if str.contains '_' then .none else String.toNat? str