part2.v 1.91 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import par.

(* PART 2: Texan triples *)
Definition strange_inc : val := λ: "p",
  let: "q" := ref #() in
  "p" <- #1 + !"p" ;; !"q".

Lemma strange_inc_spec1 `{heapG Σ} l (x : Z) :
  l  #x - WP strange_inc #l {{ v,  v = #()   l  #(1 + x) }}.
Proof.
  iIntros "?". wp_let. wp_alloc k. wp_let.
  wp_load. wp_op. wp_store. wp_load. auto.
Qed.

Definition strange_inc_twice : val := λ: "p",
  strange_inc "p";;
  strange_inc "p".

Lemma strange_inc_twice_spec1 `{heapG Σ} l (x : Z) :
  l  #x -
  WP strange_inc_twice #l {{ v,  v = #()   l  #(2 + x) }}.
Proof.
  iIntros "Hl". wp_let. wp_bind (strange_inc _).
  (* now what? *)
Abort.

Lemma strange_inc_spec2 `{heapG Σ} Φ l (x : Z) :
  l  #x -
  (l  #(1 + x) - Φ #()) -
  WP strange_inc #l {{ Φ }}.
Proof.
  iIntros "Hl Post". wp_let. wp_alloc k. wp_let.
  wp_load. wp_op. wp_store. wp_load. by iApply "Post".
Qed.

Lemma strange_inc_spec `{heapG Σ} l (x : Z) :
  {{{ l  #x }}} strange_inc #l {{{ RET #(); l  #(1 + x) }}}.
Proof.
  iIntros (Φ) "? Post". wp_let. wp_alloc k. wp_let.
  wp_load. wp_op. wp_store. wp_load. by iApply "Post".
Qed.

Lemma strange_inc_twice_spec2 `{heapG Σ} l (x : Z) :
  l  #x -
  WP strange_inc_twice #l {{ v,  v = #()   l  #(2 + x) }}.
Proof.
  iIntros "Hl". wp_let.
  wp_apply (strange_inc_spec with "Hl"); iIntros "Hl"; wp_seq.
  wp_apply (strange_inc_spec with "Hl"); iIntros "Hl".
  rewrite (_ : 2 + x = 1 + (1 + x)); last lia. auto.
Qed.

Lemma strange_inc_twice_spec `{heapG Σ} l (x : Z) :
  {{{ l  #x }}} strange_inc_twice #l {{{ RET #(); l  #(2 + x) }}}.
Proof.
  iIntros (Φ) "Hl Post". wp_let.
  wp_apply (strange_inc_spec with "Hl"); iIntros "Hl"; wp_seq.
  wp_apply (strange_inc_spec with "Hl"); iIntros "Hl".
  iApply "Post". rewrite (_ : 2 + x = 1 + (1 + x)); last lia. done.
Qed.