Separation Logic Frame Rule

Safety Monotonicity: (σ, fault) ∉ R and σ ≤ σ′ implies (σ′, fault) ∉ R. Frame Property: If (σ0, fault) ∉ R, σ = σ0•σ1 and (σ, σ′) ∈ R then ∃σ′0. σ′ = σ′0 • σ1 and (σ0, σ′0) ∈ R.

In our nrm/err defs:

Safety Monotonicity: ∀ σ σ′, σ ∉ R.(err) -> σ ≤ σ′ -> σ′ ∉ R.(err) This can be implied by: ∀ σ σ′, σ′ ∈ R.(err) -> σ ≤ σ′ -> σ ∈ R.(err)

Frame Property: ∀ σ0 σ1 σ′, σ0 ∉ R.(err) -> σ = σ0•σ1 -> (σ, σ′) ∈ R.(nrm) -> ∃σ′0. σ′ = σ′0 • σ1 /\ (σ0, σ′0) ∈ R.(nrm)

But, order-theoretically, where should fault go? The answer is on the top, as in functions f : Σ → P (Σ)^⊤. Conceptually, faulting is like Scott’s top: an inconsistent or over-determined value.

Using functions into the (topped) powerset, we can work with a much simpler condition:

locality : σ1#σ2 implies f (σ1 • σ2) ≤ (f σ1) ∗ {σ2}.

Here, the ∗ operation is extended with ⊤, by p ∗ ⊤ = ⊤ ∗ p = ⊤. It can be verified that a relation R satisfies Safety Monotonicity and Frame Property iff the corresponding function func(R) : Σ → P (Σ)^⊤ satisfies locality.1 func(R)σ returns ⊤ when (σ, fault) ∈ R, even if we also have (σ, σ′) ∈ R for some σ′ ≠ fault.

Prompts

(* Print FDenote. *)
(* Notation FDenote := (program GlobalState (option val)) *)
(* Print program. *)
(* Notation program := M
Record M (Σ A : Type) : Type := Build_M { nrm : Σ -> A -> Σ -> Prop; err : Σ -> Prop }. *)

(* program := { nrm : GlobalState -> option val -> GlobalState -> Prop; err : GlobalState -> Prop } *)

Check @Hoare GlobalState (option val).
(* Hoare
     : (GlobalState -> Prop) -> FDenote -> (option val -> GlobalState -> Prop) -> Prop *)

Other Changes

(*
Record GlobalState := mkGlobalState {
  gvars : VarsAddrType;
  gmem  : Mem.mem;
}.

Record ProgState := mkProgState {
  gstate :> GlobalState;
  lvars  : VarsAddrType
}.

对应也有两个版本的 Assertion
*)

(*
FDenote := {
  nrm: GlobalState -> option val -> GlobalState -> Prop;
  err: GlobalState -> Prop
}.

χ 需要满足 locality，才能有 frame rule：
frame property
*)