Inc.v

From Coq Require Import Bool.Bool.
From Coq Require Import Arith.Arith.
From Coq Require Import Arith.EqNat.
From Coq Require Import Arith.PeanoNat. Import Nat.
From Coq Require Import Lia.
Require Export Coq.Strings.String.
From Coq Require Import Logic.FunctionalExtensionality.
From Coq Require Import Lists.List.
Import ListNotations.

(*
  Link to the paper: http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/IncorrectnessLogic.pdf
  Inferences rules are page 8.
*)


(* Total map definitions and lemma ********************************************)

Definition total_map (A : Type) := string -> A.

Definition t_empty {A : Type} (v : A) : total_map A :=
  (fun _ => v).

Notation "'_' '!->' v" := (t_empty v)
  (at level 100, right associativity).

Definition t_update {A : Type} (m : total_map A)
                    (x : string) (v : A) :=
  fun x' => if String.eqb x x' then v else m x'.


Notation "x '!->' v ';' m" := (t_update m x v)
                              (at level 100, v at next level, right associativity).

Lemma t_update_eq : forall (A : Type) (m : total_map A) x v,
  (x !-> v ; m) x = v.
Proof.
    Admitted.

Lemma t_update_shadow : forall (A : Type) (m : total_map A) x v1 v2,
  (x !-> v2 ; x !-> v1 ; m) = (x !-> v2 ; m).
Proof.
  Admitted.

Theorem t_update_same : forall (A : Type) (m : total_map A) x,
  (x !-> m x ; m) = m.
Proof.
    Admitted.

(* Incorrectness Logic ********************************************)



Inductive aexp : Type :=
  | AAny
  | ANum (n : nat)
  | AId (x : string)
  | APlus (a1 a2 : aexp)
.

Inductive bexp : Type :=
  | BTrue
  | BFalse
  | BEq (a1 a2 : aexp)
  | BNot (b : bexp)
.

Inductive com : Type :=
  | Asign: string -> aexp -> com
.

Coercion AId : string >-> aexp.

Coercion ANum : nat >-> aexp.

Declare Custom Entry com.
Declare Scope com_scope.
Notation "<{ e }>" := e (at level 0, e custom com at level 99) : com_scope.
Notation "( x )" := x (in custom com, x at level 99) : com_scope.
Notation "x" := x (in custom com at level 0, x constr at level 0) : com_scope.
Notation "f x .. y" := (.. (f x) .. y)
                  (in custom com at level 0, only parsing,
                  f constr at level 0, x constr at level 9,
                  y constr at level 9) : com_scope.
Notation "x + y" := (APlus x y) (in custom com at level 50, left associativity).
Notation "'true'" := true (at level 1).
Notation "'true'" := BTrue (in custom com at level 0).
Notation "'false'" := false (at level 1).
Notation "'false'" := BFalse (in custom com at level 0).
Notation "x = y" := (BEq x y) (in custom com at level 70, no associativity).
Notation "'~' b" := (BNot b) (in custom com at level 75, right associativity).
Open Scope com_scope.



Definition state := total_map nat.

(* witch to aevalR *)
Fixpoint aeval (st : state) (a : aexp) : nat :=
  match a with
  | AAny => 2
  | ANum n => n
  | AId x => st x
  | <{a1 + a2}> => (aeval st a1) + (aeval st a2)
  end.

Fixpoint beval (st : state) (b : bexp): bool :=
  match b with
  | BTrue => true
  | BFalse => false
  | BEq a1 a2 => (aeval st a1) =? (aeval st a2)
  | BNot b1 => negb (beval st b1)
  end.


Notation "x := y" :=
         (Asign x y)
            (in custom com at level 0, x constr at level 0,
             y at level 85, no associativity) : com_scope.

Definition Assertion := state -> Prop.

Definition Aexp : Type := state -> nat.
Definition assert_of_Prop (P : Prop) : Assertion := fun _ => P.
Definition Aexp_of_nat (n : nat) : Aexp := fun _ => n.
Definition Aexp_of_aexp (a : aexp) : Aexp := fun st => aeval st a.

(* Sortclass, the class of sorts; its objects are the terms whose type is a sort (e.g. Prop or Type).  *)
Coercion assert_of_Prop : Sortclass >-> Assertion.
Coercion Aexp_of_nat : nat >-> Aexp.
Coercion Aexp_of_aexp : aexp >-> Aexp.

Arguments assert_of_Prop /.
Arguments Aexp_of_nat /.
Arguments Aexp_of_aexp /.
Add Printing Coercion Aexp_of_nat Aexp_of_aexp assert_of_Prop.

Declare Scope assertion_scope.
Bind Scope assertion_scope with Assertion.
Bind Scope assertion_scope with Aexp.
Delimit Scope assertion_scope with assertion.
Notation assertion P := (P%assertion : Assertion).
Notation mkAexp a := (a%assertion : Aexp).
Notation "~ P" := (fun st => ~ assertion P st) : assertion_scope.
Notation "P /\ Q" := (fun st => assertion P st /\  assertion Q st) : assertion_scope.
Notation "P \/ Q" := (fun st => assertion P st \/ assertion Q st) : assertion_scope.
Notation "P -> Q" := (fun st => assertion P st -> assertion Q st) : assertion_scope.
Notation "P <-> Q" := (fun st => assertion P st <-> assertion Q st) : assertion_scope.
Notation "a = b" := (fun st => mkAexp a st = mkAexp b st) : assertion_scope.
Notation "a + b" := (fun st => mkAexp a st + mkAexp b st) : assertion_scope.

Declare Scope inclogic_spec_scope.

Open Scope inclogic_spec_scope.

Reserved Notation
         "st '=[' c ']=>' ϵ ':' st'"
         (at level 40, c custom com at level 99,
          st constr, ϵ constr at next level).


(*
  Command evaluation raise ok if the evaluation is a success, otherwise raise a signal err.
  For the gist I only provide Asgn but we can imagine a command `assert B;`
*)

Inductive Signal: Type := 
| ok
| err.


(* Definition of commands evaluation *)

Inductive ceval : com -> state -> Signal -> state -> Prop :=
| E_Asgn : forall st a n x,
  aeval st a = n ->
  st =[ x := a ]=> ok : (x !-> n ; st)
where "st =[ c ]=> ϵ : st'" := (ceval c st ϵ st').

Local Hint Constructors ceval : core.


(*
  Definition of Incorrectness triple [P] c [signal ↑ Q].
  This triple says that the post-assertion Q be an under-approximation (subset)
  of the final states that can be reached starting from states satisfying the presumption.

  Inversely, hoare triple {P} c {Q} say that the post-condition Q over-approximate the states
  reachable upon termination when the code is executed from states satisfying the pre-condition P.
*)
Definition Inc_triple
           (P : Assertion) (c : com) (s: Signal) (Q: Assertion): Prop :=
    forall st',
    Q st' ->
    exists st,
    st =[ c ]=> s : st' /\ P st.

Notation "[[ P ]] c [[ ϵ ↑ Q ]]" :=
  (Inc_triple P c ϵ Q) (at level 90, c custom com at level 99): inclogic_spec_scope.    

Notation "[[ P ]] c [[ ok ↑ Q ]] [[ err ↑ R ]] " :=
  ([[ P ]] c [[ ok ↑ Q ]] /\ [[ P ]] c [[ err ↑ R ]]) (at level 90, c custom com at level 99): inclogic_spec_scope.


(*
  My incorectness logic implementation could be described as "model-theoretic":
  the proof rules for each of the sequent rule in the paper are presented as theorems
  about the evaluation behavior of programs, and proofs of program correctness
  (validity of Incorrectness triples) are constructed by combining these theorems.
*)


(**
 --------------------  (Empty under-approximates)
      [[p]] C [[ϵ: false]]
*)
Theorem Empty_under_approximates: forall P c ε, [[ P ]] c [[ ε ↑ False ]].
Proof.
  intros P c ε st' HFalse.
  contradiction.
Qed.

Definition assn_sub X a (P:Assertion) : Assertion :=
  fun (st : state) =>
    P (X !-> aeval st a ; st).

Notation "P [ X |-> a ]" := (assn_sub X a P)
  (at level 10, X at next level, a custom com) : inclogic_spec_scope.

(* 
  I am stuck in the proof of the assignment rule proposed in the paper.

  Incorrectness logic uses Floyd’s forward-running assignment axiom (see Figure 3)
  rather than Hoare’s backwards-running one. The Incorrectness logic cannot use Hoare's
  backward version because it is unsound here (more page 9).

  The Hoare backwards is the sequent:

  ---------------------------- (hoare_asgn)
  {{Q [X ⊢> a]}} X := a {{Q}}

  where the forward version is:

  -------------------------------- (hoare_asgn_forward)
  {{ P }}
  X := a
  {{ exists m, P[X ⊢> m] /\ X = a[X ⊢> m] }}


  The assign rule proposed in the paper is similar to hoare_asgn_forward rule.

  -------------------------------------------------- (Assignment)
  [p]x = e[ok: ∃x′.p[x′/x] ∧ x = e[x′/x]][er: false]
*)
Theorem inc_asgn : forall X P a,
  [[ fun st' => P st' ]]
    X := a
  [[ ok ↑ fun st => exists m, P (X !-> m ; st) /\ st X = aeval (X !-> m; st) a ]] [[ err ↑ False ]].
Proof.
  intros X p a.
  split.
  - admit. (* I am stuck here...*)
  - apply Empty_under_approximates.
Admitted.