import Mt.Reservation
import Mt.Task
import Mt.Thread

namespace SampleMutex

structure Data: Type
Data where
  x: Data → Nat
x : Nat: Type
Nat
  y: Data → Nat
y : Nat: Type
Nat

def Data.valid: Data → Prop
Data.valid : Data: Type
Data -> Prop: Type
Prop
| ⟨x: Nat
x, y: Nat
y⟩ => x: Nat
x = y: Nat
y

abbrev Reservation: ?m.409
Reservation :=Mt.Lock: Type → Type
Mt.Lock Data: Type
Data

structure State: Type
State where
  data: State → Data
data : Data: Type
Data
  locked: State → Bool
locked : Bool: Type
Bool

inductive validate: Reservation → State → Prop
validate : Reservation: Type
Reservation -> State: Type
State -> Prop: Type
Prop where
| unlocked: ∀ {data : Data}, Data.valid data → validate Mt.Lock.Unlocked { data := data, locked := false }
unlocked {data: Data
data : Data: Type
Data} : data: Data
data.valid: Data → Prop
valid → validate: Reservation → State → Prop
validate Mt.Lock.Unlocked: {T : Type} → Mt.Lock T
Mt.Lock.Unlocked ⟨data: Data
data, false: Bool
false⟩
| locked: ∀ (data : Data), validate (Mt.Lock.Locked data) { data := data, locked := true }
locked (data: Data
data : Data: Type
Data) : validate: Reservation → State → Prop
validate (Mt.Lock.Locked: {T : Type} → T → Mt.Lock T
Mt.Lock.Locked data: Data
data) ⟨data: Data
data, true: Bool
true⟩

def spec: Mt.Spec
spec : Mt.Spec: Type 1
Mt.Spec :={
  State: Type
State
  Reservation: Type
Reservation
  validate: Reservation → State → Prop
validate
}

open Mt
open Mt.TaskM

def thread1: Thread spec
thread1 : Thread: Spec → Type 1
Thread spec: Spec
spec :=mk_thread: {spec : Spec} → {T : Type} → TaskM spec T → Thread spec
mk_thread do
  -- lock mutex
  atomic_blocking_rmr: {spec : Spec} → {T : Type} → (spec.State → Bool) → (spec.State → T × spec.State) → TaskM spec T
atomic_blocking_rmr (λ ⟨_, locked: Bool
locked⟩ => locked: Bool
locked = false: Bool
false) λ (s: State
s : State: Type
State) => ⟨⟨⟩: PUnit
⟨⟩, {s: State
s with locked :=true: Bool
true}⟩
  
  -- two atomic modifications, one after the other
  atomic_read_modify: {spec : Spec} → (spec.State → spec.State) → TaskM spec Unit
atomic_read_modify λ s: ?m.982
s => {s: ?m.982
s with data :={s: ?m.982
s.data: State → Data
data with x :=s: ?m.982
s.data: State → Data
data.x: Data → Nat
x + 1: ?m.991
1}}
  atomic_read_modify: {spec : Spec} → (spec.State → spec.State) → TaskM spec Unit
atomic_read_modify λ s: ?m.1058
s => {s: ?m.1058
s with data :={s: ?m.1058
s.data: State → Data
data with y :=s: ?m.1058
s.data: State → Data
data.y: Data → Nat
y + 1: ?m.1067
1}}
  
  -- release mutex
  atomic_read_modify: {spec : Spec} → (spec.State → spec.State) → TaskM spec Unit
atomic_read_modify λ s: ?m.1106
s => {s: ?m.1106
s with locked :=false: Bool
false}

def thread2: Thread spec
thread2 : Thread: Spec → Type 1
Thread spec: Spec
spec :=mk_thread: {spec : Spec} → {T : Type} → TaskM spec T → Thread spec
mk_thread do
  -- lock mutex
  atomic_blocking_rmr: {spec : Spec} → {T : Type} → (spec.State → Bool) → (spec.State → T × spec.State) → TaskM spec T
atomic_blocking_rmr (λ ⟨_, locked: Bool
locked⟩ => locked: Bool
locked = false: Bool
false) λ (s: State
s : State: Type
State) => ⟨⟨⟩: PUnit
⟨⟩, {s: State
s with locked :=true: Bool
true}⟩
  
  -- two atomic reads, one after the other
  let px: ?m.1637
px <- atomic_read: {spec : Spec} → {T : Type} → (spec.State → T) → TaskM spec T
atomic_read λ s: ?m.1631
s => s: ?m.1631
s.data: State → Data
data.x: Data → Nat
x
  let py: ?m.1658
py <- atomic_read: {spec : Spec} → {T : Type} → (spec.State → T) → TaskM spec T
atomic_read λ s: ?m.1652
s => s: ?m.1652
s.data: State → Data
data.y: Data → Nat
y

  atomic_assert: {spec : Spec} → (spec.State → Bool) → TaskM spec Unit
atomic_assert λ _: ?m.1672
_ => px: ?m.1637
px = py: ?m.1658
py
  
  -- release mutex
  atomic_read_modify: {spec : Spec} → (spec.State → spec.State) → TaskM spec Unit
atomic_read_modify λ s: ?m.1704
s => {s: ?m.1704
s with locked :=false: Bool
false}

theorem validate.elim_unlocked: ∀ {r : Reservation} {s : State}, validate r s → s.locked = false → r = Lock.Unlocked ∧ Data.valid s.data
validate.elim_unlocked {r: ?m.1975
r s: State
s} :
  validate: Reservation → State → Prop
validate r: ?m.1975
r s: ?m.1978
s → s: ?m.1978
s.locked: State → Bool
locked = false: Bool
false → r: ?m.1975
r = Lock.Unlocked: {T : Type} → Lock T
Lock.Unlocked ∧ s: ?m.1978
s.data: State → Data
data.valid: Data → Prop
valid :=by
  r: Reservation

s: State

validate r s → s.locked = false → r = Lock.Unlocked ∧ Data.valid s.dataintro is_valid: validate r s
is_valid is_unlocked: s.locked = false
is_unlockedr: Reservation

s: State

is_valid: validate r s

is_unlocked: s.locked = false

r = Lock.Unlocked ∧ Data.valid s.data
  r: Reservation

s: State

validate r s → s.locked = false → r = Lock.Unlocked ∧ Data.valid s.datacases is_valid: validate r s
is_validdata✝: Data

is_unlocked: { data := data✝, locked := false }.locked = false

unlockedLock.Unlocked = Lock.Unlocked ∧ Data.valid { data := data✝, locked := false }.data
data✝: Data

is_unlocked: { data := data✝, locked := true }.locked = false

lockedLock.Locked data✝ = Lock.Unlocked ∧ Data.valid { data := data✝, locked := true }.data
  r: Reservation

s: State

validate r s → s.locked = false → r = Lock.Unlocked ∧ Data.valid s.data.data✝: Data

is_unlocked: { data := data✝, locked := false }.locked = false

unlockedLock.Unlocked = Lock.Unlocked ∧ Data.valid { data := data✝, locked := false }.data data✝: Data

is_unlocked: { data := data✝, locked := false }.locked = false

unlockedLock.Unlocked = Lock.Unlocked ∧ Data.valid { data := data✝, locked := false }.data
data✝: Data

is_unlocked: { data := data✝, locked := true }.locked = false

lockedLock.Locked data✝ = Lock.Unlocked ∧ Data.valid { data := data✝, locked := true }.dataconstructordata✝: Data

is_unlocked: { data := data✝, locked := false }.locked = false

unlocked.leftLock.Unlocked = Lock.Unlocked
data✝: Data

is_unlocked: { data := data✝, locked := false }.locked = false

unlocked.rightData.valid { data := data✝, locked := false }.data
    data✝: Data

is_unlocked: { data := data✝, locked := false }.locked = false

unlockedLock.Unlocked = Lock.Unlocked ∧ Data.valid { data := data✝, locked := false }.data
data✝: Data

is_unlocked: { data := data✝, locked := true }.locked = false

lockedLock.Locked data✝ = Lock.Unlocked ∧ Data.valid { data := data✝, locked := true }.data.data✝: Data

is_unlocked: { data := data✝, locked := false }.locked = false

unlocked.leftLock.Unlocked = Lock.Unlocked data✝: Data

is_unlocked: { data := data✝, locked := false }.locked = false

unlocked.leftLock.Unlocked = Lock.Unlocked
data✝: Data

is_unlocked: { data := data✝, locked := false }.locked = false

unlocked.rightData.valid { data := data✝, locked := false }.datarfl
Goals accomplished! 🐙
    data✝: Data

is_unlocked: { data := data✝, locked := false }.locked = false

unlockedLock.Unlocked = Lock.Unlocked ∧ Data.valid { data := data✝, locked := false }.data
data✝: Data

is_unlocked: { data := data✝, locked := true }.locked = false

lockedLock.Locked data✝ = Lock.Unlocked ∧ Data.valid { data := data✝, locked := true }.data.data✝: Data

is_unlocked: { data := data✝, locked := false }.locked = false

unlocked.rightData.valid { data := data✝, locked := false }.data data✝: Data

is_unlocked: { data := data✝, locked := false }.locked = false

unlocked.rightData.valid { data := data✝, locked := false }.dataassumption
Goals accomplished! 🐙
  r: Reservation

s: State

validate r s → s.locked = false → r = Lock.Unlocked ∧ Data.valid s.data.data✝: Data

is_unlocked: { data := data✝, locked := true }.locked = false

lockedLock.Locked data✝ = Lock.Unlocked ∧ Data.valid { data := data✝, locked := true }.data data✝: Data

is_unlocked: { data := data✝, locked := true }.locked = false

lockedLock.Locked data✝ = Lock.Unlocked ∧ Data.valid { data := data✝, locked := true }.datacontradiction
Goals accomplished! 🐙

theorem validate.elim_locked: ∀ {env_r : Reservation} {d : Data} {s' : State},
  validate (env_r + Lock.Locked d) s' → env_r = Lock.Unlocked ∧ d = s'.data ∧ s'.locked = true
validate.elim_locked {env_r: Reservation
env_r : Reservation: Type
Reservation} {d: Data
d s': State
s'} :
  validate: Reservation → State → Prop
validate (env_r: Reservation
env_r + Lock.Locked: {T : Type} → T → Lock T
Lock.Locked d: ?m.2436
d) s': ?m.2439
s' →
  env_r: Reservation
env_r = Lock.Unlocked: {T : Type} → Lock T
Lock.Unlocked ∧ d: ?m.2436
d = s': ?m.2439
s'.data: State → Data
data ∧ s': ?m.2439
s'.locked: State → Bool
locked = true: Bool
true :=by
  env_r: Reservation

d: Data

s': State

validate (env_r + Lock.Locked d) s' → env_r = Lock.Unlocked ∧ d = s'.data ∧ s'.locked = trueintro initial_valid: validate (env_r + Lock.Locked d) s'
initial_validenv_r: Reservation

d: Data

s': State

initial_valid: validate (env_r + Lock.Locked d) s'

env_r = Lock.Unlocked ∧ d = s'.data ∧ s'.locked = true
  env_r: Reservation

d: Data

s': State

validate (env_r + Lock.Locked d) s' → env_r = Lock.Unlocked ∧ d = s'.data ∧ s'.locked = truecases env_r: Reservation
env_rd: Data

s': State

initial_valid: validate (Lock.Unlocked + Lock.Locked d) s'

UnlockedLock.Unlocked = Lock.Unlocked ∧ d = s'.data ∧ s'.locked = true
d: Data

s': State

a✝: Data

initial_valid: validate (Lock.Locked a✝ + Lock.Locked d) s'

LockedLock.Locked a✝ = Lock.Unlocked ∧ d = s'.data ∧ s'.locked = true
d: Data

s': State

initial_valid: validate (Lock.Invalid + Lock.Locked d) s'

InvalidLock.Invalid = Lock.Unlocked ∧ d = s'.data ∧ s'.locked = true env_r: Reservation

d: Data

s': State

initial_valid: validate (env_r + Lock.Locked d) s'

env_r = Lock.Unlocked ∧ d = s'.data ∧ s'.locked = true<;>d: Data

s': State

initial_valid: validate (Lock.Unlocked + Lock.Locked d) s'

UnlockedLock.Unlocked = Lock.Unlocked ∧ d = s'.data ∧ s'.locked = true
d: Data

s': State

a✝: Data

initial_valid: validate (Lock.Locked a✝ + Lock.Locked d) s'

LockedLock.Locked a✝ = Lock.Unlocked ∧ d = s'.data ∧ s'.locked = true
d: Data

s': State

initial_valid: validate (Lock.Invalid + Lock.Locked d) s'

InvalidLock.Invalid = Lock.Unlocked ∧ d = s'.data ∧ s'.locked = true env_r: Reservation

d: Data

s': State

initial_valid: validate (env_r + Lock.Locked d) s'

env_r = Lock.Unlocked ∧ d = s'.data ∧ s'.locked = truecases initial_valid: validate (Lock.Unlocked + Lock.Locked d) s'
initial_valid
Goals accomplished! 🐙
  env_r: Reservation

d: Data

s': State

validate (env_r + Lock.Locked d) s' → env_r = Lock.Unlocked ∧ d = s'.data ∧ s'.locked = trueconstructord: Data

Unlocked.locked.leftLock.Unlocked = Lock.Unlocked
d: Data

Unlocked.locked.rightd = { data := d, locked := true }.data ∧ { data := d, locked := true }.locked = true
  env_r: Reservation

d: Data

s': State

validate (env_r + Lock.Locked d) s' → env_r = Lock.Unlocked ∧ d = s'.data ∧ s'.locked = true.d: Data

Unlocked.locked.leftLock.Unlocked = Lock.Unlocked d: Data

Unlocked.locked.leftLock.Unlocked = Lock.Unlocked
d: Data

Unlocked.locked.rightd = { data := d, locked := true }.data ∧ { data := d, locked := true }.locked = truerfl
Goals accomplished! 🐙
  env_r: Reservation

d: Data

s': State

validate (env_r + Lock.Locked d) s' → env_r = Lock.Unlocked ∧ d = s'.data ∧ s'.locked = trueconstructord: Data

Unlocked.locked.right.leftd = { data := d, locked := true }.data
d: Data

Unlocked.locked.right.right{ data := d, locked := true }.locked = true d: Data

Unlocked.locked.rightd = { data := d, locked := true }.data ∧ { data := d, locked := true }.locked = true<;>d: Data

Unlocked.locked.right.leftd = { data := d, locked := true }.data
d: Data

Unlocked.locked.right.right{ data := d, locked := true }.locked = true d: Data

Unlocked.locked.rightd = { data := d, locked := true }.data ∧ { data := d, locked := true }.locked = truerfl
Goals accomplished! 🐙

theorem valid_bind_mutex_lock: ∀ {T : Type} {cont : TaskM spec T} {assuming : spec.State → Bool} {motive : T → spec.Reservation → Prop},
  (∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive) →
    valid
      (do
        atomic_blocking_rmr
            (fun x =>
              match x with
              | { data := data, locked := locked } => decide (locked = false))
            fun s => (PUnit.unit, { data := s.data, locked := true })
        cont)
      Lock.Unlocked assuming motive
valid_bind_mutex_lock {T: Type
T : Type: Type 1
Type} {cont: TaskM spec T
cont : TaskM: Spec → Type → Type
TaskM spec: Spec
spec T: Type
T} {assuming: ?m.3387
assuming motive: T → spec.Reservation → Prop
motive}
  (cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive
cont_valid : ∀ x: Nat
x : Nat: Type
Nat, cont: TaskM spec T
cont.valid: {spec : Spec} →
  {T : Type} → TaskM spec T → spec.Reservation → (spec.State → Bool) → (T → spec.Reservation → Prop) → Prop
valid
    (Lock.Locked: {T : Type} → T → Lock T
Lock.Locked ⟨x: Nat
x, x: Nat
x⟩)
    (λ _: ?m.3411
_ => true: Bool
true)
    (motive: ?m.3390
motive))
  : TaskM.valid: {spec : Spec} →
  {T : Type} → TaskM spec T → spec.Reservation → (spec.State → Bool) → (T → spec.Reservation → Prop) → Prop
TaskM.valid (spec :=spec: Spec
spec) (T :=T: Type
T)
    (do
      atomic_blocking_rmr: {spec : Spec} → {T : Type} → (spec.State → Bool) → (spec.State → T × spec.State) → TaskM spec T
atomic_blocking_rmr
        (λ ⟨_, locked: Bool
locked⟩ => locked: Bool
locked = false: Bool
false)
        λ (s: State
s : State: Type
State) => ⟨⟨⟩: PUnit
⟨⟩, {s: State
s with locked :=true: Bool
true}⟩
      cont: TaskM spec T
cont
    ) Lock.Unlocked: {T : Type} → Lock T
Lock.Unlocked assuming: ?m.3387
assuming motive: ?m.3390
motive :=by
  T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

valid
  (do
    atomic_blocking_rmr
        (fun x =>
          match x with
          | { data := data, locked := locked } => decide (locked = false))
        fun s => (PUnit.unit, { data := s.data, locked := true })
    cont)
  Lock.Unlocked assuming motiveapply valid_bind: ∀ {spec : Spec} {U V : Type} {mu : TaskM spec U} {f : U → TaskM spec V} {r : spec.Reservation}
  {assuming : spec.State → Bool} {motive : V → spec.Reservation → Prop} (motive_u : U → spec.Reservation → Prop),
  valid mu r assuming motive_u →
    (∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive) →
      valid (mu >>= f) r assuming motive
valid_bind (spec :=spec: Spec
spec) λ ⟨⟩ r: ?m.3613
r => r: ?m.3613
r.is_locked_and_valid: {T : Type} → (T → Prop) → Lock T → Prop
is_locked_and_valid Data.valid: Data → Prop
Data.validT: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

mu_validvalid
  (atomic_blocking_rmr
    (fun x =>
      match x with
      | { data := data, locked := locked } => decide (locked = false))
    fun s => (PUnit.unit, { data := s.data, locked := true }))
  Lock.Unlocked assuming fun x r => Lock.is_locked_and_valid Data.valid r
T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

f_valid∀ (r' : spec.Reservation), PUnit → Lock.is_locked_and_valid Data.valid r' → valid cont r' (fun x => true) motive
  T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

valid
  (do
    atomic_blocking_rmr
        (fun x =>
          match x with
          | { data := data, locked := locked } => decide (locked = false))
        fun s => (PUnit.unit, { data := s.data, locked := true })
    cont)
  Lock.Unlocked assuming motive.T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

mu_validvalid
  (atomic_blocking_rmr
    (fun x =>
      match x with
      | { data := data, locked := locked } => decide (locked = false))
    fun s => (PUnit.unit, { data := s.data, locked := true }))
  Lock.Unlocked assuming fun x r => Lock.is_locked_and_valid Data.valid r -- verify mutex lock
    T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

mu_validvalid
  (atomic_blocking_rmr
    (fun x =>
      match x with
      | { data := data, locked := locked } => decide (locked = false))
    fun s => (PUnit.unit, { data := s.data, locked := true }))
  Lock.Unlocked assuming fun x r => Lock.is_locked_and_valid Data.valid r
T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

f_valid∀ (r' : spec.Reservation), PUnit → Lock.is_locked_and_valid Data.valid r' → valid cont r' (fun x => true) motiveapply valid_blocking_rmr: ∀ {spec : Spec} {T : Type} {block_until : spec.State → Bool} {f : spec.State → T × spec.State} {r : spec.Reservation}
  {assuming : spec.State → Bool} {motive : T → spec.Reservation → Prop},
  (∀ (env_r : spec.Reservation) (s : spec.State),
      block_until s = true →
        Spec.validate spec (env_r + r) s →
          ∃ r',
            let _discr := f s;
            match f s with
            | (t, s') => Spec.validate spec (env_r + r') s' ∧ motive t r') →
    valid (atomic_blocking_rmr block_until f) r assuming motive
valid_blocking_rmrT: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

mu_valid.f_valid∀ (env_r : spec.Reservation) (s : spec.State),
  (match s with
      | { data := data, locked := locked } => decide (locked = false)) =       true →
    Spec.validate spec (env_r + Lock.Unlocked) s →
      ∃ r',
        let _discr := (PUnit.unit, { data := s.data, locked := true });
        match (PUnit.unit, { data := s.data, locked := true }) with
        | (t, s') => Spec.validate spec (env_r + r') s' ∧ Lock.is_locked_and_valid Data.valid r'
    T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

mu_validvalid
  (atomic_blocking_rmr
    (fun x =>
      match x with
      | { data := data, locked := locked } => decide (locked = false))
    fun s => (PUnit.unit, { data := s.data, locked := true }))
  Lock.Unlocked assuming fun x r => Lock.is_locked_and_valid Data.valid r
T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

f_valid∀ (r' : spec.Reservation), PUnit → Lock.is_locked_and_valid Data.valid r' → valid cont r' (fun x => true) motivesimp only [spec: Spec
spec, Lock.add_unlocked: ∀ {T : Type} (a : Lock T), a + Lock.Unlocked = a
Lock.add_unlocked]T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

mu_valid.f_valid∀ (env_r : spec.Reservation) (s : spec.State),
  (match s with
      | { data := data, locked := locked } => decide (locked = false)) =       true →
    validate env_r s →
      ∃ r', validate (env_r + r') { data := s.data, locked := true } ∧ Lock.is_locked_and_valid Data.valid r'
    T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

mu_validvalid
  (atomic_blocking_rmr
    (fun x =>
      match x with
      | { data := data, locked := locked } => decide (locked = false))
    fun s => (PUnit.unit, { data := s.data, locked := true }))
  Lock.Unlocked assuming fun x r => Lock.is_locked_and_valid Data.valid r
T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

f_valid∀ (r' : spec.Reservation), PUnit → Lock.is_locked_and_valid Data.valid r' → valid cont r' (fun x => true) motiveintro env_r: spec.Reservation
env_r s: spec.State
s is_unlocked: (match s with
  | { data := data, locked := locked } => decide (locked = false)) =   true
is_unlocked initial_valid: validate env_r s
initial_validT: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

env_r: spec.Reservation

s: spec.State

is_unlocked: (match s with
  | { data := data, locked := locked } => decide (locked = false)) =   true

initial_valid: validate env_r s

mu_valid.f_valid∃ r', validate (env_r + r') { data := s.data, locked := true } ∧ Lock.is_locked_and_valid Data.valid r'
    T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

mu_validvalid
  (atomic_blocking_rmr
    (fun x =>
      match x with
      | { data := data, locked := locked } => decide (locked = false))
    fun s => (PUnit.unit, { data := s.data, locked := true }))
  Lock.Unlocked assuming fun x r => Lock.is_locked_and_valid Data.valid r
T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

f_valid∀ (r' : spec.Reservation), PUnit → Lock.is_locked_and_valid Data.valid r' → valid cont r' (fun x => true) motiveexists Lock.Locked: {T : Type} → T → Lock T
Lock.Locked s: spec.State
s.data: State → Data
dataT: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

env_r: spec.Reservation

s: spec.State

is_unlocked: (match s with
  | { data := data, locked := locked } => decide (locked = false)) =   true

initial_valid: validate env_r s

mu_valid.f_validvalidate (env_r + Lock.Locked s.data) { data := s.data, locked := true } ∧   Lock.is_locked_and_valid Data.valid (Lock.Locked s.data)

    T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

mu_validvalid
  (atomic_blocking_rmr
    (fun x =>
      match x with
      | { data := data, locked := locked } => decide (locked = false))
    fun s => (PUnit.unit, { data := s.data, locked := true }))
  Lock.Unlocked assuming fun x r => Lock.is_locked_and_valid Data.valid r
T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

f_valid∀ (r' : spec.Reservation), PUnit → Lock.is_locked_and_valid Data.valid r' → valid cont r' (fun x => true) motivehave is_unlocked: ?m.4889
is_unlocked :=of_decide_eq_true: ∀ {p : Prop} [inst : Decidable p], decide p = true → p
of_decide_eq_true is_unlocked: (match s with
  | { data := data, locked := locked } => decide (locked = false)) =   true
is_unlockedT: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

env_r: spec.Reservation

s: spec.State

initial_valid: validate env_r s

is_unlocked: s.locked = false

mu_valid.f_validvalidate (env_r + Lock.Locked s.data) { data := s.data, locked := true } ∧   Lock.is_locked_and_valid Data.valid (Lock.Locked s.data)
    T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

mu_validvalid
  (atomic_blocking_rmr
    (fun x =>
      match x with
      | { data := data, locked := locked } => decide (locked = false))
    fun s => (PUnit.unit, { data := s.data, locked := true }))
  Lock.Unlocked assuming fun x r => Lock.is_locked_and_valid Data.valid r
T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

f_valid∀ (r' : spec.Reservation), PUnit → Lock.is_locked_and_valid Data.valid r' → valid cont r' (fun x => true) motivehave :=initial_valid: validate env_r s
initial_valid.elim_unlocked: ∀ {r : Reservation} {s : State}, validate r s → s.locked = false → r = Lock.Unlocked ∧ Data.valid s.data
elim_unlocked is_unlocked: ?m.4889
is_unlockedT: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

env_r: spec.Reservation

s: spec.State

initial_valid: validate env_r s

is_unlocked: s.locked = false

this: env_r = Lock.Unlocked ∧ Data.valid s.data

mu_valid.f_validvalidate (env_r + Lock.Locked s.data) { data := s.data, locked := true } ∧   Lock.is_locked_and_valid Data.valid (Lock.Locked s.data)
    
    T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

mu_validvalid
  (atomic_blocking_rmr
    (fun x =>
      match x with
      | { data := data, locked := locked } => decide (locked = false))
    fun s => (PUnit.unit, { data := s.data, locked := true }))
  Lock.Unlocked assuming fun x r => Lock.is_locked_and_valid Data.valid r
T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

f_valid∀ (r' : spec.Reservation), PUnit → Lock.is_locked_and_valid Data.valid r' → valid cont r' (fun x => true) motivesimp only [spec: Spec
spec, this: ?m.4909
this, Lock.is_locked_and_valid: {T : Type} → (T → Prop) → Lock T → Prop
Lock.is_locked_and_valid, and_true: ∀ (p : Prop), (p ∧ True) = p
and_true]T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

env_r: spec.Reservation

s: spec.State

initial_valid: validate env_r s

is_unlocked: s.locked = false

this: env_r = Lock.Unlocked ∧ Data.valid s.data

mu_valid.f_validvalidate (Lock.Unlocked + Lock.Locked s.data) { data := s.data, locked := true }
    T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

mu_validvalid
  (atomic_blocking_rmr
    (fun x =>
      match x with
      | { data := data, locked := locked } => decide (locked = false))
    fun s => (PUnit.unit, { data := s.data, locked := true }))
  Lock.Unlocked assuming fun x r => Lock.is_locked_and_valid Data.valid r
T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

f_valid∀ (r' : spec.Reservation), PUnit → Lock.is_locked_and_valid Data.valid r' → valid cont r' (fun x => true) motiveexact validate.locked: ∀ (data : Data), validate (Lock.Locked data) { data := data, locked := true }
validate.locked ..
Goals accomplished! 🐙
  
  T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

valid
  (do
    atomic_blocking_rmr
        (fun x =>
          match x with
          | { data := data, locked := locked } => decide (locked = false))
        fun s => (PUnit.unit, { data := s.data, locked := true })
    cont)
  Lock.Unlocked assuming motiveintro r: spec.Reservation
r ⟨⟩ is_locked_and_valid: Lock.is_locked_and_valid Data.valid r
is_locked_and_validT: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

r: spec.Reservation

is_locked_and_valid: Lock.is_locked_and_valid Data.valid r

f_validvalid cont r (fun x => true) motive
  T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

valid
  (do
    atomic_blocking_rmr
        (fun x =>
          match x with
          | { data := data, locked := locked } => decide (locked = false))
        fun s => (PUnit.unit, { data := s.data, locked := true })
    cont)
  Lock.Unlocked assuming motivecases r: spec.Reservation
rT: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

is_locked_and_valid: Lock.is_locked_and_valid Data.valid Lock.Unlocked

f_valid.Unlockedvalid cont Lock.Unlocked (fun x => true) motive
T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

a✝: Data

is_locked_and_valid: Lock.is_locked_and_valid Data.valid (Lock.Locked a✝)

f_valid.Lockedvalid cont (Lock.Locked a✝) (fun x => true) motive
T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

is_locked_and_valid: Lock.is_locked_and_valid Data.valid Lock.Invalid

f_valid.Invalidvalid cont Lock.Invalid (fun x => true) motive T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

r: spec.Reservation

is_locked_and_valid: Lock.is_locked_and_valid Data.valid r

f_validvalid cont r (fun x => true) motive<;>T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

is_locked_and_valid: Lock.is_locked_and_valid Data.valid Lock.Unlocked

f_valid.Unlockedvalid cont Lock.Unlocked (fun x => true) motive
T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

a✝: Data

is_locked_and_valid: Lock.is_locked_and_valid Data.valid (Lock.Locked a✝)

f_valid.Lockedvalid cont (Lock.Locked a✝) (fun x => true) motive
T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

is_locked_and_valid: Lock.is_locked_and_valid Data.valid Lock.Invalid

f_valid.Invalidvalid cont Lock.Invalid (fun x => true) motive T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

r: spec.Reservation

is_locked_and_valid: Lock.is_locked_and_valid Data.valid r

f_validvalid cont r (fun x => true) motivetry T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

is_locked_and_valid: Lock.is_locked_and_valid Data.valid Lock.Unlocked

f_valid.Unlockedvalid cont Lock.Unlocked (fun x => true) motivecontradiction
Goals accomplished! 🐙
  T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

valid
  (do
    atomic_blocking_rmr
        (fun x =>
          match x with
          | { data := data, locked := locked } => decide (locked = false))
        fun s => (PUnit.unit, { data := s.data, locked := true })
    cont)
  Lock.Unlocked assuming motiverename_i data0: ?m.5018
data0T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

data0: Data

is_locked_and_valid: Lock.is_locked_and_valid Data.valid (Lock.Locked data0)

f_valid.Lockedvalid cont (Lock.Locked data0) (fun x => true) motive
  T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

valid
  (do
    atomic_blocking_rmr
        (fun x =>
          match x with
          | { data := data, locked := locked } => decide (locked = false))
        fun s => (PUnit.unit, { data := s.data, locked := true })
    cont)
  Lock.Unlocked assuming motivelet ⟨x0: Nat
x0, _⟩ :=data0: ?m.5018
data0T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

data0: Data

x0, y✝: Nat

is_locked_and_valid: Lock.is_locked_and_valid Data.valid (Lock.Locked { x := x0, y := y✝ })

f_valid.Lockedvalid cont (Lock.Locked { x := x0, y := y✝ }) (fun x => true) motive T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

valid
  (do
    atomic_blocking_rmr
        (fun x =>
          match x with
          | { data := data, locked := locked } => decide (locked = false))
        fun s => (PUnit.unit, { data := s.data, locked := true })
    cont)
  Lock.Unlocked assuming motive;T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

data0: Data

x0, y✝: Nat

is_locked_and_valid: Lock.is_locked_and_valid Data.valid (Lock.Locked { x := x0, y := y✝ })

f_valid.Lockedvalid cont (Lock.Locked { x := x0, y := y✝ }) (fun x => true) motive T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

valid
  (do
    atomic_blocking_rmr
        (fun x =>
          match x with
          | { data := data, locked := locked } => decide (locked = false))
        fun s => (PUnit.unit, { data := s.data, locked := true })
    cont)
  Lock.Unlocked assuming motiveclear data0: ?m.5018
data0T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

x0, y✝: Nat

is_locked_and_valid: Lock.is_locked_and_valid Data.valid (Lock.Locked { x := x0, y := y✝ })

f_valid.Lockedvalid cont (Lock.Locked { x := x0, y := y✝ }) (fun x => true) motive
  T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

valid
  (do
    atomic_blocking_rmr
        (fun x =>
          match x with
          | { data := data, locked := locked } => decide (locked = false))
        fun s => (PUnit.unit, { data := s.data, locked := true })
    cont)
  Lock.Unlocked assuming motivecases is_locked_and_valid: Lock.is_locked_and_valid Data.valid (Lock.Locked { x := x0, y := y✝ })
is_locked_and_validT: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

x0: Nat

f_valid.Locked.reflvalid cont (Lock.Locked { x := x0, y := x0 }) (fun x => true) motive
  T: Type

cont: TaskM spec T

assuming: spec.State → Bool

motive: T → spec.Reservation → Prop

cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive

valid
  (do
    atomic_blocking_rmr
        (fun x =>
          match x with
          | { data := data, locked := locked } => decide (locked = false))
        fun s => (PUnit.unit, { data := s.data, locked := true })
    cont)
  Lock.Unlocked assuming motiveexact cont_valid: ∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive
cont_valid x0: Nat
x0
Goals accomplished! 🐙

theorem valid_mutex_release: ∀ {assuming : spec.State → Bool} {data : Data},
  Data.valid data →
    valid (atomic_read_modify fun s => { data := s.data, locked := false }) (Lock.Locked data) assuming fun x r =>
      r = Lock.Unlocked
valid_mutex_release {assuming: spec.State → Bool
assuming data: ?m.5451
data}
  (data_valid: Data.valid data
data_valid : data: ?m.5451
data.valid: Data → Prop
valid)
  : TaskM.valid: {spec : Spec} →
  {T : Type} → TaskM spec T → spec.Reservation → (spec.State → Bool) → (T → spec.Reservation → Prop) → Prop
TaskM.valid (spec :=spec: Spec
spec) (T :=Unit: Type
Unit)
    (atomic_read_modify: {spec : Spec} → (spec.State → spec.State) → TaskM spec Unit
atomic_read_modify λ s: ?m.5462
s => {s: ?m.5462
s with locked :=false: Bool
false})
    (Lock.Locked: {T : Type} → T → Lock T
Lock.Locked data: ?m.5451
data)
    assuming: ?m.5448
assuming
    (λ _: ?m.5471
_ r: ?m.5474
r => r: ?m.5474
r = Lock.Unlocked: {T : Type} → Lock T
Lock.Unlocked) :=by
  assuming: spec.State → Bool

data: Data

data_valid: Data.valid data

valid (atomic_read_modify fun s => { data := s.data, locked := false }) (Lock.Locked data) assuming fun x r =>
  r = Lock.Unlockedapply valid_rm: ∀ {spec : Spec} {f : spec.State → spec.State} {r : spec.Reservation} {assuming : spec.State → Bool}
  {motive : Unit → spec.Reservation → Prop},
  (∀ (env_r : spec.Reservation) (s : spec.State),
      assuming s = true →
        Spec.validate spec (env_r + r) s →
          ∃ r',
            let s' := f s;
            Spec.validate spec (env_r + r') s' ∧ motive PUnit.unit r') →
    valid (atomic_read_modify f) r assuming motive
valid_rmassuming: spec.State → Bool

data: Data

data_valid: Data.valid data

f_valid∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    Spec.validate spec (env_r + Lock.Locked data) s →
      ∃ r',
        let s' := { data := s.data, locked := false };
        Spec.validate spec (env_r + r') s' ∧ r' = Lock.Unlocked
  assuming: spec.State → Bool

data: Data

data_valid: Data.valid data

valid (atomic_read_modify fun s => { data := s.data, locked := false }) (Lock.Locked data) assuming fun x r =>
  r = Lock.Unlockedsimp only [spec: Spec
spec, Lock.add_unlocked: ∀ {T : Type} (a : Lock T), a + Lock.Unlocked = a
Lock.add_unlocked]assuming: spec.State → Bool

data: Data

data_valid: Data.valid data

f_valid∀ (env_r : spec.Reservation) (s : spec.State),
  assuming s = true →
    validate (env_r + Lock.Locked data) s →
      ∃ r', validate (env_r + r') { data := s.data, locked := false } ∧ r' = Lock.Unlocked
  assuming: spec.State → Bool

data: Data

data_valid: Data.valid data

valid (atomic_read_modify fun s => { data := s.data, locked := false }) (Lock.Locked data) assuming fun x r =>
  r = Lock.Unlockedintro env_r: spec.Reservation
env_r ⟨data': Data
data', locked: Bool
locked ⟩ _: assuming { data := data', locked := locked } = true
_ initial_valid: validate (env_r + Lock.Locked data) { data := data', locked := locked }
initial_validassuming: spec.State → Bool

data: Data

data_valid: Data.valid data

env_r: spec.Reservation

data': Data

locked: Bool

initial_valid: validate (env_r + Lock.Locked data) { data := data', locked := locked }

f_valid∃ r', validate (env_r + r') { data := { data := data', locked := locked }.data, locked := false } ∧ r' = Lock.Unlocked
  assuming: spec.State → Bool

data: Data

data_valid: Data.valid data

valid (atomic_read_modify fun s => { data := s.data, locked := false }) (Lock.Locked data) assuming fun x r =>
  r = Lock.Unlockedexists Lock.Unlocked: {T : Type} → Lock T
Lock.Unlockedassuming: spec.State → Bool

data: Data

data_valid: Data.valid data

env_r: spec.Reservation

data': Data

locked: Bool

initial_valid: validate (env_r + Lock.Locked data) { data := data', locked := locked }

f_validvalidate (env_r + Lock.Unlocked) { data := { data := data', locked := locked }.data, locked := false } ∧   Lock.Unlocked = Lock.Unlocked
  assuming: spec.State → Bool

data: Data

data_valid: Data.valid data

valid (atomic_read_modify fun s => { data := s.data, locked := false }) (Lock.Locked data) assuming fun x r =>
  r = Lock.Unlockedhave : data: Data
data = data': Data
data' :=initial_valid: validate (env_r + Lock.Locked data) { data := data', locked := locked }
initial_valid.elim_locked: ∀ {env_r : Reservation} {d : Data} {s' : State},
  validate (env_r + Lock.Locked d) s' → env_r = Lock.Unlocked ∧ d = s'.data ∧ s'.locked = true
elim_locked.right: ∀ {a b : Prop}, a ∧ b → b
right.left: ∀ {a b : Prop}, a ∧ b → a
leftassuming: spec.State → Bool

data: Data

data_valid: Data.valid data

env_r: spec.Reservation

data': Data

locked: Bool

initial_valid: validate (env_r + Lock.Locked data) { data := data', locked := locked }

this: data = data'

f_validvalidate (env_r + Lock.Unlocked) { data := { data := data', locked := locked }.data, locked := false } ∧   Lock.Unlocked = Lock.Unlocked
  
  assuming: spec.State → Bool

data: Data

data_valid: Data.valid data

valid (atomic_read_modify fun s => { data := s.data, locked := false }) (Lock.Locked data) assuming fun x r =>
  r = Lock.Unlockedsimp only [initial_valid: validate (env_r + Lock.Locked data) { data := data', locked := locked }
initial_valid.elim_locked: ∀ {env_r : Reservation} {d : Data} {s' : State},
  validate (env_r + Lock.Locked d) s' → env_r = Lock.Unlocked ∧ d = s'.data ∧ s'.locked = true
elim_locked, and_true: ∀ (p : Prop), (p ∧ True) = p
and_true]assuming: spec.State → Bool

data: Data

data_valid: Data.valid data

env_r: spec.Reservation

data': Data

locked: Bool

initial_valid: validate (env_r + Lock.Locked data) { data := data', locked := locked }

this: data = data'

f_validvalidate (Lock.Unlocked + Lock.Unlocked) { data := data', locked := false }
  
  assuming: spec.State → Bool

data: Data

data_valid: Data.valid data

valid (atomic_read_modify fun s => { data := s.data, locked := false }) (Lock.Locked data) assuming fun x r =>
  r = Lock.Unlockedapply validate.unlocked: ∀ {data : Data}, Data.valid data → validate Lock.Unlocked { data := data, locked := false }
validate.unlockedassuming: spec.State → Bool

data: Data

data_valid: Data.valid data

env_r: spec.Reservation

data': Data

locked: Bool

initial_valid: validate (env_r + Lock.Locked data) { data := data', locked := locked }

this: data = data'

f_valid.aData.valid data'
  assuming: spec.State → Bool

data: Data

data_valid: Data.valid data

valid (atomic_read_modify fun s => { data := s.data, locked := false }) (Lock.Locked data) assuming fun x r =>
  r = Lock.Unlockedrw [assuming: spec.State → Bool

data: Data

data_valid: Data.valid data

env_r: spec.Reservation

data': Data

locked: Bool

initial_valid: validate (env_r + Lock.Locked data) { data := data', locked := locked }

this: data = data'

f_valid.aData.valid data'<- this: data = data'
thisassuming: spec.State → Bool

data: Data

data_valid: Data.valid data

env_r: spec.Reservation

data': Data

locked: Bool

initial_valid: validate (env_r + Lock.Locked data) { data := data', locked := locked }

this: data = data'

f_valid.aData.valid data]assuming: spec.State → Bool

data: Data

data_valid: Data.valid data

env_r: spec.Reservation

data': Data

locked: Bool

initial_valid: validate (env_r + Lock.Locked data) { data := data', locked := locked }

this: data = data'

f_valid.aData.valid data
  assuming: spec.State → Bool

data: Data

data_valid: Data.valid data

valid (atomic_read_modify fun s => { data := s.data, locked := false }) (Lock.Locked data) assuming fun x r =>
  r = Lock.Unlockedexact data_valid: Data.valid data
data_valid
Goals accomplished! 🐙

theorem thread1_valid: Thread.valid thread1
thread1_valid : thread1: Thread spec
thread1.valid: {spec : Spec} → Thread spec → Prop
valid :=by
  
Thread.valid thread1rw [
Thread.valid thread1Thread.valid: {spec : Spec} → Thread spec → Prop
Thread.valid
valid thread1.task IsReservation.empty thread1.block_until fun x r => r = IsReservation.empty]
valid thread1.task IsReservation.empty thread1.block_until fun x r => r = IsReservation.empty
  
Thread.valid thread1apply valid_bind_mutex_lock: ∀ {T : Type} {cont : TaskM spec T} {assuming : spec.State → Bool} {motive : T → spec.Reservation → Prop},
  (∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive) →
    valid
      (do
        atomic_blocking_rmr
            (fun x =>
              match x with
              | { data := data, locked := locked } => decide (locked = false))
            fun s => (PUnit.unit, { data := s.data, locked := true })
        cont)
      Lock.Unlocked assuming motive
valid_bind_mutex_lock
cont_valid∀ (x : Nat),
  valid
    (do
      atomic_read_modify fun s =>
          { data :=
              let src := s.data;
              { x := s.data.x + 1, y := src.y },
            locked := s.locked }
      atomic_read_modify fun s =>
          { data :=
              let src := s.data;
              { x := src.x, y := s.data.y + 1 },
            locked := s.locked }
      atomic_read_modify fun s => { data := s.data, locked := false })
    (Lock.Locked { x := x, y := x }) (fun x => true) fun x r => r = IsReservation.empty

  
Thread.valid thread1intro x0: Nat
x0x0: Nat

cont_validvalid
  (do
    atomic_read_modify fun s =>
        { data :=
            let src := s.data;
            { x := s.data.x + 1, y := src.y },
          locked := s.locked }
    atomic_read_modify fun s =>
        { data :=
            let src := s.data;
            { x := src.x, y := s.data.y + 1 },
          locked := s.locked }
    atomic_read_modify fun s => { data := s.data, locked := false })
  (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun x r => r = IsReservation.empty
  
Thread.valid thread1apply valid_bind: ∀ {spec : Spec} {U V : Type} {mu : TaskM spec U} {f : U → TaskM spec V} {r : spec.Reservation}
  {assuming : spec.State → Bool} {motive : V → spec.Reservation → Prop} (motive_u : U → spec.Reservation → Prop),
  valid mu r assuming motive_u →
    (∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive) →
      valid (mu >>= f) r assuming motive
valid_bind (spec :=spec: Spec
spec) λ ⟨⟩ r': ?m.6636
r' => r': ?m.6636
r' = Lock.Locked: {T : Type} → T → Lock T
Lock.Locked ⟨x0: Nat
x0 + 1: ?m.6889
1, x0: Nat
x0⟩x0: Nat

cont_valid.mu_validvalid
  (atomic_read_modify fun s =>
    { data :=
        let src := s.data;
        { x := s.data.x + 1, y := src.y },
      locked := s.locked })
  (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun x r' => r' = Lock.Locked { x := x0 + 1, y := x0 }
x0: Nat

cont_valid.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = Lock.Locked { x := x0 + 1, y := x0 } →
      valid
        (do
          atomic_read_modify fun s =>
              { data :=
                  let src := s.data;
                  { x := src.x, y := s.data.y + 1 },
                locked := s.locked }
          atomic_read_modify fun s => { data := s.data, locked := false })
        r' (fun x => true) fun x r => r = IsReservation.empty
  
Thread.valid thread1.x0: Nat

cont_valid.mu_validvalid
  (atomic_read_modify fun s =>
    { data :=
        let src := s.data;
        { x := s.data.x + 1, y := src.y },
      locked := s.locked })
  (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun x r' => r' = Lock.Locked { x := x0 + 1, y := x0 } -- validate ++x
    x0: Nat

cont_valid.mu_validvalid
  (atomic_read_modify fun s =>
    { data :=
        let src := s.data;
        { x := s.data.x + 1, y := src.y },
      locked := s.locked })
  (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun x r' => r' = Lock.Locked { x := x0 + 1, y := x0 }
x0: Nat

cont_valid.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = Lock.Locked { x := x0 + 1, y := x0 } →
      valid
        (do
          atomic_read_modify fun s =>
              { data :=
                  let src := s.data;
                  { x := src.x, y := s.data.y + 1 },
                locked := s.locked }
          atomic_read_modify fun s => { data := s.data, locked := false })
        r' (fun x => true) fun x r => r = IsReservation.emptyapply valid_rm: ∀ {spec : Spec} {f : spec.State → spec.State} {r : spec.Reservation} {assuming : spec.State → Bool}
  {motive : Unit → spec.Reservation → Prop},
  (∀ (env_r : spec.Reservation) (s : spec.State),
      assuming s = true →
        Spec.validate spec (env_r + r) s →
          ∃ r',
            let s' := f s;
            Spec.validate spec (env_r + r') s' ∧ motive PUnit.unit r') →
    valid (atomic_read_modify f) r assuming motive
valid_rmx0: Nat

cont_valid.mu_valid.f_valid∀ (env_r : spec.Reservation) (s : spec.State),
  true = true →
    Spec.validate spec (env_r + Lock.Locked { x := x0, y := x0 }) s →
      ∃ r',
        let s' :=
          { data :=
              let src := s.data;
              { x := s.data.x + 1, y := src.y },
            locked := s.locked };
        Spec.validate spec (env_r + r') s' ∧ r' = Lock.Locked { x := x0 + 1, y := x0 }
    x0: Nat

cont_valid.mu_validvalid
  (atomic_read_modify fun s =>
    { data :=
        let src := s.data;
        { x := s.data.x + 1, y := src.y },
      locked := s.locked })
  (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun x r' => r' = Lock.Locked { x := x0 + 1, y := x0 }
x0: Nat

cont_valid.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = Lock.Locked { x := x0 + 1, y := x0 } →
      valid
        (do
          atomic_read_modify fun s =>
              { data :=
                  let src := s.data;
                  { x := src.x, y := s.data.y + 1 },
                locked := s.locked }
          atomic_read_modify fun s => { data := s.data, locked := false })
        r' (fun x => true) fun x r => r = IsReservation.emptysimp only [spec: Spec
spec]x0: Nat

cont_valid.mu_valid.f_valid∀ (env_r : spec.Reservation) (s : spec.State),
  True →
    validate (env_r + Lock.Locked { x := x0, y := x0 }) s →
      ∃ r',
        validate (env_r + r') { data := { x := s.data.x + 1, y := s.data.y }, locked := s.locked } ∧           r' = Lock.Locked { x := x0 + 1, y := x0 }
    x0: Nat

cont_valid.mu_validvalid
  (atomic_read_modify fun s =>
    { data :=
        let src := s.data;
        { x := s.data.x + 1, y := src.y },
      locked := s.locked })
  (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun x r' => r' = Lock.Locked { x := x0 + 1, y := x0 }
x0: Nat

cont_valid.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = Lock.Locked { x := x0 + 1, y := x0 } →
      valid
        (do
          atomic_read_modify fun s =>
              { data :=
                  let src := s.data;
                  { x := src.x, y := s.data.y + 1 },
                locked := s.locked }
          atomic_read_modify fun s => { data := s.data, locked := false })
        r' (fun x => true) fun x r => r = IsReservation.emptyintro env_r: spec.Reservation
env_r ⟨⟨x: Nat
x, y: Nat
y⟩, locked: Bool
locked⟩ ⟨⟩ initial_valid: validate (env_r + Lock.Locked { x := x0, y := x0 }) { data := { x := x, y := y }, locked := locked }
initial_validx0: Nat

env_r: spec.Reservation

x, y: Nat

locked: Bool

initial_valid: validate (env_r + Lock.Locked { x := x0, y := x0 }) { data := { x := x, y := y }, locked := locked }

cont_valid.mu_valid.f_valid∃ r',
  validate (env_r + r')
      { data :=
          { x := { data := { x := x, y := y }, locked := locked }.data.x + 1,
            y := { data := { x := x, y := y }, locked := locked }.data.y },
        locked := { data := { x := x, y := y }, locked := locked }.locked } ∧     r' = Lock.Locked { x := x0 + 1, y := x0 }
    x0: Nat

cont_valid.mu_validvalid
  (atomic_read_modify fun s =>
    { data :=
        let src := s.data;
        { x := s.data.x + 1, y := src.y },
      locked := s.locked })
  (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun x r' => r' = Lock.Locked { x := x0 + 1, y := x0 }
x0: Nat

cont_valid.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = Lock.Locked { x := x0 + 1, y := x0 } →
      valid
        (do
          atomic_read_modify fun s =>
              { data :=
                  let src := s.data;
                  { x := src.x, y := s.data.y + 1 },
                locked := s.locked }
          atomic_read_modify fun s => { data := s.data, locked := false })
        r' (fun x => true) fun x r => r = IsReservation.emptyexists Lock.Locked: {T : Type} → T → Lock T
Lock.Locked ⟨x0: Nat
x0 + 1: ?m.7388
1, x0: Nat
x0⟩x0: Nat

env_r: spec.Reservation

x, y: Nat

locked: Bool

initial_valid: validate (env_r + Lock.Locked { x := x0, y := x0 }) { data := { x := x, y := y }, locked := locked }

cont_valid.mu_valid.f_validvalidate (env_r + Lock.Locked { x := x0 + 1, y := x0 })
    { data :=
        { x := { data := { x := x, y := y }, locked := locked }.data.x + 1,
          y := { data := { x := x, y := y }, locked := locked }.data.y },
      locked := { data := { x := x, y := y }, locked := locked }.locked } ∧   Lock.Locked { x := x0 + 1, y := x0 } = Lock.Locked { x := x0 + 1, y := x0 }
    
    x0: Nat

cont_valid.mu_validvalid
  (atomic_read_modify fun s =>
    { data :=
        let src := s.data;
        { x := s.data.x + 1, y := src.y },
      locked := s.locked })
  (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun x r' => r' = Lock.Locked { x := x0 + 1, y := x0 }
x0: Nat

cont_valid.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = Lock.Locked { x := x0 + 1, y := x0 } →
      valid
        (do
          atomic_read_modify fun s =>
              { data :=
                  let src := s.data;
                  { x := src.x, y := s.data.y + 1 },
                locked := s.locked }
          atomic_read_modify fun s => { data := s.data, locked := false })
        r' (fun x => true) fun x r => r = IsReservation.emptysimp only [initial_valid: validate (env_r + Lock.Locked { x := x0, y := x0 }) { data := { x := x, y := y }, locked := locked }
initial_valid.elim_locked: ∀ {env_r : Reservation} {d : Data} {s' : State},
  validate (env_r + Lock.Locked d) s' → env_r = Lock.Unlocked ∧ d = s'.data ∧ s'.locked = true
elim_locked, Lock.unlocked_add: ∀ {T : Type} (a : Lock T), Lock.Unlocked + a = a
Lock.unlocked_add]x0: Nat

env_r: spec.Reservation

x, y: Nat

locked: Bool

initial_valid: validate (env_r + Lock.Locked { x := x0, y := x0 }) { data := { x := x, y := y }, locked := locked }

cont_valid.mu_valid.f_validvalidate (Lock.Locked { x := x0 + 1, y := x0 }) { data := { x := x + 1, y := y }, locked := true } ∧ True
    x0: Nat

cont_valid.mu_validvalid
  (atomic_read_modify fun s =>
    { data :=
        let src := s.data;
        { x := s.data.x + 1, y := src.y },
      locked := s.locked })
  (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun x r' => r' = Lock.Locked { x := x0 + 1, y := x0 }
x0: Nat

cont_valid.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = Lock.Locked { x := x0 + 1, y := x0 } →
      valid
        (do
          atomic_read_modify fun s =>
              { data :=
                  let src := s.data;
                  { x := src.x, y := s.data.y + 1 },
                locked := s.locked }
          atomic_read_modify fun s => { data := s.data, locked := false })
        r' (fun x => true) fun x r => r = IsReservation.emptyinjection initial_valid: validate (env_r + Lock.Locked { x := x0, y := x0 }) { data := { x := x, y := y }, locked := locked }
initial_valid.elim_locked: ∀ {env_r : Reservation} {d : Data} {s' : State},
  validate (env_r + Lock.Locked d) s' → env_r = Lock.Unlocked ∧ d = s'.data ∧ s'.locked = true
elim_locked.right: ∀ {a b : Prop}, a ∧ b → b
right.left: ∀ {a b : Prop}, a ∧ b → a
leftx0: Nat

env_r: spec.Reservation

x, y: Nat

locked: Bool

initial_valid: validate (env_r + Lock.Locked { x := x0, y := x0 }) { data := { x := x, y := y }, locked := locked }

cont_valid.mu_valid.f_validvalidate (Lock.Locked { x := x0 + 1, y := x0 }) { data := { x := x + 1, y := y }, locked := true } ∧ True
    x0: Nat

cont_valid.mu_validvalid
  (atomic_read_modify fun s =>
    { data :=
        let src := s.data;
        { x := s.data.x + 1, y := src.y },
      locked := s.locked })
  (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun x r' => r' = Lock.Locked { x := x0 + 1, y := x0 }
x0: Nat

cont_valid.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = Lock.Locked { x := x0 + 1, y := x0 } →
      valid
        (do
          atomic_read_modify fun s =>
              { data :=
                  let src := s.data;
                  { x := src.x, y := s.data.y + 1 },
                locked := s.locked }
          atomic_read_modify fun s => { data := s.data, locked := false })
        r' (fun x => true) fun x r => r = IsReservation.emptyrename_i x0_def: x0 = x
x0_def y0_def: x0 = y
y0_defx0: Nat

env_r: spec.Reservation

x, y: Nat

locked: Bool

initial_valid: validate (env_r + Lock.Locked { x := x0, y := x0 }) { data := { x := x, y := y }, locked := locked }

x0_def: x0 = x

y0_def: x0 = y

cont_valid.mu_valid.f_validvalidate (Lock.Locked { x := x0 + 1, y := x0 }) { data := { x := x + 1, y := y }, locked := true } ∧ True
    x0: Nat

cont_valid.mu_validvalid
  (atomic_read_modify fun s =>
    { data :=
        let src := s.data;
        { x := s.data.x + 1, y := src.y },
      locked := s.locked })
  (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun x r' => r' = Lock.Locked { x := x0 + 1, y := x0 }
x0: Nat

cont_valid.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = Lock.Locked { x := x0 + 1, y := x0 } →
      valid
        (do
          atomic_read_modify fun s =>
              { data :=
                  let src := s.data;
                  { x := src.x, y := s.data.y + 1 },
                locked := s.locked }
          atomic_read_modify fun s => { data := s.data, locked := false })
        r' (fun x => true) fun x r => r = IsReservation.emptysimp only [<- x0_def: x0 = x
x0_def, <- y0_def: x0 = y
y0_def]x0: Nat

env_r: spec.Reservation

x, y: Nat

locked: Bool

initial_valid: validate (env_r + Lock.Locked { x := x0, y := x0 }) { data := { x := x, y := y }, locked := locked }

x0_def: x0 = x

y0_def: x0 = y

cont_valid.mu_valid.f_validvalidate (Lock.Locked { x := x0 + 1, y := x0 }) { data := { x := x0 + 1, y := x0 }, locked := true } ∧ True
    x0: Nat

cont_valid.mu_validvalid
  (atomic_read_modify fun s =>
    { data :=
        let src := s.data;
        { x := s.data.x + 1, y := src.y },
      locked := s.locked })
  (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun x r' => r' = Lock.Locked { x := x0 + 1, y := x0 }
x0: Nat

cont_valid.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = Lock.Locked { x := x0 + 1, y := x0 } →
      valid
        (do
          atomic_read_modify fun s =>
              { data :=
                  let src := s.data;
                  { x := src.x, y := s.data.y + 1 },
                locked := s.locked }
          atomic_read_modify fun s => { data := s.data, locked := false })
        r' (fun x => true) fun x r => r = IsReservation.emptyexact ⟨validate.locked: ∀ (data : Data), validate (Lock.Locked data) { data := data, locked := true }
validate.locked _: Data
_, ⟨⟩: True
⟨⟩⟩
Goals accomplished! 🐙
  
  
Thread.valid thread1intro r: spec.Reservation
r ⟨⟩ r_def: r = Lock.Locked { x := x0 + 1, y := x0 }
r_defx0: Nat

r: spec.Reservation

r_def: r = Lock.Locked { x := x0 + 1, y := x0 }

cont_valid.f_validvalid
  (do
    atomic_read_modify fun s =>
        { data :=
            let src := s.data;
            { x := src.x, y := s.data.y + 1 },
          locked := s.locked }
    atomic_read_modify fun s => { data := s.data, locked := false })
  r (fun x => true) fun x r => r = IsReservation.empty
  
Thread.valid thread1rw [x0: Nat

r: spec.Reservation

r_def: r = Lock.Locked { x := x0 + 1, y := x0 }

cont_valid.f_validvalid
  (do
    atomic_read_modify fun s =>
        { data :=
            let src := s.data;
            { x := src.x, y := s.data.y + 1 },
          locked := s.locked }
    atomic_read_modify fun s => { data := s.data, locked := false })
  r (fun x => true) fun x r => r = IsReservation.emptyr_def: r = Lock.Locked { x := x0 + 1, y := x0 }
r_defx0: Nat

r: spec.Reservation

r_def: r = Lock.Locked { x := x0 + 1, y := x0 }

cont_valid.f_validvalid
  (do
    atomic_read_modify fun s =>
        { data :=
            let src := s.data;
            { x := src.x, y := s.data.y + 1 },
          locked := s.locked }
    atomic_read_modify fun s => { data := s.data, locked := false })
  (Lock.Locked { x := x0 + 1, y := x0 }) (fun x => true) fun x r => r = IsReservation.empty]x0: Nat

r: spec.Reservation

r_def: r = Lock.Locked { x := x0 + 1, y := x0 }

cont_valid.f_validvalid
  (do
    atomic_read_modify fun s =>
        { data :=
            let src := s.data;
            { x := src.x, y := s.data.y + 1 },
          locked := s.locked }
    atomic_read_modify fun s => { data := s.data, locked := false })
  (Lock.Locked { x := x0 + 1, y := x0 }) (fun x => true) fun x r => r = IsReservation.empty 
Thread.valid thread1;x0: Nat

r: spec.Reservation

r_def: r = Lock.Locked { x := x0 + 1, y := x0 }

cont_valid.f_validvalid
  (do
    atomic_read_modify fun s =>
        { data :=
            let src := s.data;
            { x := src.x, y := s.data.y + 1 },
          locked := s.locked }
    atomic_read_modify fun s => { data := s.data, locked := false })
  (Lock.Locked { x := x0 + 1, y := x0 }) (fun x => true) fun x r => r = IsReservation.empty 
Thread.valid thread1clear r_def: r = Lock.Locked { x := x0 + 1, y := x0 }
r_def r: spec.Reservation
rx0: Nat

cont_valid.f_validvalid
  (do
    atomic_read_modify fun s =>
        { data :=
            let src := s.data;
            { x := src.x, y := s.data.y + 1 },
          locked := s.locked }
    atomic_read_modify fun s => { data := s.data, locked := false })
  (Lock.Locked { x := x0 + 1, y := x0 }) (fun x => true) fun x r => r = IsReservation.empty
  
Thread.valid thread1apply valid_bind: ∀ {spec : Spec} {U V : Type} {mu : TaskM spec U} {f : U → TaskM spec V} {r : spec.Reservation}
  {assuming : spec.State → Bool} {motive : V → spec.Reservation → Prop} (motive_u : U → spec.Reservation → Prop),
  valid mu r assuming motive_u →
    (∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive) →
      valid (mu >>= f) r assuming motive
valid_bind (spec :=spec: Spec
spec) λ ⟨⟩ r': ?m.8041
r' => r': ?m.8041
r' = Lock.Locked: {T : Type} → T → Lock T
Lock.Locked ⟨x0: Nat
x0 + 1: ?m.8311
1, x0: Nat
x0 + 1: ?m.8344
1⟩x0: Nat

cont_valid.f_valid.mu_validvalid
  (atomic_read_modify fun s =>
    { data :=
        let src := s.data;
        { x := src.x, y := s.data.y + 1 },
      locked := s.locked })
  (Lock.Locked { x := x0 + 1, y := x0 }) (fun x => true) fun x r' => r' = Lock.Locked { x := x0 + 1, y := x0 + 1 }
x0: Nat

cont_valid.f_valid.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = Lock.Locked { x := x0 + 1, y := x0 + 1 } →
      valid (atomic_read_modify fun s => { data := s.data, locked := false }) r' (fun x => true) fun x r =>
        r = IsReservation.empty
  
Thread.valid thread1.x0: Nat

cont_valid.f_valid.mu_validvalid
  (atomic_read_modify fun s =>
    { data :=
        let src := s.data;
        { x := src.x, y := s.data.y + 1 },
      locked := s.locked })
  (Lock.Locked { x := x0 + 1, y := x0 }) (fun x => true) fun x r' => r' = Lock.Locked { x := x0 + 1, y := x0 + 1 } -- validate ++y
    x0: Nat

cont_valid.f_valid.mu_validvalid
  (atomic_read_modify fun s =>
    { data :=
        let src := s.data;
        { x := src.x, y := s.data.y + 1 },
      locked := s.locked })
  (Lock.Locked { x := x0 + 1, y := x0 }) (fun x => true) fun x r' => r' = Lock.Locked { x := x0 + 1, y := x0 + 1 }
x0: Nat

cont_valid.f_valid.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = Lock.Locked { x := x0 + 1, y := x0 + 1 } →
      valid (atomic_read_modify fun s => { data := s.data, locked := false }) r' (fun x => true) fun x r =>
        r = IsReservation.emptyapply valid_rm: ∀ {spec : Spec} {f : spec.State → spec.State} {r : spec.Reservation} {assuming : spec.State → Bool}
  {motive : Unit → spec.Reservation → Prop},
  (∀ (env_r : spec.Reservation) (s : spec.State),
      assuming s = true →
        Spec.validate spec (env_r + r) s →
          ∃ r',
            let s' := f s;
            Spec.validate spec (env_r + r') s' ∧ motive PUnit.unit r') →
    valid (atomic_read_modify f) r assuming motive
valid_rmx0: Nat

cont_valid.f_valid.mu_valid.f_valid∀ (env_r : spec.Reservation) (s : spec.State),
  true = true →
    Spec.validate spec (env_r + Lock.Locked { x := x0 + 1, y := x0 }) s →
      ∃ r',
        let s' :=
          { data :=
              let src := s.data;
              { x := src.x, y := s.data.y + 1 },
            locked := s.locked };
        Spec.validate spec (env_r + r') s' ∧ r' = Lock.Locked { x := x0 + 1, y := x0 + 1 }
    x0: Nat

cont_valid.f_valid.mu_validvalid
  (atomic_read_modify fun s =>
    { data :=
        let src := s.data;
        { x := src.x, y := s.data.y + 1 },
      locked := s.locked })
  (Lock.Locked { x := x0 + 1, y := x0 }) (fun x => true) fun x r' => r' = Lock.Locked { x := x0 + 1, y := x0 + 1 }
x0: Nat

cont_valid.f_valid.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = Lock.Locked { x := x0 + 1, y := x0 + 1 } →
      valid (atomic_read_modify fun s => { data := s.data, locked := false }) r' (fun x => true) fun x r =>
        r = IsReservation.emptysimp only [spec: Spec
spec]x0: Nat

cont_valid.f_valid.mu_valid.f_valid∀ (env_r : spec.Reservation) (s : spec.State),
  True →
    validate (env_r + Lock.Locked { x := x0 + 1, y := x0 }) s →
      ∃ r',
        validate (env_r + r') { data := { x := s.data.x, y := s.data.y + 1 }, locked := s.locked } ∧           r' = Lock.Locked { x := x0 + 1, y := x0 + 1 }
    x0: Nat

cont_valid.f_valid.mu_validvalid
  (atomic_read_modify fun s =>
    { data :=
        let src := s.data;
        { x := src.x, y := s.data.y + 1 },
      locked := s.locked })
  (Lock.Locked { x := x0 + 1, y := x0 }) (fun x => true) fun x r' => r' = Lock.Locked { x := x0 + 1, y := x0 + 1 }
x0: Nat

cont_valid.f_valid.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = Lock.Locked { x := x0 + 1, y := x0 + 1 } →
      valid (atomic_read_modify fun s => { data := s.data, locked := false }) r' (fun x => true) fun x r =>
        r = IsReservation.emptyintro env_r: spec.Reservation
env_r ⟨⟨x: Nat
x, y: Nat
y⟩, locked: Bool
locked⟩ ⟨⟩ initial_valid: validate (env_r + Lock.Locked { x := x0 + 1, y := x0 }) { data := { x := x, y := y }, locked := locked }
initial_validx0: Nat

env_r: spec.Reservation

x, y: Nat

locked: Bool

initial_valid: validate (env_r + Lock.Locked { x := x0 + 1, y := x0 }) { data := { x := x, y := y }, locked := locked }

cont_valid.f_valid.mu_valid.f_valid∃ r',
  validate (env_r + r')
      { data :=
          { x := { data := { x := x, y := y }, locked := locked }.data.x,
            y := { data := { x := x, y := y }, locked := locked }.data.y + 1 },
        locked := { data := { x := x, y := y }, locked := locked }.locked } ∧     r' = Lock.Locked { x := x0 + 1, y := x0 + 1 }
    x0: Nat

cont_valid.f_valid.mu_validvalid
  (atomic_read_modify fun s =>
    { data :=
        let src := s.data;
        { x := src.x, y := s.data.y + 1 },
      locked := s.locked })
  (Lock.Locked { x := x0 + 1, y := x0 }) (fun x => true) fun x r' => r' = Lock.Locked { x := x0 + 1, y := x0 + 1 }
x0: Nat

cont_valid.f_valid.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = Lock.Locked { x := x0 + 1, y := x0 + 1 } →
      valid (atomic_read_modify fun s => { data := s.data, locked := false }) r' (fun x => true) fun x r =>
        r = IsReservation.emptyexists Lock.Locked: {T : Type} → T → Lock T
Lock.Locked ⟨x0: Nat
x0 + 1: ?m.8733
1, x0: Nat
x0 + 1: ?m.8766
1⟩x0: Nat

env_r: spec.Reservation

x, y: Nat

locked: Bool

initial_valid: validate (env_r + Lock.Locked { x := x0 + 1, y := x0 }) { data := { x := x, y := y }, locked := locked }

cont_valid.f_valid.mu_valid.f_validvalidate (env_r + Lock.Locked { x := x0 + 1, y := x0 + 1 })
    { data :=
        { x := { data := { x := x, y := y }, locked := locked }.data.x,
          y := { data := { x := x, y := y }, locked := locked }.data.y + 1 },
      locked := { data := { x := x, y := y }, locked := locked }.locked } ∧   Lock.Locked { x := x0 + 1, y := x0 + 1 } = Lock.Locked { x := x0 + 1, y := x0 + 1 }
    x0: Nat

cont_valid.f_valid.mu_validvalid
  (atomic_read_modify fun s =>
    { data :=
        let src := s.data;
        { x := src.x, y := s.data.y + 1 },
      locked := s.locked })
  (Lock.Locked { x := x0 + 1, y := x0 }) (fun x => true) fun x r' => r' = Lock.Locked { x := x0 + 1, y := x0 + 1 }
x0: Nat

cont_valid.f_valid.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = Lock.Locked { x := x0 + 1, y := x0 + 1 } →
      valid (atomic_read_modify fun s => { data := s.data, locked := false }) r' (fun x => true) fun x r =>
        r = IsReservation.emptysimp only [initial_valid: validate (env_r + Lock.Locked { x := x0 + 1, y := x0 }) { data := { x := x, y := y }, locked := locked }
initial_valid.elim_locked: ∀ {env_r : Reservation} {d : Data} {s' : State},
  validate (env_r + Lock.Locked d) s' → env_r = Lock.Unlocked ∧ d = s'.data ∧ s'.locked = true
elim_locked, Lock.unlocked_add: ∀ {T : Type} (a : Lock T), Lock.Unlocked + a = a
Lock.unlocked_add]x0: Nat

env_r: spec.Reservation

x, y: Nat

locked: Bool

initial_valid: validate (env_r + Lock.Locked { x := x0 + 1, y := x0 }) { data := { x := x, y := y }, locked := locked }

cont_valid.f_valid.mu_valid.f_validvalidate (Lock.Locked { x := x0 + 1, y := x0 + 1 }) { data := { x := x, y := y + 1 }, locked := true } ∧ True
    x0: Nat

cont_valid.f_valid.mu_validvalid
  (atomic_read_modify fun s =>
    { data :=
        let src := s.data;
        { x := src.x, y := s.data.y + 1 },
      locked := s.locked })
  (Lock.Locked { x := x0 + 1, y := x0 }) (fun x => true) fun x r' => r' = Lock.Locked { x := x0 + 1, y := x0 + 1 }
x0: Nat

cont_valid.f_valid.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = Lock.Locked { x := x0 + 1, y := x0 + 1 } →
      valid (atomic_read_modify fun s => { data := s.data, locked := false }) r' (fun x => true) fun x r =>
        r = IsReservation.emptyinjection initial_valid: validate (env_r + Lock.Locked { x := x0 + 1, y := x0 }) { data := { x := x, y := y }, locked := locked }
initial_valid.elim_locked: ∀ {env_r : Reservation} {d : Data} {s' : State},
  validate (env_r + Lock.Locked d) s' → env_r = Lock.Unlocked ∧ d = s'.data ∧ s'.locked = true
elim_locked.right: ∀ {a b : Prop}, a ∧ b → b
right.left: ∀ {a b : Prop}, a ∧ b → a
leftx0: Nat

env_r: spec.Reservation

x, y: Nat

locked: Bool

initial_valid: validate (env_r + Lock.Locked { x := x0 + 1, y := x0 }) { data := { x := x, y := y }, locked := locked }

cont_valid.f_valid.mu_valid.f_validvalidate (Lock.Locked { x := x0 + 1, y := x0 + 1 }) { data := { x := x, y := y + 1 }, locked := true } ∧ True
    x0: Nat

cont_valid.f_valid.mu_validvalid
  (atomic_read_modify fun s =>
    { data :=
        let src := s.data;
        { x := src.x, y := s.data.y + 1 },
      locked := s.locked })
  (Lock.Locked { x := x0 + 1, y := x0 }) (fun x => true) fun x r' => r' = Lock.Locked { x := x0 + 1, y := x0 + 1 }
x0: Nat

cont_valid.f_valid.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = Lock.Locked { x := x0 + 1, y := x0 + 1 } →
      valid (atomic_read_modify fun s => { data := s.data, locked := false }) r' (fun x => true) fun x r =>
        r = IsReservation.emptyrename_i x0_def: x0 + 1 = x
x0_def y0_def: x0 = y
y0_defx0: Nat

env_r: spec.Reservation

x, y: Nat

locked: Bool

initial_valid: validate (env_r + Lock.Locked { x := x0 + 1, y := x0 }) { data := { x := x, y := y }, locked := locked }

x0_def: x0 + 1 = x

y0_def: x0 = y

cont_valid.f_valid.mu_valid.f_validvalidate (Lock.Locked { x := x0 + 1, y := x0 + 1 }) { data := { x := x, y := y + 1 }, locked := true } ∧ True
    x0: Nat

cont_valid.f_valid.mu_validvalid
  (atomic_read_modify fun s =>
    { data :=
        let src := s.data;
        { x := src.x, y := s.data.y + 1 },
      locked := s.locked })
  (Lock.Locked { x := x0 + 1, y := x0 }) (fun x => true) fun x r' => r' = Lock.Locked { x := x0 + 1, y := x0 + 1 }
x0: Nat

cont_valid.f_valid.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = Lock.Locked { x := x0 + 1, y := x0 + 1 } →
      valid (atomic_read_modify fun s => { data := s.data, locked := false }) r' (fun x => true) fun x r =>
        r = IsReservation.emptysimp only [<- x0_def: x0 + 1 = x
x0_def, <- y0_def: x0 = y
y0_def]x0: Nat

env_r: spec.Reservation

x, y: Nat

locked: Bool

initial_valid: validate (env_r + Lock.Locked { x := x0 + 1, y := x0 }) { data := { x := x, y := y }, locked := locked }

x0_def: x0 + 1 = x

y0_def: x0 = y

cont_valid.f_valid.mu_valid.f_validvalidate (Lock.Locked { x := x0 + 1, y := x0 + 1 }) { data := { x := x0 + 1, y := x0 + 1 }, locked := true } ∧ True
    x0: Nat

cont_valid.f_valid.mu_validvalid
  (atomic_read_modify fun s =>
    { data :=
        let src := s.data;
        { x := src.x, y := s.data.y + 1 },
      locked := s.locked })
  (Lock.Locked { x := x0 + 1, y := x0 }) (fun x => true) fun x r' => r' = Lock.Locked { x := x0 + 1, y := x0 + 1 }
x0: Nat

cont_valid.f_valid.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = Lock.Locked { x := x0 + 1, y := x0 + 1 } →
      valid (atomic_read_modify fun s => { data := s.data, locked := false }) r' (fun x => true) fun x r =>
        r = IsReservation.emptyexact ⟨validate.locked: ∀ (data : Data), validate (Lock.Locked data) { data := data, locked := true }
validate.locked _: Data
_, ⟨⟩: True
⟨⟩⟩
Goals accomplished! 🐙

  
Thread.valid thread1intro r: spec.Reservation
r ⟨⟩ r_def: r = Lock.Locked { x := x0 + 1, y := x0 + 1 }
r_defx0: Nat

r: spec.Reservation

r_def: r = Lock.Locked { x := x0 + 1, y := x0 + 1 }

cont_valid.f_valid.f_validvalid (atomic_read_modify fun s => { data := s.data, locked := false }) r (fun x => true) fun x r =>
  r = IsReservation.empty
  
Thread.valid thread1rw [x0: Nat

r: spec.Reservation

r_def: r = Lock.Locked { x := x0 + 1, y := x0 + 1 }

cont_valid.f_valid.f_validvalid (atomic_read_modify fun s => { data := s.data, locked := false }) r (fun x => true) fun x r =>
  r = IsReservation.emptyr_def: r = Lock.Locked { x := x0 + 1, y := x0 + 1 }
r_defx0: Nat

r: spec.Reservation

r_def: r = Lock.Locked { x := x0 + 1, y := x0 + 1 }

cont_valid.f_valid.f_validvalid (atomic_read_modify fun s => { data := s.data, locked := false }) (Lock.Locked { x := x0 + 1, y := x0 + 1 })
  (fun x => true) fun x r => r = IsReservation.empty]x0: Nat

r: spec.Reservation

r_def: r = Lock.Locked { x := x0 + 1, y := x0 + 1 }

cont_valid.f_valid.f_validvalid (atomic_read_modify fun s => { data := s.data, locked := false }) (Lock.Locked { x := x0 + 1, y := x0 + 1 })
  (fun x => true) fun x r => r = IsReservation.empty;x0: Nat

r: spec.Reservation

r_def: r = Lock.Locked { x := x0 + 1, y := x0 + 1 }

cont_valid.f_valid.f_validvalid (atomic_read_modify fun s => { data := s.data, locked := false }) (Lock.Locked { x := x0 + 1, y := x0 + 1 })
  (fun x => true) fun x r => r = IsReservation.empty 
Thread.valid thread1clear r_def: r = Lock.Locked { x := x0 + 1, y := x0 + 1 }
r_def r: spec.Reservation
rx0: Nat

cont_valid.f_valid.f_validvalid (atomic_read_modify fun s => { data := s.data, locked := false }) (Lock.Locked { x := x0 + 1, y := x0 + 1 })
  (fun x => true) fun x r => r = IsReservation.empty
  
Thread.valid thread1.x0: Nat

cont_valid.f_valid.f_validvalid (atomic_read_modify fun s => { data := s.data, locked := false }) (Lock.Locked { x := x0 + 1, y := x0 + 1 })
  (fun x => true) fun x r => r = IsReservation.empty -- validate mutex release
    x0: Nat

cont_valid.f_valid.f_validvalid (atomic_read_modify fun s => { data := s.data, locked := false }) (Lock.Locked { x := x0 + 1, y := x0 + 1 })
  (fun x => true) fun x r => r = IsReservation.emptyapply valid_mutex_release: ∀ {assuming : spec.State → Bool} {data : Data},
  Data.valid data →
    valid (atomic_read_modify fun s => { data := s.data, locked := false }) (Lock.Locked data) assuming fun x r =>
      r = Lock.Unlocked
valid_mutex_releasex0: Nat

cont_valid.f_valid.f_valid.data_validData.valid { x := x0 + 1, y := x0 + 1 }
    x0: Nat

cont_valid.f_valid.f_validvalid (atomic_read_modify fun s => { data := s.data, locked := false }) (Lock.Locked { x := x0 + 1, y := x0 + 1 })
  (fun x => true) fun x r => r = IsReservation.emptyrfl
Goals accomplished! 🐙

theorem thread2_valid: Thread.valid thread2
thread2_valid : thread2: Thread spec
thread2.valid: {spec : Spec} → Thread spec → Prop
valid :=by
  
Thread.valid thread2rw [
Thread.valid thread2Thread.valid: {spec : Spec} → Thread spec → Prop
Thread.valid
valid thread2.task IsReservation.empty thread2.block_until fun x r => r = IsReservation.empty]
valid thread2.task IsReservation.empty thread2.block_until fun x r => r = IsReservation.empty
  
Thread.valid thread2apply valid_bind_mutex_lock: ∀ {T : Type} {cont : TaskM spec T} {assuming : spec.State → Bool} {motive : T → spec.Reservation → Prop},
  (∀ (x : Nat), valid cont (Lock.Locked { x := x, y := x }) (fun x => true) motive) →
    valid
      (do
        atomic_blocking_rmr
            (fun x =>
              match x with
              | { data := data, locked := locked } => decide (locked = false))
            fun s => (PUnit.unit, { data := s.data, locked := true })
        cont)
      Lock.Unlocked assuming motive
valid_bind_mutex_lock
cont_valid∀ (x : Nat),
  valid
    (do
      let px ← atomic_read fun s => s.data.x
      let py ← atomic_read fun s => s.data.y
      atomic_assert fun x => decide (px = py)
      atomic_read_modify fun s => { data := s.data, locked := false })
    (Lock.Locked { x := x, y := x }) (fun x => true) fun x r => r = IsReservation.empty
  
  
Thread.valid thread2intro x0: Nat
x0x0: Nat

cont_validvalid
  (do
    let px ← atomic_read fun s => s.data.x
    let py ← atomic_read fun s => s.data.y
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun x r => r = IsReservation.empty
  
Thread.valid thread2apply valid_bind: ∀ {spec : Spec} {U V : Type} {mu : TaskM spec U} {f : U → TaskM spec V} {r : spec.Reservation}
  {assuming : spec.State → Bool} {motive : V → spec.Reservation → Prop} (motive_u : U → spec.Reservation → Prop),
  valid mu r assuming motive_u →
    (∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive) →
      valid (mu >>= f) r assuming motive
valid_bind (spec :=spec: Spec
spec) λ px: ?m.9430
px r': ?m.9433
r' => r': ?m.9433
r' = Lock.Locked: {T : Type} → T → Lock T
Lock.Locked ⟨x0: Nat
x0, x0: Nat
x0⟩ ∧ px: ?m.9430
px = x0: Nat
x0x0: Nat

cont_valid.mu_validvalid (atomic_read fun s => s.data.x) (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun px r' =>
  r' = Lock.Locked { x := x0, y := x0 } ∧ px = x0
x0: Nat

cont_valid.f_valid∀ (r' : spec.Reservation) (u : Nat),
  r' = Lock.Locked { x := x0, y := x0 } ∧ u = x0 →
    valid
      (do
        let py ← atomic_read fun s => s.data.y
        atomic_assert fun x => decide (u = py)
        atomic_read_modify fun s => { data := s.data, locked := false })
      r' (fun x => true) fun x r => r = IsReservation.empty
  
Thread.valid thread2.x0: Nat

cont_valid.mu_validvalid (atomic_read fun s => s.data.x) (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun px r' =>
  r' = Lock.Locked { x := x0, y := x0 } ∧ px = x0 -- verify read of x; we should get x0
    x0: Nat

cont_valid.mu_validvalid (atomic_read fun s => s.data.x) (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun px r' =>
  r' = Lock.Locked { x := x0, y := x0 } ∧ px = x0
x0: Nat

cont_valid.f_valid∀ (r' : spec.Reservation) (u : Nat),
  r' = Lock.Locked { x := x0, y := x0 } ∧ u = x0 →
    valid
      (do
        let py ← atomic_read fun s => s.data.y
        atomic_assert fun x => decide (u = py)
        atomic_read_modify fun s => { data := s.data, locked := false })
      r' (fun x => true) fun x r => r = IsReservation.emptyapply valid_read: ∀ {spec : Spec} {T : Type} {f : spec.State → T} {r : spec.Reservation} {assuming : spec.State → Bool}
  {motive : T → spec.Reservation → Prop},
  (∀ (env_r : spec.Reservation) (s : spec.State),
      assuming s = true →
        Spec.validate spec (env_r + r) s →
          ∃ r',
            let t := f s;
            Spec.validate spec (env_r + r') s ∧ motive t r') →
    valid (atomic_read f) r assuming motive
valid_readx0: Nat

cont_valid.mu_valid.f_valid∀ (env_r : spec.Reservation) (s : spec.State),
  true = true →
    Spec.validate spec (env_r + Lock.Locked { x := x0, y := x0 }) s →
      ∃ r',
        let t := s.data.x;
        Spec.validate spec (env_r + r') s ∧ r' = Lock.Locked { x := x0, y := x0 } ∧ t = x0
    x0: Nat

cont_valid.mu_validvalid (atomic_read fun s => s.data.x) (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun px r' =>
  r' = Lock.Locked { x := x0, y := x0 } ∧ px = x0
x0: Nat

cont_valid.f_valid∀ (r' : spec.Reservation) (u : Nat),
  r' = Lock.Locked { x := x0, y := x0 } ∧ u = x0 →
    valid
      (do
        let py ← atomic_read fun s => s.data.y
        atomic_assert fun x => decide (u = py)
        atomic_read_modify fun s => { data := s.data, locked := false })
      r' (fun x => true) fun x r => r = IsReservation.emptysimp only [spec: Spec
spec]x0: Nat

cont_valid.mu_valid.f_valid∀ (env_r : spec.Reservation) (s : spec.State),
  True →
    validate (env_r + Lock.Locked { x := x0, y := x0 }) s →
      ∃ r', validate (env_r + r') s ∧ r' = Lock.Locked { x := x0, y := x0 } ∧ s.data.x = x0
    x0: Nat

cont_valid.mu_validvalid (atomic_read fun s => s.data.x) (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun px r' =>
  r' = Lock.Locked { x := x0, y := x0 } ∧ px = x0
x0: Nat

cont_valid.f_valid∀ (r' : spec.Reservation) (u : Nat),
  r' = Lock.Locked { x := x0, y := x0 } ∧ u = x0 →
    valid
      (do
        let py ← atomic_read fun s => s.data.y
        atomic_assert fun x => decide (u = py)
        atomic_read_modify fun s => { data := s.data, locked := false })
      r' (fun x => true) fun x r => r = IsReservation.emptyintro env_r: spec.Reservation
env_r ⟨⟨x: Nat
x, y: Nat
y⟩, locked: Bool
locked⟩ ⟨⟩ initial_valid: validate (env_r + Lock.Locked { x := x0, y := x0 }) { data := { x := x, y := y }, locked := locked }
initial_validx0: Nat

env_r: spec.Reservation

x, y: Nat

locked: Bool

initial_valid: validate (env_r + Lock.Locked { x := x0, y := x0 }) { data := { x := x, y := y }, locked := locked }

cont_valid.mu_valid.f_valid∃ r',
  validate (env_r + r') { data := { x := x, y := y }, locked := locked } ∧     r' = Lock.Locked { x := x0, y := x0 } ∧ { data := { x := x, y := y }, locked := locked }.data.x = x0
    x0: Nat

cont_valid.mu_validvalid (atomic_read fun s => s.data.x) (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun px r' =>
  r' = Lock.Locked { x := x0, y := x0 } ∧ px = x0
x0: Nat

cont_valid.f_valid∀ (r' : spec.Reservation) (u : Nat),
  r' = Lock.Locked { x := x0, y := x0 } ∧ u = x0 →
    valid
      (do
        let py ← atomic_read fun s => s.data.y
        atomic_assert fun x => decide (u = py)
        atomic_read_modify fun s => { data := s.data, locked := false })
      r' (fun x => true) fun x r => r = IsReservation.emptyexists Lock.Locked: {T : Type} → T → Lock T
Lock.Locked ⟨x0: Nat
x0, x0: Nat
x0⟩x0: Nat

env_r: spec.Reservation

x, y: Nat

locked: Bool

initial_valid: validate (env_r + Lock.Locked { x := x0, y := x0 }) { data := { x := x, y := y }, locked := locked }

cont_valid.mu_valid.f_validvalidate (env_r + Lock.Locked { x := x0, y := x0 }) { data := { x := x, y := y }, locked := locked } ∧   Lock.Locked { x := x0, y := x0 } = Lock.Locked { x := x0, y := x0 } ∧     { data := { x := x, y := y }, locked := locked }.data.x = x0
    x0: Nat

cont_valid.mu_validvalid (atomic_read fun s => s.data.x) (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun px r' =>
  r' = Lock.Locked { x := x0, y := x0 } ∧ px = x0
x0: Nat

cont_valid.f_valid∀ (r' : spec.Reservation) (u : Nat),
  r' = Lock.Locked { x := x0, y := x0 } ∧ u = x0 →
    valid
      (do
        let py ← atomic_read fun s => s.data.y
        atomic_assert fun x => decide (u = py)
        atomic_read_modify fun s => { data := s.data, locked := false })
      r' (fun x => true) fun x r => r = IsReservation.emptysimp only [initial_valid: validate (env_r + Lock.Locked { x := x0, y := x0 }) { data := { x := x, y := y }, locked := locked }
initial_valid.elim_locked: ∀ {env_r : Reservation} {d : Data} {s' : State},
  validate (env_r + Lock.Locked d) s' → env_r = Lock.Unlocked ∧ d = s'.data ∧ s'.locked = true
elim_locked, Lock.unlocked_add: ∀ {T : Type} (a : Lock T), Lock.Unlocked + a = a
Lock.unlocked_add]x0: Nat

env_r: spec.Reservation

x, y: Nat

locked: Bool

initial_valid: validate (env_r + Lock.Locked { x := x0, y := x0 }) { data := { x := x, y := y }, locked := locked }

cont_valid.mu_valid.f_validvalidate (Lock.Locked { x := x, y := y }) { data := { x := x, y := y }, locked := true } ∧ True ∧ x = x0
    x0: Nat

cont_valid.mu_validvalid (atomic_read fun s => s.data.x) (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun px r' =>
  r' = Lock.Locked { x := x0, y := x0 } ∧ px = x0
x0: Nat

cont_valid.f_valid∀ (r' : spec.Reservation) (u : Nat),
  r' = Lock.Locked { x := x0, y := x0 } ∧ u = x0 →
    valid
      (do
        let py ← atomic_read fun s => s.data.y
        atomic_assert fun x => decide (u = py)
        atomic_read_modify fun s => { data := s.data, locked := false })
      r' (fun x => true) fun x r => r = IsReservation.emptyinjection initial_valid: validate (env_r + Lock.Locked { x := x0, y := x0 }) { data := { x := x, y := y }, locked := locked }
initial_valid.elim_locked: ∀ {env_r : Reservation} {d : Data} {s' : State},
  validate (env_r + Lock.Locked d) s' → env_r = Lock.Unlocked ∧ d = s'.data ∧ s'.locked = true
elim_locked.right: ∀ {a b : Prop}, a ∧ b → b
right.left: ∀ {a b : Prop}, a ∧ b → a
leftx0: Nat

env_r: spec.Reservation

x, y: Nat

locked: Bool

initial_valid: validate (env_r + Lock.Locked { x := x0, y := x0 }) { data := { x := x, y := y }, locked := locked }

cont_valid.mu_valid.f_validvalidate (Lock.Locked { x := x, y := y }) { data := { x := x, y := y }, locked := true } ∧ True ∧ x = x0
    x0: Nat

cont_valid.mu_validvalid (atomic_read fun s => s.data.x) (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun px r' =>
  r' = Lock.Locked { x := x0, y := x0 } ∧ px = x0
x0: Nat

cont_valid.f_valid∀ (r' : spec.Reservation) (u : Nat),
  r' = Lock.Locked { x := x0, y := x0 } ∧ u = x0 →
    valid
      (do
        let py ← atomic_read fun s => s.data.y
        atomic_assert fun x => decide (u = py)
        atomic_read_modify fun s => { data := s.data, locked := false })
      r' (fun x => true) fun x r => r = IsReservation.emptyrename_i x0_def: x0 = x
x0_def y0_def: x0 = y
y0_defx0: Nat

env_r: spec.Reservation

x, y: Nat

locked: Bool

initial_valid: validate (env_r + Lock.Locked { x := x0, y := x0 }) { data := { x := x, y := y }, locked := locked }

x0_def: x0 = x

y0_def: x0 = y

cont_valid.mu_valid.f_validvalidate (Lock.Locked { x := x, y := y }) { data := { x := x, y := y }, locked := true } ∧ True ∧ x = x0
    x0: Nat

cont_valid.mu_validvalid (atomic_read fun s => s.data.x) (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun px r' =>
  r' = Lock.Locked { x := x0, y := x0 } ∧ px = x0
x0: Nat

cont_valid.f_valid∀ (r' : spec.Reservation) (u : Nat),
  r' = Lock.Locked { x := x0, y := x0 } ∧ u = x0 →
    valid
      (do
        let py ← atomic_read fun s => s.data.y
        atomic_assert fun x => decide (u = py)
        atomic_read_modify fun s => { data := s.data, locked := false })
      r' (fun x => true) fun x r => r = IsReservation.emptysimp only [<- x0_def: x0 = x
x0_def, <- y0_def: x0 = y
y0_def, and_true: ∀ (p : Prop), (p ∧ True) = p
and_true]x0: Nat

env_r: spec.Reservation

x, y: Nat

locked: Bool

initial_valid: validate (env_r + Lock.Locked { x := x0, y := x0 }) { data := { x := x, y := y }, locked := locked }

x0_def: x0 = x

y0_def: x0 = y

cont_valid.mu_valid.f_validvalidate (Lock.Locked { x := x0, y := x0 }) { data := { x := x0, y := x0 }, locked := true }
    x0: Nat

cont_valid.mu_validvalid (atomic_read fun s => s.data.x) (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun px r' =>
  r' = Lock.Locked { x := x0, y := x0 } ∧ px = x0
x0: Nat

cont_valid.f_valid∀ (r' : spec.Reservation) (u : Nat),
  r' = Lock.Locked { x := x0, y := x0 } ∧ u = x0 →
    valid
      (do
        let py ← atomic_read fun s => s.data.y
        atomic_assert fun x => decide (u = py)
        atomic_read_modify fun s => { data := s.data, locked := false })
      r' (fun x => true) fun x r => r = IsReservation.emptyexact validate.locked: ∀ (data : Data), validate (Lock.Locked data) { data := data, locked := true }
validate.locked _: Data
_
Goals accomplished! 🐙

  
Thread.valid thread2intro r: spec.Reservation
r px: Nat
px is_locked_and_valid: r = Lock.Locked { x := x0, y := x0 } ∧ px = x0
is_locked_and_validx0: Nat

r: spec.Reservation

px: Nat

is_locked_and_valid: r = Lock.Locked { x := x0, y := x0 } ∧ px = x0

cont_valid.f_validvalid
  (do
    let py ← atomic_read fun s => s.data.y
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  r (fun x => true) fun x r => r = IsReservation.empty
  
Thread.valid thread2cases is_locked_and_valid: r = Lock.Locked { x := x0, y := x0 } ∧ px = x0
is_locked_and_validx0: Nat

r: spec.Reservation

px: Nat

cont_valid.f_valid.introvalid
  (do
    let py ← atomic_read fun s => s.data.y
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  r (fun x => true) fun x r => r = IsReservation.empty 
Thread.valid thread2;x0: Nat

r: spec.Reservation

px: Nat

cont_valid.f_valid.introvalid
  (do
    let py ← atomic_read fun s => s.data.y
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  r (fun x => true) fun x r => r = IsReservation.empty 
Thread.valid thread2rename_i r_def: ?m.11024
r_def px_def: ?m.11025
px_defx0: Nat

r: spec.Reservation

px: Nat

r_def: r = Lock.Locked { x := x0, y := x0 }

px_def: px = x0

cont_valid.f_valid.introvalid
  (do
    let py ← atomic_read fun s => s.data.y
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  r (fun x => true) fun x r => r = IsReservation.empty
  
Thread.valid thread2cases r: spec.Reservation
rx0, px: Nat

px_def: px = x0

r_def: Lock.Unlocked = Lock.Locked { x := x0, y := x0 }

cont_valid.f_valid.intro.Unlockedvalid
  (do
    let py ← atomic_read fun s => s.data.y
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  Lock.Unlocked (fun x => true) fun x r => r = IsReservation.empty
x0, px: Nat

px_def: px = x0

a✝: Data

r_def: Lock.Locked a✝ = Lock.Locked { x := x0, y := x0 }

cont_valid.f_valid.intro.Lockedvalid
  (do
    let py ← atomic_read fun s => s.data.y
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  (Lock.Locked a✝) (fun x => true) fun x r => r = IsReservation.empty
x0, px: Nat

px_def: px = x0

r_def: Lock.Invalid = Lock.Locked { x := x0, y := x0 }

cont_valid.f_valid.intro.Invalidvalid
  (do
    let py ← atomic_read fun s => s.data.y
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  Lock.Invalid (fun x => true) fun x r => r = IsReservation.empty x0: Nat

r: spec.Reservation

px: Nat

r_def: r = Lock.Locked { x := x0, y := x0 }

px_def: px = x0

cont_valid.f_valid.introvalid
  (do
    let py ← atomic_read fun s => s.data.y
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  r (fun x => true) fun x r => r = IsReservation.empty<;>x0, px: Nat

px_def: px = x0

r_def: Lock.Unlocked = Lock.Locked { x := x0, y := x0 }

cont_valid.f_valid.intro.Unlockedvalid
  (do
    let py ← atomic_read fun s => s.data.y
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  Lock.Unlocked (fun x => true) fun x r => r = IsReservation.empty
x0, px: Nat

px_def: px = x0

a✝: Data

r_def: Lock.Locked a✝ = Lock.Locked { x := x0, y := x0 }

cont_valid.f_valid.intro.Lockedvalid
  (do
    let py ← atomic_read fun s => s.data.y
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  (Lock.Locked a✝) (fun x => true) fun x r => r = IsReservation.empty
x0, px: Nat

px_def: px = x0

r_def: Lock.Invalid = Lock.Locked { x := x0, y := x0 }

cont_valid.f_valid.intro.Invalidvalid
  (do
    let py ← atomic_read fun s => s.data.y
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  Lock.Invalid (fun x => true) fun x r => r = IsReservation.empty x0: Nat

r: spec.Reservation

px: Nat

r_def: r = Lock.Locked { x := x0, y := x0 }

px_def: px = x0

cont_valid.f_valid.introvalid
  (do
    let py ← atomic_read fun s => s.data.y
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  r (fun x => true) fun x r => r = IsReservation.emptytry x0, px: Nat

px_def: px = x0

r_def: Lock.Unlocked = Lock.Locked { x := x0, y := x0 }

cont_valid.f_valid.intro.Unlockedvalid
  (do
    let py ← atomic_read fun s => s.data.y
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  Lock.Unlocked (fun x => true) fun x r => r = IsReservation.emptycontradiction
Goals accomplished! 🐙
  
Thread.valid thread2rename_i data0: ?m.11069
data0x0, px: Nat

px_def: px = x0

data0: Data

r_def: Lock.Locked data0 = Lock.Locked { x := x0, y := x0 }

cont_valid.f_valid.intro.Lockedvalid
  (do
    let py ← atomic_read fun s => s.data.y
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  (Lock.Locked data0) (fun x => true) fun x r => r = IsReservation.empty
  
Thread.valid thread2let ⟨x0: Nat
x0, y0: Nat
y0⟩ :=data0: ?m.11069
data0x0✝, px: Nat

px_def: px = x0✝

data0: Data

x0, y0: Nat

r_def: Lock.Locked { x := x0, y := y0 } = Lock.Locked { x := x0✝, y := x0✝ }

cont_valid.f_valid.intro.Lockedvalid
  (do
    let py ← atomic_read fun s => s.data.y
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  (Lock.Locked { x := x0, y := y0 }) (fun x => true) fun x r => r = IsReservation.empty 
Thread.valid thread2;x0✝, px: Nat

px_def: px = x0✝

data0: Data

x0, y0: Nat

r_def: Lock.Locked { x := x0, y := y0 } = Lock.Locked { x := x0✝, y := x0✝ }

cont_valid.f_valid.intro.Lockedvalid
  (do
    let py ← atomic_read fun s => s.data.y
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  (Lock.Locked { x := x0, y := y0 }) (fun x => true) fun x r => r = IsReservation.empty 
Thread.valid thread2clear data0: ?m.11069
data0x0✝, px: Nat

px_def: px = x0✝

x0, y0: Nat

r_def: Lock.Locked { x := x0, y := y0 } = Lock.Locked { x := x0✝, y := x0✝ }

cont_valid.f_valid.intro.Lockedvalid
  (do
    let py ← atomic_read fun s => s.data.y
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  (Lock.Locked { x := x0, y := y0 }) (fun x => true) fun x r => r = IsReservation.empty
  
Thread.valid thread2cases r_def: Lock.Locked { x := x0, y := y0 } = Lock.Locked { x := x0✝, y := x0✝ }
r_defx0, px: Nat

px_def: px = x0

cont_valid.f_valid.intro.Locked.reflvalid
  (do
    let py ← atomic_read fun s => s.data.y
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun x r => r = IsReservation.empty
  
Thread.valid thread2apply valid_bind: ∀ {spec : Spec} {U V : Type} {mu : TaskM spec U} {f : U → TaskM spec V} {r : spec.Reservation}
  {assuming : spec.State → Bool} {motive : V → spec.Reservation → Prop} (motive_u : U → spec.Reservation → Prop),
  valid mu r assuming motive_u →
    (∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive) →
      valid (mu >>= f) r assuming motive
valid_bind (spec :=spec: Spec
spec) λ py: ?m.11387
py r': ?m.11390
r' => r': ?m.11390
r' = Lock.Locked: {T : Type} → T → Lock T
Lock.Locked ⟨x0: Nat
x0, x0: Nat
x0⟩ ∧ py: ?m.11387
py = x0: Nat
x0x0, px: Nat

px_def: px = x0

cont_valid.f_valid.intro.Locked.refl.mu_validvalid (atomic_read fun s => s.data.y) (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun py r' =>
  r' = Lock.Locked { x := x0, y := x0 } ∧ py = x0
x0, px: Nat

px_def: px = x0

cont_valid.f_valid.intro.Locked.refl.f_valid∀ (r' : spec.Reservation) (u : Nat),
  r' = Lock.Locked { x := x0, y := x0 } ∧ u = x0 →
    valid
      (do
        atomic_assert fun x => decide (px = u)
        atomic_read_modify fun s => { data := s.data, locked := false })
      r' (fun x => true) fun x r => r = IsReservation.empty
  
Thread.valid thread2.x0, px: Nat

px_def: px = x0

cont_valid.f_valid.intro.Locked.refl.mu_validvalid (atomic_read fun s => s.data.y) (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun py r' =>
  r' = Lock.Locked { x := x0, y := x0 } ∧ py = x0 -- verify read of x; we should get x0
    x0, px: Nat

px_def: px = x0

cont_valid.f_valid.intro.Locked.refl.mu_validvalid (atomic_read fun s => s.data.y) (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun py r' =>
  r' = Lock.Locked { x := x0, y := x0 } ∧ py = x0
x0, px: Nat

px_def: px = x0

cont_valid.f_valid.intro.Locked.refl.f_valid∀ (r' : spec.Reservation) (u : Nat),
  r' = Lock.Locked { x := x0, y := x0 } ∧ u = x0 →
    valid
      (do
        atomic_assert fun x => decide (px = u)
        atomic_read_modify fun s => { data := s.data, locked := false })
      r' (fun x => true) fun x r => r = IsReservation.emptyapply valid_read: ∀ {spec : Spec} {T : Type} {f : spec.State → T} {r : spec.Reservation} {assuming : spec.State → Bool}
  {motive : T → spec.Reservation → Prop},
  (∀ (env_r : spec.Reservation) (s : spec.State),
      assuming s = true →
        Spec.validate spec (env_r + r) s →
          ∃ r',
            let t := f s;
            Spec.validate spec (env_r + r') s ∧ motive t r') →
    valid (atomic_read f) r assuming motive
valid_readx0, px: Nat

px_def: px = x0

cont_valid.f_valid.intro.Locked.refl.mu_valid.f_valid∀ (env_r : spec.Reservation) (s : spec.State),
  true = true →
    Spec.validate spec (env_r + Lock.Locked { x := x0, y := x0 }) s →
      ∃ r',
        let t := s.data.y;
        Spec.validate spec (env_r + r') s ∧ r' = Lock.Locked { x := x0, y := x0 } ∧ t = x0
    x0, px: Nat

px_def: px = x0

cont_valid.f_valid.intro.Locked.refl.mu_validvalid (atomic_read fun s => s.data.y) (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun py r' =>
  r' = Lock.Locked { x := x0, y := x0 } ∧ py = x0
x0, px: Nat

px_def: px = x0

cont_valid.f_valid.intro.Locked.refl.f_valid∀ (r' : spec.Reservation) (u : Nat),
  r' = Lock.Locked { x := x0, y := x0 } ∧ u = x0 →
    valid
      (do
        atomic_assert fun x => decide (px = u)
        atomic_read_modify fun s => { data := s.data, locked := false })
      r' (fun x => true) fun x r => r = IsReservation.emptysimp only [spec: Spec
spec]x0, px: Nat

px_def: px = x0

cont_valid.f_valid.intro.Locked.refl.mu_valid.f_valid∀ (env_r : spec.Reservation) (s : spec.State),
  True →
    validate (env_r + Lock.Locked { x := x0, y := x0 }) s →
      ∃ r', validate (env_r + r') s ∧ r' = Lock.Locked { x := x0, y := x0 } ∧ s.data.y = x0
    x0, px: Nat

px_def: px = x0

cont_valid.f_valid.intro.Locked.refl.mu_validvalid (atomic_read fun s => s.data.y) (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun py r' =>
  r' = Lock.Locked { x := x0, y := x0 } ∧ py = x0
x0, px: Nat

px_def: px = x0

cont_valid.f_valid.intro.Locked.refl.f_valid∀ (r' : spec.Reservation) (u : Nat),
  r' = Lock.Locked { x := x0, y := x0 } ∧ u = x0 →
    valid
      (do
        atomic_assert fun x => decide (px = u)
        atomic_read_modify fun s => { data := s.data, locked := false })
      r' (fun x => true) fun x r => r = IsReservation.emptyintro env_r: spec.Reservation
env_r ⟨⟨x: Nat
x, y: Nat
y⟩, locked: Bool
locked⟩ ⟨⟩ initial_valid: validate (env_r + Lock.Locked { x := x0, y := x0 }) { data := { x := x, y := y }, locked := locked }
initial_validx0, px: Nat

px_def: px = x0

env_r: spec.Reservation

x, y: Nat

locked: Bool

initial_valid: validate (env_r + Lock.Locked { x := x0, y := x0 }) { data := { x := x, y := y }, locked := locked }

cont_valid.f_valid.intro.Locked.refl.mu_valid.f_valid∃ r',
  validate (env_r + r') { data := { x := x, y := y }, locked := locked } ∧     r' = Lock.Locked { x := x0, y := x0 } ∧ { data := { x := x, y := y }, locked := locked }.data.y = x0
    x0, px: Nat

px_def: px = x0

cont_valid.f_valid.intro.Locked.refl.mu_validvalid (atomic_read fun s => s.data.y) (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun py r' =>
  r' = Lock.Locked { x := x0, y := x0 } ∧ py = x0
x0, px: Nat

px_def: px = x0

cont_valid.f_valid.intro.Locked.refl.f_valid∀ (r' : spec.Reservation) (u : Nat),
  r' = Lock.Locked { x := x0, y := x0 } ∧ u = x0 →
    valid
      (do
        atomic_assert fun x => decide (px = u)
        atomic_read_modify fun s => { data := s.data, locked := false })
      r' (fun x => true) fun x r => r = IsReservation.emptyexists Lock.Locked: {T : Type} → T → Lock T
Lock.Locked ⟨x0: Nat
x0, x0: Nat
x0⟩x0, px: Nat

px_def: px = x0

env_r: spec.Reservation

x, y: Nat

locked: Bool

initial_valid: validate (env_r + Lock.Locked { x := x0, y := x0 }) { data := { x := x, y := y }, locked := locked }

cont_valid.f_valid.intro.Locked.refl.mu_valid.f_validvalidate (env_r + Lock.Locked { x := x0, y := x0 }) { data := { x := x, y := y }, locked := locked } ∧   Lock.Locked { x := x0, y := x0 } = Lock.Locked { x := x0, y := x0 } ∧     { data := { x := x, y := y }, locked := locked }.data.y = x0
    x0, px: Nat

px_def: px = x0

cont_valid.f_valid.intro.Locked.refl.mu_validvalid (atomic_read fun s => s.data.y) (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun py r' =>
  r' = Lock.Locked { x := x0, y := x0 } ∧ py = x0
x0, px: Nat

px_def: px = x0

cont_valid.f_valid.intro.Locked.refl.f_valid∀ (r' : spec.Reservation) (u : Nat),
  r' = Lock.Locked { x := x0, y := x0 } ∧ u = x0 →
    valid
      (do
        atomic_assert fun x => decide (px = u)
        atomic_read_modify fun s => { data := s.data, locked := false })
      r' (fun x => true) fun x r => r = IsReservation.emptysimp only [initial_valid: validate (env_r + Lock.Locked { x := x0, y := x0 }) { data := { x := x, y := y }, locked := locked }
initial_valid.elim_locked: ∀ {env_r : Reservation} {d : Data} {s' : State},
  validate (env_r + Lock.Locked d) s' → env_r = Lock.Unlocked ∧ d = s'.data ∧ s'.locked = true
elim_locked, Lock.unlocked_add: ∀ {T : Type} (a : Lock T), Lock.Unlocked + a = a
Lock.unlocked_add]x0, px: Nat

px_def: px = x0

env_r: spec.Reservation

x, y: Nat

locked: Bool

initial_valid: validate (env_r + Lock.Locked { x := x0, y := x0 }) { data := { x := x, y := y }, locked := locked }

cont_valid.f_valid.intro.Locked.refl.mu_valid.f_validvalidate (Lock.Locked { x := x, y := y }) { data := { x := x, y := y }, locked := true } ∧ True ∧ y = x0
    x0, px: Nat

px_def: px = x0

cont_valid.f_valid.intro.Locked.refl.mu_validvalid (atomic_read fun s => s.data.y) (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun py r' =>
  r' = Lock.Locked { x := x0, y := x0 } ∧ py = x0
x0, px: Nat

px_def: px = x0

cont_valid.f_valid.intro.Locked.refl.f_valid∀ (r' : spec.Reservation) (u : Nat),
  r' = Lock.Locked { x := x0, y := x0 } ∧ u = x0 →
    valid
      (do
        atomic_assert fun x => decide (px = u)
        atomic_read_modify fun s => { data := s.data, locked := false })
      r' (fun x => true) fun x r => r = IsReservation.emptyinjection initial_valid: validate (env_r + Lock.Locked { x := x0, y := x0 }) { data := { x := x, y := y }, locked := locked }
initial_valid.elim_locked: ∀ {env_r : Reservation} {d : Data} {s' : State},
  validate (env_r + Lock.Locked d) s' → env_r = Lock.Unlocked ∧ d = s'.data ∧ s'.locked = true
elim_locked.right: ∀ {a b : Prop}, a ∧ b → b
right.left: ∀ {a b : Prop}, a ∧ b → a
leftx0, px: Nat

px_def: px = x0

env_r: spec.Reservation

x, y: Nat

locked: Bool

initial_valid: validate (env_r + Lock.Locked { x := x0, y := x0 }) { data := { x := x, y := y }, locked := locked }

cont_valid.f_valid.intro.Locked.refl.mu_valid.f_validvalidate (Lock.Locked { x := x, y := y }) { data := { x := x, y := y }, locked := true } ∧ True ∧ y = x0
    x0, px: Nat

px_def: px = x0

cont_valid.f_valid.intro.Locked.refl.mu_validvalid (atomic_read fun s => s.data.y) (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun py r' =>
  r' = Lock.Locked { x := x0, y := x0 } ∧ py = x0
x0, px: Nat

px_def: px = x0

cont_valid.f_valid.intro.Locked.refl.f_valid∀ (r' : spec.Reservation) (u : Nat),
  r' = Lock.Locked { x := x0, y := x0 } ∧ u = x0 →
    valid
      (do
        atomic_assert fun x => decide (px = u)
        atomic_read_modify fun s => { data := s.data, locked := false })
      r' (fun x => true) fun x r => r = IsReservation.emptyrename_i x0_def: x0 = x
x0_def y0_def: x0 = y
y0_defx0, px: Nat

px_def: px = x0

env_r: spec.Reservation

x, y: Nat

locked: Bool

initial_valid: validate (env_r + Lock.Locked { x := x0, y := x0 }) { data := { x := x, y := y }, locked := locked }

x0_def: x0 = x

y0_def: x0 = y

cont_valid.f_valid.intro.Locked.refl.mu_valid.f_validvalidate (Lock.Locked { x := x, y := y }) { data := { x := x, y := y }, locked := true } ∧ True ∧ y = x0
    x0, px: Nat

px_def: px = x0

cont_valid.f_valid.intro.Locked.refl.mu_validvalid (atomic_read fun s => s.data.y) (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun py r' =>
  r' = Lock.Locked { x := x0, y := x0 } ∧ py = x0
x0, px: Nat

px_def: px = x0

cont_valid.f_valid.intro.Locked.refl.f_valid∀ (r' : spec.Reservation) (u : Nat),
  r' = Lock.Locked { x := x0, y := x0 } ∧ u = x0 →
    valid
      (do
        atomic_assert fun x => decide (px = u)
        atomic_read_modify fun s => { data := s.data, locked := false })
      r' (fun x => true) fun x r => r = IsReservation.emptysimp only [<- x0_def: x0 = x
x0_def, <- y0_def: x0 = y
y0_def, and_true: ∀ (p : Prop), (p ∧ True) = p
and_true]x0, px: Nat

px_def: px = x0

env_r: spec.Reservation

x, y: Nat

locked: Bool

initial_valid: validate (env_r + Lock.Locked { x := x0, y := x0 }) { data := { x := x, y := y }, locked := locked }

x0_def: x0 = x

y0_def: x0 = y

cont_valid.f_valid.intro.Locked.refl.mu_valid.f_validvalidate (Lock.Locked { x := x0, y := x0 }) { data := { x := x0, y := x0 }, locked := true }
    x0, px: Nat

px_def: px = x0

cont_valid.f_valid.intro.Locked.refl.mu_validvalid (atomic_read fun s => s.data.y) (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun py r' =>
  r' = Lock.Locked { x := x0, y := x0 } ∧ py = x0
x0, px: Nat

px_def: px = x0

cont_valid.f_valid.intro.Locked.refl.f_valid∀ (r' : spec.Reservation) (u : Nat),
  r' = Lock.Locked { x := x0, y := x0 } ∧ u = x0 →
    valid
      (do
        atomic_assert fun x => decide (px = u)
        atomic_read_modify fun s => { data := s.data, locked := false })
      r' (fun x => true) fun x r => r = IsReservation.emptyexact validate.locked: ∀ (data : Data), validate (Lock.Locked data) { data := data, locked := true }
validate.locked _: Data
_
Goals accomplished! 🐙

  
Thread.valid thread2intro r: spec.Reservation
r py: Nat
py is_locked_and_valid: r = Lock.Locked { x := x0, y := x0 } ∧ py = x0
is_locked_and_validx0, px: Nat

px_def: px = x0

r: spec.Reservation

py: Nat

is_locked_and_valid: r = Lock.Locked { x := x0, y := x0 } ∧ py = x0

cont_valid.f_valid.intro.Locked.refl.f_validvalid
  (do
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  r (fun x => true) fun x r => r = IsReservation.empty
  
Thread.valid thread2cases is_locked_and_valid: r = Lock.Locked { x := x0, y := x0 } ∧ py = x0
is_locked_and_validx0, px: Nat

px_def: px = x0

r: spec.Reservation

py: Nat

cont_valid.f_valid.intro.Locked.refl.f_valid.introvalid
  (do
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  r (fun x => true) fun x r => r = IsReservation.empty 
Thread.valid thread2;x0, px: Nat

px_def: px = x0

r: spec.Reservation

py: Nat

cont_valid.f_valid.intro.Locked.refl.f_valid.introvalid
  (do
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  r (fun x => true) fun x r => r = IsReservation.empty 
Thread.valid thread2rename_i r_def: ?m.12999
r_def py_def: ?m.13000
py_defx0, px: Nat

px_def: px = x0

r: spec.Reservation

py: Nat

r_def: r = Lock.Locked { x := x0, y := x0 }

py_def: py = x0

cont_valid.f_valid.intro.Locked.refl.f_valid.introvalid
  (do
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  r (fun x => true) fun x r => r = IsReservation.empty
  
Thread.valid thread2cases r: spec.Reservation
rx0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

r_def: Lock.Unlocked = Lock.Locked { x := x0, y := x0 }

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Unlockedvalid
  (do
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  Lock.Unlocked (fun x => true) fun x r => r = IsReservation.empty
x0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

a✝: Data

r_def: Lock.Locked a✝ = Lock.Locked { x := x0, y := x0 }

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Lockedvalid
  (do
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  (Lock.Locked a✝) (fun x => true) fun x r => r = IsReservation.empty
x0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

r_def: Lock.Invalid = Lock.Locked { x := x0, y := x0 }

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Invalidvalid
  (do
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  Lock.Invalid (fun x => true) fun x r => r = IsReservation.empty x0, px: Nat

px_def: px = x0

r: spec.Reservation

py: Nat

r_def: r = Lock.Locked { x := x0, y := x0 }

py_def: py = x0

cont_valid.f_valid.intro.Locked.refl.f_valid.introvalid
  (do
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  r (fun x => true) fun x r => r = IsReservation.empty<;>x0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

r_def: Lock.Unlocked = Lock.Locked { x := x0, y := x0 }

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Unlockedvalid
  (do
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  Lock.Unlocked (fun x => true) fun x r => r = IsReservation.empty
x0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

a✝: Data

r_def: Lock.Locked a✝ = Lock.Locked { x := x0, y := x0 }

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Lockedvalid
  (do
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  (Lock.Locked a✝) (fun x => true) fun x r => r = IsReservation.empty
x0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

r_def: Lock.Invalid = Lock.Locked { x := x0, y := x0 }

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Invalidvalid
  (do
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  Lock.Invalid (fun x => true) fun x r => r = IsReservation.empty x0, px: Nat

px_def: px = x0

r: spec.Reservation

py: Nat

r_def: r = Lock.Locked { x := x0, y := x0 }

py_def: py = x0

cont_valid.f_valid.intro.Locked.refl.f_valid.introvalid
  (do
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  r (fun x => true) fun x r => r = IsReservation.emptytry x0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

r_def: Lock.Unlocked = Lock.Locked { x := x0, y := x0 }

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Unlockedvalid
  (do
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  Lock.Unlocked (fun x => true) fun x r => r = IsReservation.emptycontradiction
Goals accomplished! 🐙
  
Thread.valid thread2rename_i data0: ?m.13044
data0x0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

data0: Data

r_def: Lock.Locked data0 = Lock.Locked { x := x0, y := x0 }

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Lockedvalid
  (do
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  (Lock.Locked data0) (fun x => true) fun x r => r = IsReservation.empty
  
Thread.valid thread2let ⟨x0: Nat
x0, y0: Nat
y0⟩ :=data0: ?m.13044
data0x0✝, px: Nat

px_def: px = x0✝

py: Nat

py_def: py = x0✝

data0: Data

x0, y0: Nat

r_def: Lock.Locked { x := x0, y := y0 } = Lock.Locked { x := x0✝, y := x0✝ }

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Lockedvalid
  (do
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  (Lock.Locked { x := x0, y := y0 }) (fun x => true) fun x r => r = IsReservation.empty 
Thread.valid thread2;x0✝, px: Nat

px_def: px = x0✝

py: Nat

py_def: py = x0✝

data0: Data

x0, y0: Nat

r_def: Lock.Locked { x := x0, y := y0 } = Lock.Locked { x := x0✝, y := x0✝ }

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Lockedvalid
  (do
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  (Lock.Locked { x := x0, y := y0 }) (fun x => true) fun x r => r = IsReservation.empty 
Thread.valid thread2clear data0: ?m.13044
data0x0✝, px: Nat

px_def: px = x0✝

py: Nat

py_def: py = x0✝

x0, y0: Nat

r_def: Lock.Locked { x := x0, y := y0 } = Lock.Locked { x := x0✝, y := x0✝ }

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Lockedvalid
  (do
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  (Lock.Locked { x := x0, y := y0 }) (fun x => true) fun x r => r = IsReservation.empty
  
Thread.valid thread2cases r_def: Lock.Locked { x := x0, y := y0 } = Lock.Locked { x := x0✝, y := x0✝ }
r_defx0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Locked.reflvalid
  (do
    atomic_assert fun x => decide (px = py)
    atomic_read_modify fun s => { data := s.data, locked := false })
  (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun x r => r = IsReservation.empty
  
Thread.valid thread2apply valid_bind: ∀ {spec : Spec} {U V : Type} {mu : TaskM spec U} {f : U → TaskM spec V} {r : spec.Reservation}
  {assuming : spec.State → Bool} {motive : V → spec.Reservation → Prop} (motive_u : U → spec.Reservation → Prop),
  valid mu r assuming motive_u →
    (∀ (r' : spec.Reservation) (u : U), motive_u u r' → valid (f u) r' (fun x => true) motive) →
      valid (mu >>= f) r assuming motive
valid_bind (spec :=spec: Spec
spec) λ ⟨⟩ r': ?m.13340
r' => r': ?m.13340
r' = Lock.Locked: {T : Type} → T → Lock T
Lock.Locked ⟨x0: Nat
x0, x0: Nat
x0⟩x0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Locked.refl.mu_validvalid (atomic_assert fun x => decide (px = py)) (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun x r' =>
  r' = Lock.Locked { x := x0, y := x0 }
x0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Locked.refl.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = Lock.Locked { x := x0, y := x0 } →
      valid (atomic_read_modify fun s => { data := s.data, locked := false }) r' (fun x => true) fun x r =>
        r = IsReservation.empty
  
Thread.valid thread2.x0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Locked.refl.mu_validvalid (atomic_assert fun x => decide (px = py)) (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun x r' =>
  r' = Lock.Locked { x := x0, y := x0 } -- verify assertion
    x0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Locked.refl.mu_validvalid (atomic_assert fun x => decide (px = py)) (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun x r' =>
  r' = Lock.Locked { x := x0, y := x0 }
x0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Locked.refl.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = Lock.Locked { x := x0, y := x0 } →
      valid (atomic_read_modify fun s => { data := s.data, locked := false }) r' (fun x => true) fun x r =>
        r = IsReservation.emptyapply valid_assert: ∀ {spec : Spec} {cond : spec.State → Bool} {r : spec.Reservation} {assuming : spec.State → Bool}
  {motive : Unit → spec.Reservation → Prop},
  motive PUnit.unit r →
    (∀ (env_r : spec.Reservation) (s : spec.State),
        assuming s = true → Spec.validate spec (env_r + r) s → cond s = true) →
      valid (atomic_assert cond) r assuming motive
valid_assert rfl: ∀ {α : Sort ?u.13581} {a : α}, a = a
rflx0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Locked.refl.mu_valid∀ (env_r : spec.Reservation) (s : spec.State),
  true = true → Spec.validate spec (env_r + Lock.Locked { x := x0, y := x0 }) s → decide (px = py) = true
    x0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Locked.refl.mu_validvalid (atomic_assert fun x => decide (px = py)) (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun x r' =>
  r' = Lock.Locked { x := x0, y := x0 }
x0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Locked.refl.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = Lock.Locked { x := x0, y := x0 } →
      valid (atomic_read_modify fun s => { data := s.data, locked := false }) r' (fun x => true) fun x r =>
        r = IsReservation.emptyintrosx0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

env_r✝: spec.Reservation

s✝: spec.State

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Locked.refl.mu_validdecide (px = py) = true
    x0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Locked.refl.mu_validvalid (atomic_assert fun x => decide (px = py)) (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun x r' =>
  r' = Lock.Locked { x := x0, y := x0 }
x0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Locked.refl.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = Lock.Locked { x := x0, y := x0 } →
      valid (atomic_read_modify fun s => { data := s.data, locked := false }) r' (fun x => true) fun x r =>
        r = IsReservation.emptyrw [x0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

env_r✝: spec.Reservation

s✝: spec.State

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Locked.refl.mu_validdecide (px = py) = truepx_def: ?m.11025
px_def,x0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

env_r✝: spec.Reservation

s✝: spec.State

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Locked.refl.mu_validdecide (x0 = py) = true x0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

env_r✝: spec.Reservation

s✝: spec.State

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Locked.refl.mu_validdecide (px = py) = truepy_def: ?m.13000
py_defx0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

env_r✝: spec.Reservation

s✝: spec.State

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Locked.refl.mu_validdecide (x0 = x0) = true]x0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

env_r✝: spec.Reservation

s✝: spec.State

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Locked.refl.mu_validdecide (x0 = x0) = true
    x0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Locked.refl.mu_validvalid (atomic_assert fun x => decide (px = py)) (Lock.Locked { x := x0, y := x0 }) (fun x => true) fun x r' =>
  r' = Lock.Locked { x := x0, y := x0 }
x0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Locked.refl.f_valid∀ (r' : spec.Reservation),
  Unit →
    r' = Lock.Locked { x := x0, y := x0 } →
      valid (atomic_read_modify fun s => { data := s.data, locked := false }) r' (fun x => true) fun x r =>
        r = IsReservation.emptyexact decide_eq_true: ∀ {p : Prop} [inst : Decidable p], p → decide p = true
decide_eq_true rfl: ∀ {α : Sort ?u.13642} {a : α}, a = a
rfl
Goals accomplished! 🐙
  
  
Thread.valid thread2intro r: spec.Reservation
r ⟨⟩ r_def: r = Lock.Locked { x := x0, y := x0 }
r_defx0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

r: spec.Reservation

r_def: r = Lock.Locked { x := x0, y := x0 }

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Locked.refl.f_validvalid (atomic_read_modify fun s => { data := s.data, locked := false }) r (fun x => true) fun x r =>
  r = IsReservation.empty
  
Thread.valid thread2rw [x0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

r: spec.Reservation

r_def: r = Lock.Locked { x := x0, y := x0 }

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Locked.refl.f_validvalid (atomic_read_modify fun s => { data := s.data, locked := false }) r (fun x => true) fun x r =>
  r = IsReservation.emptyr_def: r = Lock.Locked { x := x0, y := x0 }
r_defx0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

r: spec.Reservation

r_def: r = Lock.Locked { x := x0, y := x0 }

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Locked.refl.f_validvalid (atomic_read_modify fun s => { data := s.data, locked := false }) (Lock.Locked { x := x0, y := x0 })
  (fun x => true) fun x r => r = IsReservation.empty]x0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

r: spec.Reservation

r_def: r = Lock.Locked { x := x0, y := x0 }

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Locked.refl.f_validvalid (atomic_read_modify fun s => { data := s.data, locked := false }) (Lock.Locked { x := x0, y := x0 })
  (fun x => true) fun x r => r = IsReservation.empty;x0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

r: spec.Reservation

r_def: r = Lock.Locked { x := x0, y := x0 }

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Locked.refl.f_validvalid (atomic_read_modify fun s => { data := s.data, locked := false }) (Lock.Locked { x := x0, y := x0 })
  (fun x => true) fun x r => r = IsReservation.empty 
Thread.valid thread2clear r_def: r = Lock.Locked { x := x0, y := x0 }
r_def r: spec.Reservation
rx0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Locked.refl.f_validvalid (atomic_read_modify fun s => { data := s.data, locked := false }) (Lock.Locked { x := x0, y := x0 })
  (fun x => true) fun x r => r = IsReservation.empty
  
Thread.valid thread2.x0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Locked.refl.f_validvalid (atomic_read_modify fun s => { data := s.data, locked := false }) (Lock.Locked { x := x0, y := x0 })
  (fun x => true) fun x r => r = IsReservation.empty -- validate mutex release
    x0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Locked.refl.f_validvalid (atomic_read_modify fun s => { data := s.data, locked := false }) (Lock.Locked { x := x0, y := x0 })
  (fun x => true) fun x r => r = IsReservation.emptyapply valid_mutex_release: ∀ {assuming : spec.State → Bool} {data : Data},
  Data.valid data →
    valid (atomic_read_modify fun s => { data := s.data, locked := false }) (Lock.Locked data) assuming fun x r =>
      r = Lock.Unlocked
valid_mutex_releasex0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Locked.refl.f_valid.data_validData.valid { x := x0, y := x0 }
    x0, px: Nat

px_def: px = x0

py: Nat

py_def: py = x0

cont_valid.f_valid.intro.Locked.refl.f_valid.intro.Locked.refl.f_validvalid (atomic_read_modify fun s => { data := s.data, locked := false }) (Lock.Locked { x := x0, y := x0 })
  (fun x => true) fun x r => r = IsReservation.emptyrfl
Goals accomplished! 🐙

end SampleMutex