prf_counter.v

From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype.
From pcm Require Import options axioms prelude pred.
From pcm Require Import pcm unionmap heap.
From htt Require Import options interlude model heapauto.

(* counter that hides local state with an abstract predicate *)

Record cnt : Type :=
  Counter {inv : nat -> Pred heap;
           method : {v : nat}, STsep (inv v,
                                     [vfun (_ : unit) m => m \In inv v.+1])}.

Program Definition new : STsep (emp, [vfun y m => m \In inv y 0]) :=
  Do (x <-- alloc 0;
      ret (@Counter (fun v => [Pred h | h = x :-> v])
                    (Do (y <-- !x;
                         x ::= y.+1)))).
Next Obligation.
by move=>x [v][] _ /= ->; do 2!step.
Qed.
Next Obligation.
move=>[] _ /= ->.
apply/vrf_bind/vrf_alloc=>x; rewrite unitR=>_.
by step.
Qed.

Opaque new.

Program Definition foo : STsep (emp,
                               [vfun _ m => exists c, m \In inv c 3]) :=
  Do (cnt <-- new;
      method cnt;;
      method cnt;;
      method cnt).
Next Obligation.
move=>[] _ /= ->.
apply: [stepE]=>//= cnt m Hm.
apply: [stepE 0]=>//= _ {}m {}Hm.
apply: [stepE 1]=>//= _ {}m {}Hm.
apply: [gE 2]=>//= _ {}m {}Hm.
by exists cnt.
Qed.