From 1a701a257a0ec29b4fbb24e3a2e3d0aeea502ce5 Mon Sep 17 00:00:00 2001 From: Kathrin Stark Date: Thu, 27 Jun 2024 08:43:40 +0100 Subject: [PATCH] Changes in specification for uint63 to unsigned; add spec/proof for uint63_add --- BUILD | 2 +- examples/uint63nat/prims_verif.v | 38 +++++++++++++++++++++++--------- examples/uint63nat/specs.v | 36 ++++++++++++++++++++++-------- 3 files changed, 56 insertions(+), 20 deletions(-) diff --git a/BUILD b/BUILD index ca6e0e8..28dbbd7 100755 --- a/BUILD +++ b/BUILD @@ -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" diff --git a/examples/uint63nat/prims_verif.v b/examples/uint63nat/prims_verif.v index 64ccfeb..1aed146 100644 --- a/examples/uint63nat/prims_verif.v +++ b/examples/uint63nat/prims_verif.v @@ -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. @@ -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)) @@ -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. @@ -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) @@ -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'. @@ -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. @@ -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. diff --git a/examples/uint63nat/specs.v b/examples/uint63nat/specs.v index 4e73532..21dbe24 100644 --- a/examples/uint63nat/specs.v +++ b/examples/uint63nat/specs.v @@ -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. @@ -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 @@ -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) @@ -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) @@ -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 @@ -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 *) ] .