Add Brexit example as a "after this date" example.

text/0000-datetime-extension.md

@@ -118,6 +118,21 @@ permit(
 };
 ```
 
+**Forbid access to EU resources after Brexit**
+
+```cedar
+forbid(
+  principal,
+  action,
+  resource
+) when {
+  context.currentTime > datetime("20200131T23:00:00Z") &&
+  context.location.countryOfOrigin == 'GB' &&
+  resource.owner == 'EU'
+}
+```
+
+
 ## Detailed design
 
 This RFC proposes supporting two new extension types: `datetime`, which represents a particular instant of time, up to second accuracy, and `duration` which represents a duration of time.
@@ -148,7 +163,7 @@ Internally, the datetime object will have a structure such as:
 }
 ```
 
-The datetime parsing function will be responsible for ensuring validity of the structure (e.g., that `month` is between 1 and 12, see full details below).
+The datetime parsing function will be responsible for ensuring validity of the structure (e.g., that `month` is between 1 and 12, see below for full details).
 
 The `d.since(d1)` function returns a `duration` object.
 
@@ -186,7 +201,7 @@ For the functions `offset`, `since`, and `dayOfWeek` there are cases where we mu
 
 - **Conversion between UTC and epochs:** this will be particularly difficult to model and verify in Lean (although it's technically possible, see [this paper](https://dl.acm.org/doi/abs/10.1145/3636501.3636958) which does something similar in the Coq proof assistant). Since it will likely require input-dependent loops, it is unlikely that this can be reasoned about efficiently with SMT.
 - **Conversion between UTC and other Time Zones:** Time Zones are a notoriously complex system that evolves constantly. We avoid this complexity by offering `datetime.offset(duration).` Policy authors that require "local time" can use `context` to pass in a `duration` that shifts the current time appropriately.
-- **Leap Seconds:** Cedar does not have a clock; only arithmetic operations over instants of time, at second resolution. We recognize that without leap second support, functions such as `isBefore()` or `offset()` cannot be precise.
+- **Leap Seconds:** Cedar does not have a clock, and this proposal does not add one. We aim only to provide arithmetic operations over instants of time, at second resolution. We recognize that without leap second support, functions such as `isBefore()` or `offset()` cannot be precise.
 
 ### Support for date/time in other authorization systems
 
@@ -196,7 +211,7 @@ AWS IAM supports [date condition operators](https://docs.aws.amazon.com/IAM/late
 
 ## Drawbacks
 
-**TODO**
+
 
 ## Alternatives
 
@@ -260,6 +275,20 @@ With Unix Time, this requires `/` and `%` operators to compute the `dayOfWeek`,
 
 With Unix Time, this requires `/` and `%` operators to compute whether or not it is a leap year, which isn't currently expressible in Cedar.
 
+**Forbid access to EU resources after Brexit**
+
+```cedar
+forbid(
+  principal,
+  action,
+  resource
+) when {
+  context.currentTime > 1580511600 &&
+  context.location.countryOfOrigin == 'GB' &&
+  resource.owner == 'EU'
+}
+```
+
 ### Alt. B: Pass results of time checks in the context
 
 Another workaround we have suggested is to simply handle date/time logic _outside_ of Cedar, and pass the results of checks in the context. For example, you could pass in fields like  `context.isWorkingHours` or `context.dayOfTheWeek`.
@@ -331,6 +360,21 @@ permit(
 };
 ```
 
+**Forbid access to EU resources after Brexit**
+
+```cedar
+forbid(
+  principal,
+  action,
+  resource
+) when {
+  context.afterBrexit &&
+  context.location.countryOfOrigin == 'GB' &&
+  resource.owner == 'EU'
+}
+```
+
+
 ### Alt. C: Combine Unix Time with additional Pre-Computed context.
 
 The use of [Unix time](https://en.wikipedia.org/wiki/Unix_time), could be augmented with additional provided context, as in Alt. B.. To solve the readability problem of `context.now < 1723000000`, we could introduce `datetime(s)`, but instead return the Unix Time as a `long`.
@@ -412,15 +456,21 @@ permit(
 };
 ```
 
-We must provide the `currentDate` as we can't truncate `currentTime` to eliminate the time component. Additionally, `birthDate` is a time zone sensitive value.
-
-### Alt. D: Represent dates with records
+We must provide the `currentDate` as we can't truncate `currentTime` to eliminate the time component. 
 
-Most of the complexity in the current proposal will come from the need to parse timestamps. In the Rust library (and in other implementations of Cedar in standard languages), this can be done with a library function, but Lean does not provide these utilities, so we will have to build them ourselves.
+**Forbid access to EU resources after Brexit**
 
-We can avoid some of this complexity by changing the signature of the `datetime` function to take a record, like `{year: 2024, month: 7, day: 31, hour: 12, minute: 15, second: 0}`. This will require parsing on the user side, which presumably can be done with a library.
-
-But once we remove parsing from the equation, this extension looks more like an application of _Cedar function macros_ than a proper extension function. See the (currently archived) [RFC 61](https://github.com/cedar-policy/rfcs/pull/61) for more details.
+```cedar
+forbid(
+  principal,
+  action,
+  resource
+) when {
+  context.currentTime > datetime("20200131T23:00:00Z") &&
+  context.location.countryOfOrigin == 'GB' &&
+  resource.owner == 'EU'
+}
+```
 
 ## Potential extensions
 
@@ -433,3 +483,8 @@ The examples above expect `currentTime` to be passed in the context during the a
 ### Should we consider local time at all?
 
 Writing programs that involve dates and time is tricky. Standardizing on UTC representations for all dates and times trades achieving evaluator correctness more quickly at the expense of decreased readability for policy authors and auditors.
+
+### Does second level granularity make sense?
+
+
+