import Mt.Utils.Nat

namespace Mt

/-- Class to represent 'reservations'

  Reservations are the main method for reasoning about inter-thread behaviour.
  
  Basic idea: Only threads with a certain reservation are allowed to do certain
  things. In many cases, some operation cannot be done atomically. Instead,
  a thread needs to do several steps. Using reservations, the thread can keep
  track about how many of those steps it has already accomplished. Other
  threads have no way to manipulate each other's reservation, only their own.

  For reasoning, the reservations of all threads have to be taken into account.
  However, we want:
  * The order of the other threads should not matter
  * It should not matter if there are 10 other threads, or only one which
    achieved those reservations
  
  As a consequence, we require an addition operator for reservations. Invariants
  used for reasoning may use both the shared state and the sum of all
  reservations, but not individual reservations. Each thread has to guarantee the
  invariant, but it only knows about its own reservation, i.e. it has a lower
  bound on the reservation, but nothing more. Therefore, it's actions are limited
  by the reservation it has already achieved on its own.

  ### Example:
  * There is one shared `Nat` variable `x`
  * Each thread performs the following three steps:
    - generate a random variable `n : Nat`
    - increase `x` by `n + 1` atomically
    - decrease `x` by `n` atomically
  * We want to reason that - in the end - `x` is never zero.

    Solution: We introduce a `reservation : Nat` reservation which keeps track of how much
    we have increased `x`. Therefore, the have the invariant ∑reservation = x.
    Now, we can easily reason about the thread:
  * Step 1: Generating the random number has no effect on the shared variable
  * Step 2: We increase `x` by `n + 1` and assign `reservation :=n + 1`. Since the
    reservations of the other threads have not changed, the invariant still holds
  * Step 3: Since no other thread can affect our reservation, we still know that
    `reservation = n + 1`. Because of our invariant, we also know
    `x = ∑reservation ≥ reservation = n + 1`. Therefore, we can safely decrease both `x`
    and `reservation` by `n` and we still have `x > 0`
-/
class 
IsReservation: Type → Type
IsReservation (
T: Type
T : 
Type: Type 1
Type)
  extends
    
Add: Type ?u.6 → Type ?u.6
Add 
T: Type
T,
    
Lean.IsAssociative: {α : Sort ?u.10} → (α → α → α) → Type
Lean.IsAssociative (@
HAdd.hAdd: {α : Type ?u.14} → {β : Type ?u.13} → {γ : Type ?u.12} → [self : HAdd α β γ] → α → β → γ
HAdd.hAdd 
T: Type
T 
T: Type
T 
T: Type
T _),
    
Lean.IsCommutative: {α : Sort ?u.37} → (α → α → α) → Type
Lean.IsCommutative (@
HAdd.hAdd: {α : Type ?u.41} → {β : Type ?u.40} → {γ : Type ?u.39} → [self : HAdd α β γ] → α → β → γ
HAdd.hAdd 
T: Type
T 
T: Type
T 
T: Type
T _)
  where
    
empty: {T : Type} → [self : IsReservation T] → T
empty : 
T: Type
T
    
empty_add: ∀ {T : Type} [self : IsReservation T] (t : T), IsReservation.empty + t = t
empty_add : ∀ 
t: T
t : 
T: Type
T, 
empty: T
empty + 
t: T
t = 
t: T
t

/-- Specification for a multithreading system

  This specification specifies the context for threads but not the
  threads itself. Threads encode a specification in their type. Only
  threads with the same specification can be executed in parallel
-/
structure 
Spec: Type 1
Spec where
  
State: Spec → Type
State : 
Type: Type 1
Type
  
Reservation: Spec → Type
Reservation : 
Type: Type 1
Type
  [
is_reservation: (self : Spec) → IsReservation self.Reservation
is_reservation : 
IsReservation: Type → Type
IsReservation 
Reservation: Type
Reservation]
  
validate: (self : Spec) → self.Reservation → self.State → Prop
validate : 
Reservation: Type
Reservation -> 
State: Type
State -> 
Prop: Type
Prop

end Mt

namespace Mt
instance: IsReservation Nat
instance : 
IsReservation: Type → Type
IsReservation 
Nat: Type
Nat where
  assoc     := 
Nat.add_assoc: ∀ (n m k : Nat), n + m + k = n + (m + k)
Nat.add_assoc
  comm      := 
Nat.add_comm: ∀ (n m : Nat), n + m = m + n
Nat.add_comm
  empty     := 
0: ?m.816
0
  empty_add := 
Nat.zero_add: ∀ (n : Nat), 0 + n = n
Nat.zero_add

def 
LowerBound: Type
LowerBound :=
Nat: Type
Nat

instance: Add LowerBound
instance : 
Add: Type ?u.897 → Type ?u.897
Add 
LowerBound: Type
LowerBound :=⟨
Nat.max: Nat → Nat → Nat
Nat.max⟩

instance 
LowerBound.instance: IsReservation LowerBound
LowerBound.instance : 
IsReservation: Type → Type
IsReservation 
LowerBound: Type
LowerBound where
  assoc :=
Utils.Nat.max_assoc: ∀ (a b c : Nat), Nat.max (Nat.max a b) c = Nat.max a (Nat.max b c)
Utils.Nat.max_assoc
  comm :=
Utils.Nat.max_comm: ∀ (a b : Nat), Nat.max a b = Nat.max b a
Utils.Nat.max_comm
  empty :=(
0: ?m.958
0 : 
Nat: Type
Nat)
  empty_add :=
Utils.Nat.zero_max: ∀ (a : Nat), Nat.max 0 a = a
Utils.Nat.zero_max

structure 
UnitReservation: UnitReservation
UnitReservation

instance: IsReservation UnitReservation
instance : 
IsReservation: Type → Type
IsReservation 
UnitReservation: Type
UnitReservation where
  add := λ 
_: ?m.1270
_ 
_: ?m.1273
_ => 
⟨⟩: UnitReservation
⟨⟩
  assoc :=by 
∀ (a b c : UnitReservation), a + b + c = a + (b + c)intros
a✝, b✝, c✝: UnitReservation

a✝ + b✝ + c✝ = a✝ + (b✝ + c✝) 
∀ (a b c : UnitReservation), a + b + c = a + (b + c);
a✝, b✝, c✝: UnitReservation

a✝ + b✝ + c✝ = a✝ + (b✝ + c✝) 
∀ (a b c : UnitReservation), a + b + c = a + (b + c)rfl
Goals accomplished! 🐙
  comm :=by 
∀ (a b : UnitReservation), a + b = b + aintros
a✝, b✝: UnitReservation

a✝ + b✝ = b✝ + a✝ 
∀ (a b : UnitReservation), a + b = b + a;
a✝, b✝: UnitReservation

a✝ + b✝ = b✝ + a✝ 
∀ (a b : UnitReservation), a + b = b + arfl
Goals accomplished! 🐙
  empty :=
⟨⟩: UnitReservation
⟨⟩
  empty_add :=by 
∀ (t : UnitReservation), {  }    + t = tintros
t✝: UnitReservation

{  }    + t✝ = t✝ 
∀ (t : UnitReservation), {  }    + t = t;
t✝: UnitReservation

{  }    + t✝ = t✝ 
∀ (t : UnitReservation), {  }    + t = trfl
Goals accomplished! 🐙

inductive 
Lock: Type → Type
Lock (
T: Type
T : 
Type: Type 1
Type) where
| 
Unlocked: {T : Type} → Lock T
Unlocked
| 
Locked: {T : Type} → T → Lock T
Locked : 
T: Type
T -> 
Lock: Type → Sort ?u.1353
Lock 
T: Type
T
| 
Invalid: {T : Type} → Lock T
Invalid

def 
Lock.is_locked: {T : Type} → Lock T → Bool
Lock.is_locked {
T: Type
T : 
Type: Type 1
Type} : 
Lock: Type → Type
Lock 
T: Type
T -> 
Bool: Type
Bool
| 
Locked: {T : Type} → T → Lock T
Locked _ => 
true: Bool
true
| _ => 
false: Bool
false

def 
Lock.is_locked_and_valid: {T : Type} → (T → Prop) → Lock T → Prop
Lock.is_locked_and_valid {
T: Type
T : 
Type: Type 1
Type} (
valid: T → Prop
valid : 
T: Type
T -> 
Prop: Type
Prop) : 
Lock: Type → Type
Lock 
T: Type
T -> 
Prop: Type
Prop
| 
Locked: {T : Type} → T → Lock T
Locked 
s: T
s => 
valid: T → Prop
valid 
s: T
s
| _ => 
False: Prop
False

def 
Lock.is_unlocked: {T : Type} → Lock T → Bool
Lock.is_unlocked {
T: Type
T : 
Type: Type 1
Type} : 
Lock: Type → Type
Lock 
T: Type
T -> 
Bool: Type
Bool
| 
Unlocked: {T : Type} → Lock T
Unlocked => 
true: Bool
true
| _ => 
false: Bool
false

def 
Lock.add: {T : Type} → Lock T → Lock T → Lock T
Lock.add {
T: Type
T : 
Type: Type 1
Type} : 
Lock: Type → Type
Lock 
T: Type
T -> 
Lock: Type → Type
Lock 
T: Type
T -> 
Lock: Type → Type
Lock 
T: Type
T
| 
Unlocked: {T : Type} → Lock T
Unlocked, 
a: Lock T
a => 
a: Lock T
a
| 
a: Lock T
a, 
Unlocked: {T : Type} → Lock T
Unlocked => 
a: Lock T
a
| _, _ => 
Invalid: {T : Type} → Lock T
Invalid

theorem 
Lock.eq_of_is_unlocked: ∀ {T : Type} {r : Lock T}, is_unlocked r = true → r = Unlocked
Lock.eq_of_is_unlocked {
T: Type
T : 
Type: Type 1
Type} {
r: Lock T
r : 
Lock: Type → Type
Lock 
T: Type
T} :
  
r: Lock T
r.
is_unlocked: {T : Type} → Lock T → Bool
is_unlocked → 
r: Lock T
r = 
Lock.Unlocked: {T : Type} → Lock T
Lock.Unlocked :=by
  
T: Type

r: Lock T

is_unlocked r = true → r = Unlockedcases 
r: Lock T
r
T: Type

Unlocked
is_unlocked Unlocked = true → Unlocked = Unlocked
T: Type

a✝: T

Locked
is_unlocked (Locked a✝) = true → Locked a✝ = Unlocked
T: Type

Invalid
is_unlocked Invalid = true → Invalid = Unlocked
  
T: Type

r: Lock T

is_unlocked r = true → r = Unlocked.
T: Type

Unlocked
is_unlocked Unlocked = true → Unlocked = Unlocked 
T: Type

Unlocked
is_unlocked Unlocked = true → Unlocked = Unlocked
T: Type

a✝: T

Locked
is_unlocked (Locked a✝) = true → Locked a✝ = Unlocked
T: Type

Invalid
is_unlocked Invalid = true → Invalid = Unlockedintros
T: Type

Unlocked
Unlocked = Unlocked 
T: Type

Unlocked
is_unlocked Unlocked = true → Unlocked = Unlocked
T: Type

a✝: T

Locked
is_unlocked (Locked a✝) = true → Locked a✝ = Unlocked
T: Type

Invalid
is_unlocked Invalid = true → Invalid = Unlocked;
T: Type

Unlocked
Unlocked = Unlocked 
T: Type

Unlocked
is_unlocked Unlocked = true → Unlocked = Unlocked
T: Type

a✝: T

Locked
is_unlocked (Locked a✝) = true → Locked a✝ = Unlocked
T: Type

Invalid
is_unlocked Invalid = true → Invalid = Unlockedrfl
Goals accomplished! 🐙
  
T: Type

r: Lock T

is_unlocked r = true → r = Unlocked.
T: Type

a✝: T

Locked
is_unlocked (Locked a✝) = true → Locked a✝ = Unlocked 
T: Type

a✝: T

Locked
is_unlocked (Locked a✝) = true → Locked a✝ = Unlocked
T: Type

Invalid
is_unlocked Invalid = true → Invalid = Unlockedintros
T: Type

a✝¹: T

Locked
Locked a✝¹ = Unlocked 
T: Type

a✝: T

Locked
is_unlocked (Locked a✝) = true → Locked a✝ = Unlocked
T: Type

Invalid
is_unlocked Invalid = true → Invalid = Unlocked;
T: Type

a✝¹: T

Locked
Locked a✝¹ = Unlocked 
T: Type

a✝: T

Locked
is_unlocked (Locked a✝) = true → Locked a✝ = Unlocked
T: Type

Invalid
is_unlocked Invalid = true → Invalid = Unlockedcontradiction
Goals accomplished! 🐙
  
T: Type

r: Lock T

is_unlocked r = true → r = Unlocked.
T: Type

Invalid
is_unlocked Invalid = true → Invalid = Unlocked 
T: Type

Invalid
is_unlocked Invalid = true → Invalid = Unlockedintros
T: Type

Invalid
Invalid = Unlocked 
T: Type

Invalid
is_unlocked Invalid = true → Invalid = Unlocked;
T: Type

Invalid
Invalid = Unlocked 
T: Type

Invalid
is_unlocked Invalid = true → Invalid = Unlockedcontradiction
Goals accomplished! 🐙

instance: {T : Type} → Add (Lock T)
instance {
T: Type
T : 
Type: Type 1
Type} : 
Add: Type ?u.2811 → Type ?u.2811
Add (
Lock: Type → Type
Lock 
T: Type
T) :=⟨
Lock.add: {T : Type} → Lock T → Lock T → Lock T
Lock.add⟩

theorem 
Lock.unlocked_add: ∀ {T : Type} (a : Lock T), Unlocked + a = a
Lock.unlocked_add {
T: Type
T : 
Type: Type 1
Type} : ∀ 
a: Lock T
a : 
Lock: Type → Type
Lock 
T: Type
T, 
Unlocked: {T : Type} → Lock T
Unlocked + 
a: Lock T
a = 
a: Lock T
a :=by
  
T: Type

∀ (a : Lock T), Unlocked + a = aintro 
a: Lock T
a
T: Type

a: Lock T

Unlocked + a = a 
T: Type

∀ (a : Lock T), Unlocked + a = a;
T: Type

a: Lock T

Unlocked + a = a 
T: Type

∀ (a : Lock T), Unlocked + a = acases 
a: Lock T
a
T: Type

Unlocked
Unlocked + Unlocked = Unlocked
T: Type

a✝: T

Locked
Unlocked + Locked a✝ = Locked a✝
T: Type

Invalid
Unlocked + Invalid = Invalid 
T: Type

a: Lock T

Unlocked + a = a<;>
T: Type

Unlocked
Unlocked + Unlocked = Unlocked
T: Type

a✝: T

Locked
Unlocked + Locked a✝ = Locked a✝
T: Type

Invalid
Unlocked + Invalid = Invalid 
T: Type

a: Lock T

Unlocked + a = arfl
Goals accomplished! 🐙

theorem 
Lock.add_unlocked: ∀ {T : Type} (a : Lock T), a + Unlocked = a
Lock.add_unlocked {
T: Type
T : 
Type: Type 1
Type} : ∀ 
a: Lock T
a : 
Lock: Type → Type
Lock 
T: Type
T, 
a: Lock T
a + 
Unlocked: {T : Type} → Lock T
Unlocked = 
a: Lock T
a :=by
  
T: Type

∀ (a : Lock T), a + Unlocked = aintro 
a: Lock T
a
T: Type

a: Lock T

a + Unlocked = a 
T: Type

∀ (a : Lock T), a + Unlocked = a;
T: Type

a: Lock T

a + Unlocked = a 
T: Type

∀ (a : Lock T), a + Unlocked = acases 
a: Lock T
a
T: Type

Unlocked
Unlocked + Unlocked = Unlocked
T: Type

a✝: T

Locked
Locked a✝ + Unlocked = Locked a✝
T: Type

Invalid
Invalid + Unlocked = Invalid 
T: Type

a: Lock T

a + Unlocked = a<;>
T: Type

Unlocked
Unlocked + Unlocked = Unlocked
T: Type

a✝: T

Locked
Locked a✝ + Unlocked = Locked a✝
T: Type

Invalid
Invalid + Unlocked = Invalid 
T: Type

a: Lock T

a + Unlocked = arfl
Goals accomplished! 🐙

theorem 
Lock.invalid_add: ∀ {T : Type} (a : Lock T), Invalid + a = Invalid
Lock.invalid_add {
T: Type
T : 
Type: Type 1
Type} : ∀ 
a: Lock T
a : 
Lock: Type → Type
Lock 
T: Type
T, 
Invalid: {T : Type} → Lock T
Invalid + 
a: Lock T
a = 
Invalid: {T : Type} → Lock T
Invalid :=by
  
T: Type

∀ (a : Lock T), Invalid + a = Invalidintro 
a: Lock T
a
T: Type

a: Lock T

Invalid + a = Invalid 
T: Type

∀ (a : Lock T), Invalid + a = Invalid;
T: Type

a: Lock T

Invalid + a = Invalid 
T: Type

∀ (a : Lock T), Invalid + a = Invalidcases 
a: Lock T
a
T: Type

Unlocked
Invalid + Unlocked = Invalid
T: Type

a✝: T

Locked
Invalid + Locked a✝ = Invalid
T: Type

Invalid
Invalid + Invalid = Invalid 
T: Type

a: Lock T

Invalid + a = Invalid<;>
T: Type

Unlocked
Invalid + Unlocked = Invalid
T: Type

a✝: T

Locked
Invalid + Locked a✝ = Invalid
T: Type

Invalid
Invalid + Invalid = Invalid 
T: Type

a: Lock T

Invalid + a = Invalidrfl
Goals accomplished! 🐙

theorem 
Lock.add_comm: ∀ {T : Type} (a b : Lock T), a + b = b + a
Lock.add_comm {
T: Type
T : 
Type: Type 1
Type} : ∀ 
a: Lock T
a 
b: Lock T
b : 
Lock: Type → Type
Lock 
T: Type
T, 
a: Lock T
a + 
b: Lock T
b = 
b: Lock T
b + 
a: Lock T
a :=by
  
T: Type

∀ (a b : Lock T), a + b = b + aintro 
a: Lock T
a 
b: Lock T
b
T: Type

a, b: Lock T

a + b = b + a
  
T: Type

∀ (a b : Lock T), a + b = b + acases 
a: Lock T
a
T: Type

b: Lock T

Unlocked
Unlocked + b = b + Unlocked
T: Type

b: Lock T

a✝: T

Locked
Locked a✝ + b = b + Locked a✝
T: Type

b: Lock T

Invalid
Invalid + b = b + Invalid 
T: Type

a, b: Lock T

a + b = b + a<;>
T: Type

b: Lock T

Unlocked
Unlocked + b = b + Unlocked
T: Type

b: Lock T

a✝: T

Locked
Locked a✝ + b = b + Locked a✝
T: Type

b: Lock T

Invalid
Invalid + b = b + Invalid 
T: Type

a, b: Lock T

a + b = b + acases 
b: Lock T
b
T: Type

Invalid.Unlocked
Invalid + Unlocked = Unlocked + Invalid
T: Type

a✝: T

Invalid.Locked
Invalid + Locked a✝ = Locked a✝ + Invalid
T: Type

Invalid.Invalid
Invalid + Invalid = Invalid + Invalid 
T: Type

b: Lock T

Unlocked
Unlocked + b = b + Unlocked<;>
T: Type

a✝: T

Locked.Unlocked
Locked a✝ + Unlocked = Unlocked + Locked a✝
T: Type

a✝¹, a✝: T

Locked.Locked
Locked a✝¹ + Locked a✝ = Locked a✝ + Locked a✝¹
T: Type

a✝: T

Locked.Invalid
Locked a✝ + Invalid = Invalid + Locked a✝ 
T: Type

b: Lock T

Unlocked
Unlocked + b = b + Unlockedrfl
Goals accomplished! 🐙

theorem 
Lock.add_assoc: ∀ {T : Type} (a b c : Lock T), a + b + c = a + (b + c)
Lock.add_assoc {
T: Type
T : 
Type: Type 1
Type} : ∀ 
a: Lock T
a 
b: Lock T
b 
c: Lock T
c : 
Lock: Type → Type
Lock 
T: Type
T,
  
a: Lock T
a + 
b: Lock T
b + 
c: Lock T
c = 
a: Lock T
a + (
b: Lock T
b + 
c: Lock T
c) :=by
  
T: Type

∀ (a b c : Lock T), a + b + c = a + (b + c)intro 
a: Lock T
a 
b: Lock T
b 
c: Lock T
c
T: Type

a, b, c: Lock T

a + b + c = a + (b + c)
  
T: Type

∀ (a b c : Lock T), a + b + c = a + (b + c)cases 
a: Lock T
a
T: Type

b, c: Lock T

Unlocked
Unlocked + b + c = Unlocked + (b + c)
T: Type

b, c: Lock T

a✝: T

Locked
Locked a✝ + b + c = Locked a✝ + (b + c)
T: Type

b, c: Lock T

Invalid
Invalid + b + c = Invalid + (b + c) 
T: Type

a, b, c: Lock T

a + b + c = a + (b + c)<;>
T: Type

b, c: Lock T

Unlocked
Unlocked + b + c = Unlocked + (b + c)
T: Type

b, c: Lock T

a✝: T

Locked
Locked a✝ + b + c = Locked a✝ + (b + c)
T: Type

b, c: Lock T

Invalid
Invalid + b + c = Invalid + (b + c) 
T: Type

a, b, c: Lock T

a + b + c = a + (b + c)cases 
b: Lock T
b
T: Type

c: Lock T

a✝: T

Locked.Unlocked
Locked a✝ + Unlocked + c = Locked a✝ + (Unlocked + c)
T: Type

c: Lock T

a✝¹, a✝: T

Locked.Locked
Locked a✝¹ + Locked a✝ + c = Locked a✝¹ + (Locked a✝ + c)
T: Type

c: Lock T

a✝: T

Locked.Invalid
Locked a✝ + Invalid + c = Locked a✝ + (Invalid + c) 
T: Type

b, c: Lock T

a✝: T

Locked
Locked a✝ + b + c = Locked a✝ + (b + c)<;>
T: Type

c: Lock T

Invalid.Unlocked
Invalid + Unlocked + c = Invalid + (Unlocked + c)
T: Type

c: Lock T

a✝: T

Invalid.Locked
Invalid + Locked a✝ + c = Invalid + (Locked a✝ + c)
T: Type

c: Lock T

Invalid.Invalid
Invalid + Invalid + c = Invalid + (Invalid + c) 
T: Type

b, c: Lock T

a✝: T

Locked
Locked a✝ + b + c = Locked a✝ + (b + c)cases 
c: Lock T
c
T: Type

Unlocked.Invalid.Unlocked
Unlocked + Invalid + Unlocked = Unlocked + (Invalid + Unlocked)
T: Type

a✝: T

Unlocked.Invalid.Locked
Unlocked + Invalid + Locked a✝ = Unlocked + (Invalid + Locked a✝)
T: Type

Unlocked.Invalid.Invalid
Unlocked + Invalid + Invalid = Unlocked + (Invalid + Invalid) 
T: Type

c: Lock T

Invalid.Invalid
Invalid + Invalid + c = Invalid + (Invalid + c)<;>
T: Type

a✝: T

Locked.Invalid.Unlocked
Locked a✝ + Invalid + Unlocked = Locked a✝ + (Invalid + Unlocked)
T: Type

a✝¹, a✝: T

Locked.Invalid.Locked
Locked a✝¹ + Invalid + Locked a✝ = Locked a✝¹ + (Invalid + Locked a✝)
T: Type

a✝: T

Locked.Invalid.Invalid
Locked a✝ + Invalid + Invalid = Locked a✝ + (Invalid + Invalid) 
T: Type

c: Lock T

Invalid.Invalid
Invalid + Invalid + c = Invalid + (Invalid + c)rfl
Goals accomplished! 🐙

instance: {T : Type} → IsReservation (Lock T)
instance {
T: Type
T : 
Type: Type 1
Type} : 
IsReservation: Type → Type
IsReservation (
Lock: Type → Type
Lock 
T: Type
T) where
  assoc :=
Lock.add_assoc: ∀ {T : Type} (a b c : Lock T), a + b + c = a + (b + c)
Lock.add_assoc
  comm :=
Lock.add_comm: ∀ {T : Type} (a b : Lock T), a + b = b + a
Lock.add_comm
  empty :=
Lock.Unlocked: {T : Type} → Lock T
Lock.Unlocked
  empty_add :=
Lock.unlocked_add: ∀ {T : Type} (a : Lock T), Lock.Unlocked + a = a
Lock.unlocked_add

end Mt