Skip to content

GitLab

Commit e5f526c3 authored by Tej Chajed's avatar Tej Chajed Committed by Ralf Jung
Browse files

Add a verified interpreter for HeapLang

parent d3e1e7ff
Show whitespace changes
Inline Side-by-side
_CoqProject
View file @ e5f526c3
......@@ -142,6 +142,7 @@ iris/proofmode/modality_instances.v
iris_heap_lang/locations.v
iris_heap_lang/lang.v
iris_heap_lang/class_instances.v
iris_heap_lang/pretty.v
iris_heap_lang/metatheory.v
iris_heap_lang/tactics.v
iris_heap_lang/primitive_laws.v
......@@ -174,3 +175,5 @@ iris_deprecated/base_logic/auth.v
iris_deprecated/base_logic/sts.v
iris_deprecated/base_logic/viewshifts.v
iris_deprecated/program_logic/hoare.v
iris_staging/heap_lang/interpreter.v
coq-iris-staging.opam
View file @ e5f526c3
......@@ -14,6 +14,7 @@ work is needed before they are ready for this.
depends: [
"coq-iris" {= version}
"coq-iris-heap-lang" {= version}
]
build: ["./make-package" "iris_staging" "-j%{jobs}%"]
......
iris_heap_lang/locations.v
View file @ e5f526c3
......@@ -2,15 +2,17 @@ From stdpp Require Import countable numbers gmap.
From iris.prelude Require Export prelude.
From iris.prelude Require Import options.
Record loc := { loc_car : Z }.
Record loc := Loc { loc_car : Z }.
Add Printing Constructor loc.
Global Instance loc_eq_decision : EqDecision loc.
Proof. solve_decision. Qed.
Proof. solve_decision. Defined.
Global Instance loc_inhabited : Inhabited loc := populate {|loc_car := 0 |}.
Global Instance loc_countable : Countable loc.
Proof. by apply (inj_countable' loc_car (λ i, {| loc_car := i |})); intros []. Qed.
Proof. by apply (inj_countable' loc_car Loc); intros []. Defined.
Program Instance loc_infinite : Infinite loc :=
inj_infinite (λ p, {| loc_car := p |}) (λ l, Some (loc_car l)) _.
......
iris_heap_lang/pretty.v 0 → 100644
View file @ e5f526c3
From stdpp Require Export pretty.
From iris.heap_lang Require Import lang.
From iris.prelude Require Import options.
(** * Pretty printing for HeapLang values *)
Global Instance pretty_loc : Pretty loc :=
λ l, pretty l.(loc_car).
Global Instance pretty_base_lit : Pretty base_lit :=
λ l, match l with
| LitInt z => pretty z
| LitBool b => if b then "true" else "false"
| LitUnit => "()"
| LitPoison => "<poison>"
| LitLoc l => "(loc " +:+ pretty l +:+ ")"
| LitProphecy i => "(prophecy " +:+ pretty i +:+ ")"
end.
Global Instance pretty_binder : Pretty binder :=
λ b, match b with
| BNamed x => x
| BAnon => "<>"
end.
(** Note that this instance does not print function bodies and is thus not
injective (unlike most `pretty` instances). *)
Global Instance pretty_val : Pretty val :=
fix go v :=
match v with
| LitV l => "#" +:+ pretty l
| RecV f x e =>
match f with
| BNamed f => "rec: " +:+ f +:+ " " +:+ pretty x +:+ " := <body>"
| BAnon => "λ: " +:+ pretty x +:+ ", <body>"
end
| PairV v1 v2 => "(" +:+ go v1 +:+ ", " +:+ go v2 +:+ ")"
| InjLV v => "inl (" +:+ go v +:+ ")"
| InjRV v => "inr (" +:+ go v +:+ ")"
end.
Global Instance pretty_un_op : Pretty un_op :=
λ op, match op with
| NegOp => "~"
| MinusUnOp => "-"
end.
Global Instance pretty_bin_op : Pretty bin_op :=
λ op, match op with
| PlusOp => "+"
| MinusOp => "-"
| MultOp => "*"
| QuotOp => "`quot`"
| RemOp => "`rem`"
| AndOp => "&"
| OrOp => "|"
| XorOp => "`xor`"
| ShiftLOp => "<<"
| ShiftROp => ">>"
| LeOp => "≤"
| LtOp => "<"
| EqOp => "="
| OffsetOp => "+ₗ"
end .
iris_staging/heap_lang/interpreter.v 0 → 100644
View file @ e5f526c3
(* This file is still experimental. See its tracking issue
https://gitlab.mpi-sws.org/iris/iris/-/issues/405 for details on remaining
issues before stabilization. *)
(** A verified interpreter for HeapLang.
This file defines a function [exec (fuel:nat) (e:expr) : val + Error] which
runs a HeapLang expression to [inl v] if [e] terminates in a value [v], or
returns [inr msg] with a structured error message [msg] if [e] gets stuck at
some point. Use [pretty msg] to turn the message into a readable string.
The point of this interpreter is to allow you to test your code or small
snippets of HeapLang code and see what the semantics does. We prove it
correct so that you can trust that the interpreter actually reflects the
semantics, particularly when it says the program is stuck. The interpreter
also goes through some pain to report specific error messages on failure,
although these explanations are of course not verified.
We prove a correctness theorem [exec_spec] about [exec] summarizing its
guarantees. It distinguishes two cases:
1. If [exec] returns [inl v], then [e] can execute to [v] according to [rtc
erased_step] (following the semantics of HeapLang).
2. If [exec] returns [inr (Stuck msg)], then [e] can execute to some [e']
that is stuck according to the HeapLang semantics, so [e] really does "go
wrong". [msg] is a human-readable string describing how [e] got stuck.
3. Finally, [exec] can also fail due to running out of fuel or encountering
an unsupported prophecy variable operation, in which case it returns a
distinct error case and the correctness theorem provides no guarantees.
The interpreter is _sequential_ and _deterministic_, which means it has some
limitations. It will ignore forked threads and continue to execute the main
thread, which may cause some programs to live-lock that would otherwise make
progress under a fair scheduler.
Determinism creates a subtle difference between the interpreter and the
semantics. The interpreter only guarantees properties of one execution while
the semantics and any safety property proven using Iris conceptually regard
all executions. Concretely, consider this program: [let: "x" := ref #0 in
!(LitLoc 1)]. There is one execution where this program terminates in [#0],
and many where the allocation results in some other location and it is
stuck. The interpeter happens to allocate starting at [LitLoc 1] and will
say it produces [#0]. This is technically correct but not useful - there is
a stuck execution the interpreter didn't find. The only non-determinism in
sequential HeapLang is allocation, so we believe only strange programs like
this that correctly "guess" the interpreter's allocations are affected.
The interpreter is heavily based on Sydney Gibson's MEng thesis:
https://pdos.csail.mit.edu/papers/gibsons-meng.pdf. That thesis includes an
interpreter for sequential GooseLang, a fork of HeapLang.
*)
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import tactics pretty.
From iris.prelude Require Import options.
Local Ltac invc H := inversion H; subst; clear H.
(** Errors are tagged to give [exec] a stronger specification. [Stuck s] is
distinguished from the other cases because it comes with a proof that the
expression is eventually stuck. *)
Inductive Error :=
| Stuck (s:string)
| Unsupported (s:string)
| OutOfFuel.
Global Instance error_pretty : Pretty Error :=
λ err, match err with
| Stuck s => "stuck: " +:+ s
| Unsupported s => "unsupported operation: " +:+ s
| OutOfFuel => "out of fuel"
end.
Module interp_monad.
Record interp_state :=
InterpState { lang_state : state; next_loc : Z; forked_threads : list expr; }.
Add Printing Constructor interp_state.
Definition modify_lang_state (f: state → state): interp_state → interp_state :=
λ s, InterpState (f s.(lang_state)) s.(next_loc) (s.(forked_threads)).
Definition add_forked_thread (e: expr) : interp_state → interp_state :=
λ s, InterpState s.(lang_state) s.(next_loc) (s.(forked_threads) ++ [e]).
Definition interp_state_alloc (n: Z) : interp_state → interp_state :=
λ s, InterpState s.(lang_state) (n + s.(next_loc)) s.(forked_threads).
Inductive state_wf (s: interp_state): Prop :=
{ state_wf_holds (l: loc) : (s.(next_loc) ≤ l.(loc_car))%Z →
s.(lang_state).(heap) !! l = None; }.
Definition InterpretM (A:Type) : Type :=
interp_state → (A+Error) * interp_state.
Definition init_state : state := {| heap := ∅; used_proph_id := ∅ |}.
Definition init_interp_state : interp_state :=
InterpState init_state 1 [].
(** [run] runs an interpreter monad value starting from an empty initial
state. *)
Local Definition run {A} (f: InterpretM A) : A + Error :=
(f init_interp_state).1.
Lemma init_interp_state_wf : state_wf init_interp_state.
Proof. constructor; rewrite /init_interp_state //=. Qed.
(* basic monad *)
Global Instance interp_ret : MRet InterpretM := λ A (x:A), λ s, (inl x, s).
Global Instance interp_bind : MBind InterpretM :=
λ A B (f: A → InterpretM B) (x: InterpretM A),
λ s, let (r, s') := x s in
match r with
| inl x' => f x' s'
| inr e => (inr e, s')
end.
Global Instance interp_fmap : FMap InterpretM :=
λ A B (f: A → B) (x: InterpretM A),
λ s, let (r, s') := x s in
match r with
| inl x' => (inl (f x'), s')
| inr e => (inr e, s')
end.
(* state+error-specific monadic constants *)
Definition interp_modify (f: interp_state → interp_state): InterpretM () :=
λ s, (inl (), f s).
Definition interp_modify_state (f: state → state): InterpretM () :=
interp_modify (modify_lang_state f).
Definition interp_read {A} (f: state → A): InterpretM A :=
λ s, (inl (f s.(lang_state)), s).
Definition interp_error {A} (msg: string) : InterpretM A := λ s, (inr (Stuck msg), s).
Definition interp_alloc (n:Z): InterpretM loc :=
λ s, (inl {| loc_car := s.(next_loc)|}, interp_state_alloc n s).
Definition read_loc (method: string) (vl: val) : InterpretM (loc*val) :=
match vl with
| LitV (LitLoc l) =>
mv ← interp_read (λ σ, σ.(heap) !! l);
match mv with
| Some (Some v) => mret (l, v)
| Some None =>
interp_error $ method +:+ ": use after free at location: " +:+ pretty l
| None =>
interp_error $ method +:+ ": unallocated location: " +:+ pretty l
end
| _ => interp_error $ method +:+ ": applied to non-loc " +:+ pretty vl
end.
Lemma error_not_inl {A} {msg s} {v: A} {s'} :
interp_error msg s = (inl v, s') → False.
Proof. by inversion 1. Qed.
Lemma mret_inv {A} (v: A) s v' s' :
mret v s = (inl v', s') → v = v' ∧ s = s'.
Proof. by inversion 1. Qed.
Lemma interp_bind_inv A B (x: InterpretM A) (f: A → InterpretM B) r s s' :
(x ≫= f) s = (r, s') →
(∃ e, x s = (inr e, s') ∧ r = inr e) ∨
(∃ s0 x', x s = (inl x', s0) ∧
f x' s0 = (r, s')).
Proof.
rewrite /mbind /interp_bind.
repeat case_match; inversion 1; subst; eauto.
Qed.
Lemma interp_bind_inl_inv A B (x: InterpretM A) (f: A → InterpretM B) (r: B) s s' :
(x ≫= f) s = (inl r, s') →
∃ s0 x', x s = (inl x', s0) ∧
f x' s0 = (inl r, s').
Proof.
intros [(e & ? & ?) | (s0 & x' & H1 & H2)]%interp_bind_inv.
- congruence.
- rewrite H1.
eexists _, _; eauto.
Qed.
Lemma interp_fmap_inv {A B} (f: A → B) x s v s' :
(f <$> x) s = (inl v, s') →
∃ v0, v = f v0 ∧ x s = (inl v0, s').
Proof.
rewrite /fmap /interp_fmap.
repeat case_match; inversion 1; subst; eauto.
Qed.
Lemma read_loc_inv method vl s l v s' :
read_loc method vl s = (inl (l, v), s') →
vl = LitV (LitLoc l) ∧
s' = s ∧
s.(lang_state).(heap) !! l = Some (Some v).
Proof.
rewrite /read_loc.
destruct vl as [l' | | | | ]; try by inversion 1.
destruct l' as [| | | | l' |]; intro H; try by inversion H.
apply interp_bind_inl_inv in H as (s0 & mv & Heq1 & Heq2).
destruct mv as [mv|]; try by inversion Heq2.
destruct mv; inversion Heq2; subst; clear Heq2.
inversion Heq1; subst; clear Heq1.
eauto.
Qed.
Ltac errored :=
lazymatch goal with
| H: interp_error _ _ = (inl _, _) |- _ => solve [ exfalso; apply (error_not_inl H) ]
| H: (inr _, _) = (inl _, _) |- _ => solve [ exfalso; inversion H ]
end.
Ltac success :=
repeat
lazymatch goal with
| H: mret _ _ = (inl _, _) |- _ =>
let Heqv := fresh "Heqv" in
let Heqs := fresh "Heqs" in
apply mret_inv in H as [Heqv Heqs]; subst
| H: (_ ≫= (λ x, _)) _ = (inl _, _) |- _ =>
let s := fresh "s" in
let x := fresh x in
let Heq1 := fresh "Heq" in
let Heq2 := fresh "Heq" in
apply interp_bind_inl_inv in H as (s & x & Heq1 & Heq2); subst
| H: (_ <$> _) _ = (inl ?v, _) |- _ =>
let s := fresh "s" in
let v_tmp := fresh "v" in
rename v into v_tmp;
apply interp_fmap_inv in H as (v & -> & H)
| H: interp_modify _ _ = (inl _, _) |- _ => invc H
| H: interp_modify_state _ _ = (inl _, _) |- _ => invc H
| H: interp_read _ _ = (inl _, _) |- _ => invc H
| H: read_loc _ _ _ = (inl _, _) |- _ =>
apply read_loc_inv in H as (-> & -> & H)
end; subst.
Lemma interp_bind_inr_inv {A B} (x: InterpretM A) (f: A → InterpretM B) r s s' :
(x ≫= f) s = (inr r, s') →
(x s = (inr r, s')) ∨
(∃ s0 x', x s = (inl x', s0) ∧ f x' s0 = (inr r, s')).
Proof.
rewrite /mbind /interp_bind.
repeat case_match; intros; simplify_eq/=; eauto.
Qed.
Lemma interp_fmap_inr_inv {A B} (f: A → B) (x: InterpretM A) s e s' :
(f <$> x) s = (inr e, s') →
x s = (inr e, s').
Proof.
rewrite /fmap /interp_fmap.
repeat case_match; intros; simplify_eq/=; auto.
Qed.
Lemma read_loc_inr_inv method vl s err s' :
read_loc method vl s = (inr err, s') →
s = s' ∧ match vl with
| LitV (LitLoc l) => ∀ v, s.(lang_state).(heap) !! l ≠ Some (Some v)
| _ => True
end.
Proof.
rewrite /read_loc.
repeat case_match; subst; try solve [ inversion 1; subst; auto ].
intros H.
apply interp_bind_inr_inv in H as [H|(s0&x& Hexec1 & Hexec2)]; success.
- invc H.
- repeat case_match; invc Hexec2.
+ intuition congruence.
+ intuition congruence.
Qed.
Ltac failure :=
repeat
match goal with
| H: (_ ≫= _) _ = (inr _, _) |- _ =>
let s := fresh "s" in
let x := fresh "x" in
let Heq := fresh "Heq" in
apply interp_bind_inr_inv in H as [H | (s & x & Heq & H)]
| H: interp_error _ _ = (inr _, _) |- _ => invc H
| H: mret _ _ = (inr _, _) |- _ => solve [ inversion H ]
| H: interp_modify _ _ = (inr _, _) |- _ => solve [ inversion H ]
| H: interp_modify_state _ _ = (inr _, _) |- _ => solve [ inversion H ]
| H: (_ <$> _) _ = (inr _, _) |- _ =>
apply interp_fmap_inr_inv in H
| H: read_loc _ _ _ = (inr _, _) |- _ =>
apply read_loc_inr_inv in H as [-> H]
end; subst.
End interp_monad.
Import interp_monad.
Section interpreter.
(* to make the below definition work with strings as well we add an
instance of [Pretty string] *)
Local Instance pretty_string : Pretty string := λ s, s.
Local Definition pretty_app (s: string) {A} `{Pretty A} (x:A) : string :=
s +:+ pretty x.
Infix "+" := pretty_app.
(* We explain errors which in the semantics are represented by a pure function
returning None; to sanity-check these definitions, we prove they cover
exactly the cases where the underlying operation returns None. *)
Definition option_opposites {A B} (m1 : option A) (m2 : option B) :=
is_Some m1 ↔ m2 = None.
Lemma option_opposites_alt {A B} (m1 : option A) (m2 : option B) :
option_opposites m1 m2 ↔ match m1, m2 with
| Some _, None => True
| None , Some _ => True
| _ , _ => False
end.
Proof.
rewrite /option_opposites is_Some_alt.
repeat case_match; intuition congruence.
Qed.
(** produce an error message for [un_op_eval] *)
Definition explain_un_op_fail op v : option string :=
match op with
| NegOp => match v with
| LitV (LitInt _) => None
| LitV (LitBool _) => None
| _ => Some $ "~ (NegOp) can only be applied to integers and booleans, got " + v
end
| MinusUnOp =>
match v with
| LitV (LitInt _) => None
| _ => Some $ "unary - (MinusUnOp) can only be applied to integers, got " + v
end
end.
Lemma explain_un_op_fail_wf op v :
option_opposites (explain_un_op_fail op v) (un_op_eval op v).
Proof.
apply option_opposites_alt.
rewrite /explain_un_op_fail /un_op_eval.
repeat case_match; simplify_eq/=; auto.
Qed.
Definition explain_unboxed v : option string :=
match v with
| LitV l | InjLV (LitV l) | InjRV (LitV l) =>
match l with
| LitPoison => Some "poison values (from erasing prophecies) cannot be compared"
| LitProphecy _ => Some "prophecies cannot be compared"
| _ => None
end
| InjLV _ | InjRV _ => Some "sum values can only be compared if they contain literals"
| PairV _ _ => Some "pairs are large and considered boxed, must compare by field"
| RecV _ _ _ => Some "closures are large and cannot be compared"
end.
Lemma explain_unboxed_wf v :
match explain_unboxed v with
| Some _ => ~val_is_unboxed v
| None => val_is_unboxed v
end.
Proof.
rewrite /explain_unboxed /val_is_unboxed /lit_is_unboxed.
repeat case_match; intuition congruence.
Qed.
Definition explain_vals_compare_safe_fail v1 v2 : option string :=
match explain_unboxed v1, explain_unboxed v2 with
| Some msg1, Some msg2 =>
Some $ "one of " + v1 + " and " + v2 + " must be unboxed to compare: "
+ v1 + ": " + msg1 + ", "
+ v2 + ": " + msg2
| _, _ => None
end.
(** [explain_vals_compare_safe_fail] gives an explanation when
[vals_compare_safe] would be false (that is, when v1 and v2 cannot be
compared) *)
Lemma explain_vals_compare_safe_fail_wf v1 v2 :
is_Some (explain_vals_compare_safe_fail v1 v2) ↔ ~vals_compare_safe v1 v2.
Proof.
cut (explain_vals_compare_safe_fail v1 v2 = None ↔ vals_compare_safe v1 v2).
{ rewrite is_Some_alt.
destruct (explain_vals_compare_safe_fail _ _); intuition congruence. }
rewrite /explain_vals_compare_safe_fail /vals_compare_safe.
pose proof (explain_unboxed_wf v1).
pose proof (explain_unboxed_wf v2).
destruct (explain_unboxed v1), (explain_unboxed v2); intuition congruence.
Qed.
(** produce an error message for [bin_op_eval] *)
Definition explain_bin_op_fail op v1 v2 : option string :=
if decide (op = EqOp)
then (explain_vals_compare_safe_fail v1 v2)
else match v1, v2 with
| LitV (LitInt _), LitV (LitInt _) =>
match op with
| OffsetOp => Some $ "cannot add to integer " + v1 + " with +ₗ (only locations)"
| _ => None
end
| LitV (LitBool b1), LitV (LitBool b2) =>
match bin_op_eval_bool op b1 b2 with
| Some _ => None
| None => Some $ "non-boolean operator applied to booleans " + op
end
| LitV (LitLoc _), _ =>
match op, v2 with
| OffsetOp, LitV (LitInt _) => None
| OffsetOp, _ => Some $ "can only call +ₗ on integers, got " + v2
| _, _ => Some $ "the only supported operation on locations is +ₗ #i, got "
+ op + " " + v2
end
| _, _ => Some $ "mismatched types of values " + v1 + " and " + v2
end.
Lemma explain_bin_op_fail_wf op v1 v2 :
option_opposites (explain_bin_op_fail op v1 v2) (bin_op_eval op v1 v2).
Proof.
apply option_opposites_alt.
rewrite /explain_bin_op_fail /bin_op_eval
/bin_op_eval_int /bin_op_eval_bool /bin_op_eval_loc.
repeat (case_match; simplify_eq/=; auto).
- pose proof (explain_vals_compare_safe_fail_wf v1 v2).
intuition eauto.
- pose proof (explain_vals_compare_safe_fail_wf v1 v2) as H.
replace (explain_vals_compare_safe_fail v1 v2) in H.
rewrite -> is_Some_alt in H.
intuition eauto.
Qed.
(* define a shorthand for readability below *)
Local Notation error := interp_error.
Fixpoint interpret (fuel:nat) (e: expr) {struct fuel} : InterpretM val :=
match fuel with
| 0 => λ s, (inr OutOfFuel, s)
| S fuel' => let interp := interpret fuel' in
match e with
(* lambda calculus *)
| Val v => mret v
| Var x => error $ "free var: " + x
| Rec f x e => mret (RecV f x e)
| App f e =>
v2 ← interp e;
f ← interp f;
match f with