Commit 64f63272 authored by Robbert's avatar Robbert

Merge branch 'heap_lang_lib' into 'master'

Add some trivial but useful heaplang libraries.

See merge request !291
parents 6c620a09 3f9e2ea5
Pipeline #18947 passed with stage
in 14 minutes and 21 seconds
......@@ -116,6 +116,8 @@ theories/heap_lang/lib/clairvoyant_coin.v
theories/heap_lang/lib/counter.v
theories/heap_lang/lib/atomic_heap.v
theories/heap_lang/lib/increment.v
theories/heap_lang/lib/diverge.v
theories/heap_lang/lib/arith.v
theories/proofmode/base.v
theories/proofmode/tokens.v
theories/proofmode/coq_tactics.v
......
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
(** A library defining binary [minimum] and [maximum] functions, together with
their expected specs. These operations come up often when working manipulating
array indices (checking for bounds). *)
Definition minimum : val :=
λ: "m" "n", if: "m" < "n" then "m" else "n".
Definition maximum : val :=
λ: "m" "n", if: "m" < "n" then "n" else "m".
Lemma minimum_spec `{!heapG Σ} s E (Φ : val iProp Σ) (m n : Z) :
Φ #(m `min` n) -
WP minimum #m #n @ s;E {{ Φ }}.
Proof.
iIntros "HΦ". wp_lam. wp_pures. case_bool_decide; wp_pures.
- rewrite Z.min_l; [ done | by lia ].
- rewrite Z.min_r; [ done | by lia ].
Qed.
Lemma minimum_spec_nat `{!heapG Σ} s E (Φ : val iProp Σ) (m n : nat) :
Φ #(m `min` n)%nat -
WP minimum #m #n @ s;E {{ Φ }}.
Proof. iIntros "HΦ". iApply minimum_spec. by rewrite Nat2Z.inj_min. Qed.
Lemma maximum_spec `{!heapG Σ} s E (Φ : val iProp Σ) (m n : Z) :
Φ #(m `max` n) -
WP maximum #m #n @ s;E {{ Φ }}.
Proof.
iIntros "HΦ". wp_lam. wp_pures. case_bool_decide; wp_pures.
- rewrite Z.max_r; [ done | by lia ].
- rewrite Z.max_l; [ done | by lia ].
Qed.
Lemma maximum_spec_nat `{!heapG Σ} s E (Φ : val iProp Σ) (m n : nat) :
Φ #(m `max` n)%nat -
WP maximum #m #n @ s;E {{ Φ }}.
Proof. iIntros "HΦ". iApply maximum_spec. by rewrite Nat2Z.inj_max. Qed.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
(** This library provides a [diverge] function that goes into an infinite loop
when provided with an (arbitrary) argument value. This function can be used to
let the program diverge in corner cases that one wants to omit in proofs. This
mechanism should be used with care and communicated clearly, obviously.
Note that this mechanism only works when establishing partial correctness with
the ordinary version of weakest preconditions, and not when establishing total
correctness using the total version of weakest preconditions.
A typical application for [diverge] is insertion functions for data structures
having a fixed capacity. In such cases, we can choose divergence instead of an
explicit error handling when the full capacity has already been reached. *)
Definition diverge : val :=
rec: "diverge" "v" := "diverge" "v".
Lemma wp_diverge `{!heapG Σ} s E (Φ : val iProp Σ) (v : val) :
WP diverge v @ s;E {{ Φ }}%I.
Proof.
iLöb as "IH". wp_lam. iApply "IH".
Qed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment