IndisputableMonolith.Recognition.Consent

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace Recognition
   5
   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)
  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 _ =>
  48          simpa [htrue] using And.intro this rfl
  49  | inr hfalse =>
  50      simp [permitsAt, hfalse] at h
  51
  52end ConsentWindow
  53
  54/-- A ledger of consent windows. -/
  55structure ConsentLedger (A : Type u) where
  56  windows : List (ConsentWindow A)
  57
  58namespace ConsentLedger
  59
  60def permits {A} (L : ConsentLedger A) (t : Nat) (a : A) : Bool :=
  61  L.windows.any (fun w => ConsentWindow.permitsAt w t a)
  62
  63@[simp] lemma permits_append {A} (L1 L2 : List (ConsentWindow A)) (t : Nat) (a : A) :
  64  (ConsentLedger.permits { windows := L1 ++ L2 } t a)
  65  = (ConsentLedger.permits { windows := L1 } t a
  66     || ConsentLedger.permits { windows := L2 } t a) := by
  67  unfold ConsentLedger.permits
  68  simp [List.any_append]
  69
  70end ConsentLedger
  71
  72end Recognition
  73end IndisputableMonolith
  74
  75