core - shaolintl/fstar-type-checker GitHub Wiki

Hoare style

Copied from http://prosecco.gforge.inria.fr/personal/hritcu/teaching/mpri-jan2017/

Syntax

f ::= True | False | e₁ == eβ‚‚ | b2t e | f₁ ∧ fβ‚‚ | ~f | … (formulas)

c ::= Tot t | ST t (fun hβ‚€ -> fpre) (fun hβ‚€ x h₁ -> fpost) (computation types)

t ::= unit | bool | int | ref int | heap | t -> c (types)

k ::= () | true | false | i | l | sel | upd | (=) | (<) | not | …(constants)

v ::= k | fun x -> e | rec (f:t) x -> e (values)

e ::= x | v | e₁ eβ‚‚ | if e then e₁ else eβ‚‚ !e | e₁ := eβ‚‚ | let x = e₁ in e₂… (expressions)

Typing

Formula well-formedness

Implicitly assumed everywhere

Ξ“ ⊒ True ok

Ξ“ ⊒ False ok

Ξ“ ⊒ e₁ : Tot t Ξ“ ⊒ eβ‚‚ : Tot t

β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”

Ξ“ ⊒ (e₁ == e2) ok

Ξ“ ⊒ e : Tot bool

β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”

Ξ“ ⊒ (b2t e) ok

Ξ“ ⊒ f₁ ok Ξ“ ⊒ fβ‚‚ ok

β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”β€”

Ξ“ ⊒ f₁ ∧ fβ‚‚ ok

Ξ“ ⊒ f ok

β€”β€”β€”β€”β€”β€”β€”β€”β€”

Ξ“ ⊒ ~f ok

Total expressions (Ξ“ ⊒ e : Tot t)

Ξ“ ⊒ () : Tot unit

Ξ“ ⊒ true : Tot bool

Ξ“ ⊒ false : Tot bool

Ξ“ ⊒ i : Tot int

Ξ“ ⊒ l : Tot (ref int)

Ξ“ ⊒ sel : heap -> ref int -> Tot int

Ξ“ ⊒ upd : heap -> ref int -> int -> Tot heap

x:t ∈ Ξ“

————————–———– (T-Var)

Ξ“ ⊒ x : Tot t

Ξ“,x:t ⊒ e : c

————————–———–————————–———————————– (T-Fun)

Ξ“ ⊒ fun x -> e : Tot (t -> c)

t = t’ -> c where c is not Tot Ξ“,f:t,x:t’ ⊒ e : c

——––————————–———–————————–————— (T-Rec)

Ξ“ ⊒ rec (f:t) x -> e : Tot t

Ξ“ ⊒ e₁ : Tot (t -> c) Ξ“ ⊒ eβ‚‚ : Tot t

————————–———–———————— (T-App)

Ξ“ ⊒ e₁ eβ‚‚ : c

Ξ“ ⊒ e : Tot bool Ξ“ ⊒ e₁ : Tot t Ξ“ ⊒ eβ‚‚ : Tot t

————————–———–————————–————————–– (T-IfTot)

Ξ“ ⊒ if e then e₁ else eβ‚‚ : Tot t

Stateful expressions (Ξ“ ⊒ e : ST t pre post)

Ξ“ ⊒ e : Tot t

————————–———–————————–—————————–———————————————————————————————– (T-Lift)

Ξ“ ⊒ e : ST t (fun hβ‚€ -> True) (fun hβ‚€ x h₁ -> hβ‚€ == h₁ ∧ x == e)

Ξ“ ⊒ e : ST t (fun hβ‚€ -> fpre) (fun hβ‚€ x h₁ -> fpost) Ξ“ ⊧ (βˆ€hβ‚€. fpre’ β‡’ fpre) ∧ (βˆ€hβ‚€ x h₁. fpost β‡’ fpost’)

————————–———–————————–—————————–—————————————————————— (T-Consequence)

Ξ“ ⊒ e : ST t (fun hβ‚€ -> fpre’) (fun hβ‚€ x h₁ -> fpost’)

Ξ“ ⊒ e : Tot (ref int)

————————–———–————————–—————————–———————————————————————————————–—————————– (T-Read)

Ξ“ ⊒ !e : ST int (fun hβ‚€ -> True) (fun hβ‚€ x h₁ -> hβ‚€ == h₁ ∧ x == sel hβ‚€ e)

Ξ“ ⊒ e₁ : Tot (ref int) Ξ“ ⊒ eβ‚‚ : Tot int

————————–———–————————–—————————–———————————————————————————————–—————————–—– (T-Update)

Ξ“ ⊒ e₁ := eβ‚‚ : ST unit (fun hβ‚€ -> True) (fun hβ‚€ () h₁ -> h₁ == upd hβ‚€ e₁ eβ‚‚)

Ξ“ ⊒ e : Tot bool Ξ“ ⊒ e₁ : ST t (fun hβ‚€ -> fpre ∧ b2t e) (fun hβ‚€ x h₁ -> fpost) Ξ“ ⊒ eβ‚‚ : ST t (fun hβ‚€ -> fpre ∧ ~b2t e) (fun hβ‚€ x h₁ -> fpost)

————————–———–————————–———————————————————–——————————————————————————— (T-IfST)

Ξ“ ⊒ if e then e₁ else eβ‚‚ : ST (fun hβ‚€ -> fpre) (fun hβ‚€ x h₁ -> fpost)

Ξ“ ⊒ e₁ : ST t₁ (fun hβ‚€ -> fpre₁) (fun hβ‚€ x₁ h₁ -> fpost₁) Ξ“,x₁:t₁ ⊒ eβ‚‚ : ST tβ‚‚ (fun h₁ -> fpreβ‚‚) (fun h₁ xβ‚‚ hβ‚‚ -> fpostβ‚‚)

–————————–———–————————–—————————–—————————————————————————————–———— (T-Let)

Ξ“ ⊒ let x₁ = e₁ in eβ‚‚ : ST tβ‚‚ (fun hβ‚€ -> fpre₁ ∧ βˆ€x₁ h₁. fpost₁ β‡’ fpreβ‚‚) (fun hβ‚€ xβ‚‚ hβ‚‚ -> fpre₁ β‡’ βˆƒx₁ h₁. fpost₁ ∧ (fpreβ‚‚ β‡’ fpostβ‚‚))

Swap example

val swap : r₁:ref int -> rβ‚‚:ref int -> ST unit (requires (fun hβ‚€ -> True)) (ensures (fun hβ‚€ _ h₁ -> h₁ == upd (upd hβ‚€ r₁ (sel hβ‚€ rβ‚‚)) rβ‚‚ (sel hβ‚€ r₁))) let swap r₁ rβ‚‚ = let x₁ = !r₁ in let xβ‚‚ = !rβ‚‚ in let () = (r₁ := xβ‚‚) in rβ‚‚ := x₁

by (T-Read) Ξ“ ⊒ !r₁ : ST int (fun hβ‚€ -> True) (fun hβ‚€ x₁ h₁ -> hβ‚€ == h₁ ∧ x₁ == sel hβ‚€ r₁)

by (T-Read) Ξ“,x₁:int ⊒ !rβ‚‚ : ST int (fun h₁ -> True) (fun h₁ xβ‚‚ hβ‚‚ -> h₁ == hβ‚‚ ∧ xβ‚‚ == sel h₁ rβ‚‚)

by (T-Update) Ξ“,x₁:int,xβ‚‚:int ⊒ r₁ := xβ‚‚ : ST unit (fun hβ‚‚ -> True) (fun hβ‚‚ () h₃ -> h₃ == upd hβ‚‚ r₁ xβ‚‚)

by (T-Update) Ξ“,x₁:int,xβ‚‚:int ⊒ rβ‚‚ := x₁ : ST unit (fun h₃ -> True) (fun h₃ () hβ‚„ -> hβ‚„ == upd h₃ rβ‚‚ x₁)

by (T-Let) Ξ“,x₁:int,xβ‚‚:int ⊒ let _ = (r₁ := xβ‚‚) in rβ‚‚ := x₁ : ST unit (fun hβ‚‚ -> True) (fun hβ‚‚ () hβ‚„ -> βˆƒh₃. h₃ == upd hβ‚‚ r₁ xβ‚‚ ∧ hβ‚„ == upd h₃ rβ‚‚ x₁) by (T-Consequence) (fun hβ‚‚ () hβ‚„ -> hβ‚„ == upd (upd hβ‚‚ r₁ xβ‚‚) rβ‚‚ x₁)

by (T-Let) Ξ“,x₁:int ⊒ let xβ‚‚ = !rβ‚‚ in (let _ = (r₁ := xβ‚‚) in rβ‚‚ := x₁) : ST unit (fun h₁ -> True) (fun h₁ () hβ‚„ -> βˆƒxβ‚‚ hβ‚‚. h₁ == hβ‚‚ ∧ xβ‚‚ == sel h₁ rβ‚‚ ∧ hβ‚„ == upd (upd hβ‚‚ r₁ xβ‚‚) rβ‚‚ x₁) by (T-Consequence) (fun h₁ () hβ‚„ -> hβ‚„ == upd (upd h₁ r₁ (sel h₁ rβ‚‚)) rβ‚‚ x₁)

by (T-Let) Ξ“ ⊒ let x₁ = !r₁ in (let xβ‚‚ = !rβ‚‚ in (let _ = (r₁ := xβ‚‚) in rβ‚‚ := x₁)) : ST unit (fun h₁ -> True) (fun h₁ () hβ‚„ -> βˆƒx₁ h₁. hβ‚€ == h₁ ∧ x₁ == sel hβ‚€ r₁ ∧ hβ‚„ == upd (upd h₁ r₁ (sel h₁ rβ‚‚)) rβ‚‚ x₁)

by (T-Consequence) val swap : r₁:ref int -> rβ‚‚:ref int -> ST unit (requires (fun hβ‚€ -> True)) (fun hβ‚€ () hβ‚„ -> hβ‚„ == upd (upd hβ‚€ r₁ (sel hβ‚€ rβ‚‚)) rβ‚‚ (sel hβ‚€ r₁))

Weaker spec

Ξ“ ⊧ (βˆ€hβ‚€. True β‡’ True) ∧ (βˆ€hβ‚€ x hβ‚„. hβ‚„ == upd (upd hβ‚€ r₁ (sel hβ‚€ rβ‚‚)) rβ‚‚ (sel hβ‚€ r₁) β‡’ sel hβ‚„ r₁ = sel hβ‚€ rβ‚‚ ∧ sel hβ‚„ rβ‚‚ = sel hβ‚€ r₁)

——————————————————————————————————————————————–——————————————– (T-Consequence)

val swap : r₁:ref int -> rβ‚‚:ref int -> ST unit (requires (fun hβ‚€ -> True)) (ensures (fun hβ‚€ _ hβ‚„ -> sel hβ‚„ r₁ = sel hβ‚€ rβ‚‚ ∧ sel hβ‚„ rβ‚‚ = sel hβ‚€ r₁))

Advantages and disadvantages

  • very intuitive specifications (Hoare logic)
  • specs are clunkier to compose
    • T-Let pushing preconditions backwards and postcondition forwards at the same time
    • directional variants possible though
  • hard to automate because of quantifier proliferation (each T-Let adds 4 quantifiers!)
  • rules are hard to derive directly

Weakest precondition style

Syntax

wp, f ::= True | False | e₁ == eβ‚‚ | b2t e | f₁ ∧ fβ‚‚ | ~f | … p | fun x -> f | fun p -> f | f₁ fβ‚‚ | (wps and formulas)

c ::= Tot t | ST t wp (computation types)

Intuitively: postβ‚œ : t -> heap[final] -> Prop preβ‚œ : heap[initial] -> Prop wpβ‚œ : postβ‚œ -> Tot preβ‚œ

Can obtain old spec syntax as follows:

ST’ t fpre fpost = ST t (fun p hβ‚€ -> fpre hβ‚€ ∧ (βˆ€x h₁. fpost hβ‚€ x h₁ β‡’ p x h₁))

For instance:

val swap : r₁:ref int -> rβ‚‚:ref int -> ST’ unit (requires (fun hβ‚€ -> True)) (ensures (fun hβ‚€ _ h₁ -> h₁ == upd (upd hβ‚€ r₁ (sel hβ‚€ rβ‚‚)) rβ‚‚ (sel hβ‚€ r₁))) becomes val swap : r₁:ref int -> rβ‚‚:ref int -> ST unit (fun p hβ‚€ -> βˆ€x h₁. h₁ == upd (upd hβ‚€ r₁ (sel hβ‚€ rβ‚‚)) rβ‚‚ (sel hβ‚€ r₁) β‡’ p x h₁) by (T-Consequence) (fun p hβ‚€ -> p () (upd (upd hβ‚€ r₁ (sel hβ‚€ rβ‚‚)) rβ‚‚ (sel hβ‚€ r₁)))

And the same for a weaker spec:

val swap : r₁:ref int -> rβ‚‚:ref int -> ST’ unit (requires (fun hβ‚€ -> True)) (ensures (fun hβ‚€ _ h₁ -> sel h₁ r₁ = sel hβ‚€ rβ‚‚ ∧ sel h₁ rβ‚‚ = sel hβ‚€ r₁)) becomes val swap : r₁:ref int -> rβ‚‚:ref int -> ST unit (fun p hβ‚€ -> βˆ€h₁. sel h₁ r₁ = sel hβ‚€ rβ‚‚ ∧ sel h₁ rβ‚‚ = sel hβ‚€ r₁ β‡’ p x h₁)

Typing stateful expressions

Ξ“ ⊒ e : Tot t

————————–———–————————–————————— (T-Lift)

Ξ“ ⊒ e : ST t (fun p h -> p e h)

Ξ“ ⊒ e : ST t wp Ξ“ ⊧ (βˆ€p h. wp’ p h β‡’ wp p h)

————————–———–————————–——————— (T-Consequence)

Ξ“ ⊒ e : ST t wp’

Ξ“ ⊒ e : Tot (ref int)

————————–———–————————–—————————–—————————– (T-Read)

Ξ“ ⊒ !e : ST int (fun p h -> p (sel h e) h)

Ξ“ ⊒ e₁ : Tot (ref int) Ξ“ ⊒ eβ‚‚ : Tot int

————————–———–————————–—————————–—————————————————————– (T-Update)

Ξ“ ⊒ e₁ := eβ‚‚ : ST unit (fun p h -> p () (upd h e₁ eβ‚‚))

Ξ“ ⊒ e₁ : ST t₁ wp₁ Ξ“,x₁:t₁ ⊒ eβ‚‚ : ST tβ‚‚ wpβ‚‚

–————————–———–————————–—————————–—————————–——————————————————– (T-Let)

Ξ“ ⊒ let x₁ = e₁ in eβ‚‚ : ST tβ‚‚ (fun p -> wp₁ (fun x₁ -> wpβ‚‚ p))

Ξ“ ⊒ e : Tot bool Ξ“ ⊒ e₁ : ST t₁ wp₁ Ξ“ ⊒ eβ‚‚ : ST tβ‚‚ wpβ‚‚

–————————–———–—————————-—–—————————–—————————–——————————————————–————– (T-IfST)

Ξ“ ⊒ if e then e₁ else eβ‚‚ : ST tβ‚‚ (fun p -> if e then wp₁ p else wpβ‚‚ p)

Swap example

val swap : r₁:ref int -> rβ‚‚:ref int -> ST unit (fun p hβ‚€ -> p x (upd (upd hβ‚€ r₁ (sel hβ‚€ rβ‚‚)) rβ‚‚ (sel hβ‚€ r₁))) let swap r₁ rβ‚‚ = hβ‚€ let x₁ = !r₁ in h₁ let xβ‚‚ = !rβ‚‚ in hβ‚‚ let () = (r₁ := xβ‚‚) in h₃ rβ‚‚ := x₁ hβ‚„

by (T-Read) Ξ“ ⊒ !r₁ : ST int (fun pβ‚€ hβ‚€ -> pβ‚€ (sel hβ‚€ r₁) hβ‚€)

by (T-Read) Ξ“,x₁:int ⊒ !rβ‚‚ : ST int (fun p₁ h₁ -> p₁ (sel h₁ rβ‚‚) h₁)

by (T-Update) Ξ“,x₁:int,xβ‚‚:int ⊒ r₁ := xβ‚‚ : ST unit (fun pβ‚‚ hβ‚‚ -> pβ‚‚ () (upd hβ‚‚ r₁ xβ‚‚))

by (T-Update) Ξ“,x₁:int,xβ‚‚:int ⊒ rβ‚‚ := x₁ : ST unit (fun p₃ h₃ -> p₃ () (upd hβ‚‚ rβ‚‚ x₁))

by (T-Let) Ξ“,x₁:int,xβ‚‚:int ⊒ let _ = (r₁ := xβ‚‚) in rβ‚‚ := x₁ : ST unit (fun p -> (fun pβ‚‚ hβ‚‚ -> pβ‚‚ () (upd hβ‚‚ r₁ xβ‚‚)) (fun _ -> (fun h₃ -> p () (upd hβ‚‚ rβ‚‚ x₁)))) = (fun p hβ‚‚ -> (fun _ -> (fun h₃ -> p () (upd hβ‚‚ rβ‚‚ x₁))) () (upd hβ‚‚ r₁ xβ‚‚)) = (fun p hβ‚‚ -> (fun h₃ -> p () (upd hβ‚‚ rβ‚‚ x₁)) (upd hβ‚‚ r₁ xβ‚‚)) = (fun p hβ‚‚ -> p () (upd (upd hβ‚‚ r₁ xβ‚‚) rβ‚‚ x₁))

by (T-Let) Ξ“,x₁:int ⊒ let xβ‚‚ = !rβ‚‚ in (let _ = (r₁ := xβ‚‚) in rβ‚‚ := x₁) : ST unit (fun p -> (fun p₁ h₁ -> p₁ (sel h₁ rβ‚‚) h₁) (fun xβ‚‚ hβ‚‚ -> p () (upd (upd hβ‚‚ r₁ xβ‚‚) rβ‚‚ x₁))) = (fun p h₁ -> (fun xβ‚‚ hβ‚‚ -> p () (upd (upd hβ‚‚ r₁ xβ‚‚) rβ‚‚ x₁)) (sel h₁ rβ‚‚) h₁) = (fun p h₁ -> p () (upd (upd h₁ r₁ (sel h₁ rβ‚‚)) rβ‚‚ x₁))

by (T-Let) Ξ“ ⊒ let x₁ = !r₁ in (let xβ‚‚ = !rβ‚‚ in (let _ = (r₁ := xβ‚‚) in rβ‚‚ := x₁)) : ST unit (fun p -> (fun pβ‚€ hβ‚€ -> pβ‚€ (sel hβ‚€ r₁) hβ‚€) (fun x₁ h₁ -> p () (upd (upd h₁ r₁ (sel h₁ rβ‚‚)) rβ‚‚ x₁))) = (fun p hβ‚€ -> (fun x₁ h₁ -> p () (upd (upd h₁ r₁ (sel h₁ rβ‚‚)) rβ‚‚ x₁)) (sel hβ‚€ r₁) hβ‚€) = (fun p hβ‚€ -> p () (upd (upd hβ‚€ r₁ (sel hβ‚€ rβ‚‚)) rβ‚‚ (sel hβ‚€ r₁)))

val swap : r₁:ref int -> rβ‚‚:ref int -> ST unit (fun p hβ‚€ -> p () (upd (upd hβ‚€ r₁ (sel hβ‚€ rβ‚‚)) rβ‚‚ (sel hβ‚€ r₁)))

Weaker spec

Ξ“ ⊧ (βˆ€p hβ‚€. (βˆ€hβ‚„. sel hβ‚„ r₁ = sel hβ‚€ rβ‚‚ ∧ sel hβ‚„ rβ‚‚ = sel hβ‚€ r₁ β‡’ p () hβ‚„) β‡’ p () (upd (upd hβ‚€ r₁ (sel hβ‚€ rβ‚‚)) rβ‚‚ (sel hβ‚€ r₁)))

can instantiate premise for hβ‚„ = (upd (upd hβ‚€ r₁ (sel hβ‚€ rβ‚‚)) rβ‚‚ (sel hβ‚€ r₁)) and show the conclusion

⇐ (βˆ€p hβ‚€. (sel (upd (upd hβ‚€ r₁ (sel hβ‚€ rβ‚‚)) rβ‚‚ (sel hβ‚€ r₁)) r₁ = sel hβ‚€ rβ‚‚ ∧ sel (upd (upd hβ‚€ r₁ (sel hβ‚€ rβ‚‚)) rβ‚‚ (sel hβ‚€ r₁)) rβ‚‚ = sel hβ‚€ r₁ β‡’ p () (upd (upd hβ‚€ r₁ (sel hβ‚€ rβ‚‚)) rβ‚‚ (sel hβ‚€ r₁))) β‡’ p () (upd (upd hβ‚€ r₁ (sel hβ‚€ rβ‚‚)) rβ‚‚ (sel hβ‚€ r₁))) ⇔ (βˆ€p hβ‚€. p () (upd (upd hβ‚€ r₁ (sel hβ‚€ rβ‚‚)) rβ‚‚ (sel hβ‚€ r₁)) β‡’ p () (upd (upd hβ‚€ r₁ (sel hβ‚€ rβ‚‚)) rβ‚‚ (sel hβ‚€ r₁))) ⇔ True

——————————————————————————————————————————————–——————————————–—————– (T-Consequence)

val swap : r₁:ref int -> rβ‚‚:ref int -> ST unit (fun p hβ‚€ -> βˆ€hβ‚„. sel hβ‚„ r₁ = sel hβ‚€ rβ‚‚ ∧ sel hβ‚„ rβ‚‚ = sel hβ‚€ r₁ β‡’ p x hβ‚„)

Factorial example

val factorial_tot : nat -> Tot nat let rec factorial_tot x = if x = 0 then 1 else x * factorial_tot (x - 1)

val factorial : r₁:ref nat -> rβ‚‚:ref nat -> ST unit (requires (fun hβ‚€ -> True)) (ensures (fun hβ‚€ a h₁ -> βˆƒx. h₁ == (upd (upd hβ‚€ r₁ x) rβ‚‚ (factorial_tot (sel hβ‚€ r₁)))))

  • which desugars to:

val factorial : r₁:ref nat -> rβ‚‚:ref nat -> ST unit (fun p hβ‚€ -> βˆ€h₆. βˆƒx. h₆ == (upd (upd hβ‚€ r₁ x) rβ‚‚ (factorial_tot (sel hβ‚€ r₁))) β‡’ p () h₆)

  • which is equivalent to

val factorial : r₁:ref nat -> rβ‚‚:ref nat -> ST unit (fun p hβ‚€ -> βˆƒx. p () (upd (upd hβ‚€ r₁ x) rβ‚‚ (factorial_tot (sel hβ‚€ r₁))))

let rec factorial r₁ rβ‚‚ = hβ‚€ let x₁ = !r₁ in h₁ if x₁ = 0 then rβ‚‚ := 1 h₆ else (r₁ := x₁ - 1; h₃ factorial r₁ rβ‚‚; hβ‚„ let xβ‚‚ = !rβ‚‚ in hβ‚… rβ‚‚ := xβ‚‚ * x₁) h₆

by (T-Update) r₁ : ref int, rβ‚‚ : ref int, x₁:int, xβ‚‚:int ⊒ rβ‚‚ := xβ‚‚ * x₁ : ST unit (fun pβ‚… hβ‚… -> pβ‚… () (upd hβ‚… rβ‚‚ (xβ‚‚ * x₁)))

by (T-Read) r₁ : ref int, rβ‚‚ : ref int, x₁:int ⊒ !rβ‚‚ : ST int (fun pβ‚„ hβ‚„ -> pβ‚„ (sel hβ‚„ rβ‚‚) hβ‚„)

by (T-Let) r₁ : ref int, rβ‚‚ : ref int, x₁:int ⊒ (let xβ‚‚ = !rβ‚‚ in rβ‚‚ := xβ‚‚ * x₁) : ST (fun p -> (fun pβ‚„ hβ‚„ -> pβ‚„ (sel hβ‚„ rβ‚‚) hβ‚„) (fun xβ‚‚ hβ‚… -> p () (upd hβ‚… rβ‚‚ (xβ‚‚ * x₁)))) = (fun p hβ‚„ -> (fun xβ‚‚ hβ‚… -> p () (upd hβ‚… rβ‚‚ (xβ‚‚ * x₁))) (sel hβ‚„ rβ‚‚) hβ‚„) = (fun p hβ‚„ -> p () (upd hβ‚„ rβ‚‚ (sel hβ‚„ rβ‚‚ * x₁)))

by (T-App) r₁ : ref int, rβ‚‚ : ref int, x₁:int ⊒ factorial r₁ rβ‚‚ : ST unit (fun p₃ h₃ -> βˆƒx. p₃ () (upd (upd h₃ r₁ x) rβ‚‚ (factorial_tot (sel h₃ r₁))))

by (T-Let) r₁ : ref int, rβ‚‚ : ref int, x₁:int ⊒ (factorial r₁ rβ‚‚; let xβ‚‚ = !rβ‚‚ in rβ‚‚ := xβ‚‚ * x₁) : ST unit (fun p -> (fun p₃ h₃ -> βˆƒx. p₃ () (upd (upd h₃ r₁ x) rβ‚‚ (factorial_tot (sel h₃ r₁)))) (fun _ hβ‚„ -> p () (upd hβ‚„ rβ‚‚ (sel hβ‚„ rβ‚‚ * x₁)))) = (fun p h₃ -> βˆƒx. (fun hβ‚„ -> p () (upd hβ‚„ rβ‚‚ (sel hβ‚„ rβ‚‚ * x₁))) (upd (upd h₃ r₁ x) rβ‚‚ (factorial_tot (sel h₃ r₁)))) = (fun p h₃ -> βˆƒx. p () (upd (upd (upd h₃ r₁ x) rβ‚‚ (factorial_tot (sel h₃ r₁))) rβ‚‚ (sel (upd (upd h₃ r₁ x) rβ‚‚ (factorial_tot (sel h₃ r₁))) rβ‚‚ * x₁))) ⇔ (fun p h₃ -> βˆƒx. p () (upd (upd (upd h₃ r₁ x) rβ‚‚ (factorial_tot (sel h₃ r₁))) rβ‚‚ (factorial_tot (sel h₃ r₁)) * x₁)) ⇔ (fun p h₃ -> βˆƒx. p () (upd (upd h₃ r₁ x) rβ‚‚ (factorial_tot (sel h₃ r₁)) * x₁))

by (T-Update) r₁ : ref int, rβ‚‚ : ref int, x₁:int ⊒ r₁ := x₁ - 1 : ST unit (fun pβ‚‚ h₁ -> pβ‚‚ () (upd h₁ r₁ (x₁-1)))

by (T-Let) r₁ : ref int, rβ‚‚ : ref int, x₁:int ⊒ (r₁ := x₁ - 1; factorial r₁ rβ‚‚; let xβ‚‚ = !rβ‚‚ in rβ‚‚ := xβ‚‚ * x₁) : ST unit (fun p -> (fun pβ‚‚ h₁ -> pβ‚‚ () (upd h₁ r₁ (x₁-1))) (fun _ h₃ -> βˆƒx. p () (upd (upd h₃ r₁ x) rβ‚‚ (factorial_tot (sel h₃ r₁)) * x₁))) = (fun p h₁ -> βˆƒx. p () (upd (upd (upd h₁ r₁ (x₁-1)) r₁ x) rβ‚‚ (factorial_tot (sel (upd h₁ r₁ (x₁-1)) r₁)) * x₁)) ⇔ (fun p h₁ -> βˆƒx. p () (upd (upd h₁ r₁ x) rβ‚‚ (factorial_tot (x₁-1)) * x₁))

by (T-Update) r₁ : ref int, rβ‚‚ : ref int, x₁:int ⊒ rβ‚‚ := 1 : ST unit (fun p h₁ -> p () (upd h₁ rβ‚‚ 1))

by (T-IfST) r₁ : ref int, rβ‚‚ : ref int, x₁:int ⊒(if x₁ = 0 then rβ‚‚ := 1 else r₁ := x₁ - 1; factorial r₁ rβ‚‚; let xβ‚‚ = !rβ‚‚ in rβ‚‚ := xβ‚‚ * x₁) : ST unit (fun p -> if x₁ = 0 then (fun h₁ -> p () (upd h₁ rβ‚‚ 1)) else (fun h₁ -> βˆƒx. p () (upd (upd h₁ r₁ x) rβ‚‚ (factorial_tot (x₁-1)) * x₁)))

by (T-Read) r₁ : ref int, rβ‚‚ : ref int, x₁:int ⊒ !r₁ : ST int (fun pβ‚€ hβ‚€ -> pβ‚€ (sel hβ‚€ r₁) hβ‚€)

by (T-Let) r₁ : ref int, rβ‚‚ : ref int ⊒ factorial_body : ST (fun p -> (fun pβ‚€ hβ‚€ -> pβ‚€ (sel hβ‚€ r₁) hβ‚€) (fun x₁ -> if x₁ = 0 then (fun h₁ -> p () (upd h₁ rβ‚‚ 1)) else (fun h₁ -> βˆƒx. p () (upd (upd h₁ r₁ x) rβ‚‚ (factorial_tot (x₁-1)) * x₁)))) = (fun p hβ‚€ -> if sel hβ‚€ r₁ = 0 then p () (upd hβ‚€ rβ‚‚ 1) else βˆƒx. p () (upd (upd hβ‚€ r₁ x) rβ‚‚ (factorial_tot (sel hβ‚€ r₁ - 1)) * (sel hβ‚€ r₁))) ⇔ (fun p hβ‚€ -> βˆƒx. p () (upd (upd hβ‚€ r₁ x) rβ‚‚ (factorial_tot (sel hβ‚€ r₁))))

[Advanced] Deriving Hoare-Style T-Let from WP-Style T-Let

What do Dijkstra monads say in this case? Convert triples to WPs and use WP bind … what does one get?

ST’ t pre post = ST t (fun p hβ‚€ -> pre hβ‚€ ∧ (βˆ€ x h₁. post hβ‚€ x h₁ β‡’ p x h₁))

Ξ“ ⊒ e₁ : ST’ t₁ (fun hβ‚€ -> fpre₁) (fun hβ‚€ x₁ h₁ -> fpost₁) Ξ“,x₁:t₁ ⊒ eβ‚‚ : ST’ tβ‚‚ (fun h₁ -> fpreβ‚‚) (fun h₁ xβ‚‚ hβ‚‚ -> fpostβ‚‚)

–————————–———–————————–—————————–—————————————————————————————–————– (T-Let)

Ξ“ ⊒ let x₁ = e₁ in eβ‚‚ : ST’ tβ‚‚ (fun hβ‚€ -> fpre) (fun hβ‚€ x hβ‚‚ -> fpost)

Ξ“ ⊒ e₁ : ST t₁ (fun post hβ‚€ -> fpre₁ hβ‚€ ∧ βˆ€x₁ h₁. fpost₁ hβ‚€ x₁ h₁ β‡’ post x₁ h₁) = wp₁ Ξ“,x₁:t₁ ⊒ eβ‚‚ : ST tβ‚‚ (fun post h₁ -> fpreβ‚‚ h₁ ∧ βˆ€xβ‚‚ hβ‚‚. fpostβ‚‚ h₁ xβ‚‚ hβ‚‚ β‡’ post xβ‚‚ hβ‚‚) = wpβ‚‚

———————————————————–————————–———–————————–—————————–—————————————————————————————– (T-Let) Ξ“ ⊒ let x₁ = e₁ in eβ‚‚ : ST tβ‚‚ wp

The WP-based (T-Let) rule works like this: Ξ“ ⊒ let x₁ = e₁ in eβ‚‚ : ST tβ‚‚ (bindβ‚›β‚œ x ← wp₁ in wpβ‚‚) Ξ“ ⊒ let x₁ = e₁ in eβ‚‚ : ST tβ‚‚ (fun post hβ‚€ -> wp₁ (fun x h₁ -> wpβ‚‚ post h₁) hβ‚€) if we plug in the WPs above we get: Ξ“ ⊒ let x₁ = e₁ in eβ‚‚ : ST tβ‚‚ (fun post hβ‚€ -> (fun post hβ‚€ -> fpre₁ hβ‚€ ∧ βˆ€x₁ h₁. fpost₁ hβ‚€ x₁ h₁ β‡’ post x₁ h₁) (fun x₁ h₁ -> (fun post h₁ -> fpreβ‚‚ h₁ ∧ βˆ€xβ‚‚ hβ‚‚. fpostβ‚‚ h₁ xβ‚‚ hβ‚‚ β‡’ post xβ‚‚ hβ‚‚) post h₁) hβ‚€) = ST t2 (fun post hβ‚€ -> fpre₁ hβ‚€ ∧ βˆ€x₁ h₁. fpost₁ hβ‚€ x₁ h₁ β‡’ fpreβ‚‚ h₁ ∧ βˆ€xβ‚‚ hβ‚‚. fpostβ‚‚ h₁ xβ‚‚ hβ‚‚ β‡’ post xβ‚‚ hβ‚‚) = wp

  • this already allows us to derive fpre fpre = wp (fun x h -> True) = fpre₁ hβ‚€ ∧ βˆ€x₁ h₁. fpost₁ hβ‚€ x₁ h₁ β‡’ fpreβ‚‚ h₁
  • and fpost too using the following relation: let as_ensures (#a:Type) (wp:st_wp a) = fun hβ‚€ x h₁ -> ~(wp (fun x’ h₁’ -> x=!=x’ \/ h₁=!=h₁’) hβ‚€)

    fpost hβ‚€ xβ‚‚ hβ‚‚ = ~( (fun post hβ‚€ -> fpre₁ hβ‚€ ∧ βˆ€x₁ h₁. fpost₁ hβ‚€ x₁ h₁ β‡’ fpreβ‚‚ h₁ ∧ βˆ€xβ‚‚ hβ‚‚. fpostβ‚‚ h₁ xβ‚‚ hβ‚‚ β‡’ post xβ‚‚ hβ‚‚) (fun x₂’ h₂’ -> x₂’!=xβ‚‚ \/ hβ‚‚'!=hβ‚‚) hβ‚€ ) = ~ (fpre₁ hβ‚€ ∧ (βˆ€x₁ h₁. fpost₁ hβ‚€ x₁ h₁ β‡’ (fpreβ‚‚ h₁ ∧ βˆ€x₂” h₂”. fpostβ‚‚ h₁ xβ‚‚ hβ‚‚ β‡’ xβ‚‚=!=x₂” ∨ hβ‚‚=!=h₂”))) = fpre₁ hβ‚€ β‡’ (βˆƒx₁ h₁. fpost₁ hβ‚€ x₁ h₁ ∧ ~(fpreβ‚‚ h₁ ∧ βˆ€x₂” h₂”. fpostβ‚‚ h₁ xβ‚‚ hβ‚‚ β‡’ xβ‚‚=!=x₂” ∨ hβ‚‚=!=h₂”))) = fpre₁ hβ‚€ β‡’ βˆƒx₁ h₁. fpost₁ hβ‚€ x₁ h₁ ∧ (fpreβ‚‚ h₁ β‡’ βˆƒx₂” h₂”. fpostβ‚‚ h₁ xβ‚‚ hβ‚‚ ∧ xβ‚‚==x₂” ∧ hβ‚‚==h₂”) = fpre₁ hβ‚€ β‡’ βˆƒx₁ h₁. fpost₁ hβ‚€ x₁ h₁ ∧ (fpreβ‚‚ h₁ β‡’ fpostβ‚‚ h₁ xβ‚‚ hβ‚‚)

    Ξ“ ⊒ e₁ : ST t₁ (fun hβ‚€ -> fpre₁) (fun hβ‚€ x₁ h₁ -> fpost₁)

Ξ“,x₁:t₁ ⊒ eβ‚‚ : ST tβ‚‚ (fun h₁ -> fpreβ‚‚) (fun h₁ xβ‚‚ hβ‚‚ -> fpostβ‚‚)

–————————–———–————————–—————————–—————————————————————————————–————–————————— (T-Let)

Ξ“ ⊒ let x₁ = e₁ in eβ‚‚ : ST tβ‚‚ (fun hβ‚€ -> fpre₁ hβ‚€ ∧ βˆ€x₁ h₁. fpost₁ hβ‚€ x₁ h₁ β‡’ fpreβ‚‚ h₁) (fun hβ‚€ xβ‚‚ hβ‚‚ -> fpre₁ hβ‚€ β‡’ βˆƒx₁ h₁. fpost₁ hβ‚€ x₁ h₁ ∧ (fpreβ‚‚ h₁ β‡’ fpostβ‚‚ h₁ xβ‚‚ hβ‚‚))

Better T-Let rule?

Ξ“ ⊒ e₁ : ST t₁ (fun hβ‚€ -> fpre₁) (fun hβ‚€ x₁ h₁ -> fpost₁) Ξ“,x₁:t₁ ⊒ eβ‚‚ : ST tβ‚‚ (fun h₁ -> fpreβ‚‚) (fun h₁ xβ‚‚ hβ‚‚ -> fpostβ‚‚)

–————————–———–————————–—————————–—————————————————————————————–——————– (T-Let template)

Ξ“ ⊒ let x₁ = e₁ in eβ‚‚ : ST’ tβ‚‚ (fun hβ‚€ -> fpre) (fun hβ‚€ xβ‚‚ hβ‚‚ -> fpost) = ST tβ‚‚ (fun p hβ‚€ -> fpre hβ‚€ ∧ (βˆ€xβ‚‚ hβ‚‚. fpost hβ‚€ xβ‚‚ hβ‚‚ β‡’ p xβ‚‚ hβ‚‚))

Ξ“ ⊒ e₁ : ST t₁ (fun post hβ‚€ -> fpre₁ hβ‚€ ∧ βˆ€x₁ h₁. fpost₁ hβ‚€ x₁ h₁ β‡’ post x₁ h₁) = wp₁ Ξ“,x₁:t₁ ⊒ eβ‚‚ : ST tβ‚‚ (fun post h₁ -> fpreβ‚‚ h₁ ∧ βˆ€xβ‚‚ hβ‚‚. fpostβ‚‚ h₁ xβ‚‚ hβ‚‚ β‡’ post xβ‚‚ hβ‚‚) = wpβ‚‚

–————————–———–————————–—————————–—————————————————————————————–———— (T-Let on WPs)

Ξ“ ⊒ let x₁ = e₁ in eβ‚‚ : ST tβ‚‚ (fun p hβ‚€ -> fpre₁ hβ‚€ ∧ (βˆ€x₁ h₁. fpost₁ hβ‚€ x₁ h₁ β‡’ fpreβ‚‚ h₁ ∧ βˆ€xβ‚‚ hβ‚‚. fpostβ‚‚ h₁ xβ‚‚ hβ‚‚ β‡’ p xβ‚‚ hβ‚‚))

Problem: find fpre₁, fpost₁, fpreβ‚‚, fpostβ‚‚ in terms of fpre and fpost so that (fpre hβ‚€ ∧ (βˆ€xβ‚‚ hβ‚‚. fpost hβ‚€ xβ‚‚ hβ‚‚ β‡’ p xβ‚‚ hβ‚‚)) ⇔ (fpre₁ hβ‚€ ∧ (βˆ€x₁ h₁. fpost₁ hβ‚€ x₁ h₁ β‡’ fpreβ‚‚ h₁ ∧ βˆ€xβ‚‚ hβ‚‚. fpostβ‚‚ h₁ xβ‚‚ hβ‚‚ β‡’ p xβ‚‚ hβ‚‚))

First step is easy: fpre₁ = fpre Might need to keep fpost₁ (in hoare there is also a magic interpolant) Can I derive fpreβ‚‚ from fpost₁? For instance: fpreβ‚‚ = βˆƒhβ‚€. fpost₁ hβ‚€ Can I derive fpostβ‚‚ from fpost? from previous derivation we had fpost = fpre β‡’ βˆƒx₁ h₁. fpost₁ ∧ (fpreβ‚‚ β‡’ fpostβ‚‚)

… not there yet …

⚠️ **GitHub.com Fallback** ⚠️