RFC 9557 (IXDTF): time zones and tags after the timestamp, proved

Main.lean

@@ -32,6 +32,12 @@
     fromsi N          prints  the printed form of the UTC timestamp N SI
                       seconds after 1972-01-01T00:00:00Z, with second 60
                       at a leap second, or NONE outside 1972 to 9999
+    ixdtf HEX         prints  OK, then tab-separated: the printed form of
+                      the RFC 9557 string, whether the example
+                      application of `Spec.exampleProcessor` must treat
+                      it as erroneous (`true` or `false`), and the values
+                      of the first `u-ca` tag joined by `-`, or `-`;
+                      or REJECT
 
   A malformed request prints `error`: an unknown operation, hex digits
   that are not in pairs, bytes that are not UTF-8, or a number that is
@@ -42,11 +48,13 @@
   `Timestamp.print`, `Timestamp.unixSeconds`,
   `Timestamp.compareInstant`, `fromUnixSeconds`,
   `Timestamp.isValidKnown`, `Timestamp.siSeconds`,
-  `Timestamp.taiMinusUtc` and `fromSiSeconds`. The hex decoding and the request handling
+  `Timestamp.taiMinusUtc`, `fromSiSeconds`, `parseExt`, `Ext.print`,
+  `Ext.erroneous` and `Ext.lookup`. The hex decoding and the request handling
   here are covered by the tests, not by a proof.
 -/
 
 import Rfc3339
+import Spec.Ixdtf
 
 open Rfc3339
 
@@ -114,6 +122,15 @@ def request (line : String) : Option String :=
           s!"OK\t{t.siSeconds}\t{tai}"
         else "NOLEAP"
       | none => "REJECT"
+  | ["ixdtf", h] => do
+    let s ← fromHex h
+    pure <| match parseExt s with
+      | some e =>
+        let cal := match e.lookup "u-ca".toList with
+          | some t => String.ofList (['-'].intercalate t.values)
+          | none => "-"
+        s!"OK\t{e.print}\t{e.erroneous Spec.exampleProcessor}\t{cal}"
+      | none => "REJECT"
   | ["fromsi", n] => do
     let s ← decimal n
     pure <| match fromSiSeconds s with

Proofs.lean

@@ -7,3 +7,4 @@
 import Proofs.Main
 import Proofs.FromUnix.Main
 import Proofs.Leap.Main
+import Proofs.Ixdtf.Main

Proofs/Ixdtf/Parse.lean

@@ -0,0 +1,118 @@
+/-
+  `parseExt` and `Ext.print` against the grammar.
+-/
+
+import Proofs.Ixdtf.Suffix
+import Proofs.Main
+
+open Rfc3339
+
+namespace Rfc3339.Proofs.Ixdtf
+
+theorem px_digitChar_lt (n : Nat) : (Spec.digitChar n).toNat < 91 := by
+  unfold Spec.digitChar
+  rcases Nat.lt_or_ge n 10 with h | h
+  · have : ∀ i : Fin 10, ("0123456789".toList.getD i.val '?').toNat < 91 := by decide
+    exact this ⟨n, h⟩
+  · obtain ⟨k, rfl⟩ : ∃ k, n = k + 10 := ⟨n - 10, by omega⟩
+    simp [List.getD_eq_getElem?_getD]
+
+theorem px_digits_lt (k n : Nat) : ∀ c ∈ Spec.digits k n, c.toNat < 91 := by
+  intro c hc
+  simp only [Spec.digits, List.mem_map] at hc
+  obtain ⟨_, _, rfl⟩ := hc
+  exact px_digitChar_lt _
+
+theorem px_renderOffset_lt (o : Offset) : ∀ c ∈ Spec.renderOffset o, c.toNat < 91 := by
+  cases o with
+  | z => decide
+  | plus h m | minus h m =>
+    simp only [Spec.renderOffset, List.forall_mem_append, List.forall_mem_cons]
+    exact ⟨⟨⟨⟨by decide, by simp⟩, px_digits_lt _ _⟩, ⟨by decide, by simp⟩⟩, px_digits_lt _ _⟩
+
+theorem px_render_lt (t : Timestamp) : ∀ c ∈ Spec.render t, c.toNat < 91 := by
+  simp only [Spec.render, List.forall_mem_append, List.forall_mem_cons]
+  and_intros
+  all_goals first
+    | exact px_digits_lt _ _
+    | exact px_renderOffset_lt _
+    | decide
+    | (intro _ h; cases h)
+    | skip
+  split
+  · simp
+  · simp only [List.forall_mem_append, List.forall_mem_cons,
+      List.forall_mem_map]
+    exact ⟨⟨by decide, by simp⟩, fun _ _ => px_digitChar_lt _⟩
+
+/-- A list whose upper case is a rendered timestamp has no `[`. -/
+theorem px_no_bracket {dt : List Char} {t : Timestamp}
+    (h : dt.map Spec.asciiUpper = Spec.render t) : ∀ c ∈ dt, c ≠ '[' := by
+  intro c hc hb
+  subst hb
+  have hm : Spec.asciiUpper '[' ∈ Spec.render t := h ▸ List.mem_map_of_mem hc
+  have : Spec.asciiUpper '[' = '[' := by decide
+  rw [this] at hm
+  have := px_render_lt t _ hm
+  simp at this
+
+theorem px_takeWhile_split {dt r : List Char} (hd : ∀ c ∈ dt, c ≠ '[')
+    (hr : r = [] ∨ r.head? = some '[') :
+    (dt ++ r).takeWhile (fun x => decide (x ≠ '[')) = dt := by
+  rw [List.takeWhile_append_of_pos (by simpa using hd)]
+  rcases hr with rfl | hr
+  · simp
+  · match r, hr with
+    | _ :: _, hr =>
+      simp only [List.head?_cons, Option.some.injEq] at hr
+      subst hr
+      simp
+
+theorem parseExt_iff (s : String) (e : Ext) :
+    parseExt s = some e ↔
+      Spec.ExtValid e ∧ ∃ dt, s.toList = dt ++ Spec.renderSuffix e ∧
+        dt.map Spec.asciiUpper = Spec.render e.stamp := by
+  constructor
+  · intro h
+    simp only [parseExt, bind, Option.bind_eq_some_iff] at h
+    obtain ⟨t, ht, ⟨zone, tags⟩, hs, he⟩ := h
+    simp only [pure, Option.some.injEq] at he
+    subst he
+    obtain ⟨hv, hu⟩ := (Spec.parse_iff _ t).mp ht
+    rw [String.toList_ofList] at hu
+    obtain ⟨⟨hz, htags⟩, hsuf⟩ :=
+      (parseSuffix_iff _ ⟨t, zone, tags⟩).mp hs
+    refine ⟨⟨hv, hz, htags⟩, _, ?_, hu⟩
+    obtain ⟨r, hr⟩ := List.takeWhile_prefix (fun x => decide (x ≠ '[')) (l := s.toList)
+    rw [← hsuf]
+    generalize s.toList.takeWhile (fun x => decide (x ≠ '[')) = tw at hr ⊢
+    rw [← hr, List.drop_left]
+  · rintro ⟨⟨hv, hz, htags⟩, dt, hs, hu⟩
+    have htw : s.toList.takeWhile (fun x => decide (x ≠ '[')) = dt := by
+      rw [hs]; exact px_takeWhile_split (px_no_bracket hu) (renderSuffix_head e)
+    have hp : parse (String.ofList dt) = some e.stamp :=
+      (Spec.parse_iff _ _).mpr ⟨hv, by rw [String.toList_ofList]; exact hu⟩
+    have hsuf : parseSuffix (Spec.renderSuffix e) = some (e.zone, e.tags) :=
+      (parseSuffix_iff _ e).mpr ⟨⟨hz, htags⟩, rfl⟩
+    simp only [parseExt, htw, hp]
+    rw [hs, List.drop_left, hsuf]
+    rfl
+
+theorem printExt_eq (e : Ext) (h : Spec.ExtValid e) :
+    e.print.toList = Spec.render e.stamp ++ Spec.renderSuffix e := by
+  rw [Ext.print, String.toList_ofList,
+    Format.render_eq _ ((Spec.isValid_iff _).mpr h.1), renderSuffix_eq e h.2.1]
+
+theorem parseExt_print (e : Ext) (h : Spec.ExtValid e) : parseExt e.print = some e :=
+  (parseExt_iff _ e).mpr ⟨h, Spec.render e.stamp, printExt_eq e h, Main.upper_render _⟩
+
+theorem parseExt_plain (s : String) (h : '[' ∉ s.toList) :
+    parseExt s = (parse s).map fun t => ⟨t, none, []⟩ := by
+  have htw : s.toList.takeWhile (fun x => decide (x ≠ '[')) = s.toList := by
+    have := px_takeWhile_split (dt := s.toList) (r := [])
+      (fun c hc hb => h (hb ▸ hc)) (Or.inl rfl)
+    simpa using this
+  simp only [parseExt, htw, String.ofList_toList, List.drop_length]
+  cases parse s <;> rfl
+
+end Rfc3339.Proofs.Ixdtf

Proofs/Ixdtf/Rules.lean

@@ -0,0 +1,89 @@
+/-
+  `Ext.lookup` and `Ext.erroneous` against sections 3.2 to 3.4.
+-/
+
+import Rfc3339
+import Spec.Ixdtf
+import Proofs.Valid
+
+open Rfc3339
+
+namespace Rfc3339.Proofs.Ixdtf
+
+private theorem rx_find_iff (k : List Char) (t : Tag) : ∀ (ts : List Tag),
+    ts.find? (fun u => u.key == k) = some t ↔ ∃ l r, ts = l ++ t :: r ∧ t.key = k ∧ ∀ u ∈ l, u.key ≠ k
+  | [] => by simp
+  | u :: us => by
+    rw [List.find?_cons]
+    by_cases h : u.key = k
+    · simp only [h, beq_self_eq_true, Option.some.injEq]
+      constructor
+      · rintro rfl
+        exact ⟨[], us, by simp, h, by simp⟩
+      · rintro ⟨l, r, hl, hk, hu⟩
+        cases l with
+        | nil => simp at hl; exact hl.1
+        | cons a l =>
+          simp at hl
+          exact absurd (hl.1 ▸ h) (hu a (by simp))
+    · have hb : (u.key == k) = false := by simpa using h
+      rw [hb]
+      simp only
+      rw [rx_find_iff k t us]
+      constructor
+      · rintro ⟨l, r, hl, hk, hu⟩
+        refine ⟨u :: l, r, by simp [hl], hk, ?_⟩
+        intro v hv
+        simp at hv
+        rcases hv with rfl | hv
+        · exact h
+        · exact hu v hv
+      · rintro ⟨l, r, hl, hk, hu⟩
+        cases l with
+        | nil =>
+          simp at hl
+          exact absurd (hl.1 ▸ hk) h
+        | cons a l =>
+          simp at hl
+          exact ⟨l, r, hl.2, hk, fun v hv => hu v (by simp [hv])⟩
+
+theorem lookup_iff (e : Ext) (k : List Char) (t : Tag) :
+    e.lookup k = some t ↔ ∃ l r, e.tags = l ++ t :: r ∧ t.key = k ∧ ∀ u ∈ l, u.key ≠ k := by
+  exact rx_find_iff k t e.tags
+
+
+private theorem rx_assertsOffset_iff (o : Offset) : assertsOffset o = true ↔ Spec.AssertsOffset o := by
+  cases o with
+  | z => simp [assertsOffset, Spec.AssertsOffset]
+  | plus h m => simp [assertsOffset, Spec.AssertsOffset]
+  | minus h m =>
+    by_cases hh : h = 0 <;> by_cases hm : m = 0 <;> subst_vars <;>
+      simp_all [assertsOffset, Spec.AssertsOffset]
+
+private theorem rx_zoneAgrees_iff (p : Processor) (t : Timestamp) (z : Zone) :
+    zoneAgrees p t z = true ↔ Spec.ZoneConsistent p t z := by
+  cases z with
+  | offset o =>
+    simp only [zoneAgrees, Spec.ZoneConsistent, Bool.or_eq_true, Bool.not_eq_true', beq_iff_eq,
+      Rfc3339.Proofs.Valid.offsetMinutes_eq, ← rx_assertsOffset_iff]
+    cases assertsOffset t.offset <;> simp
+  | name parts =>
+    simp only [zoneAgrees, Spec.ZoneConsistent]
+    cases hz : p.zoneOffset parts t with
+    | none => simp
+    | some m =>
+      simp only [Bool.or_eq_true, Bool.not_eq_true', beq_iff_eq, Rfc3339.Proofs.Valid.offsetMinutes_eq,
+        ← rx_assertsOffset_iff, Option.some.injEq, exists_eq_left']
+      cases assertsOffset t.offset <;> simp
+
+theorem erroneous_iff (p : Processor) (e : Ext) :
+    e.erroneous p = true ↔ Spec.MustReject p e := by
+  simp only [Ext.erroneous, Spec.MustReject, Bool.or_eq_true, List.any_eq_true,
+    Bool.and_eq_true, Bool.not_eq_true', beq_iff_eq, bne_iff_ne, ne_eq, or_assoc]
+  apply or_congr _ Iff.rfl
+  rcases h : e.zone with _ | ⟨_ | _, z⟩
+  · simp
+  · simp
+  · simp [← rx_zoneAgrees_iff]
+
+end Rfc3339.Proofs.Ixdtf