Merge branch 'lennard/static' into 'main'

Support for statics

See merge request !25

Makefile

@@ -17,7 +17,7 @@ clean: clean_all
 frontend:
 	cd rr_frontend && ./refinedrust build && ./refinedrust install
 
-RUST_SRC = stdlib/alloc stdlib/option stdlib/vec case_studies/paper-examples case_studies/tests case_studies/minivec
+RUST_SRC = stdlib/alloc stdlib/option stdlib/result stdlib/spin stdlib/vec case_studies/paper-examples case_studies/tests case_studies/minivec
 
 %.gen: % phony
 	cd $< && cargo refinedrust

SPEC_FORMAT.md

@@ -98,6 +98,15 @@ enum option<T> {
 
 In addition, enums also support the `export_as` attribute (same as structs).
 
+## Static attributes
+RefinedRust supports `static` (but currently not `static mut`) variables.
+They can be used as if they were behind a shared reference with `static` lifetime.
+
+For a static variable to be used by the RefinedRust type checker, the respective function needs to require it to be initialized,
+using the `initialized π "name" r` predicate, where `r` is the assumed refinement of the static variable.
+To specify the name that is used to refer to the variable here, `static` variables can be annotated with a `rr::name` attribute:
+- `#[rr::name("my_static_int")]` indicates that the name `my_static_int` should be used to refer to the static in specifications.
+
 ## Module attributes
 Inside a module, the following mod-level attributes can be specified:
 - `#![rr::import("A.B.C", "D")]`: imports the file `D` from logical Coq path `A.B.C` in all spec and proof files

case_studies/minivec/extra_specs.v

 Section resolve_ghost.
-  Context `{!typeGS Σ}.
   Context {T_rt : Type}.
   Context (T_ty : type (T_rt)).
 

case_studies/minivec/output/minivec/proofs/proof_RawVec_T_cap.v

@@ -6,7 +6,7 @@ From refinedrust.examples.minivec.generated Require Import generated_template_Ra
 Set Default Proof Using "Type".
 
 Section proof.
-Context `{!typeGS Σ}.
+Context `{!refinedrustGS Σ}.
 Lemma RawVec_T_cap_proof (π : thread_id) :
   RawVec_T_cap_lemma π.
 Proof.
@@ -19,4 +19,4 @@ Proof.
   Unshelve. all: sidecond_hammer.
   Unshelve. all: print_remaining_sidecond.
 Qed.
-End proof.
+End proof.
\ No newline at end of file

case_studies/minivec/output/minivec/proofs/proof_RawVec_T_grow.v

@@ -6,7 +6,7 @@ From refinedrust.examples.minivec.generated Require Import generated_template_Ra
 Set Default Proof Using "Type".
 
 Section proof.
-Context `{!typeGS Σ}.
+Context `{!refinedrustGS Σ}.
 Lemma RawVec_T_grow_proof (π : thread_id) :
   RawVec_T_grow_lemma π.
 Proof.

case_studies/minivec/output/minivec/proofs/proof_RawVec_T_new.v

@@ -6,7 +6,7 @@ From refinedrust.examples.minivec.generated Require Import generated_template_Ra
 Set Default Proof Using "Type".
 
 Section proof.
-Context `{!typeGS Σ}.
+Context `{!refinedrustGS Σ}.
 Lemma RawVec_T_new_proof (π : thread_id) :
   RawVec_T_new_lemma π.
 Proof.

case_studies/minivec/output/minivec/proofs/proof_RawVec_T_ptr.v

@@ -6,7 +6,7 @@ From refinedrust.examples.minivec.generated Require Import generated_template_Ra
 Set Default Proof Using "Type".
 
 Section proof.
-Context `{!typeGS Σ}.
+Context `{!refinedrustGS Σ}.
 Lemma RawVec_T_ptr_proof (π : thread_id) :
   RawVec_T_ptr_lemma π.
 Proof.
@@ -19,4 +19,4 @@ Proof.
   Unshelve. all: sidecond_hammer.
   Unshelve. all: print_remaining_sidecond.
 Qed.
-End proof.
+End proof.
\ No newline at end of file

case_studies/minivec/output/minivec/proofs/proof_Vec_T_cap.v

@@ -6,7 +6,7 @@ From refinedrust.examples.minivec.generated Require Import generated_template_Ve
 Set Default Proof Using "Type".
 
 Section proof.
-Context `{!typeGS Σ}.
+Context `{!refinedrustGS Σ}.
 Lemma Vec_T_cap_proof (π : thread_id) :
   Vec_T_cap_lemma π.
 Proof.
@@ -19,4 +19,4 @@ Proof.
   Unshelve. all: sidecond_hammer.
   Unshelve. all: print_remaining_sidecond.
 Qed.
-End proof.
+End proof.
\ No newline at end of file

case_studies/minivec/output/minivec/proofs/proof_Vec_T_get.v

@@ -6,7 +6,7 @@ From refinedrust.examples.minivec.generated Require Import generated_template_Ve
 Set Default Proof Using "Type".
 
 Section proof.
-Context `{!typeGS Σ}.
+Context `{!refinedrustGS Σ}.
 Lemma Vec_T_get_proof (π : thread_id) :
   Vec_T_get_lemma π.
 Proof.
@@ -19,4 +19,4 @@ Proof.
   Unshelve. all: sidecond_hammer.
   Unshelve. all: print_remaining_sidecond.
 Qed.
-End proof.
+End proof.
\ No newline at end of file

case_studies/minivec/output/minivec/proofs/proof_Vec_T_get_mut.v

@@ -6,7 +6,7 @@ From refinedrust.examples.minivec.generated Require Import generated_template_Ve
 Set Default Proof Using "Type".
 
 Section proof.
-Context `{!typeGS Σ}.
+Context `{!refinedrustGS Σ}.
 Lemma Vec_T_get_mut_proof (π : thread_id) :
   Vec_T_get_mut_lemma π.
 Proof.

case_studies/minivec/output/minivec/proofs/proof_Vec_T_get_unchecked.v

@@ -6,7 +6,7 @@ From refinedrust.examples.minivec.generated Require Import generated_template_Ve
 Set Default Proof Using "Type".
 
 Section proof.
-Context `{!typeGS Σ}.
+Context `{!refinedrustGS Σ}.
 Lemma Vec_T_get_unchecked_proof (π : thread_id) :
   Vec_T_get_unchecked_lemma π.
 Proof.

case_studies/minivec/output/minivec/proofs/proof_Vec_T_get_unchecked_mut.v

@@ -6,7 +6,7 @@ From refinedrust.examples.minivec.generated Require Import generated_template_Ve
 Set Default Proof Using "Type".
 
 Section proof.
-Context `{!typeGS Σ}.
+Context `{!refinedrustGS Σ}.
 Lemma Vec_T_get_unchecked_mut_proof (π : thread_id) :
   Vec_T_get_unchecked_mut_lemma π.
 Proof.

case_studies/minivec/output/minivec/proofs/proof_Vec_T_len.v

@@ -6,7 +6,7 @@ From refinedrust.examples.minivec.generated Require Import generated_template_Ve
 Set Default Proof Using "Type".
 
 Section proof.
-Context `{!typeGS Σ}.
+Context `{!refinedrustGS Σ}.
 Lemma Vec_T_len_proof (π : thread_id) :
   Vec_T_len_lemma π.
 Proof.

case_studies/minivec/output/minivec/proofs/proof_Vec_T_new.v

@@ -6,7 +6,7 @@ From refinedrust.examples.minivec.generated Require Import generated_template_Ve
 Set Default Proof Using "Type".
 
 Section proof.
-Context `{!typeGS Σ}.
+Context `{!refinedrustGS Σ}.
 Lemma Vec_T_new_proof (π : thread_id) :
   Vec_T_new_lemma π.
 Proof.
@@ -19,4 +19,4 @@ Proof.
   Unshelve. all: sidecond_hammer.
   Unshelve. all: print_remaining_sidecond.
 Qed.
-End proof.
+End proof.
\ No newline at end of file

case_studies/minivec/output/minivec/proofs/proof_Vec_T_pop.v

@@ -6,7 +6,7 @@ From refinedrust.examples.minivec.generated Require Import generated_template_Ve
 Set Default Proof Using "Type".
 
 Section proof.
-Context `{!typeGS Σ}.
+Context `{!refinedrustGS Σ}.
 Lemma Vec_T_pop_proof (π : thread_id) :
   Vec_T_pop_lemma π.
 Proof.

case_studies/minivec/output/minivec/proofs/proof_Vec_T_ptr.v

@@ -6,7 +6,7 @@ From refinedrust.examples.minivec.generated Require Import generated_template_Ve
 Set Default Proof Using "Type".
 
 Section proof.
-Context `{!typeGS Σ}.
+Context `{!refinedrustGS Σ}.
 Lemma Vec_T_ptr_proof (π : thread_id) :
   Vec_T_ptr_lemma π.
 Proof.
@@ -19,4 +19,4 @@ Proof.
   Unshelve. all: sidecond_hammer.
   Unshelve. all: print_remaining_sidecond.
 Qed.
-End proof.
+End proof.
\ No newline at end of file

case_studies/minivec/output/minivec/proofs/proof_Vec_T_push.v

@@ -6,7 +6,7 @@ From refinedrust.examples.minivec.generated Require Import generated_template_Ve
 Set Default Proof Using "Type".
 
 Section proof.
-Context `{!typeGS Σ}.
+Context `{!refinedrustGS Σ}.
 Lemma Vec_T_push_proof (π : thread_id) :
   Vec_T_push_lemma π.
 Proof.

case_studies/minivec/output/minivec/proofs/proof_client_get_mut_client.v

@@ -6,7 +6,7 @@ From refinedrust.examples.minivec.generated Require Import generated_template_cl
 Set Default Proof Using "Type".
 
 Section proof.
-Context `{!typeGS Σ}.
+Context `{!refinedrustGS Σ}.
 Lemma client_get_mut_client_proof (π : thread_id) :
   client_get_mut_client_lemma π.
 Proof.

case_studies/tests/output/tests/proofs/proof_vec_client_init_vec.v

@@ -6,7 +6,7 @@ From refinedrust.examples.tests.generated Require Import generated_template_vec_
 Set Default Proof Using "Type".
 
 Section proof.
-Context `{!typeGS Σ}.
+Context `{!refinedrustGS Σ}.
 Lemma vec_client_init_vec_proof (π : thread_id) :
   vec_client_init_vec_lemma π.
 Proof.
@@ -15,7 +15,7 @@ Proof.
   repeat liRStep; liShow.
   liInst Hevar (int i32).
   repeat liRStep; liShow.
-
+  
   all: print_remaining_goal.
   Unshelve. all: sidecond_solver.
   Unshelve. all: sidecond_hammer.

case_studies/tests/src/lib.rs

@@ -6,5 +6,6 @@ mod enums;
 mod structs;
 mod char;
 mod traits;
+mod statics;
 
 mod vec_client;