Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Gaurav Parthasarathy
examples_rdcss_old
Commits
90225068
Commit
90225068
authored
Apr 30, 2018
by
Dan Frumin
Browse files
Bump Iris version
 Fix a file broken due to wp_binop changes
parent
6a6b8cad
Changes
2
Hide whitespace changes
Inline
Sidebyside
opam
View file @
90225068
...
...
@@ 9,6 +9,6 @@ build: [make "j%{jobs}%"]
install: [make "install"]
remove: ["rm" "rf" "%{lib}%/coq/usercontrib/iris_examples"]
depends: [
"coqiris" { (= "dev.20180
305.0
")  (= "dev") }
"coqiris" { (= "dev.20180
427.2.1ab890fc
")  (= "dev") }
"coqautosubst" { = "dev.coq86" }
]
theories/lecture_notes/recursion_through_the_store.v
View file @
90225068
...
...
@@ 11,9 +11,9 @@ From iris.program_logic Require Export weakestpre.
the lang file contains the actual language syntax. *)
From
iris
.
heap_lang
Require
Export
notation
lang
.
(* Files related to the interactive proof mode. The first import includes the
general tactics of the proof mode. The second provides some more specialized
tactics particular to the instantiation of Iris to a particular programming
(* Files related to the interactive proof mode. The first import includes the
general tactics of the proof mode. The second provides some more specialized
tactics particular to the instantiation of Iris to a particular programming
language. *)
From
iris
.
proofmode
Require
Export
tactics
.
From
iris
.
heap_lang
Require
Import
proofmode
.
...
...
@@ 23,7 +23,7 @@ From iris.heap_lang Require Import proofmode.
From
iris
.
base_logic
.
lib
Require
Export
invariants
.
(* The following line makes Coq check that we do not use any admitted facts /
(* The following line makes Coq check that we do not use any admitted facts /
additional assumptions not in the statement of the theorems being proved. *)
Set
Default
Proof
Using
"Type"
.
...
...
@@ 34,7 +34,7 @@ Section recursion_through_the_store.
instantiation of Iris. The particular, even the heap is handled in an
analogous way as other ghost state. This line states that we assume the
Iris instantiation has sufficient structure to manipulate the heap, e.g.,
it allows us to use the pointsto predicate. *)
it allows us to use the pointsto predicate. *)
Context
`
{!
heapG
Σ
}.
Implicit
Types
l
:
loc
.
...
...
@@ 42,16 +42,16 @@ Implicit Types l : loc.
(* This is the code for the recursion through the store operator *)
Definition
myrec
:
val
:
=
λ
:
"f"
,
λ
:
"f"
,
let
:
"r"
:
=
ref
(
λ
:
"x"
,
"x"
)
in
"r"
<
(
λ
:
"x"
,
"f"
(!
"r"
)
"x"
)
;;
!
"r"
.
!
"r"
.
(* Here is the specification for the recursion through the store function.
See the Iris Lecture Notes for an indepth discussion of both the specification and
(* Here is the specification for the recursion through the store function.
See the Iris Lecture Notes for an indepth discussion of both the specification and
the proof. *)
Lemma
myrec_spec
(
P
:
val
>
iProp
Σ
)
(
Q
:
val
>
val
>
iProp
Σ
)
(
F
v1
:
val
)
(
e_F
e_v
:
expr
)
`
{
HeF
:
!
IntoVal
e_F
F
}
`
{
Hev1
:
!
IntoVal
e_v
v1
}
:
`
{
HeF
:
!
IntoVal
e_F
F
}
`
{
Hev1
:
!
IntoVal
e_v
v1
}
:
{{{
(
∀
e_f
:
expr
,
∀
f
:
val
,
∀
v2
:
val
,
⌜
IntoVal
e_f
f
⌝

∗
{{{(
∀
v3
:
val
,
{{{
P
v3
}}}
e_f
v3
{{{
u
,
RET
u
;
Q
u
v3
}}})
∗
P
v2
}}}
...
...
@@ 89,11 +89,11 @@ Section factorial_client.
Context
`
{!
heapG
Σ
}.
Implicit
Types
l
:
loc
.
(* In this section we show how to specify and prove correctness of a
factorial fucntion implemented using our recursion through the
(* In this section we show how to specify and prove correctness of a
factorial fucntion implemented using our recursion through the
store function *)
(* Here is the mathematical factorial function and a few properties
(* Here is the mathematical factorial function and a few properties
related to that. *)
Fixpoint
factorial
(
n
:
nat
)
:
nat
:
=
match
n
with
...
...
@@ 117,7 +117,7 @@ Section factorial_client.
1
≤
x
→
fac_int
x
=
fac_int
(
x

1
)
*
x
.
Proof
.
intros
?.
rewrite
Z
.
mul_comm
.
rewrite
Z
.
mul_comm
.
rewrite
/
fac_int
.
assert
(
Z
.
to_nat
x
=
S
(
Z
.
to_nat
(
x

1
)))
as
Heq
.
{
transitivity
(
Z
.
to_nat
(
1
+
(
x

1
))).
...
...
@@ 125,11 +125,11 @@ Section factorial_client.

rewrite
Z2Nat
.
inj_add
;
first
auto
;
lia
.
}
rewrite
Heq
factorial_spec_S

Heq
Nat2Z
.
inj_mul
Z2Nat
.
id
//
;
lia
.
Qed
.
Qed
.
(* Now, for the code of the implementation of factorial *)
(* Here is code for a multiplication function, which we will use
(* Here is code for a multiplication function, which we will use
to implement factorial. *)
Definition
times
:
val
:
=
rec
:
"times"
"x"
"y"
:
=
...
...
@@ 140,20 +140,18 @@ Section factorial_client.
Proof
.
iL
ö
b
as
"IH"
.
iIntros
(
n
Φ
)
"ret"
.
destruct
(
decide
(
n
=
0
))
as
[>

?].

wp_lam
.
wp_lam
.
wp_binop
.
wp_if
.
iApply
"ret"
;
done
.

wp_lam
;
wp_lam
.
wp_binop
.
rewrite
bool_decide_false
;
last
auto
.
wp_if
.
wp_lam
.
wp_lam
.
wp_binop
.
case_bool_decide
;
simplify_eq
/=.

wp_if
.
iApply
"ret"
.

wp_if
.
wp_bind
(
_

_
)%
E
.
wp_binop
.
wp_bind
((
times
_
)
_
).
iApply
"IH"
;
iNext
.
wp_binop
.
wp_binop
;
first
by
replace
(
m
+
((
n

1
)
*
m
))
with
(
n
*
m
)
by
lia
.
Qed
.
Qed
.
Lemma
times_spec
(
n
m
:
Z
)
:
{{{
True
}}}
...
...
@@ 167,7 +165,7 @@ Section factorial_client.
Qed
.
(* Here is the implementation code for factorial, implemented using the recursion
(* Here is the implementation code for factorial, implemented using the recursion
through the store function *)
Definition
myfac
:
=
myrec
(
λ
:
"f"
,
...
...
@@ 177,10 +175,10 @@ Section factorial_client.
else
times
(
"f"
(
"n"

#
1
)
)
"n"
)%
E
.
(* Finally, here is the specification that our implementation of factorial
(* Finally, here is the specification that our implementation of factorial
really does implement the mathematical factorial function. *)
Lemma
myfac_spec
(
n
:
expr
)
(
n'
:
Z
)
:
IntoVal
n
#
n'
→
(
0
≤
n'
)
→
IntoVal
n
#
n'
→
(
0
≤
n'
)
→
{{{
True
}}}
myfac
n
{{{
v
,
RET
v
;
⌜
v
=
#(
fac_int
n'
)
⌝
}}}.
...
...
@@ 188,18 +186,19 @@ Section factorial_client.
iIntros
(
H
%
of_to_val
Hleq
Φ
)
"_ ret"
;
simplify_eq
.
iApply
(
myrec_spec
(
fun
v
=>
⌜
∃
m'
:
Z
,
0
≤
m'
∧
to_val
v
=
Some
#
m'
⌝
%
I
)
(
fun
u
=>
fun
v
=>
⌜
∃
m'
:
Z
,
to_val
v
=
Some
#
m'
∧
u
=
#(
fac_int
m'
)
⌝
%
I
)).

iSplit
.
iIntros
(
e_f
f
v
)
"%"
.
iAlways
.
iIntros
(
Φ
'
)
"spec_f ret"
.

iSplit
;
last
eauto
.
iIntros
(
e_f
f
v
)
"%"
.
iAlways
.
iIntros
(
Φ
'
)
"spec_f ret"
.
apply
of_to_val
in
a
as
<.
wp_lam
.
wp_lam
.
iDestruct
"spec_f"
as
"[spec_f %]"
.
destruct
H
as
[
m'
[
Hleqm'
Heq
%
of_to_val
]]
;
simplify_eq
.
destruct
(
decide
(
m'
=
0
))
as
[>

?].
+
wp_binop
.
wp_if
.
iApply
"ret"
.
iPureIntro
.
exists
0
;
done
.
+
wp_binop
.
rewrite
bool_decide_false
;
last
auto
.
wp_if
.
wp_binop
.
wp_bind
(
f
_
)%
E
.
wp_binop
.
case_bool_decide
;
simplify_eq
/=
;
wp_if
.
+
iApply
"ret"
.
iPureIntro
.
exists
0
;
done
.
+
assert
(
m'
≠
0
)
by
naive_solver
.
wp_binop
.
wp_bind
(
f
_
)%
E
.
iApply
(
"spec_f"
$!
(#(
m'

1
))).
*
iIntros
"!%"
.
exists
(
m'

1
)
;
split
;
first
lia
;
last
auto
.
*
iNext
.
iIntros
(
u
)
"**"
.
destruct
a
as
[
x
[
Heq
>]].
*
iNext
.
iIntros
(
u
)
"**"
.
destruct
a
as
[
x
[
Heq
>]].
iApply
times_spec
;
first
done
.
iNext
;
iIntros
(
u
)
"%"
;
subst
;
iApply
"ret"
.
iIntros
"!%"
.
...
...
@@ 207,8 +206,7 @@ Section factorial_client.
simpl
in
Heq
;
simplify_eq
.
split
;
first
auto
.
rewrite

fac_int_eq
;
first
auto
;
lia
.
+
iIntros
"!%"
.
by
exists
n'
.

iNext
.
iIntros
"**"
.
destruct
a
as
(?&[=]&>)
;
simplify_eq
.
by
iApply
"ret"
.

iNext
.
iIntros
"**"
.
destruct
a
as
(?&[=]&>)
;
simplify_eq
.
by
iApply
"ret"
.
Qed
.
End
factorial_client
.
\ No newline at end of file
End
factorial_client
.
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment