activeAt

formal source

  14
  15namespace ConsentWindow
  16
  17def activeAt {A} (w : ConsentWindow A) (t : Nat) : Bool :=
  18  (w.tStart ≤ t) && (match w.tEnd? with | none => True | some te => t ≤ te)
  19  && (match w.revokedAt? with | none => True | some tr => t < tr)
  20
  21def permitsAt {A} (w : ConsentWindow A) (t : Nat) (a : A) : Bool :=
  22  activeAt w t && w.scope a
  23
  24def revokeAt {A} (w : ConsentWindow A) (r : Nat) : ConsentWindow A :=
  25  { w with revokedAt? := some (match w.revokedAt? with | none => r | some tr => Nat.min tr r) }
  26
  27@[simp] lemma revoke_narrows_active {A} (w : ConsentWindow A) (r t : Nat) :
  28  activeAt (revokeAt w r) t → activeAt w t := by
  29  unfold activeAt revokeAt
  30  intro h
  31  by_cases h1 : w.tEnd? = none
  32  · cases w.tEnd? <;> simp [h1] at h ⊢
  33  · cases w.tEnd? <;> simp at h ⊢
  34
  35@[simp] lemma revoke_narrows_perm {A} (w : ConsentWindow A) (r t : Nat) (a : A) :
  36  permitsAt (revokeAt w r) t a → permitsAt w t a := by
  37  unfold permitsAt
  38  intro h
  39  have := revoke_narrows_active (w:=w) (r:=r) (t:=t) (by exact And.left h)
  40  -- conservative boolean reasoning
  41  have hs : w.scope a = true ∨ w.scope a = false := by
  42    by_cases hh : w.scope a = true <;> [exact Or.inl hh, exact Or.inr hh]
  43  cases hs with
  44  | inl htrue =>
  45      simp [permitsAt, htrue] at h ⊢
  46      cases h with
  47      | intro hact _ =>