Library Scat.Examples
Require Import Conditions.
Require Import NaiveAbstractionLib.
Require Import LoopsUnrolling.
Require Import BasicExamples.
Require Import NaiveGuardAbstractions.
Require Import Kernel.
Source of the example
Let source : prog :=
ensure (1 ≤ x ∧ x ≤ 10) -;
ifc (x ≤ 5) then
assign y (x+5)
else
assign y (x-5)
fi -;
assign r (x×y) -;
require (6 ≤ r ∧ r ≤ 50) -;
assign r (r+x+y) -;
require (13 ≤ r ∧ r ≤ 65).
Let label := mkjoinlabel 1%positive.
Let convexhull :=
-5 ≤ x-y ∧ x-y ≤ 5
∧ 7 ≤ x+y ∧ x+y ≤ 15
∧ x+y+5 ≤ r×2 ∧ r×2 ≤ x×5 + y×5 + 25
∧ x+y×5-25 ≤ r ∧ r ≤ x×7 + y×3 - 15.
Open Scope certif_scope.
ensure (1 ≤ x ∧ x ≤ 10) -;
ifc (x ≤ 5) then
assign y (x+5)
else
assign y (x-5)
fi -;
assign r (x×y) -;
require (6 ≤ r ∧ r ≤ 50) -;
assign r (r+x+y) -;
require (13 ≤ r ∧ r ≤ 65).
Let label := mkjoinlabel 1%positive.
Let convexhull :=
-5 ≤ x-y ∧ x-y ≤ 5
∧ 7 ≤ x+y ∧ x+y ≤ 15
∧ x+y+5 ≤ r×2 ∧ r×2 ≤ x×5 + y×5 + 25
∧ x+y×5-25 ≤ r ∧ r ≤ x×7 + y×3 - 15.
Open Scope certif_scope.
Certificate of the example
Let annotated : certif :=
ensure (1 ≤ x ∧ x ≤ 10) -;
joinchseq
(ensure (x ≤ 5) -; assign y (x+5))
(abs_ensure (not_LE x 5) -; assign y (x-5))
label
(abs_assign r (ht_branch (mult_pos_interv x y) label (fun v ⇒ match v with 0 ⇒ (6,10) | _ ⇒ (1,5) end)))
convexhull -;
require (6 ≤ r ∧ r ≤ 50) -;
assign r (r+x+y) -;
require (13 ≤ r ∧ r ≤ 65).
ensure (1 ≤ x ∧ x ≤ 10) -;
joinchseq
(ensure (x ≤ 5) -; assign y (x+5))
(abs_ensure (not_LE x 5) -; assign y (x-5))
label
(abs_assign r (ht_branch (mult_pos_interv x y) label (fun v ⇒ match v with 0 ⇒ (6,10) | _ ⇒ (1,5) end)))
convexhull -;
require (6 ≤ r ∧ r ≤ 50) -;
assign r (r+x+y) -;
require (13 ≤ r ∧ r ≤ 65).
Computes the VCs
Proof of source safety
Goal is_ok source.
Proof.
apply vcg_correctness with (cert:=annotated).
vm_compute; auto.
simplify_vc_eval; try omega.
Qed.
Close Scope certif_scope.
End RunningExample.
Proof.
apply vcg_correctness with (cert:=annotated).
vm_compute; auto.
simplify_vc_eval; try omega.
Qed.
Close Scope certif_scope.
End RunningExample.
Section JoinseqUnrollInvariant.
Let x := "x"!1.
Let y := "y"!2.
Let i := "i"!3.
Let r := "r"!4.
Let source : prog :=
ensure (x ≤ 10) -;
ifc (x ≤ 5) then
assign y (x+5)
else
assign y (x-5)
fi -;
assign i 0 -;
assign r 0 -;
while i ≤ x-1 do
assign i (i+1) -;
assign r (r+y)
done -;
require (0 ≤ r ∧ r ≤ 50).
Let label := mkjoinlabel 1%positive.
Open Scope certif_scope.
Let approx_convexhull :=
-5 ≤ x-y ∧ x-y ≤ 5
∧ x+y ≤ 15
∧ 0 ≤ r ∧ r ≤ 50.
Let annotated : certif :=
ensure (x ≤ 10) -;
joinchseq
(ensure (x ≤ 5) -; assign y (x+5))
(abs_ensure (not_LE x 5) -; assign y (x-5))
label
(assign i 0 -;
assign r 0 -;
bloop
ensure (i ≤ x-1) -;
assign i (i+1) -;
assign r (r+y)
fwd 1
invariant (i ≤ x ∧ 0 ≤ r & inv label & branch label (fun v ⇒ match v with 0 ⇒ r ≤ i×10 | _ ⇒ r ≤ i×5 end))
then (abs_ensure (not_LE i (x-1)))
done)
approx_convexhull -;
require (0 ≤ r ∧ r ≤ 50).
Goal is_ok source.
Proof.
apply vcg_correctness with (cert:=annotated).
vm_compute; auto.
simplify_vc_eval; try omega.
Qed.
Close Scope certif_scope.
End JoinseqUnrollInvariant.
Let x := "x"!1.
Let y := "y"!2.
Let i := "i"!3.
Let r := "r"!4.
Let source : prog :=
ensure (x ≤ 10) -;
ifc (x ≤ 5) then
assign y (x+5)
else
assign y (x-5)
fi -;
assign i 0 -;
assign r 0 -;
while i ≤ x-1 do
assign i (i+1) -;
assign r (r+y)
done -;
require (0 ≤ r ∧ r ≤ 50).
Let label := mkjoinlabel 1%positive.
Open Scope certif_scope.
Let approx_convexhull :=
-5 ≤ x-y ∧ x-y ≤ 5
∧ x+y ≤ 15
∧ 0 ≤ r ∧ r ≤ 50.
Let annotated : certif :=
ensure (x ≤ 10) -;
joinchseq
(ensure (x ≤ 5) -; assign y (x+5))
(abs_ensure (not_LE x 5) -; assign y (x-5))
label
(assign i 0 -;
assign r 0 -;
bloop
ensure (i ≤ x-1) -;
assign i (i+1) -;
assign r (r+y)
fwd 1
invariant (i ≤ x ∧ 0 ≤ r & inv label & branch label (fun v ⇒ match v with 0 ⇒ r ≤ i×10 | _ ⇒ r ≤ i×5 end))
then (abs_ensure (not_LE i (x-1)))
done)
approx_convexhull -;
require (0 ≤ r ∧ r ≤ 50).
Goal is_ok source.
Proof.
apply vcg_correctness with (cert:=annotated).
vm_compute; auto.
simplify_vc_eval; try omega.
Qed.
Close Scope certif_scope.
End JoinseqUnrollInvariant.
Section MinetBarycentreExample.
Let x := "x"!1.
Let y := "y"!2.
Let z := "z"!3.
Let r := "r"!4.
Let source : prog :=
ensure (1 ≤ x ∧ x ≤ 5 ∧ 1 ≤ y ∧ y ≤ 3 ∧ 1 ≤ z ∧ z ≤ 3) -;
assign r (y×x + z*(0 - x) + z×5) -;
require (1 ≤ r ∧ r ≤ 27).
Open Scope certif_scope.
Let annotated : certif :=
ensure (1 ≤ x ∧ x ≤ 5 ∧ 1 ≤ y ∧ y ≤ 3 ∧ 1 ≤ z ∧ z ≤ 3) -;
abs_assign r
(let_term y := mult_pos_interv y x (1,5) in
let_term r := mult_pos_interv z (0-x) (-5,-1) in
y+r+z×5) -;
require (1 ≤ r ∧ r ≤ 27).
Eval vm_compute in abstract annotated.
Goal is_ok source.
Proof.
apply vcg_correctness with (cert:=annotated).
vm_compute; auto.
simplify_vc_eval; try omega.
Qed.
Close Scope certif_scope.
End MinetBarycentreExample.
Let x := "x"!1.
Let y := "y"!2.
Let z := "z"!3.
Let r := "r"!4.
Let source : prog :=
ensure (1 ≤ x ∧ x ≤ 5 ∧ 1 ≤ y ∧ y ≤ 3 ∧ 1 ≤ z ∧ z ≤ 3) -;
assign r (y×x + z*(0 - x) + z×5) -;
require (1 ≤ r ∧ r ≤ 27).
Open Scope certif_scope.
Let annotated : certif :=
ensure (1 ≤ x ∧ x ≤ 5 ∧ 1 ≤ y ∧ y ≤ 3 ∧ 1 ≤ z ∧ z ≤ 3) -;
abs_assign r
(let_term y := mult_pos_interv y x (1,5) in
let_term r := mult_pos_interv z (0-x) (-5,-1) in
y+r+z×5) -;
require (1 ≤ r ∧ r ≤ 27).
Eval vm_compute in abstract annotated.
Goal is_ok source.
Proof.
apply vcg_correctness with (cert:=annotated).
vm_compute; auto.
simplify_vc_eval; try omega.
Qed.
Close Scope certif_scope.
End MinetBarycentreExample.
Section MinetBarycentreExample2.
Let x := "x"!1.
Let y := "y"!2.
Let z := "z"!3.
Let r := "r"!4.
Let source : prog :=
ensure (1 ≤ x ∧ x ≤ 5 ∧ 1 ≤ y ∧ y ≤ 3 ∧ 1 ≤ z ∧ z ≤ 3) -;
assign r (y×x + z*(0 - x) + z×5) -;
require (5 ≤ r ∧ r ≤ 15).
Open Scope certif_scope.
Program Definition rewriting1: term_rewrite ((y - z)*x + z×5) :=
{|
rwin := y×x + z*(0 - x) + z*5 ;
rwproof := _
|}.
Obligation 1.
zof_ring_rewrite.
Qed.
Let label := mkjoinlabel 1%positive.
Let annotated : certif :=
ensure (1 ≤ x ∧ x ≤ 5 ∧ 1 ≤ y ∧ y ≤ 3 ∧ 1 ≤ z ∧ z ≤ 3) -;
(casescmp 0 (y-z) label
(abs_assign r
(abs_rewrite
(let_term x := (htb2 label (fun b ⇒
if b then
mult_pos_interv (y-z) x (1,5)
else
mult_neg_interv (y-z) x (1,5)
)) in
x+z×5)
rewriting1))) -;
require (5 ≤ r ∧ r ≤ 15).
Eval vm_compute in vcg annotated.
Goal is_ok source.
Proof.
apply vcg_correctness with (cert:=annotated).
vm_compute; auto.
simplify_vc_eval; try omega.
Qed.
Close Scope certif_scope.
End MinetBarycentreExample2.
Let x := "x"!1.
Let y := "y"!2.
Let z := "z"!3.
Let r := "r"!4.
Let source : prog :=
ensure (1 ≤ x ∧ x ≤ 5 ∧ 1 ≤ y ∧ y ≤ 3 ∧ 1 ≤ z ∧ z ≤ 3) -;
assign r (y×x + z*(0 - x) + z×5) -;
require (5 ≤ r ∧ r ≤ 15).
Open Scope certif_scope.
Program Definition rewriting1: term_rewrite ((y - z)*x + z×5) :=
{|
rwin := y×x + z*(0 - x) + z*5 ;
rwproof := _
|}.
Obligation 1.
zof_ring_rewrite.
Qed.
Let label := mkjoinlabel 1%positive.
Let annotated : certif :=
ensure (1 ≤ x ∧ x ≤ 5 ∧ 1 ≤ y ∧ y ≤ 3 ∧ 1 ≤ z ∧ z ≤ 3) -;
(casescmp 0 (y-z) label
(abs_assign r
(abs_rewrite
(let_term x := (htb2 label (fun b ⇒
if b then
mult_pos_interv (y-z) x (1,5)
else
mult_neg_interv (y-z) x (1,5)
)) in
x+z×5)
rewriting1))) -;
require (5 ≤ r ∧ r ≤ 15).
Eval vm_compute in vcg annotated.
Goal is_ok source.
Proof.
apply vcg_correctness with (cert:=annotated).
vm_compute; auto.
simplify_vc_eval; try omega.
Qed.
Close Scope certif_scope.
End MinetBarycentreExample2.
Section MauborgneRival_LinearInterpolation.
Notation "'#tc'" := (ctefun 1).
Notation "'#tx'" := (ctefun 2).
Notation "'#ty'" := (ctefun 3).
Coercion vcte: Z >-> Value.value.
Hypothesis tc_0: #tc 0 =0.
Hypothesis tc_1: #tc 1 =3.
Hypothesis tc_2: #tc 2 =6.
Hypothesis tc_3: #tc 3 =0.
Hypothesis tx_1: #tx 1 =-1.
Hypothesis tx_2: #tx 2 =1.
Hypothesis tx_3: #tx 3 =3.
Hypothesis ty_0: #ty 0 =-6.
Hypothesis ty_1: #ty 1 =-6.
Hypothesis ty_2: #ty 2 =-0.
Hypothesis ty_3: #ty 3 =12.
Hint Rewrite tc_0 tc_1 tc_2 tc_3 tx_1 tx_2 tx_3 ty_0 ty_1 ty_2 ty_3: ctefun.
Let tc := "tc"!1.
Let tx := "tx"!2.
Let ty := "ty"!3.
Coercion tapp: var >-> Funclass.
Let x := "x"!1.
Let y := "y"!2.
Let i := "i"!3.
Let source : prog :=
assign i 0 -;
while (i ≤ 2 ∧ tx(i+1) + 1 ≤ x) do
assign i (i+1)
done -;
assign y ((tc i)*(x-(tx i))+(ty i)) -;
require (-6 ≤ y ∧ y ≤ 12).
Open Scope certif_scope.
Let label := mklabel 0 4 1%positive.
Let annotated : certif :=
assign i 0 -;
bloop
split label
ensure (i ≤ 2 ∧ tx(i+1) + 1 ≤ x) -;
assign i (i+1)
all 3
then
abs_ensure (abs_not ((i ≤ 2 ∧ tx(i+1) + 1 ≤ x))) -;
abs_assign y (let_term x := ht_branch (mult_left_cte (tc i) (x-(tx i))) label (fun z ⇒ (match z with | 1 ⇒ 3 | 2 ⇒ 6 | _ ⇒ 0 end))
in x+(ty i))
done -;
require (-6 ≤ y ∧ y ≤ 12).
Eval vm_compute in abstract (abs_ensure (abs_not ((i ≤ 2 ∧ tx(i+1) + 1 ≤ x)))).
Eval vm_compute in vcg annotated.
Ltac simplify_ctefun :=
try (rewrite (ctefun_Zof 1) in × |- *);
try (rewrite (ctefun_Zof 2) in × |- *);
try (rewrite (ctefun_Zof 3) in × |- *);
autorewrite with zof_value in × |- *; simpl in × |- × ;
autorewrite with ctefun in × |- *;
autorewrite with zof_value in × |- *;simpl in × |- ×.
Goal is_ok source.
Proof.
apply vcg_correctness with (cert:=annotated).
vm_compute; auto.
simplify_vc_eval; try (simplify_ctefun; omega).
Qed.
Close Scope certif_scope.
End MauborgneRival_LinearInterpolation.
Notation "'#tc'" := (ctefun 1).
Notation "'#tx'" := (ctefun 2).
Notation "'#ty'" := (ctefun 3).
Coercion vcte: Z >-> Value.value.
Hypothesis tc_0: #tc 0 =0.
Hypothesis tc_1: #tc 1 =3.
Hypothesis tc_2: #tc 2 =6.
Hypothesis tc_3: #tc 3 =0.
Hypothesis tx_1: #tx 1 =-1.
Hypothesis tx_2: #tx 2 =1.
Hypothesis tx_3: #tx 3 =3.
Hypothesis ty_0: #ty 0 =-6.
Hypothesis ty_1: #ty 1 =-6.
Hypothesis ty_2: #ty 2 =-0.
Hypothesis ty_3: #ty 3 =12.
Hint Rewrite tc_0 tc_1 tc_2 tc_3 tx_1 tx_2 tx_3 ty_0 ty_1 ty_2 ty_3: ctefun.
Let tc := "tc"!1.
Let tx := "tx"!2.
Let ty := "ty"!3.
Coercion tapp: var >-> Funclass.
Let x := "x"!1.
Let y := "y"!2.
Let i := "i"!3.
Let source : prog :=
assign i 0 -;
while (i ≤ 2 ∧ tx(i+1) + 1 ≤ x) do
assign i (i+1)
done -;
assign y ((tc i)*(x-(tx i))+(ty i)) -;
require (-6 ≤ y ∧ y ≤ 12).
Open Scope certif_scope.
Let label := mklabel 0 4 1%positive.
Let annotated : certif :=
assign i 0 -;
bloop
split label
ensure (i ≤ 2 ∧ tx(i+1) + 1 ≤ x) -;
assign i (i+1)
all 3
then
abs_ensure (abs_not ((i ≤ 2 ∧ tx(i+1) + 1 ≤ x))) -;
abs_assign y (let_term x := ht_branch (mult_left_cte (tc i) (x-(tx i))) label (fun z ⇒ (match z with | 1 ⇒ 3 | 2 ⇒ 6 | _ ⇒ 0 end))
in x+(ty i))
done -;
require (-6 ≤ y ∧ y ≤ 12).
Eval vm_compute in abstract (abs_ensure (abs_not ((i ≤ 2 ∧ tx(i+1) + 1 ≤ x)))).
Eval vm_compute in vcg annotated.
Ltac simplify_ctefun :=
try (rewrite (ctefun_Zof 1) in × |- *);
try (rewrite (ctefun_Zof 2) in × |- *);
try (rewrite (ctefun_Zof 3) in × |- *);
autorewrite with zof_value in × |- *; simpl in × |- × ;
autorewrite with ctefun in × |- *;
autorewrite with zof_value in × |- *;simpl in × |- ×.
Goal is_ok source.
Proof.
apply vcg_correctness with (cert:=annotated).
vm_compute; auto.
simplify_vc_eval; try (simplify_ctefun; omega).
Qed.
Close Scope certif_scope.
End MauborgneRival_LinearInterpolation.
Section MauborgneRival_Barycentre.
Let x := "x"!1.
Let y := "y"!2.
Let r := "r"!3.
Let source : prog :=
ensure (-10 ≤ x ∧ x ≤ 10) -;
bloop
guassign [r;y] (0 ≤ r ∧ r ≤ 5 ∧ -10 ≤ y ∧ y ≤ 10) -;
assign x ((x×r + y) / (r+1))
done -;
require (-10 ≤ x ∧ x ≤ 10).
Open Scope certif_scope.
Let label := mklabel 0 5 1%positive.
Let annotated : certif :=
ensure (-10 ≤ x ∧ x ≤ 10) -;
bloop
guassign [r;y] (0 ≤ r ∧ r ≤ 5 ∧ -10 ≤ y ∧ y ≤ 10) -;
explore r 0 5 label (
abs_assign x (let_term x := ht_branch (mult_right_cte x r) label (fun cr ⇒ cr) in
ht_branch (Zdiv_by_pos_cte (x+y) (r+1)) label Zsucc))
invariant -10 ≤ x ∧ x ≤ 10
done -;
require (-10 ≤ x ∧ x ≤ 10).
Goal is_ok source.
Proof.
apply vcg_correctness with (cert:=annotated).
vm_compute; auto.
simplify_vc_eval; try omega.
Qed.
Close Scope certif_scope.
End MauborgneRival_Barycentre.
Let x := "x"!1.
Let y := "y"!2.
Let r := "r"!3.
Let source : prog :=
ensure (-10 ≤ x ∧ x ≤ 10) -;
bloop
guassign [r;y] (0 ≤ r ∧ r ≤ 5 ∧ -10 ≤ y ∧ y ≤ 10) -;
assign x ((x×r + y) / (r+1))
done -;
require (-10 ≤ x ∧ x ≤ 10).
Open Scope certif_scope.
Let label := mklabel 0 5 1%positive.
Let annotated : certif :=
ensure (-10 ≤ x ∧ x ≤ 10) -;
bloop
guassign [r;y] (0 ≤ r ∧ r ≤ 5 ∧ -10 ≤ y ∧ y ≤ 10) -;
explore r 0 5 label (
abs_assign x (let_term x := ht_branch (mult_right_cte x r) label (fun cr ⇒ cr) in
ht_branch (Zdiv_by_pos_cte (x+y) (r+1)) label Zsucc))
invariant -10 ≤ x ∧ x ≤ 10
done -;
require (-10 ≤ x ∧ x ≤ 10).
Goal is_ok source.
Proof.
apply vcg_correctness with (cert:=annotated).
vm_compute; auto.
simplify_vc_eval; try omega.
Qed.
Close Scope certif_scope.
End MauborgneRival_Barycentre.