Skip to content

Commit 4774c3c

Browse files
adpaco-awsadpaco-aws
authored
Lean: Add parsing for datetime in the datetime extension (#519)
Signed-off-by: Adrian Palacios <accorell@amazon.com>
1 parent 7e2d4b8 commit 4774c3c

File tree

2 files changed

+157
-59
lines changed

2 files changed

+157
-59
lines changed

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

Lines changed: 47 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -15,13 +15,60 @@
1515
-/
1616

1717
import Cedar.Data.Int64
18+
import Std.Time
19+
import Std.Time.Format
1820

1921
/-! This file defines Cedar datetime values and functions. -/
2022

2123
namespace Cedar.Spec.Ext
2224

2325
open Cedar.Data
2426

27+
namespace Datetime
28+
29+
/--
30+
A datetime value is measured in milliseconds and constructed from a datetime string.
31+
A datetime string must be of one of the forms:
32+
- `YYYY-MM-DD` (date only)
33+
- `YYYY-MM-DDThh:mm:ssZ` (UTC)
34+
- `YYYY-MM-DDThh:mm:ss.SSSZ` (UTC with millisecond precision)
35+
- `YYYY-MM-DDThh:mm:ss(+|-)hhmm` (With timezone offset in hours and minutes)
36+
- `YYYY-MM-DDThh:mm:ss.SSS(+|-)hhmm` (With timezone offset in hours and minutes and millisecond precision)
37+
38+
Regardless of the timezone, offset is always normalized to UTC.
39+
40+
The datetime type does not provide a way to create a datetime from a Unix timestamp.
41+
One of the readable formats listed above must be used instead.
42+
-/
43+
abbrev Datetime := Int64
44+
45+
def MAX_OFFSET_SECONDS: Nat := 86400
46+
47+
def DateOnly : Std.Time.GenericFormat .any := datespec("uuuu-MM-dd")
48+
def DateUTC : Std.Time.GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ss'Z'")
49+
def DateUTCWithMillis : Std.Time.GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSS'Z'")
50+
def DateWithOffset : Std.Time.GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ssxx")
51+
def DateWithOffsetAndMillis : Std.Time.GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSxx")
52+
53+
abbrev datetime? := Int64.ofInt?
54+
55+
def dateContainsLeapSeconds (str: String) : Bool :=
56+
str.length >= 20 && str.get? ⟨17⟩ == some '6' && str.get? ⟨18⟩ == some '0'
57+
58+
def parse (str: String) : Option Datetime := do
59+
if dateContainsLeapSeconds str then failure
60+
let val :=
61+
DateOnly.parse str <|>
62+
DateUTC.parse str <|>
63+
DateUTCWithMillis.parse str <|>
64+
DateWithOffset.parse str <|>
65+
DateWithOffsetAndMillis.parse str
66+
67+
let zonedTime ← val.toOption
68+
if zonedTime.timezone.offset.second.val.natAbs < MAX_OFFSET_SECONDS
69+
then datetime? zonedTime.toTimestamp.toMillisecondsSinceUnixEpoch.toInt
70+
else none
71+
2572
/--
2673
A duration value is measured in milliseconds and constructed from a duration string.
2774
A duration string is a concatenated sequence of quantity-unit pairs where the quantity
@@ -40,8 +87,6 @@ open Cedar.Data
4087
-/
4188
abbrev Duration := Int64
4289

43-
namespace Datetime
44-
4590
def MILLISECONDS_PER_SECOND: Int := 1000
4691
def MILLISECONDS_PER_MINUTE: Int := 60000
4792
def MILLISECONDS_PER_HOUR: Int := 360000

‎cedar-lean/UnitTest/Datetime.lean‎

Lines changed: 110 additions & 57 deletions
Original file line numberDiff line numberDiff line change
@@ -23,77 +23,130 @@ namespace UnitTest.Datetime
2323

2424
open Cedar.Spec.Ext.Datetime
2525

26-
theorem test1 : toString ((Duration.parse "1ms").get!) = "1" := by native_decide
27-
theorem test2 : toString ((Duration.parse "1s").get!) = "1000" := by native_decide
28-
theorem test3 : toString ((Duration.parse "1m").get!) = "60000" := by native_decide
29-
theorem test4 : toString ((Duration.parse "1h").get!) = "360000" := by native_decide
30-
theorem test5 : toString ((Duration.parse "1d").get!) = "86400000" := by native_decide
31-
theorem test6 : toString ((Duration.parse "1d2h3m4s5ms").get!) = "87304005" := by native_decide
32-
theorem test7 : toString ((Duration.parse "2d12h").get!) = "177120000" := by native_decide
33-
theorem test8 : toString ((Duration.parse "3m30s").get!) = "210000" := by native_decide
34-
theorem test9 : toString ((Duration.parse "1h30m45s").get!) = "2205000" := by native_decide
35-
theorem test10 : toString ((Duration.parse "2d5h20m").get!) = "175800000" := by native_decide
36-
theorem test11 : toString ((Duration.parse "-1d12h").get!) = "-90720000" := by native_decide
37-
theorem test12 : toString ((Duration.parse "-3h45m").get!) = "-3780000" := by native_decide
38-
theorem test13 : toString ((Duration.parse "1d1ms").get!) = "86400001" := by native_decide
39-
theorem test14 : toString ((Duration.parse "59m59s999ms").get!) = "3599999" := by native_decide
40-
theorem test15 : toString ((Duration.parse "23h59m59s999ms").get!) = "11879999" := by native_decide
41-
theorem test16 : toString ((Duration.parse "0d0h0m0s0ms").get!) = "0" := by native_decide
42-
43-
private def testValid (str : String) (rep : Int) : TestCase IO :=
26+
private def testValidDatetime (str : String) (rep : Int) : TestCase IO :=
27+
test str ⟨λ _ => checkEq (parse str) (datetime? rep)⟩
28+
29+
def testsForValidDatetimeStrings :=
30+
suite "Datetime.parse for valid strings"
31+
[
32+
testValidDatetime "2022-10-10" 1665360000000,
33+
testValidDatetime "1969-12-31" (-86400000 : Int),
34+
testValidDatetime "1969-12-31T23:59:59Z" (-1000 : Int),
35+
-- Commented out tests following this comment are impacted by a bug we
36+
-- encountered in Lean. Enable them when the bug has been fixed. More
37+
-- details in https://github.com/cedar-policy/cedar-spec/issues/525
38+
-- testValidDatetime "1969-12-31T23:59:59.001Z" (-999 : Int),
39+
-- testValidDatetime "1969-12-31T23:59:59.999Z" (-1 : Int),
40+
testValidDatetime "2024-10-15" 1728950400000,
41+
testValidDatetime "2024-10-15T11:38:02Z" 1728992282000,
42+
testValidDatetime "2024-10-15T11:38:02.101Z" 1728992282101,
43+
testValidDatetime "2024-10-15T11:38:02.101-1134" 1729033922101,
44+
testValidDatetime "2024-10-15T11:38:02.101+1134" 1728950642101,
45+
testValidDatetime "2024-10-15T11:38:02+1134" 1728950642000,
46+
testValidDatetime "2024-10-15T11:38:02-1134" 1729033922000,
47+
]
48+
49+
private def testInvalidDatetime (str : String) (msg : String) : TestCase IO :=
50+
test s!"{str} [{msg}]" ⟨λ _ => checkEq (parse str) .none⟩
51+
52+
def testsForInvalidDatetimeStrings :=
53+
suite "Datetime.parse for invalid strings"
54+
[
55+
testInvalidDatetime "" "empty string",
56+
testInvalidDatetime "a" "string is letter",
57+
testInvalidDatetime "-" "string is character",
58+
testInvalidDatetime "-1" "string is integer",
59+
testInvalidDatetime "11-12-13" "two digits for year",
60+
testInvalidDatetime "1111-1x-20" "invalid month",
61+
testInvalidDatetime "2024-10-15Z" "Zulu code invalid for date",
62+
testInvalidDatetime "2024-10-15T11:38:02ZZ" "double Zulu code",
63+
testInvalidDatetime "2024-01-01T" "separator not needed",
64+
testInvalidDatetime "2024-01-01Ta" "unexpected character 'a'",
65+
testInvalidDatetime "2024-01-01T01:" "only hours",
66+
testInvalidDatetime "2024-01-01T01:02" "no seconds",
67+
testInvalidDatetime "2024-01-01T01:02:0b" "unexpected character 'b'",
68+
testInvalidDatetime "2024-01-01T01::02:03" "double colon",
69+
testInvalidDatetime "2024-01-01T01::02::03" "double colons",
70+
testInvalidDatetime "2024-01-01T31:02:03Z" "invalid hour range",
71+
testInvalidDatetime "2024-01-01T01:60:03Z" "invalid minute range",
72+
testInvalidDatetime "2016-12-31T23:59:60Z" "leap second",
73+
testInvalidDatetime "2016-12-31T23:59:61Z" "invalid second range",
74+
testInvalidDatetime "2024-01-01T00:00:00" "timezone not specified",
75+
testInvalidDatetime "2024-01-01T00:00:00T" "separator is not timezone",
76+
testInvalidDatetime "2024-01-01T00:00:00ZZ" "double Zulu code",
77+
testInvalidDatetime "2024-01-01T00:00:00x001Z" "typo in milliseconds separator",
78+
testInvalidDatetime "2024-01-01T00:00:00.001ZZ" "double Zulu code w/ millis",
79+
testInvalidDatetime "2016-12-31T23:59:60.000Z" "leap second (millis/UTC)",
80+
testInvalidDatetime "2016-12-31T23:59:60.000+0200" "leap second (millis/offset)",
81+
testInvalidDatetime "2024-01-01T00:00:00➕0000" "sign `+` is an emoji",
82+
testInvalidDatetime "2024-01-01T00:00:00➖0000" "sign `-` is an emoji",
83+
testInvalidDatetime "2024-01-01T00:00:00.0001Z" "fraction of seconds is 4 digits",
84+
testInvalidDatetime "2024-01-01T00:00:00.001➖0000" "sign `+` is an emoji",
85+
testInvalidDatetime "2024-01-01T00:00:00.001➕0000" "sign `-` is an emoji",
86+
testInvalidDatetime "2024-01-01T00:00:00.001+00000" "offset is 5 digits",
87+
testInvalidDatetime "2024-01-01T00:00:00.001-00000" "offset is 5 digits",
88+
testInvalidDatetime "2016-12-31T00:00:00+2400" "invalid offset range",
89+
testInvalidDatetime "2016-12-31T00:00:00+9999" "invalid offset range",
90+
]
91+
92+
theorem testDuration16 : toString ((Duration.parse "0d0h0m0s0ms").get!) = "0" := by native_decide
93+
94+
private def testValidDuration (str : String) (rep : Int) : TestCase IO :=
4495
test str ⟨λ _ => checkEq (Duration.parse str) (duration? rep)⟩
4596

4697
def testsForValidDurationStrings :=
4798
suite "Duration.parse for valid strings"
4899
[
49-
testValid "0ms" 0,
50-
testValid "0d0s" 0,
51-
testValid "1ms" 1,
52-
testValid "1s" 1000,
53-
testValid "1m" 60000,
54-
testValid "1h" 360000,
55-
testValid "1d" 86400000,
56-
testValid "12s340ms" 12340,
57-
testValid "1s234ms" 1234,
58-
testValid "-1s" (-1000),
59-
testValid "-4s200ms" (-4200),
60-
testValid "-9s876ms" (-9876),
61-
testValid "106751d23h47m16s854ms" 9223297516854,
62-
testValid "-106751d23h47m16s854ms" (-9223297516854),
63-
testValid "1d2h3m4s5ms" 87304005,
64-
testValid "2d12h" 177120000,
65-
testValid "3m30s" 210000,
66-
testValid "1h30m45s" 2205000,
67-
testValid "2d5h20m" 175800000,
68-
testValid "-1d12h" (-90720000),
69-
testValid "-3h45m" (-3780000),
70-
testValid "1d1ms" 86400001,
71-
testValid "59m59s999ms" 3599999,
72-
testValid "23h59m59s999ms" 11879999
100+
testValidDuration "0ms" 0,
101+
testValidDuration "0d0s" 0,
102+
testValidDuration "1ms" 1,
103+
testValidDuration "1s" 1000,
104+
testValidDuration "1m" 60000,
105+
testValidDuration "1h" 360000,
106+
testValidDuration "1d" 86400000,
107+
testValidDuration "12s340ms" 12340,
108+
testValidDuration "1s234ms" 1234,
109+
testValidDuration "-1s" (-1000),
110+
testValidDuration "-4s200ms" (-4200),
111+
testValidDuration "-9s876ms" (-9876),
112+
testValidDuration "106751d23h47m16s854ms" 9223297516854,
113+
testValidDuration "-106751d23h47m16s854ms" (-9223297516854),
114+
testValidDuration "1d2h3m4s5ms" 87304005,
115+
testValidDuration "2d12h" 177120000,
116+
testValidDuration "3m30s" 210000,
117+
testValidDuration "1h30m45s" 2205000,
118+
testValidDuration "2d5h20m" 175800000,
119+
testValidDuration "-1d12h" (-90720000),
120+
testValidDuration "-3h45m" (-3780000),
121+
testValidDuration "1d1ms" 86400001,
122+
testValidDuration "59m59s999ms" 3599999,
123+
testValidDuration "23h59m59s999ms" 11879999,
124+
testValidDuration "0d0h0m0s0ms" 0
73125
]
74126

75-
private def testInvalid (str : String) (msg : String) : TestCase IO :=
127+
private def testInvalidDuration (str : String) (msg : String) : TestCase IO :=
76128
test s!"{str} [{msg}]" ⟨λ _ => checkEq (Duration.parse str) .none⟩
77129

78130
def testsForInvalidDurationStrings :=
79131
suite "Duration.parse for invalid strings"
80132
[
81-
testInvalid "" "empty string",
82-
testInvalid "d" "unit but no amount",
83-
testInvalid "1d-1s" "invalid use of -",
84-
testInvalid "1d2h3m4s5ms6" "trailing amount",
85-
testInvalid "1x2m3s" "invalid unit",
86-
testInvalid "1.23s" "amounts must be integral",
87-
testInvalid "1s1d" "invalid order",
88-
testInvalid "1s1s" "repeated units",
89-
testInvalid "1d2h3m4s5ms " "trailing space",
90-
testInvalid " 1d2h3m4s5ms" "leading space",
91-
testInvalid "1d9223372036854775807ms" "overflow",
92-
testInvalid "1d92233720368547758071ms" "overflow ms",
93-
testInvalid "9223372036854776s1ms" "overflow s"
133+
testInvalidDuration "" "empty string",
134+
testInvalidDuration "d" "unit but no amount",
135+
testInvalidDuration "1d-1s" "invalid use of -",
136+
testInvalidDuration "1d2h3m4s5ms6" "trailing amount",
137+
testInvalidDuration "1x2m3s" "invalid unit",
138+
testInvalidDuration "1.23s" "amounts must be integral",
139+
testInvalidDuration "1s1d" "invalid order",
140+
testInvalidDuration "1s1s" "repeated units",
141+
testInvalidDuration "1d2h3m4s5ms " "trailing space",
142+
testInvalidDuration " 1d2h3m4s5ms" "leading space",
143+
testInvalidDuration "1d9223372036854775807ms" "overflow",
144+
testInvalidDuration "1d92233720368547758071ms" "overflow ms",
145+
testInvalidDuration "9223372036854776s1ms" "overflow s"
94146
]
95147

96-
def tests := [testsForValidDurationStrings, testsForInvalidDurationStrings]
148+
def tests := [testsForValidDatetimeStrings, testsForInvalidDatetimeStrings,
149+
testsForValidDurationStrings, testsForInvalidDurationStrings]
97150

98151
-- Uncomment for interactive debugging
99152
-- #eval TestSuite.runAll tests

0 commit comments

Comments
 (0)