Reject tz offset minutes >=60 (#581)

Signed-off-by: John Kastner <[email protected]>

Author: john-h-kastner-aws

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

@@ -80,6 +80,23 @@ def datetime? (i: Int) : Option Datetime :=
 def dateContainsLeapSeconds (str: String) : Bool :=
   str.length >= 20 && str.get? ⟨17⟩ == some '6' && str.get? ⟨18⟩ == some '0'
 
+/--
+  Check that the minutes for the timezone offset are in bounds (<60). We
+  separately check that the whole offset is less than `MAX_OFFSET_SECONDS` which
+  ensures that the hour component is in bounds. The timezone offset does not
+  have a seconds component.
+-/
+def tzOffsetMinsLt60 (str : String) : Bool :=
+  -- Short string is `DateOnly`, so no offset
+  str.length <= 10 ||
+  -- Ends in `Z` is either `DateUTC` or `DateUTCWithMillis`, so no offset
+  str.endsWith "Z" ||
+  -- `DateWithOffset` or `DateWithOffsetAndMillis` offset is last 4 chars.
+  -- Minutes component is last two chars.
+  match (str.takeRight 2).toNat? with
+  | .some minsOffset => minsOffset < 60
+  | .none => false
+
 /--
   Workaround an issue in the datetime library by checking that the year, month,
   day, hour, minute, and second components of the datetime string are not longer
@@ -107,6 +124,7 @@ def checkComponentLen (str : String) : Bool :=
 def parse (str: String) : Option Datetime := do
   if dateContainsLeapSeconds str then failure
   if !checkComponentLen str then failure
+  if !tzOffsetMinsLt60 str then failure
   let val :=
     DateOnly.parse str <|>
     DateUTC.parse str <|>

cedar-lean/UnitTest/Datetime.lean

@@ -108,8 +108,9 @@ def testsForInvalidDatetimeStrings :=
     testInvalidDatetime "2024-01-01T00:00:00.001➕0000" "sign `-` is an emoji",
     testInvalidDatetime "2024-01-01T00:00:00.001+00000" "offset is 5 digits",
     testInvalidDatetime "2024-01-01T00:00:00.001-00000" "offset is 5 digits",
-    testInvalidDatetime "2016-12-31T00:00:00+2400" "invalid offset range",
-    testInvalidDatetime "2016-12-31T00:00:00+9999" "invalid offset range",
+    testInvalidDatetime "2016-01-01T00:00:00+2400" "invalid offset hour range",
+    testInvalidDatetime "2016-01-01T00:00:00+0060" "invalid offset minute range",
+    testInvalidDatetime "2016-01-01T00:00:00+9999" "invalid offset hour and minute range",
   ]
 
 -- Note: The instances below are only used for tests.