RecordsReasoning about Records
Set Implicit Arguments.
From SLF Require Import LibSepReference LibSepTLCbuffer.
From SLF Require Import Arrays. Import Realization.
Implicit Types P : Prop.
Implicit Types H : hprop.
Implicit Types Q : val→hprop.
Implicit Type p q : loc.
Implicit Type k : nat.
Implicit Type i : int.
Implicit Type n z : nat.
Implicit Type v : val.
Implicit Type L : list val.
From SLF Require Import LibSepReference LibSepTLCbuffer.
From SLF Require Import Arrays. Import Realization.
Implicit Types P : Prop.
Implicit Types H : hprop.
Implicit Types Q : val→hprop.
Implicit Type p q : loc.
Implicit Type k : nat.
Implicit Type i : int.
Implicit Type n z : nat.
Implicit Type v : val.
Implicit Type L : list val.
First Pass
- a header at location p, storing the number of fields, that is, the value 2;
- a cell at location p+1, storing the contents of the head field,
- a cell at location p+2, storing the contents of the tail field.
Representation of Individual Records Fields
The predicate hfield p k v, written p`.k ~~> v, asserts that the field
k of the record p stores the value v. This predicate is presented as
an abstract predicate to the end user. Internally, it may be defined using
pointer arithmetic.
Definition hfield (p:loc) (k:field) (v:val) : hprop :=
(p+1+k)%nat ~~> v.
Global Opaque hfield.
Notation "p `. k '~~>' v" := (hfield p k v)
(at level 32, k at level 0, no associativity,
format "p `. k '~~>' v").
(p+1+k)%nat ~~> v.
Global Opaque hfield.
Notation "p `. k '~~>' v" := (hfield p k v)
(at level 32, k at level 0, no associativity,
format "p `. k '~~>' v").
To describe a list cell record, writing
(hheader 2 p) \* (p`.head ~~> x) \* (p`.tail ~~> q) is fairly verbose and
cumbersome to manipulate. To improve the situation, we introduce a generic
representation predicate for records. This predicate allows to describe the
same list cell much more concisely as p ~~~>`{ head := x; tail := q }.
It what follows, we show how to implement this notation by introducing the
heap predicates hfields and hrecords. These predicates will be used for
stating small-footprint specifications and large-footprint specifications
for record operations.
Representation of Fields
A record is described as a list of fields.
We let the meta-variable kvs denote such lists.
The heap predicate hfields kvs p asserts that, at location p, one finds
the representation of the fields described by the list kvs. The predicate
hfields kvs p is defined recursively on the list kvs. If kvs is empty,
the predicate describes the empty heap predicate. Otherwise, kvs
decomposes as a head (k,v) and a tail kvs'. The predicate p`.k ~~> v
describes the field at offset k, with contents v. The predicate
hfields kvs' p describes the remaining fields.
Fixpoint hfields (kvs:hrecord_fields) (p:loc) : hprop :=
match kvs with
| nil ⇒ \[]
| (k,v)::kvs' ⇒ (p`.k ~~> v) \* (hfields kvs' p)
end.
match kvs with
| nil ⇒ \[]
| (k,v)::kvs' ⇒ (p`.k ~~> v) \* (hfields kvs' p)
end.
A list cell with head field x and tail field q is represented by the
list (head,x)::(tail,q)::nil. To support the syntax
`{ head := x; tail := q }, we introduce the following notation. For
technical reasons associated with coercions, we need to separately define
notation for parsing, where a cast to the type val is included, from
notation for printing, where such a cast is not included.
Notation "`{ k1 := v1 }" :=
((k1,(v1:val))::nil)
(at level 0, k1 at level 0, only parsing).
Notation "`{ k1 := v1 ; k2 := v2 }" :=
((k1,(v1:val))::(k2,(v2:val))::nil)
(at level 0, k1, k2 at level 0, only parsing).
Notation "`{ k1 := v1 ; k2 := v2 ; k3 := v3 }" :=
((k1,(v1:val))::(k2,(v2:val))::(k3,(v3:val))::nil)
(at level 0, k1, k2, k3 at level 0, only parsing).
Notation "`{ k1 := v1 }" :=
((k1,v1)::nil)
(at level 0, k1 at level 0, only printing).
Notation "`{ k1 := v1 ; k2 := v2 }" :=
((k1,v1)::(k2,v2)::nil)
(at level 0, k1, k2 at level 0, only printing).
Notation "`{ k1 := v1 ; k2 := v2 ; k3 := v3 }" :=
((k1,v1)::(k2,v2)::(k3,v3)::nil)
(at level 0, k1, k2, k3 at level 0, only printing).
Open Scope val_scope.
((k1,(v1:val))::nil)
(at level 0, k1 at level 0, only parsing).
Notation "`{ k1 := v1 ; k2 := v2 }" :=
((k1,(v1:val))::(k2,(v2:val))::nil)
(at level 0, k1, k2 at level 0, only parsing).
Notation "`{ k1 := v1 ; k2 := v2 ; k3 := v3 }" :=
((k1,(v1:val))::(k2,(v2:val))::(k3,(v3:val))::nil)
(at level 0, k1, k2, k3 at level 0, only parsing).
Notation "`{ k1 := v1 }" :=
((k1,v1)::nil)
(at level 0, k1 at level 0, only printing).
Notation "`{ k1 := v1 ; k2 := v2 }" :=
((k1,v1)::(k2,v2)::nil)
(at level 0, k1, k2 at level 0, only printing).
Notation "`{ k1 := v1 ; k2 := v2 ; k3 := v3 }" :=
((k1,v1)::(k2,v2)::(k3,v3)::nil)
(at level 0, k1, k2, k3 at level 0, only printing).
Open Scope val_scope.
Representation of Records
Definition maps_all_fields (n:nat) (kvs:hrecord_fields) : Prop :=
LibList.map fst kvs = nat_seq 0 n.
LibList.map fst kvs = nat_seq 0 n.
The predicate hrecord kvs p exploits maps_all_fields n kvs to relate the
value nb stored in the header with the association list kvs that
describes the contents of the fields.
Definition hrecord (kvs:hrecord_fields) (p:loc) : hprop :=
\∃ n, hheader n p \* hfields kvs p \* \[maps_all_fields n kvs].
\∃ n, hheader n p \* hfields kvs p \* \[maps_all_fields n kvs].
We introduce the notation p ~~~> kvs for hrecord kvs p, allowing to
write, e.g., p ~~~>`{ head := x; tail := q }.
The following lemma may be used to convert a concrete hrecord predicate
into a hheader and a conjunction of hfield predicates. In the statement
below, LibListExec.length is a variant of LibList.length that computes
in Coq using simpl or reflexivity.
Lemma hrecord_elim : ∀ p kvs,
hrecord kvs p ==> hheader (LibListExec.length kvs) p \* hfields kvs p.
Proof using.
intros. unfold hrecord. xpull. intros z Hz. xsimpl. xsimpl.
rewrite LibListExec.length_eq. applys himpl_of_eq. fequal. gen Hz.
unfold maps_all_fields. generalize 0%nat. gen z.
induction kvs; intros; destruct z as [|z']; rew_listx in *; tryfalse.
{ math. } { inverts Hz. forwards*: IHkvs H1. math. }
Qed.
hrecord kvs p ==> hheader (LibListExec.length kvs) p \* hfields kvs p.
Proof using.
intros. unfold hrecord. xpull. intros z Hz. xsimpl. xsimpl.
rewrite LibListExec.length_eq. applys himpl_of_eq. fequal. gen Hz.
unfold maps_all_fields. generalize 0%nat. gen z.
induction kvs; intros; destruct z as [|z']; rew_listx in *; tryfalse.
{ math. } { inverts Hz. forwards*: IHkvs H1. math. }
Qed.
For example, let us show how to convert from
p ~~~> `{ head := x ; tail := q } to the conjunction of hheader 2 p and
p`.head ~~> x and p`.tail ~~> q.
Definition head : field := 0%nat.
Definition tail : field := 1%nat.
Lemma demo_hrecord_intro_elim : ∀ p x q,
p ~~~> `{ head := x ; tail := q } ==> \[].
Proof using. intros. xchange hrecord_elim; simpl. Abort.
Definition tail : field := 1%nat.
Lemma demo_hrecord_intro_elim : ∀ p x q,
p ~~~> `{ head := x ; tail := q } ==> \[].
Proof using. intros. xchange hrecord_elim; simpl. Abort.
Declare Scope trm_scope_ext.
The read operation is described by an expression of the form
val_get_field k p, where k denotes a field name, and where p denotes
the location of a record. Observe that k is not a program value of type
val, but a name for a natural number. The expression val_get_field has
type field → val, and for a given field k the expression
val_get_field k is a value, which may be applied in the program syntax to
a pointer p.
The read operation val_get_field k p is written p`.k.
Notation "t1 '`.' k" :=
(val_get_field k t1)
(in custom trm at level 56, k at level 0, format "t1 '`.' k" )
: trm_scope_ext.
(val_get_field k t1)
(in custom trm at level 56, k at level 0, format "t1 '`.' k" )
: trm_scope_ext.
The operation val_get_field k p can be specified at three levels.
First, its small-footprint specification operates at the level of a single
field, described by p`.k ~~> v. The specification is very similar to that
of val_get. The return value is exactly v.
Parameter triple_get_field : ∀ p k v,
triple (val_get_field k p)
(p`.k ~~> v)
(fun r ⇒ \[r = v] \* (p`.k ~~> v)).
triple (val_get_field k p)
(p`.k ~~> v)
(fun r ⇒ \[r = v] \* (p`.k ~~> v)).
Second, the read operation val_get_field can be specified with respect to
a list of fields, described in the form hfields kvs p. To that end, we
introduce a function called hfields_lookup for extracting the value v
associated with a field k in a list of record fields kvs. Note: the
operation hfields_lookup k kvs returns a result of type option val,
because we cannot presume that the field k occurs in kvs.
Fixpoint hfields_lookup (k:field) (kvs:hrecord_fields) : option val :=
match kvs with
| nil ⇒ None
| (ki,vi)::kvs' ⇒ if Nat.eq_dec k ki
then Some vi
else hfields_lookup k kvs'
end.
match kvs with
| nil ⇒ None
| (ki,vi)::kvs' ⇒ if Nat.eq_dec k ki
then Some vi
else hfields_lookup k kvs'
end.
Under the assumption that hfields_lookup k kvs returns Some v, the read
operation val_get_field k p is specified to return v. The corresponding
specification appears below.
Parameter triple_get_field_hfields : ∀ kvs p k v,
hfields_lookup k kvs = Some v →
triple (val_get_field k p)
(hfields kvs p)
(fun r ⇒ \[r = v] \* hfields kvs p).
hfields_lookup k kvs = Some v →
triple (val_get_field k p)
(hfields kvs p)
(fun r ⇒ \[r = v] \* hfields kvs p).
Third and last, the read operation val_get_field can be specified with
respect to the predicate hrecord kvs p, describing the full record,
including its header. The corresponding specification shown below follows a
similar pattern as the specification of hfield.
Parameter triple_get_field_hrecord : ∀ kvs p k v,
hfields_lookup k kvs = Some v →
triple (val_get_field k p)
(hrecord kvs p)
(fun r ⇒ \[r = v] \* hrecord kvs p).
hfields_lookup k kvs = Some v →
triple (val_get_field k p)
(hrecord kvs p)
(fun r ⇒ \[r = v] \* hrecord kvs p).
Writing in Record Fields
The write operation val_get_field k p v is abbreviated as Set p`.k ':= v
.
Notation "t1 '`.' k ':=' t2" :=
(val_set_field k t1 t2)
(in custom trm at level 56, k at level 0, format "t1 '`.' k ':=' t2")
: trm_scope_ext.
(val_set_field k t1 t2)
(in custom trm at level 56, k at level 0, format "t1 '`.' k ':=' t2")
: trm_scope_ext.
Like for the read operation, the write operation can be specified at three
levels. First, it may be specified at the level of an individual field.
Parameter triple_set_field : ∀ v p k v',
triple (val_set_field k p v)
(p`.k ~~> v')
(fun _ ⇒ p`.k ~~> v).
triple (val_set_field k p v)
(p`.k ~~> v')
(fun _ ⇒ p`.k ~~> v).
Alternatively, it may be specified in terms of hfields or hrecord, using
an auxiliary function called hrecord_update. This function computes an
updated list of fields to reflect the action of a write operation.
Concretely, hrecord_update k w kvs replaces the contents of the field
named k with the value w. It returns a description kvs' of the record
fields, provided the update operation succeeded, i.e., provided that the
field k on which the update is to be performed actually occurs in the list
kvs.
Fixpoint hfields_update (k:field) (v:val) (kvs:hrecord_fields)
: option hrecord_fields :=
match kvs with
| nil ⇒ None
| (ki,vi)::kvs' ⇒ if Nat.eq_dec k ki
then Some ((k,v)::kvs')
else match hfields_update k v kvs' with
| None ⇒ None
| Some LR ⇒ Some ((ki,vi)::LR)
end
end.
: option hrecord_fields :=
match kvs with
| nil ⇒ None
| (ki,vi)::kvs' ⇒ if Nat.eq_dec k ki
then Some ((k,v)::kvs')
else match hfields_update k v kvs' with
| None ⇒ None
| Some LR ⇒ Some ((ki,vi)::LR)
end
end.
The specification in terms of hfields is as follows.
Parameter triple_set_field_hfields : ∀ kvs kvs' k p v,
hfields_update k v kvs = Some kvs' →
triple (val_set_field k p v)
(hfields kvs p)
(fun _ ⇒ hfields kvs' p).
hfields_update k v kvs = Some kvs' →
triple (val_set_field k p v)
(hfields kvs p)
(fun _ ⇒ hfields kvs' p).
The specification in terms of hrecord follows a similar pattern.
Parameter triple_set_field_hrecord : ∀ kvs kvs' k p v,
hfields_update k v kvs = Some kvs' →
triple (val_set_field k p v)
(hrecord kvs p)
(fun _ ⇒ hrecord kvs' p).
hfields_update k v kvs = Some kvs' →
triple (val_set_field k p v)
(hrecord kvs p)
(fun _ ⇒ hrecord kvs' p).
Allocation of Records with Initializers
Parameter val_new_hrecord_2 : field → field → val.
Notation "`{ k1 := v1 ; k2 := v2 }" :=
(val_new_hrecord_2 k1 k2 v1 v2)
(in custom trm at level 65,
k1, k2 at level 0,
v1, v2 at level 65).
Notation "`{ k1 := v1 ; k2 := v2 }" :=
(val_new_hrecord_2 k1 k2 v1 v2)
(in custom trm at level 65,
k1, k2 at level 0,
v1, v2 at level 65).
The record allocation operation `{ k1 := v1 ; k2 := v2 } is specified as
shown below. The premises k1 = 0 and k2 = 1 enforce the field names to
be provided in increasing order, starting from zero. The postcondition
describes a record at address p using the predicate
p ~~~> `{ k1 := v1 ; k2 := v2 }, which is a notation for
hrecord ((k1,v1)::(k2,v2)::nil) p.
Parameter triple_new_hrecord_2 : ∀ (k1 k2:field) (v1 v2:val),
k1 = 0%nat →
k2 = 1%nat →
triple <{ `{ k1 := v1; k2 := v2 } }>
\[]
(funloc p ⇒ p ~~~> `{ k1 := v1 ; k2 := v2 }).
k1 = 0%nat →
k2 = 1%nat →
triple <{ `{ k1 := v1; k2 := v2 } }>
\[]
(funloc p ⇒ p ~~~> `{ k1 := v1 ; k2 := v2 }).
For example, the operation mcons x q allocates a list cell with head value
x and tail pointer q.
Definition mcons : val :=
val_new_hrecord_2 head tail.
Lemma triple_mcons : ∀ (x q:val),
triple (mcons x q)
\[]
(funloc p ⇒ p ~~~> `{ head := x ; tail := q }).
Proof using. intros. applys* triple_new_hrecord_2. Qed.
val_new_hrecord_2 head tail.
Lemma triple_mcons : ∀ (x q:val),
triple (mcons x q)
\[]
(funloc p ⇒ p ~~~> `{ head := x ; tail := q }).
Proof using. intros. applys* triple_new_hrecord_2. Qed.
This completes the presentation of the formalization of the mechanisms at
play for reasoning about records. These mechanisms were illustrated
throughout the chapter Repr.
In this section, we explain how val_get_field, val_set_field, and
val_new_hrecord_2 can be realized in terms of block allocation and pointer
arithmetic, following the same approach as in the previous chapter on
arrays. In particular, we use a similar proof set up.
Global Transparent hfield.
#[local] Hint Extern 1 (_ ≥ _) ⇒ math : triple.
Ltac is_additional_arith_type T ::=
match T with
| loc ⇒ constr:(true)
| field ⇒ constr:(true)
end.
#[local] Hint Extern 1 (_ ≥ _) ⇒ math : triple.
Ltac is_additional_arith_type T ::=
match T with
| loc ⇒ constr:(true)
| field ⇒ constr:(true)
end.
Implementation of Record Accesses using Pointer Arithmetic
Definition val_get_field (k:field) : val :=
<{ fun 'p ⇒
let 'p1 = val_ptr_add 'p 1 in
let 'q = val_ptr_add 'p1 {nat_to_Z k} in
val_get 'q }>.
Notation "t1 '`.' f" :=
(val_get_field f t1)
(in custom trm at level 56, f at level 0, format "t1 '`.' f" ).
#[export]Hint Resolve triple_ptr_add_nonneg : triple.
Lemma triple_get_field : ∀ p k v,
triple ((val_get_field k) p)
(p`.k ~~> v)
(fun r ⇒ \[r = v] \* (p`.k ~~> v)).
Proof using.
unfold hfield. xwp. xapp. xapp. unfolds field.
math_rewrite (p + abs 1 + abs k = p+1+k)%nat. xapp. xsimpl*.
Qed.
<{ fun 'p ⇒
let 'p1 = val_ptr_add 'p 1 in
let 'q = val_ptr_add 'p1 {nat_to_Z k} in
val_get 'q }>.
Notation "t1 '`.' f" :=
(val_get_field f t1)
(in custom trm at level 56, f at level 0, format "t1 '`.' f" ).
#[export]Hint Resolve triple_ptr_add_nonneg : triple.
Lemma triple_get_field : ∀ p k v,
triple ((val_get_field k) p)
(p`.k ~~> v)
(fun r ⇒ \[r = v] \* (p`.k ~~> v)).
Proof using.
unfold hfield. xwp. xapp. xapp. unfolds field.
math_rewrite (p + abs 1 + abs k = p+1+k)%nat. xapp. xsimpl*.
Qed.
The set operation on a field, written Set p`.k := v, is encoded as
val_set (p+1+k) v.
Definition val_set_field (k:field) : val :=
<{ fun 'p 'v ⇒
let 'p1 = val_ptr_add 'p 1 in
let 'q = val_ptr_add 'p1 {nat_to_Z k} in
val_set 'q 'v }>.
Lemma triple_set_field : ∀ v1 p k v2,
triple ((val_set_field k) p v2)
(p`.k ~~> v1)
(fun _ ⇒ p`.k ~~> v2).
Proof using.
unfold hfield. intros. xwp. xapp. xapp.
math_rewrite (p + abs 1 + abs k = p+1+k)%nat. xapp. xsimpl.
Qed.
Notation "t1 '`.' f ':=' t2" :=
(val_set_field f t1 t2)
(in custom trm at level 56, f at level 0, format "t1 '`.' f ':=' t2").
<{ fun 'p 'v ⇒
let 'p1 = val_ptr_add 'p 1 in
let 'q = val_ptr_add 'p1 {nat_to_Z k} in
val_set 'q 'v }>.
Lemma triple_set_field : ∀ v1 p k v2,
triple ((val_set_field k) p v2)
(p`.k ~~> v1)
(fun _ ⇒ p`.k ~~> v2).
Proof using.
unfold hfield. intros. xwp. xapp. xapp.
math_rewrite (p + abs 1 + abs k = p+1+k)%nat. xapp. xsimpl.
Qed.
Notation "t1 '`.' f ':=' t2" :=
(val_set_field f t1 t2)
(in custom trm at level 56, f at level 0, format "t1 '`.' f ':=' t2").
Specification of Record Accesses w.r.t. hfields
Lemma triple_get_field_hfields : ∀ kvs p k v,
hfields_lookup k kvs = Some v →
triple (val_get_field k p)
(hfields kvs p)
(fun r ⇒ \[r = v] \* hfields kvs p).
Proof using.
intros L. induction L as [| [ki vi] L']; simpl; introv E.
{ inverts E. }
{ case_if.
{ inverts E. subst ki. applys triple_conseq_frame.
{ applys triple_get_field. } { xsimpl. } { xsimpl*. } }
{ applys triple_conseq_frame.
{ applys IHL' E. }
{ xsimpl. }
{ xsimpl*. } } }
Qed.
Lemma triple_set_field_hfields : ∀ kvs kvs' k p v,
hfields_update k v kvs = Some kvs' →
triple (val_set_field k p v)
(hfields kvs p)
(fun _ ⇒ hfields kvs' p).
Proof using.
intros kvs. induction kvs as [| [ki vi] kvs']; simpl; introv E.
{ inverts E. }
{ case_if.
{ inverts E. subst ki. applys triple_conseq_frame.
{ applys triple_set_field. } { xsimpl. } { xsimpl*. } }
{ cases (hfields_update k v kvs') as C2; tryfalse. inverts E.
applys triple_conseq_frame. { applys IHkvs' C2. }
{ xsimpl. } { simpl. xsimpl*. } } }
Qed.
hfields_lookup k kvs = Some v →
triple (val_get_field k p)
(hfields kvs p)
(fun r ⇒ \[r = v] \* hfields kvs p).
Proof using.
intros L. induction L as [| [ki vi] L']; simpl; introv E.
{ inverts E. }
{ case_if.
{ inverts E. subst ki. applys triple_conseq_frame.
{ applys triple_get_field. } { xsimpl. } { xsimpl*. } }
{ applys triple_conseq_frame.
{ applys IHL' E. }
{ xsimpl. }
{ xsimpl*. } } }
Qed.
Lemma triple_set_field_hfields : ∀ kvs kvs' k p v,
hfields_update k v kvs = Some kvs' →
triple (val_set_field k p v)
(hfields kvs p)
(fun _ ⇒ hfields kvs' p).
Proof using.
intros kvs. induction kvs as [| [ki vi] kvs']; simpl; introv E.
{ inverts E. }
{ case_if.
{ inverts E. subst ki. applys triple_conseq_frame.
{ applys triple_set_field. } { xsimpl. } { xsimpl*. } }
{ cases (hfields_update k v kvs') as C2; tryfalse. inverts E.
applys triple_conseq_frame. { applys IHkvs' C2. }
{ xsimpl. } { simpl. xsimpl*. } } }
Qed.
Specification of Record Accesses w.r.t. hrecord
Lemma triple_get_field_hrecord : ∀ kvs p k v,
hfields_lookup k kvs = Some v →
triple (val_get_field k p)
(hrecord kvs p)
(fun r ⇒ \[r = v] \* hrecord kvs p).
Proof using.
introv M. unfold hrecord. xtriple. xpull. intros z Hz.
xapp (>> triple_get_field_hfields M). xsimpl*.
Qed.
hfields_lookup k kvs = Some v →
triple (val_get_field k p)
(hrecord kvs p)
(fun r ⇒ \[r = v] \* hrecord kvs p).
Proof using.
introv M. unfold hrecord. xtriple. xpull. intros z Hz.
xapp (>> triple_get_field_hfields M). xsimpl*.
Qed.
For val_set_field, however, we need an auxiliary lemma about
hfields_update, showing that the update operation preserves the names of
the fields. This lemma is established in two steps.
Lemma hfields_update_preserves_fields : ∀ kvs kvs' k v,
hfields_update k v kvs = Some kvs' →
LibList.map fst kvs' = LibList.map fst kvs.
Proof using.
intros kvs. induction kvs as [|[ki vi] kvs1]; simpl; introv E.
{ introv _ H. inverts H. }
{ case_if.
{ inverts E. rew_listx*. subst. fequals. }
{ cases (hfields_update k v kvs1).
{ inverts E. rew_listx. fequals*. }
{ inverts E. } } }
Qed.
Lemma hfields_update_preserves_maps_all_fields : ∀ kvs kvs' z k v,
hfields_update k v kvs = Some kvs' →
maps_all_fields z kvs = maps_all_fields z kvs'.
Proof using.
introv M. unfold maps_all_fields. extens.
rewrites* (>> hfields_update_preserves_fields M).
Qed.
hfields_update k v kvs = Some kvs' →
LibList.map fst kvs' = LibList.map fst kvs.
Proof using.
intros kvs. induction kvs as [|[ki vi] kvs1]; simpl; introv E.
{ introv _ H. inverts H. }
{ case_if.
{ inverts E. rew_listx*. subst. fequals. }
{ cases (hfields_update k v kvs1).
{ inverts E. rew_listx. fequals*. }
{ inverts E. } } }
Qed.
Lemma hfields_update_preserves_maps_all_fields : ∀ kvs kvs' z k v,
hfields_update k v kvs = Some kvs' →
maps_all_fields z kvs = maps_all_fields z kvs'.
Proof using.
introv M. unfold maps_all_fields. extens.
rewrites* (>> hfields_update_preserves_fields M).
Qed.
We are then ready to derive the specification for val_set_field.
Lemma triple_set_field_hrecord : ∀ kvs kvs' k p v,
hfields_update k v kvs = Some kvs' →
triple (val_set_field k p v)
(hrecord kvs p)
(fun _ ⇒ hrecord kvs' p).
Proof using.
introv M. unfold hrecord. xtriple. xpull. intros z Hz.
xapp (>> triple_set_field_hfields M). xsimpl.
rewrites* <- (>> hfields_update_preserves_maps_all_fields z M).
Qed.
hfields_update k v kvs = Some kvs' →
triple (val_set_field k p v)
(hrecord kvs p)
(fun _ ⇒ hrecord kvs' p).
Proof using.
introv M. unfold hrecord. xtriple. xpull. intros z Hz.
xapp (>> triple_set_field_hfields M). xsimpl.
rewrites* <- (>> hfields_update_preserves_maps_all_fields z M).
Qed.
Implementation of Record Allocation without Initialization
Definition val_alloc_hrecord (ks:list field) : val :=
<{ fun 'v ⇒
let 'm = {LibListExec.length ks} + 1 in
let 'p = val_alloc 'm in
val_set 'p {LibListExec.length ks};
'p }>.
<{ fun 'v ⇒
let 'm = {LibListExec.length ks} + 1 in
let 'p = val_alloc 'm in
val_set 'p {LibListExec.length ks};
'p }>.
A key auxiliary result asserts that if kvs is a list of key-value pairs
such as the keys correspond to consecutive field names, then a list of
fields described as hfields kvs p corresponds to a range of consecutive
cells as described by hrange (List.map snd kvs) (p+1), for the definition
of hrange given in Arrays.
Lemma hfields_eq_hrange : ∀ z L p kvs,
maps_all_fields z kvs →
z = length L →
L = LibList.map snd kvs →
hfields kvs p = hrange L (p+1)%nat.
Proof using.
asserts Ind: (∀ L p kvs o,
LibList.map fst kvs = nat_seq o (length L) →
L = LibList.map snd kvs →
hfields kvs p = hrange L (p+1+o)%nat).
{ intros L. induction L as [|v L']; introv M E; rew_listx in *;
destruct kvs as [|[k v'] kvs']; tryfalse; rew_listx in *.
{ auto. }
{ simpls. inverts M as M'. inverts E as E'. rew_listx in *.
unfold hfield. fequals. math_rewrite (p+1+o+1=p+1+(o+1))%nat.
applys* IHL'. math_rewrite* (o+1=S o)%nat. } }
introv M HL E. subst z. rewrites (>> Ind M E). fequals. unfold loc. math.
Qed.
maps_all_fields z kvs →
z = length L →
L = LibList.map snd kvs →
hfields kvs p = hrange L (p+1)%nat.
Proof using.
asserts Ind: (∀ L p kvs o,
LibList.map fst kvs = nat_seq o (length L) →
L = LibList.map snd kvs →
hfields kvs p = hrange L (p+1+o)%nat).
{ intros L. induction L as [|v L']; introv M E; rew_listx in *;
destruct kvs as [|[k v'] kvs']; tryfalse; rew_listx in *.
{ auto. }
{ simpls. inverts M as M'. inverts E as E'. rew_listx in *.
unfold hfield. fequals. math_rewrite (p+1+o+1=p+1+(o+1))%nat.
applys* IHL'. math_rewrite* (o+1=S o)%nat. } }
introv M HL E. subst z. rewrites (>> Ind M E). fequals. unfold loc. math.
Qed.
The specification of val_alloc_hrecord ks involves an empty precondition
and a postcondition of the form hrecord kvs p, where the list kvs maps
the fields names from ks to the value val_uninit. The premise
ks = nat_seq 0 (length ks) checks that the list ks contains consecutive
offsets starting from zero.
Recall that LibListExec.length is a variant of LibList.length that
computes in Coq (using simpl or reflexivity). Likewise LibListExec.map
is a computable version of LibList.map.
Lemma triple_alloc_hrecord : ∀ ks,
ks = nat_seq 0 (LibListExec.length ks) →
triple ((val_alloc_hrecord ks) ())
\[]
(funloc p ⇒ hrecord (LibListExec.map (fun k ⇒ (k,val_uninit)) ks) p).
Proof using.
introv Hks. xwp. xapp. xapp. intros p Hp. unfolds field.
rewrite LibListExec.length_eq in *. set (n := length ks) in *.
math_rewrite (abs (n + 1) = S n). rew_listx. simpl.
xapp. xval. xsimpl*. unfold hrecord. autorewrite with rew_list_exec.
asserts R: (maps_all_fields n (LibList.map (fun k ⇒ (k, val_uninit)) ks)).
{ unfolds. rewrite Hks. clears ks p. generalize 0%nat as o.
induction n as [|n']; intros; simpl; rew_listx; fequals*. }
xsimpl* n. xchange* <- (@hfields_eq_hrange n). { rew_listx*. }
{ unfold n. clears n p. induction ks as [|ks']; rew_listx; fequals*. }
Qed.
#[global] Hint Resolve triple_alloc_hrecord : triple.
ks = nat_seq 0 (LibListExec.length ks) →
triple ((val_alloc_hrecord ks) ())
\[]
(funloc p ⇒ hrecord (LibListExec.map (fun k ⇒ (k,val_uninit)) ks) p).
Proof using.
introv Hks. xwp. xapp. xapp. intros p Hp. unfolds field.
rewrite LibListExec.length_eq in *. set (n := length ks) in *.
math_rewrite (abs (n + 1) = S n). rew_listx. simpl.
xapp. xval. xsimpl*. unfold hrecord. autorewrite with rew_list_exec.
asserts R: (maps_all_fields n (LibList.map (fun k ⇒ (k, val_uninit)) ks)).
{ unfolds. rewrite Hks. clears ks p. generalize 0%nat as o.
induction n as [|n']; intros; simpl; rew_listx; fequals*. }
xsimpl* n. xchange* <- (@hfields_eq_hrange n). { rew_listx*. }
{ unfold n. clears n p. induction ks as [|ks']; rew_listx; fequals*. }
Qed.
#[global] Hint Resolve triple_alloc_hrecord : triple.
The interest of using the computable counterparts of the function length
and map is that a call to simpl will yield exactly the expected result,
with lists indexed using field names. For example, the allocation of a list
cell is specified as follows.
Lemma triple_alloc_mcons :
triple (val_alloc_hrecord (head::tail::nil) ())
\[]
(funloc p ⇒ p ~~~> `{ head := val_uninit ; tail := val_uninit }).
Proof using. applys* triple_alloc_hrecord. Qed.
triple (val_alloc_hrecord (head::tail::nil) ())
\[]
(funloc p ⇒ p ~~~> `{ head := val_uninit ; tail := val_uninit }).
Proof using. applys* triple_alloc_hrecord. Qed.
Implementation of Record Allocation with Initialization
Definition val_new_hrecord_2 (k1:field) (k2:field) : val :=
<{ fun 'x1 'x2 ⇒
let 'p = {val_alloc_hrecord (k1::k2::nil)} () in
'p`.k1 := 'x1;
'p`.k2 := 'x2;
'p }>.
<{ fun 'x1 'x2 ⇒
let 'p = {val_alloc_hrecord (k1::k2::nil)} () in
'p`.k1 := 'x1;
'p`.k2 := 'x2;
'p }>.
To improve readability, we introduce notation to allow writing, e.g.,
`{ head := x; tail := q } for the allocation and initialization of a list
cell.
Notation "`{ k1 := v1 ; k2 := v2 }" :=
(val_new_hrecord_2 k1 k2 v1 v2)
(in custom trm at level 65,
k1, k2 at level 0,
v1, v2 at level 65) : trm_scope_ext.
(val_new_hrecord_2 k1 k2 v1 v2)
(in custom trm at level 65,
k1, k2 at level 0,
v1, v2 at level 65) : trm_scope_ext.
This operation is specified as follows.
Lemma triple_new_hrecord_2 : ∀ k1 k2 v1 v2,
k1 = 0%nat →
k2 = 1%nat →
triple <{ `{ k1 := v1; k2 := v2 } }>
\[]
(funloc p ⇒ p ~~~> `{ k1 := v1 ; k2 := v2 }).
Proof using.
introv → →. xwp. xapp triple_alloc_hrecord. { reflexivity. }
intros p. simpl.
xapp triple_set_field_hrecord. { reflexivity. }
xapp triple_set_field_hrecord. { reflexivity. }
xval. xsimpl*.
Qed.
End Realization.
k1 = 0%nat →
k2 = 1%nat →
triple <{ `{ k1 := v1; k2 := v2 } }>
\[]
(funloc p ⇒ p ~~~> `{ k1 := v1 ; k2 := v2 }).
Proof using.
introv → →. xwp. xapp triple_alloc_hrecord. { reflexivity. }
intros p. simpl.
xapp triple_set_field_hrecord. { reflexivity. }
xapp triple_set_field_hrecord. { reflexivity. }
xval. xsimpl*.
Qed.
End Realization.
This completes the verification of the implementation of record operations
in terms of block allocation and pointer arithmetic. The generalization of
val_new_hrecord_2 to handle arbitrary arities involves more technical
meta-programming, beyond the scope of this course.
Extending xapp to Support Record Access Operations
Lemma xapp_get_field_lemma : ∀ H k p Q,
H ==> \∃ kvs, (hrecord kvs p) \*
match hfields_lookup k kvs with
| None ⇒ \[False]
| Some v ⇒ ((fun r ⇒ \[r = v] \* hrecord kvs p) \−−∗ protect Q) end →
H ==> wpgen_app (val_get_field k p) Q.
Proof using.
introv N. xchange N. intros kvs. cases (hfields_lookup k kvs).
{ unfold wpgen_app. xsimpl. applys* triple_conseq_frame triple_get_field_hrecord.
{ xsimpl. }
{ xpull. intros r →. xchange (qwand_specialize v). rewrite* hwand_hpure_l. } }
{ xpull. }
Qed.
H ==> \∃ kvs, (hrecord kvs p) \*
match hfields_lookup k kvs with
| None ⇒ \[False]
| Some v ⇒ ((fun r ⇒ \[r = v] \* hrecord kvs p) \−−∗ protect Q) end →
H ==> wpgen_app (val_get_field k p) Q.
Proof using.
introv N. xchange N. intros kvs. cases (hfields_lookup k kvs).
{ unfold wpgen_app. xsimpl. applys* triple_conseq_frame triple_get_field_hrecord.
{ xsimpl. }
{ xpull. intros r →. xchange (qwand_specialize v). rewrite* hwand_hpure_l. } }
{ xpull. }
Qed.
Likewise, the lemma xapp_set_field_lemma reformulates the specification
triple_set_field_hrecord. The assumption
hfields_update k v kvs = Some ks' is also captured by a pattern matching.
Lemma xapp_set_field_lemma : ∀ H k p v Q,
H ==> \∃ kvs, (hrecord kvs p) \*
match hfields_update k v kvs with
| None ⇒ \[False]
| Some kvs' ⇒ ((fun _ ⇒ hrecord kvs' p) \−−∗ protect Q) end →
H ==> wpgen_app (val_set_field k p v) Q.
Proof using.
introv N. xchange N. intros kvs. cases (hfields_update k v kvs).
{ unfold wpgen_app. xsimpl. applys* triple_conseq_frame triple_set_field_hrecord.
{ xsimpl. }
{ xpull. intros r. xchange (qwand_specialize r). } }
{ xpull. }
Qed.
H ==> \∃ kvs, (hrecord kvs p) \*
match hfields_update k v kvs with
| None ⇒ \[False]
| Some kvs' ⇒ ((fun _ ⇒ hrecord kvs' p) \−−∗ protect Q) end →
H ==> wpgen_app (val_set_field k p v) Q.
Proof using.
introv N. xchange N. intros kvs. cases (hfields_update k v kvs).
{ unfold wpgen_app. xsimpl. applys* triple_conseq_frame triple_set_field_hrecord.
{ xsimpl. }
{ xpull. intros r. xchange (qwand_specialize r). } }
{ xpull. }
Qed.
The hook xapp_nosubst_for_records, invoked by xapp, is then implemented
by exploiting the two lemmas above, in conjunction with xsimpl.
Ltac xapp_nosubst_for_records tt ::=
first [ applys xapp_set_field_lemma; xsimpl; simpl; xapp_simpl
| applys xapp_get_field_lemma; xsimpl; simpl; xapp_simpl ].
first [ applys xapp_set_field_lemma; xsimpl; simpl; xapp_simpl
| applys xapp_get_field_lemma; xsimpl; simpl; xapp_simpl ].
The above definition is the one used in LibSepReference. It was put to
practice in the chapters Basic and Repr.
(* 2024-01-03 14:19 *)