Commit 3fd1be7c authored by Rodolphe Lepigre's avatar Rodolphe Lepigre Committed by Michael Sammler
Browse files

Remove generated files and associated CI checks.

This requires adding an option [--soft] to [refinedc clean] in order
to prevent the [_CoqProject] file to be edited locally when building
or cleaning the examples.
parent d9766f68
Pipeline #50483 passed with stage
in 23 minutes and 25 seconds
......@@ -6,12 +6,11 @@ _build/
*.bak
.coq-native/
builddep/
Makefile.coq
.Makefile.coq.d
Makefile.coq.conf
_opam
/theories/examples/tutorial/tutorial
*.timing
.lia.cache
.nia.cache
.vscode/
**/proofs/*/generated*
**/proofs/*/dune
**/proofs/*/proof_files
......@@ -4,7 +4,8 @@ stages:
- build
variables:
CPU_CORES: "10"
# dune takes care of parallelization itself and does not like running in parallel
CPU_CORES: "1"
MAKE_TARGET: "all_with_examples"
OCAML: "ocaml-base-compiler.4.07.1"
......@@ -39,7 +40,7 @@ build-coq.8.12.0-timing:
only:
- master@iris/refinedc
- /^time/@iris/refinedc
# timing only for master and /time branches
# timing only for master and time/ branches
tags:
- fp-timing
......@@ -51,15 +52,6 @@ build-coq.8.12.0:
only:
- /^ci/@iris/refinedc
check-generated:
<<: *template
variables:
OPAM_PINS: "coq version 8.12.0 cerberus git git+https://github.com/rems-project/cerberus.git#7eb94d628845555cb5425f4f4b48890b345efdc5 z3 version 4.8.9-1"
DENY_WARNINGS: "1"
MAKE_TARGET: "check_generate_all"
# necessary because dune does not like running in parallel
CPU_CORES: 1
trigger-iris.dev:
<<: *template
variables:
......
......@@ -2,14 +2,10 @@ all:
@dune build _build/default/refinedc.install --display short
.PHONY: all
all_with_examples:
all_with_examples: generate_all
@dune build --display short
.PHONY: all_with_examples
clean:
@dune clean
.PHONY: clean
install:
@dune install
.PHONY: install
......@@ -31,6 +27,15 @@ check_generate_all: generate_all
git diff --exit-code
.PHONY: check_generate_all
clean_generated:
@for FILE in ${C_SRC} ; do dune exec -- refinedc clean --soft $$FILE ; done
@rm -f $(addsuffix .gen, $(C_SRC))
.PHONY: clean_generated
clean: clean_generated
@dune clean
.PHONY: clean
builddep-opamfiles: builddep/refinedc-builddep.opam
@true
.PHONY: builddep-opamfiles
......
; Generated by [refinedc], do not edit.
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
(name refinedc.examples.binary_search)
(theories refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
This diff is collapsed.
From refinedc.typing Require Import typing.
From refinedc.examples.binary_search Require Import generated_code.
From refinedc.examples.binary_search Require Import generated_spec.
From refinedc.examples.binary_search Require Import binary_search_extra.
Set Default Proof Using "Type".
(* Generated from [examples/binary_search.c]. *)
Section proof_binary_search.
Context `{!typeG Σ} `{!globalG Σ}.
(* Typing proof for [binary_search]. *)
Lemma type_binary_search :
typed_function impl_binary_search type_of_binary_search.
Proof.
Open Scope printing_sugar.
start_function "binary_search" ([[[[[R ls] x] p] ty] px]) => arg_comp arg_xs arg_n arg_x local_r local_l local_k.
split_blocks ((
<[ "#1" :=
vl : nat,
vr : nat,
arg_comp ◁ₗ (function_ptr (fn( (x, y, px, py) : (Z * Z * loc * loc); px @ &own (ty x), py @ &own (ty y); True) (b) : (bool), b @ boolean bool_it; px ◁ₗ ty x py ◁ₗ ty y b R x y))
arg_xs ◁ₗ (p @ (&own (array (void*) ((fun x => &own (ty x) : type) <$> ls))))
arg_n ◁ₗ ((length ls) @ (int (i32)))
arg_x ◁ₗ (px @ (&own (ty x)))
local_k ◁ₗ uninit (it_layout i32)
local_l ◁ₗ (vl @ (int (i32)))
local_r ◁ₗ (vr @ (int (i32)))
vl <= vr
vr <= length ls
i y, (i < vl)%nat ls !! i = Some y R y x
i y, (vr i)%nat ls !! i = Some y ¬ R y x
]> $
)%I : gmap label (iProp Σ)) ((
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "binary_search" "#0".
- repeat liRStep; liShow.
all: print_typesystem_goal "binary_search" "#1".
Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
all: try by [revert select ( i j, _ _ ¬ R _ _); apply; [| done];solve_goal].
all: try by apply: binary_search_cond_1; [solve_goal|..]; solve_goal.
all: try by apply: binary_search_cond_2; [solve_goal|..]; solve_goal.
all: print_sidecondition_goal "binary_search".
Qed.
End proof_binary_search.
From refinedc.typing Require Import typing.
From refinedc.examples.binary_search Require Import generated_code.
From refinedc.examples.binary_search Require Import generated_spec.
From refinedc.examples.binary_search Require Import binary_search_extra.
Set Default Proof Using "Type".
(* Generated from [examples/binary_search.c]. *)
Section proof_compare_int.
Context `{!typeG Σ} `{!globalG Σ}.
(* Typing proof for [compare_int]. *)
Lemma type_compare_int :
typed_function impl_compare_int type_of_compare_int.
Proof.
Open Scope printing_sugar.
start_function "compare_int" ([[[x y] px] py]) => arg_x arg_y local_xi local_yi.
split_blocks ((
)%I : gmap label (iProp Σ)) ((
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "compare_int" "#0".
Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
all: print_sidecondition_goal "compare_int".
Qed.
End proof_compare_int.
From refinedc.typing Require Import typing.
From refinedc.examples.binary_search Require Import generated_code.
From refinedc.examples.binary_search Require Import generated_spec.
From refinedc.examples.binary_search Require Import binary_search_extra.
Set Default Proof Using "Type".
(* Generated from [examples/binary_search.c]. *)
Section proof_test.
Context `{!typeG Σ} `{!globalG Σ}.
(* Typing proof for [test]. *)
Lemma type_test (global_alloc global_binary_search global_compare_int global_free : loc) :
global_alloc ◁ᵥ global_alloc @ function_ptr type_of_alloc -
global_binary_search ◁ᵥ global_binary_search @ function_ptr type_of_binary_search -
global_compare_int ◁ᵥ global_compare_int @ function_ptr type_of_compare_int -
global_free ◁ᵥ global_free @ function_ptr type_of_free -
typed_function (impl_test global_alloc global_binary_search global_compare_int global_free) type_of_test.
Proof.
Open Scope printing_sugar.
start_function "test" ([]) => local_res local_ptrs local_needle.
split_blocks ((
)%I : gmap label (iProp Σ)) ((
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "test" "#0".
Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
all: try by repeat constructor; lia.
all: try by apply _.
all: try by do 4 (destruct x'; [ naive_solver lia |]); exfalso; apply: (H0 3%nat) => //; lia.
all: print_sidecondition_goal "test".
Qed.
End proof_test.
From refinedc.typing Require Import typing.
From refinedc.examples.binary_search Require Import generated_code.
From refinedc.examples.binary_search Require Import binary_search_extra.
Set Default Proof Using "Type".
(* Generated from [examples/binary_search.c]. *)
Section spec.
Context `{!typeG Σ} `{!globalG Σ}.
(* Inlined code. *)
Definition alloc_initialized := initialized "allocator_state" ().
(* Type definitions. *)
(* Specifications for function [alloc]. *)
Definition type_of_alloc :=
fn( size : nat; (size @ (int (size_t))); size + 16 max_int size_t (8 | size) (alloc_initialized))
() : (), (&own (uninit (Layout size 3))); True.
(* Specifications for function [free]. *)
Definition type_of_free :=
fn( size : nat; (size @ (int (size_t))), (&own (uninit (Layout size 3))); (alloc_initialized) (8 | size))
() : (), (void); True.
(* Specifications for function [alloc_array]. *)
Definition type_of_alloc_array :=
fn( (size, n) : nat * nat; (size @ (int (size_t))), (n @ (int (size_t))); size * n + 16 max_int size_t (8 | size) (alloc_initialized))
() : (), (&own (array (Layout size 3) (replicate n (uninit (Layout size 3))))); True.
(* Specifications for function [free_array]. *)
Definition type_of_free_array :=
fn( (size, n) : nat * nat; (size @ (int (size_t))), (n @ (int (size_t))), (&own (array (Layout size 3) (replicate n (uninit (Layout size 3))))); size * n max_int size_t (8 | size) (alloc_initialized))
() : (), (void); True.
(* Specifications for function [binary_search]. *)
Definition type_of_binary_search :=
fn( (R, ls, x, p, ty, px) : (Z Z Prop) * (list Z) * Z * loc * (Z type) * loc; (function_ptr (fn( (x, y, px, py) : (Z * Z * loc * loc); px @ &own (ty x), py @ &own (ty y); True) (b) : (bool), b @ boolean bool_it; px ◁ₗ ty x py ◁ₗ ty y b R x y)), (p @ (&own (array (void*) ((fun x => &own (ty x) : type) <$> ls)))), ((length ls) @ (int (i32))), (px @ (&own (ty x))); StronglySorted R ls Transitive R)
n : nat, (n @ (int (i32))); i y, (i < n)%nat ls !! i = Some y R y x i y, (n i)%nat ls !! i = Some y ¬ R y x (p ◁ₗ (array (void*) ((fun x => &own (ty x) : type) <$> ls))) (px ◁ₗ (ty (x))).
(* Specifications for function [compare_int]. *)
Definition type_of_compare_int :=
fn( (x, y, px, py) : Z * Z * loc * loc; (px @ (&own (x @ (int (size_t))))), (py @ (&own (y @ (int (size_t))))); True)
b : bool, (b @ (boolean (bool_it))); (px ◁ₗ (x @ (int (size_t)))) (py ◁ₗ (y @ (int (size_t)))) b Z.le x y.
(* Specifications for function [test]. *)
Definition type_of_test :=
fn( () : (); (alloc_initialized)) () : (), (void); True.
End spec.
generated_proof_alloc.v
generated_proof_alloc_array.v
generated_proof_binary_search.v
generated_proof_compare_int.v
generated_proof_free.v
generated_proof_free_array.v
generated_proof_test.v
; Generated by [refinedc], do not edit.
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
(name refinedc.examples.btree)
(theories refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
This diff is collapsed.
(* Let's skip that, you seem to have some faith. *)
(* Let's skip that, you seem to have some faith. *)
(* Let's skip that, you seem to have some faith. *)
From refinedc.typing Require Import typing.
From refinedc.examples.btree Require Import generated_code.
From refinedc.examples.btree Require Import generated_spec.
From refinedc.examples.btree Require Import btree_extra.
From refinedc.examples.btree Require Import btree_learn.
Set Default Proof Using "Type".
(* Generated from [examples/btree.c]. *)
Section proof_btree_member.
Context `{!typeG Σ} `{!globalG Σ}.
(* Typing proof for [btree_member]. *)
Lemma type_btree_member (global_key_index : loc) :
global_key_index ◁ᵥ global_key_index @ function_ptr type_of_key_index -
typed_function (impl_btree_member global_key_index) type_of_btree_member.
Proof.
Open Scope printing_sugar.
start_function "btree_member" ([[[p h] m] k]) => arg_t arg_k local_i local_cur.
split_blocks ((
<[ "#1" :=
cur_p : loc,
cur_m : gmap Z type,
b : bool,
cur_h : nat,
min_k : Z,
max_k : Z,
arg_k ◁ₗ (k @ (int (i32)))
local_i ◁ₗ uninit (it_layout i32)
local_cur ◁ₗ (cur_p @ (&own ((BR b cur_h min_k max_k cur_m) @ (btree_t))))
arg_t ◁ₗ (p @ (&own (wand (cur_p ◁ₗ ((BR b cur_h min_k max_k cur_m) @ (btree_t)) ) ((BRroot h m) @ (btree_t)))))
min_k k k max_k
m !! k = cur_m !! k
]> $
)%I : gmap label (iProp Σ)) ((
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "btree_member" "#0".
- repeat liRStep; liShow.
all: print_typesystem_goal "btree_member" "#1".
Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+ unfold btree_invariant in *; by solve_goal.
+ rewrite H1; by apply: (btree_invariant_in_keys_not_None H2).
+ by rewrite list_insert_id.
+ apply: (btree_invariant_in_range_child H2); naive_solver lia.
+ rewrite H1; apply: (btree_invariant_lookup_child H2); by naive_solver.
+ do 2 rewrite list_insert_id //; by destruct y0.
+ assert (k x0) as Hx1. { move => /H7 Hk. apply lookup_lt_Some in Hk. lia. } apply: (btree_invariant_in_range_child H2); by naive_solver.
+ assert (k x0) as Hx1. { move => /H7 Hk. apply lookup_lt_Some in Hk. lia. } rewrite H1. apply: (btree_invariant_lookup_child H2); by naive_solver.
+ rewrite list_insert_id //; by destruct y.
all: print_sidecondition_goal "btree_member".
Qed.
End proof_btree_member.
From refinedc.typing Require Import typing.
From refinedc.examples.btree Require Import generated_code.
From refinedc.examples.btree Require Import generated_spec.
From refinedc.examples.btree Require Import btree_extra.
From refinedc.examples.btree Require Import btree_learn.
Set Default Proof Using "Type".
(* Generated from [examples/btree.c]. *)
Section proof_free_btree.
Context `{!typeG Σ} `{!globalG Σ}.
(* Typing proof for [free_btree]. *)
Lemma type_free_btree (global_free global_free_btree_nodes : loc) :
global_free ◁ᵥ global_free @ function_ptr type_of_free -
global_free_btree_nodes ◁ᵥ global_free_btree_nodes @ function_ptr type_of_free_btree_nodes -
typed_function (impl_free_btree global_free global_free_btree_nodes) type_of_free_btree.
Proof.
Open Scope printing_sugar.
start_function "free_btree" ([]) => arg_t.
split_blocks ((
)%I : gmap label (iProp Σ)) ((
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "free_btree" "#0".
Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
all: print_sidecondition_goal "free_btree".
Qed.
End proof_free_btree.
(* Let's skip that, you seem to have some faith. *)
(* You were too lazy to even write a spec for this function. *)
From refinedc.typing Require Import typing.
From refinedc.examples.btree Require Import generated_code.
From refinedc.examples.btree Require Import generated_spec.
From refinedc.examples.btree Require Import btree_extra.
From refinedc.examples.btree Require Import btree_learn.
Set Default Proof Using "Type".
(* Generated from [examples/btree.c]. *)
Section proof_key_index.
Context `{!typeG Σ} `{!globalG Σ}.
(* Typing proof for [key_index]. *)
Lemma type_key_index :
typed_function impl_key_index type_of_key_index.
Proof.
Open Scope printing_sugar.
start_function "key_index" ([[[[p l] n] k] sz]) => arg_ar arg_n arg_k local_slot.
split_blocks ((
<[ "#1" :=
s : nat,
arg_ar ◁ₗ (p @ (&own (array (it_layout i32) ((l `at_type` int i32) ++ replicate (sz - n)%nat (uninit i32 : type)))))
arg_n ◁ₗ (n @ (int (i32)))
arg_k ◁ₗ (k @ (int (i32)))
local_slot ◁ₗ (s @ (int (i32)))
i : nat, v : Z, i < s l !! i = Some v v < k
s length l
]> $
)%I : gmap label (iProp Σ)) ((
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "key_index" "#0".
- repeat liRStep; liShow.
all: print_typesystem_goal "key_index" "#1".
Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+ destruct (decide (i = s)); by naive_solver lia.
+ move: (elem_of_list_lookup_1 _ _ H14) => [i Hi]. destruct (decide (y = k)); [ done | exfalso ]. assert (k < y) as Hky by lia. assert (i < s)%nat as Hle by by eapply StronglySorted_lookup_index_lt. assert (i < s) as His by lia. assert (k < k) by by eapply H0. by lia.
+ apply StronglySorted_insert_drop_take; last done. * move => z Hz. destruct (l !! z) eqn:?; naive_solver lia. * move: (elem_of_list_lookup_2 l s y H7) => Hy. rewrite H7 /=. assert (k y); [ by set_solver | by lia ].
+ assert (s = length l) as -> by lia. assert (k < k); last by lia. move: (elem_of_list_lookup_1 _ _ H7) => [i Hi]. move: (lookup_lt_Some _ _ _ Hi) => Hlt. naive_solver lia.
+ assert (s = length l) as -> by lia. rewrite drop_all. apply StronglySorted_app; [ .. | done | by do 2 constructor ]. move => x y Hx Hy. assert (y = k) as -> by set_solver. move: (elem_of_list_lookup_1 _ _ Hx) => [i Hi]. move: (lookup_lt_Some _ _ _ Hi) => Hlt. naive_solver lia.
all: print_sidecondition_goal "key_index".
Qed.
End proof_key_index.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment