ConsentWindow

formal source

   6universe u
   7
   8/-- Consent window over actions `A` with time bounds and optional revocation. -/
   9structure ConsentWindow (A : Type u) where
  10  scope : A → Bool
  11  tStart : Nat
  12  tEnd? : Option Nat := none
  13  revokedAt? : Option Nat := none
  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)