Skip to content

Commit

Permalink
Changes in specification for uint63 to unsigned; add spec/proof for u…
Browse files Browse the repository at this point in the history 
…int63_add
  • Loading branch information
@KatStark
KatStark committed Jun 27, 2024
1 parent e42c747 commit 1a701a2
Show file tree
Hide file tree
Showing 3 changed files with 56 additions and 20 deletions.
2 changes: 1 addition & 1 deletion BUILD
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ echo "RUN: opam switch create veriffi-coq8.19.1 4.14.1"
opam switch create veriffi-coq8.19.1 4.14.1 # this will fail if the switch already exists
echo "RUN: opam switch veriffi-coq8.19.1"
opam switch veriffi-coq8.19.1 # do this in case the previous command failed, harmless if succeeded
eval $(opam env --switch=veriffi-coq8.19.1)
eval $(opam env --switch=veriffi-coq8.19.1 --set-switch)

# RUN opam repo add coq-released http://coq.inria.fr/opam/released && opam pin add coq 8.19.1
echo "RUN: opam repo add coq-released http://coq.inria.fr/opam/released"
Expand Down
38 changes: 28 additions & 10 deletions examples/uint63nat/prims_verif.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,21 +12,40 @@ Defined.
Definition description_S := @desc _ S _.

Lemma decode_encode_Z:
forall n, min_signed <= encode_Z (Z.of_nat n) <= max_signed ->
forall n, (* min_signed <= *) encode_Z (Z.of_nat n) <= Int64.max_unsigned ->
Int64.shru (Int64.repr (encode_Z (Z.of_nat n)))
(Int64.repr (Int.unsigned (Int.repr 1)))
= Int64.repr (Z.of_nat n).
Proof.
intros.
unfold encode_Z, min_signed, max_signed in *.
unfold encode_Z in *.
autorewrite with norm. rewrite Int64.shru_div_two_p.
change (two_p _) with 2.
rewrite !Int64.unsigned_repr by rep_lia.
rewrite !Int64.unsigned_repr by lia.
rewrite Z.div_add_l by lia.
simpl Z.div; rewrite Z.add_0_r.
auto.
Qed.

Lemma body_uint63_add:
semax_body Vprog Gprog f_uint63_add uint63_add_spec.
Proof.
start_function.
forward. entailer!.
unfold encode_Z in *.
autorewrite with norm. rewrite !Int64.shru_div_two_p.
change (two_p _) with 2.
rewrite !Int64.unsigned_repr by lia.
rewrite Z.div_add_l by lia.
rewrite Int64.shl_mul_two_p.
autorewrite with norm. change (two_p _) with 2.
f_equal. f_equal.
assert ((Z.of_nat n * 2 + 1) / 2 = Z.of_nat n) as ->.
{ rewrite Z.add_comm. rewrite Z_div_plus; try lia.
replace (1/2) with 0 by reflexivity.
lia. }
lia.
Qed.

Lemma body_uint63_from_nat:
semax_body Vprog Gprog f_uint63_from_nat uint63_from_nat_spec.
Expand All @@ -36,7 +55,7 @@ Proof.
fold (rep_type_val g p).
forward.
rewrite Int.signed_repr
by (unfold encode_Z, max_signed in H; rep_lia).
by (unfold encode_Z in H; rep_lia).
forward_loop ( EX m : nat, EX p': rep_type,
PROP ( (m <= n)%nat; is_in_graph g outlier (n - m)%nat p';
nat_has_tag_prop (n - m)%nat (nat_get_desc (n-m)%nat))
Expand Down Expand Up @@ -144,8 +163,7 @@ Proof.
enough (n- m = 0)%nat.
{ assert (n = m) by lia. subst. eauto. }
apply repr_inj_unsigned64 in HRE; try rep_lia.
unfold encode_Z in H0.
unfold min_signed, max_signed in H0. rep_lia.
unfold encode_Z in H0. rep_lia.
Qed.

#[export] Instance CCE: change_composite_env env_graph_gc.CompSpecs CompSpecs.
Expand Down Expand Up @@ -197,7 +215,7 @@ semax (func_tycontext f_uint63_to_nat Vprog Gprog nil)
gvars gv)
SEP (full_gc g t_info roots outlier ti sh gv;
frame_rep_ Tsh v___FRAME__ v___ROOT__ (ti_fp t_info) 1;
library.mem_mgr gv))
VST.floyd.library.mem_mgr gv))
GC_SAVE1
(normal_ret_assert
(EX (g' : graph) (v0' : rep_type) (roots' : roots_t)
Expand All @@ -212,7 +230,7 @@ semax (func_tycontext f_uint63_to_nat Vprog Gprog nil)
gvars gv)
SEP (full_gc g' t_info' roots' outlier ti sh gv;
frame_rep_ Tsh v___FRAME__ v___ROOT__ (ti_fp t_info') 1;
library.mem_mgr gv))%argsassert).
VST.floyd.library.mem_mgr gv))%argsassert).
Proof.
intros.
eapply semax_post_flipped'.
Expand Down Expand Up @@ -264,7 +282,7 @@ forward_while
gvars gv)
SEP (full_gc g' t_info' roots' outlier ti sh gv;
frame_rep_ Tsh v___FRAME__ v___ROOT__ (ti_fp t_info') 1;
library.mem_mgr gv)
VST.floyd.library.mem_mgr gv)
).
- (* Before the while *)
Exists v O g t_info roots.
Expand Down Expand Up @@ -318,7 +336,7 @@ SEP (full_gc g' t_info' roots' outlier ti sh gv;
- (* after the loop *)
forward.
assert (m=n). {
clear - H3 H HRE. unfold encode_Z, min_signed, max_signed in H.
clear - H3 H HRE. unfold encode_Z in H.
apply repr_inj_unsigned64 in HRE; rep_lia.
}
subst m.
Expand Down
36 changes: 27 additions & 9 deletions examples/uint63nat/specs.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -108,10 +108,9 @@ Definition args_make_Coq_Init_Datatypes_nat_S_spec : ident * funspec :=
DECLARE _get_args
(args_spec_S').

(* Same as in UVRooster - TODO: encode_Z as relation to fit our general scheme *)
(* Same as in UVRooster
- TODO: encode_Z as relation to fit our general scheme *)
Definition encode_Z (x: Z): Z := x * 2 + 1.
Definition min_signed: Z := - 2^62.
Definition max_signed: Z := 2^62 - 1.

#[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.

Expand All @@ -128,18 +127,18 @@ Definition uint63_to_nat_spec : ident * funspec :=
ti : val, outlier : outlier_t, t_info : GCGraph.thread_info
PRE [ tptr (Tstruct _thread_info noattr ), (talignas 3%N (tptr tvoid)) ]
PROP ( writable_share sh;
min_signed <= encode_Z (Z.of_nat n) <= max_signed
encode_Z (Z.of_nat n) <= Int64.max_unsigned
)
PARAMS (ti; Vlong (Int64.repr (encode_Z (Z.of_nat n))))
GLOBALS (gv)
SEP (full_gc g t_info roots outlier ti sh gv; library.mem_mgr gv)
SEP (full_gc g t_info roots outlier ti sh gv; VST.floyd.library.mem_mgr gv)
POST [ (talignas 3%N (tptr tvoid)) ]
EX (p' : rep_type) (g' : graph) (t_info' : GCGraph.thread_info) (roots': roots_t),
PROP (@is_in_graph nat (@in_graph nat _) g' outlier n p' ;
gc_graph_iso g roots g' roots';
frame_shells_eq (ti_frames t_info) (ti_frames t_info'))
RETURN (rep_type_val g' p')
SEP (full_gc g' t_info' roots' outlier ti sh gv; library.mem_mgr gv).
SEP (full_gc g' t_info' roots' outlier ti sh gv; VST.floyd.library.mem_mgr gv).

Definition uint63_to_nat_no_gc_spec : ident * funspec :=
DECLARE _uint63_to_nat_no_gc
Expand All @@ -148,7 +147,7 @@ WITH gv : globals, g : graph, roots : roots_t, sh : share, n: nat,
PRE [ tptr (Tstruct _thread_info noattr ), (talignas 3%N (tptr tvoid)) ]
PROP ( 2 * (Z.of_nat n) < headroom t_info ;
writable_share sh;
min_signed <= encode_Z (Z.of_nat n) <= max_signed
encode_Z (Z.of_nat n) <= Int64.max_unsigned
)
PARAMS (ti; Vlong (Int64.repr (encode_Z (Z.of_nat n))))
GLOBALS (gv)
Expand All @@ -165,7 +164,7 @@ DECLARE _uint63_from_nat
WITH gv : globals, g : graph, roots : roots_t, sh : share, n: nat, p : rep_type,
ti : val, outlier : outlier_t, t_info : GCGraph.thread_info
PRE [ int_or_ptr_type ]
PROP ( encode_Z (Z.of_nat n) <= max_signed;
PROP ( encode_Z (Z.of_nat n) <= Int64.max_signed;
@is_in_graph nat (@in_graph nat _) g outlier n p ;
writable_share sh)
PARAMS (rep_type_val g p)
Expand All @@ -177,6 +176,23 @@ POST [ int_or_ptr_type ]
SEP (full_gc g t_info roots outlier ti sh gv).
(* KS: Existential *)

Definition uint63_add_spec : ident * funspec :=
DECLARE _uint63_add
WITH m : nat, n : nat
PRE [ int_or_ptr_type, int_or_ptr_type ]
PROP (encode_Z (Z.of_nat m) <= Int64.max_unsigned;
encode_Z (Z.of_nat n) <= Int64.max_unsigned;
encode_Z (Z.of_nat (m + n)) <= Int64.max_unsigned
)
PARAMS (Vlong (Int64.repr (encode_Z (Z.of_nat m)));
Vlong (Int64.repr (encode_Z (Z.of_nat n))))
GLOBALS ()
SEP ()
POST [ int_or_ptr_type ]
PROP ()
RETURN (Vlong (Int64.repr (encode_Z (Z.of_nat (m + n)))))
SEP ().

(* Function Spec
- This is the definition of a Coq function from X to Y/the specification that hopefully CertiCoq
Expand Down Expand Up @@ -265,10 +281,12 @@ POST [ int_or_ptr_type ]
SEP (full_gc g' t_info' roots outlier ti sh gv).



Definition Vprog : varspecs. mk_varspecs prog. Defined.
Definition Gprog := [ tag_spec_S; alloc_make_Coq_Init_Datatypes_nat_O_spec; alloc_make_Coq_Init_Datatypes_nat_S_spec
; args_make_Coq_Init_Datatypes_nat_S_spec ; uint63_to_nat_spec ; uint63_from_nat_spec;
uint63_to_nat_no_gc_spec;
gc_spec.garbage_collect_spec
gc_spec.garbage_collect_spec;
uint63_add_spec
(* _call, call_spec *)
] .

0 comments on commit 1a701a2

Please sign in to comment.