diff --git a/Makefile b/Makefile index c2d5abfad4989da5290a7366c4d778625f5d02e3..c5d1656add03db65204f3b923e5023929024a7a9 100644 --- a/Makefile +++ b/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 diff --git a/SPEC_FORMAT.md b/SPEC_FORMAT.md index 25ac7ca0124f6f23c3be220cd5bbc88c3c26f34f..6a3de99c5869fe28a967267a942fc16de3f78f3b 100644 --- a/SPEC_FORMAT.md +++ b/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 diff --git a/case_studies/minivec/extra_specs.v b/case_studies/minivec/extra_specs.v index 54f68ac295a807826e2a105972be3b53373861d7..9f616a6a7248f1557222b684912e1a0e1240d828 100644 --- a/case_studies/minivec/extra_specs.v +++ b/case_studies/minivec/extra_specs.v @@ -1,5 +1,4 @@ Section resolve_ghost. - Context `{!typeGS Σ}. Context {T_rt : Type}. Context (T_ty : type (T_rt)). diff --git a/case_studies/minivec/output/minivec/proofs/proof_RawVec_T_cap.v b/case_studies/minivec/output/minivec/proofs/proof_RawVec_T_cap.v index 621354bbf78b0cfc81d8eaaa1d8c011459d84687..294b7b3ff12f7fae3b423db677dfc6cf703e2d9b 100644 --- a/case_studies/minivec/output/minivec/proofs/proof_RawVec_T_cap.v +++ b/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. \ No newline at end of file +End proof. diff --git a/case_studies/minivec/output/minivec/proofs/proof_RawVec_T_grow.v b/case_studies/minivec/output/minivec/proofs/proof_RawVec_T_grow.v index e159458af350995d098b8e7db785d943dcdaa4e2..36592f2902e7dc1272b90ab68069404c6fc81a13 100644 --- a/case_studies/minivec/output/minivec/proofs/proof_RawVec_T_grow.v +++ b/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. diff --git a/case_studies/minivec/output/minivec/proofs/proof_RawVec_T_new.v b/case_studies/minivec/output/minivec/proofs/proof_RawVec_T_new.v index 8fbf9e962f2b850dba16364e40f5197bc7fd0fa5..79e8db58664b572d74389973f67d4c01ed4f3dc7 100644 --- a/case_studies/minivec/output/minivec/proofs/proof_RawVec_T_new.v +++ b/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. diff --git a/case_studies/minivec/output/minivec/proofs/proof_RawVec_T_ptr.v b/case_studies/minivec/output/minivec/proofs/proof_RawVec_T_ptr.v index e3696759ab0e64da81fffcaa221610eba8a43aff..543abc9279be1199ced0785e2a9c54464752f346 100644 --- a/case_studies/minivec/output/minivec/proofs/proof_RawVec_T_ptr.v +++ b/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. \ No newline at end of file +End proof. diff --git a/case_studies/minivec/output/minivec/proofs/proof_Vec_T_cap.v b/case_studies/minivec/output/minivec/proofs/proof_Vec_T_cap.v index 2c9f2f90c1453943ac068ddc7a0a99e310f5da9f..a2edd4bf66e33ebe48f2307be73c4f07563475e7 100644 --- a/case_studies/minivec/output/minivec/proofs/proof_Vec_T_cap.v +++ b/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. \ No newline at end of file +End proof. diff --git a/case_studies/minivec/output/minivec/proofs/proof_Vec_T_get.v b/case_studies/minivec/output/minivec/proofs/proof_Vec_T_get.v index df8cd1f60ccdcc8c3f22dd0b71ead3a79bb27465..453d1aa391e2e525325a1b7639d119b9c8679aa1 100644 --- a/case_studies/minivec/output/minivec/proofs/proof_Vec_T_get.v +++ b/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. \ No newline at end of file +End proof. diff --git a/case_studies/minivec/output/minivec/proofs/proof_Vec_T_get_mut.v b/case_studies/minivec/output/minivec/proofs/proof_Vec_T_get_mut.v index 459a0947c4b7d92ff4b2fdf00cac062a9c73eb30..0fe385cdcfd8e3f2f753789ff13b940cc3c9f828 100644 --- a/case_studies/minivec/output/minivec/proofs/proof_Vec_T_get_mut.v +++ b/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. diff --git a/case_studies/minivec/output/minivec/proofs/proof_Vec_T_get_unchecked.v b/case_studies/minivec/output/minivec/proofs/proof_Vec_T_get_unchecked.v index 590f7e77b5a1e4716cda7223e41e5a0f44305ba8..20ec98910bc76eae5c544969522ee2fda98538ae 100644 --- a/case_studies/minivec/output/minivec/proofs/proof_Vec_T_get_unchecked.v +++ b/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. diff --git a/case_studies/minivec/output/minivec/proofs/proof_Vec_T_get_unchecked_mut.v b/case_studies/minivec/output/minivec/proofs/proof_Vec_T_get_unchecked_mut.v index d800c749e0ed8409958be7f348923dfa2c0b5197..3558db864fa9bf4185c731170536ba72d7d5f4ff 100644 --- a/case_studies/minivec/output/minivec/proofs/proof_Vec_T_get_unchecked_mut.v +++ b/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. diff --git a/case_studies/minivec/output/minivec/proofs/proof_Vec_T_len.v b/case_studies/minivec/output/minivec/proofs/proof_Vec_T_len.v index dca1eb3ae7c4854ae6a6d57adab61065e152da05..bc28a31159ad84da5ad756b3c21700252540da37 100644 --- a/case_studies/minivec/output/minivec/proofs/proof_Vec_T_len.v +++ b/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. diff --git a/case_studies/minivec/output/minivec/proofs/proof_Vec_T_new.v b/case_studies/minivec/output/minivec/proofs/proof_Vec_T_new.v index 5fb51ac721bf2860df7c54653068c9bb6a2db917..35e97b838615faa21ad72eb1b391f633fa0d1d07 100644 --- a/case_studies/minivec/output/minivec/proofs/proof_Vec_T_new.v +++ b/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. \ No newline at end of file +End proof. diff --git a/case_studies/minivec/output/minivec/proofs/proof_Vec_T_pop.v b/case_studies/minivec/output/minivec/proofs/proof_Vec_T_pop.v index 5e2e97d31bc791a995a6ac36eb7cfffa9b172f4c..b7e5b5dab2a4eb2c0185be9ef9b522dcc957d56e 100644 --- a/case_studies/minivec/output/minivec/proofs/proof_Vec_T_pop.v +++ b/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. diff --git a/case_studies/minivec/output/minivec/proofs/proof_Vec_T_ptr.v b/case_studies/minivec/output/minivec/proofs/proof_Vec_T_ptr.v index 825aedc5deccdb0e1d80ab5ae6daf3c4334f2bd3..7ac80b9663704c9b68f230ba282fe9ff33fda74a 100644 --- a/case_studies/minivec/output/minivec/proofs/proof_Vec_T_ptr.v +++ b/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. \ No newline at end of file +End proof. diff --git a/case_studies/minivec/output/minivec/proofs/proof_Vec_T_push.v b/case_studies/minivec/output/minivec/proofs/proof_Vec_T_push.v index 318248a5350cc1f6cfb66c28946fd2b941637389..d55773241d8f2fbc7fe0af09b5a6ddf71179618c 100644 --- a/case_studies/minivec/output/minivec/proofs/proof_Vec_T_push.v +++ b/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. diff --git a/case_studies/minivec/output/minivec/proofs/proof_client_get_mut_client.v b/case_studies/minivec/output/minivec/proofs/proof_client_get_mut_client.v index 0141025a622c472281cda440f413585f35f5fd49..564a057ee770af73c4504b1106b9e5138474bd75 100644 --- a/case_studies/minivec/output/minivec/proofs/proof_client_get_mut_client.v +++ b/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. diff --git a/case_studies/tests/output/tests/proofs/proof_vec_client_init_vec.v b/case_studies/tests/output/tests/proofs/proof_vec_client_init_vec.v index 93b6af4f0c4f9ab255d735663b288ae5af94c043..ac2d665040ea84ecdffe10225427cdfc5dad1493 100644 --- a/case_studies/tests/output/tests/proofs/proof_vec_client_init_vec.v +++ b/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. diff --git a/case_studies/tests/src/lib.rs b/case_studies/tests/src/lib.rs index 38d66367d1c28dabd57205b62cc17a6315eec938..01cb8147d1b28ae9656d997f9aa02f77bdd4989f 100644 --- a/case_studies/tests/src/lib.rs +++ b/case_studies/tests/src/lib.rs @@ -6,5 +6,6 @@ mod enums; mod structs; mod char; mod traits; +mod statics; mod vec_client; diff --git a/case_studies/tests/src/statics.rs b/case_studies/tests/src/statics.rs new file mode 100644 index 0000000000000000000000000000000000000000..ce590e3af20ba73b77c767cc91d8df28d4b0002c --- /dev/null +++ b/case_studies/tests/src/statics.rs @@ -0,0 +1,9 @@ + +#[rr::name("MYINT")] +static MYINT: i32 = 42; + +#[rr::requires(#iris "initialized Ï€ \"MYINT\" 42")] +#[rr::returns("42")] +fn read_static_1() -> i32 { + MYINT +} diff --git a/rr_frontend/radium/src/code.rs b/rr_frontend/radium/src/code.rs index 0e20998038c3af1fb6e2e1b52e2761b1b5adbed1..16b29a8d3d9f44d2758992300b82f98ed10c3c46 100644 --- a/rr_frontend/radium/src/code.rs +++ b/rr_frontend/radium/src/code.rs @@ -193,6 +193,8 @@ pub enum Literal { LitU64(u64), LitU128(u128), LitBool(bool), + // name of the loc + LitLoc(String), // dummy literal for ZST values (e.g. ()) LitZST, //TODO: add chars @@ -214,6 +216,7 @@ impl Display for Literal { Self::LitU128(i) => format_int(i.to_string(), IntType::U128), Self::LitBool(b) => write!(f, "val_of_bool {}", b.to_string()), Self::LitZST => write!(f, "zst_val"), + Self::LitLoc(name) => write!(f, "{name}"), } } } @@ -811,9 +814,7 @@ impl FunctionCode { // format Coq parameters let mut formatted_params = String::with_capacity(20); - let mut sorted_params = self.required_parameters.clone(); - sorted_params.sort_by(|(a, _), (b, _)| a.cmp(b)); - for (ref name, ref ty) in sorted_params.iter() { + for (ref name, ref ty) in self.required_parameters.iter() { formatted_params.push_str(format!(" ({} : {})", name, ty).as_str()); } @@ -967,6 +968,8 @@ pub struct Function<'def> { layoutable_syntys: Vec<SynType>, /// Custom tactics for the generated proof manual_tactics: Vec<String>, + /// used statics + used_statics: Vec<StaticMeta<'def>>, /// invariants for loop head bbs loop_invariants: InvariantMap, @@ -989,7 +992,10 @@ impl<'def> Function<'def> { writeln!(f, "Definition {}_lemma (Ï€ : thread_id) : Prop :=", self.name())?; // write coq parameters - if !self.spec.coq_params.is_empty() || !self.other_functions.is_empty() { + let has_params = !self.spec.coq_params.is_empty() + || !self.other_functions.is_empty() + || !self.used_statics.is_empty(); + if has_params { write!(f, "∀ ")?; for param in self.spec.coq_params.iter() { // TODO use CoqParam::format instead @@ -1005,13 +1011,23 @@ impl<'def> Function<'def> { for (loc_name, _, _, _) in self.other_functions.iter() { write!(f, "({} : loc) ", loc_name)?; } + + // assume locations for statics + for s in self.used_statics.iter() { + write!(f, "({} : loc) ", s.loc_name)?; + } writeln!(f, ", ")?; } // assume Coq assumptions + // layoutable for st in self.layoutable_syntys.iter() { write!(f, "syn_type_is_layoutable ({}) →\n", st)?; } + // statics are registered + for s in self.used_statics.iter() { + write!(f, "static_is_registered \"{}\" {} (existT _ {}) →\n", s.ident, s.loc_name, s.ty)?; + } // write iris assums if self.other_functions.len() == 0 { @@ -1051,7 +1067,9 @@ impl<'def> Function<'def> { for names in self.generic_types.iter() { code_params.push(names.syn_type.clone()); } - code_params.sort(); + for s in self.used_statics.iter() { + code_params.push(s.loc_name.clone()); + } for x in code_params.iter() { write!(f, "{} ", x)?; } @@ -1245,6 +1263,14 @@ impl<'def> Function<'def> { } } +/// Information on a used static variable +#[derive(Debug, Clone)] +pub struct StaticMeta<'def> { + pub ident: String, + pub loc_name: String, + pub ty: Type<'def>, +} + /// A CaesiumFunctionBuilder allows to incrementally construct the functions's code and the spec /// at the same time. It ensures that both definitions line up in the right way (for instance, by /// ensuring that other functions are linked up in a consistent way). @@ -1269,6 +1295,8 @@ pub struct FunctionBuilder<'def> { generic_lifetimes: Vec<(Option<String>, Lft)>, /// Syntypes we assume to be layoutable in the typing proof layoutable_syntys: Vec<SynType>, + /// used statics + used_statics: Vec<StaticMeta<'def>>, /// manually specified tactics that will be emitted in the typing proof tactics: Vec<String>, @@ -1293,6 +1321,7 @@ impl<'def> FunctionBuilder<'def> { layoutable_syntys: Vec::new(), loop_invariants: InvariantMap(HashMap::new()), tactics: Vec::new(), + used_statics: Vec::new(), } } @@ -1313,6 +1342,12 @@ impl<'def> FunctionBuilder<'def> { self.rfn_types.push(t); } + /// Require a static variable to be in scope. + pub fn require_static(&mut self, s: StaticMeta<'def>) { + info!("Requiring static {:?}", s); + self.used_statics.push(s); + } + /// Adds a lifetime parameter to the function. pub fn add_universal_lifetime(&mut self, name: Option<String>, lft: Lft) -> Result<(), String> { self.generic_lifetimes.push((name, lft.to_string())); @@ -1407,6 +1442,11 @@ impl<'def> FunctionBuilder<'def> { impl<'def> Into<Function<'def>> for FunctionBuilder<'def> { fn into(mut self) -> Function<'def> { + // sort parameters for code + self.other_functions.sort_by(|a, b| a.0.cmp(&b.0)); + //self.generic_types.sort_by(|a, b| a.rust_name.cmp(&b.rust_name)); + self.used_statics.sort_by(|a, b| a.ident.cmp(&b.ident)); + // generate location parameters for other functions used by this one. let mut parameters: Vec<(CoqName, CoqType)> = self .other_functions @@ -1414,6 +1454,14 @@ impl<'def> Into<Function<'def>> for FunctionBuilder<'def> { .map(|f_inst| (CoqName::Named(f_inst.0.to_string()), CoqType::Loc)) .collect(); + // generate location parameters for statics used by this function + let mut statics_parameters = self + .used_statics + .iter() + .map(|s| (CoqName::Named(s.loc_name.to_string()), CoqType::Loc)) + .collect(); + parameters.append(&mut statics_parameters); + // add generic syntype parameters for generics that this function uses. let mut gen_st_parameters = self .generic_types @@ -1440,6 +1488,7 @@ impl<'def> Into<Function<'def>> for FunctionBuilder<'def> { layoutable_syntys: self.layoutable_syntys, loop_invariants: self.loop_invariants, manual_tactics: self.tactics, + used_statics: self.used_statics, } } } diff --git a/rr_frontend/radium/src/specs.rs b/rr_frontend/radium/src/specs.rs index 08beed8c2b7a41d096c7e64b05c1a23d04983a6f..ae25e1c3c842a560ab1ff3d031b57c08683e8620 100644 --- a/rr_frontend/radium/src/specs.rs +++ b/rr_frontend/radium/src/specs.rs @@ -1093,7 +1093,7 @@ impl InvariantSpec { let indent = " "; // the write_str impl will always return Ok. write!(out, "Section {}.\n", self.type_name).unwrap(); - write!(out, "{}Context `{{!typeGS Σ}}.\n", indent).unwrap(); + write!(out, "{}Context `{{!refinedrustGS Σ}}.\n", indent).unwrap(); // add type parameters if generic_params.len() > 0 { @@ -1294,7 +1294,7 @@ impl<'def> AbstractVariant<'def> { let indent = " "; write!(out, "Section {}.\n", self.sls_def_name).unwrap(); - write!(out, "{}Context `{{!typeGS Σ}}.\n", indent).unwrap(); + write!(out, "{}Context `{{!refinedrustGS Σ}}.\n", indent).unwrap(); // add syntype parameters let mut typarams = Vec::new(); @@ -1380,7 +1380,7 @@ impl<'def> AbstractVariant<'def> { let indent = " "; // the write_str impl will always return Ok. write!(out, "Section {}.\n", self.plain_ty_name).unwrap(); - write!(out, "{}Context `{{!typeGS Σ}}.\n", indent).unwrap(); + write!(out, "{}Context `{{!refinedrustGS Σ}}.\n", indent).unwrap(); // add type parameters, and build a list of terms to apply the sls def to if ty_params.len() > 0 { @@ -1866,7 +1866,7 @@ impl<'def> AbstractEnum<'def> { let indent = " "; write!(out, "Section {}.\n", self.els_def_name).unwrap(); - write!(out, "{}Context `{{!typeGS Σ}}.\n", indent).unwrap(); + write!(out, "{}Context `{{!refinedrustGS Σ}}.\n", indent).unwrap(); // add syntype parameters let mut typarams = Vec::new(); @@ -2072,7 +2072,7 @@ impl<'def> AbstractEnum<'def> { let indent = " "; // the write_str impl will always return Ok. write!(out, "Section {}.\n", self.plain_ty_name).unwrap(); - write!(out, "{}Context `{{!typeGS Σ}}.\n", indent).unwrap(); + write!(out, "{}Context `{{!refinedrustGS Σ}}.\n", indent).unwrap(); // add type parameters, and build a list of terms to apply the els def to if self.ty_params.len() > 0 { diff --git a/rr_frontend/translation/src/function_body.rs b/rr_frontend/translation/src/function_body.rs index 1aeaccef46d65d0457cb92b59541bc44e7420907..d33b3993806364fcfd7b7064b666ab2a6b13abff 100644 --- a/rr_frontend/translation/src/function_body.rs +++ b/rr_frontend/translation/src/function_body.rs @@ -144,8 +144,12 @@ impl<'def> ProcedureScope<'def> { } /// Register a function. - pub fn register_function(&mut self, did: &DefId, meta: ProcedureMeta) { - assert!(self.name_map.insert(*did, meta).is_none()); + pub fn register_function(&mut self, did: &DefId, meta: ProcedureMeta) -> Result<(), String> { + if let Some(_) = self.name_map.insert(*did, meta) { + Err(format!("function for defid {:?} has already been registered", did)) + } else { + Ok(()) + } } /// Provide the code for a translated function. @@ -173,6 +177,11 @@ impl<'def> ProcedureScope<'def> { } } +/// Scope of consts that are available +pub struct ConstScope<'def> { + pub statics: HashMap<DefId, radium::StaticMeta<'def>>, +} + pub struct FunctionTranslator<'a, 'def, 'tcx> { env: &'def Environment<'tcx>, /// this needs to be annotated with the right borrowck things @@ -184,6 +193,8 @@ pub struct FunctionTranslator<'a, 'def, 'tcx> { /// registry of other procedures procedure_registry: &'a ProcedureScope<'def>, + /// registry of consts + const_registry: &'a ConstScope<'def>, /// attributes on this function attrs: &'a [&'a rustc_ast::ast::AttrItem], /// polonius info for this function @@ -207,6 +218,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> FunctionTranslator<'a, 'def, 'tcx> { attrs: &'a [&'a rustc_ast::ast::AttrItem], ty_translator: &'def TypeTranslator<'def, 'tcx>, proc_registry: &'a ProcedureScope<'def>, + const_registry: &'a ConstScope<'def>, ) -> Result<Self, TranslationError> { let mut translated_fn = radium::FunctionBuilder::new(&meta.name, &meta.spec_name); @@ -366,6 +378,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> FunctionTranslator<'a, 'def, 'tcx> { ty_translator, inputs, output, + const_registry, }; Ok(t) }, @@ -613,6 +626,8 @@ impl<'a, 'def: 'a, 'tcx: 'def> FunctionTranslator<'a, 'def, 'tcx> { inputs: self.inputs, output: self.output, checked_op_temporaries: checked_op_locals, + const_registry: self.const_registry, + collected_statics: HashSet::new(), }; translator.translate() } @@ -640,12 +655,16 @@ struct BodyTranslator<'a, 'def, 'tcx> { /// (code_loc_parameter_name, spec_name, type_inst, syntype_of_all_args) collected_procedures: HashMap<(DefId, FnGenericKey<'tcx>), (String, String, Vec<radium::Type<'def>>, Vec<radium::SynType>)>, + /// used statics + collected_statics: HashSet<DefId>, /// tracking lifetime inclusions for the generation of lifetime inclusions inclusion_tracker: InclusionTracker<'a, 'tcx>, /// registry of other procedures procedure_registry: &'a ProcedureScope<'def>, + /// scope of used consts + const_registry: &'a ConstScope<'def>, /// attributes on this function attrs: &'a [&'a rustc_ast::ast::AttrItem], /// polonius info for this function @@ -766,6 +785,12 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> { ); } + // generate dependencies on statics + for did in self.collected_statics.iter() { + let s = self.const_registry.statics.get(did).unwrap(); + self.translated_fn.require_static(s.clone()); + } + self.ty_translator.leave_procedure(); Ok(self.translated_fn.into()) } @@ -2965,6 +2990,38 @@ impl<'a, 'def: 'a, 'tcx: 'def> BodyTranslator<'a, 'def, 'tcx> { }) } }, + TyKind::Ref(_, _, _) => match sc { + Scalar::Int(_) => { + unreachable!(); + }, + Scalar::Ptr(pointer, _) => { + let glob_alloc = self.env.tcx().global_alloc(pointer.provenance); + match glob_alloc { + rustc_middle::mir::interpret::GlobalAlloc::Static(did) => { + info!( + "Found static GlobalAlloc {:?} for Ref scalar {:?} at type {:?}", + did, sc, ty + ); + match self.const_registry.statics.get(&did) { + None => Err(TranslationError::UnknownError(format!( + "Did not find a registered static for GlobalAlloc {:?} for scalar {:?} at type {:?}; registered: {:?}", + glob_alloc, sc, ty, self.const_registry.statics + ))), + Some(s) => { + self.collected_statics.insert(did); + Ok(radium::Expr::Literal(radium::Literal::LitLoc(s.loc_name.clone()))) + }, + } + }, + _ => Err(TranslationError::UnsupportedFeature { + description: format!( + "Unsupported GlobalAlloc {:?} for scalar {:?} at type {:?}", + glob_alloc, sc, ty + ), + }), + } + }, + }, _ => Err(TranslationError::UnsupportedFeature { description: format!("Unsupported layout for const value: {:?}", ty), }), diff --git a/rr_frontend/translation/src/lib.rs b/rr_frontend/translation/src/lib.rs index 2ded3739a93ed36b85c887e41fe4a81fe93996e5..e0d6e99495b8c7740ae95f9187b9556c4e09b996 100644 --- a/rr_frontend/translation/src/lib.rs +++ b/rr_frontend/translation/src/lib.rs @@ -55,13 +55,16 @@ mod utils; use std::fs::File; +use const_parser::ConstAttrParser; use crate_parser::CrateAttrParser; use environment::Environment; -use function_body::{FunctionTranslator, ProcedureMode, ProcedureScope}; +use function_body::{ConstScope, FunctionTranslator, ProcedureMode, ProcedureScope}; use mod_parser::ModuleAttrParser; use parse::{MToken, Parse, ParseResult, ParseStream, Peek}; use spec_parsers::verbose_function_spec_parser::{get_export_as_attr, get_shim_attrs}; -use spec_parsers::{crate_attr_parser as crate_parser, module_attr_parser as mod_parser}; +use spec_parsers::{ + const_attr_parser as const_parser, crate_attr_parser as crate_parser, module_attr_parser as mod_parser, +}; use topological_sort::TopologicalSort; use type_translator::TypeTranslator; use {attribute_parse as parse, rrconfig}; @@ -98,6 +101,7 @@ fn order_adt_defs<'tcx>(deps: HashMap<DefId, HashSet<DefId>>) -> Vec<DefId> { pub struct VerificationCtxt<'tcx, 'rcx> { env: &'rcx Environment<'tcx>, procedure_registry: ProcedureScope<'rcx>, + const_registry: ConstScope<'rcx>, type_translator: &'rcx TypeTranslator<'rcx, 'tcx>, functions: &'rcx [LocalDefId], /// the second component determines whether to include it in the code file as well @@ -352,7 +356,7 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> { code_file .write( "Section code.\n\ - Context `{!typeGS Σ}.\n\ + Context `{!refinedrustGS Σ}.\n\ Open Scope printing_sugar.\n\n" .as_bytes(), ) @@ -370,7 +374,7 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> { .write( "\ Section specs.\n\ - Context `{!typeGS Σ}.\n\n" + Context `{!refinedrustGS Σ}.\n\n" .as_bytes(), ) .unwrap(); @@ -456,7 +460,7 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> { .write( "\ Section proof.\n\ - Context `{!typeGS Σ}.\n" + Context `{!refinedrustGS Σ}.\n" .as_bytes(), ) .unwrap(); @@ -500,7 +504,7 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> { write!( proof_file, "\ - From caesium Require Import lang notation.\n\ + From caesium Require Import lang notation.\n\ From refinedrust Require Import typing shims.\n\ From {}.{stem}.generated Require Import generated_code_{stem} generated_specs_{stem}.\n\ From {}.{stem}.generated Require Import generated_template_{}.\n", @@ -520,7 +524,7 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> { .write( "\ Section proof.\n\ - Context `{!typeGS Σ}.\n" + Context `{!refinedrustGS Σ}.\n" .as_bytes(), ) .unwrap(); @@ -690,7 +694,7 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> { (name {proof_module_path})\n\ (modules {})\n\ (theories stdpp iris Ltac2 Equations RecordUpdate lrust caesium lithium refinedrust {} {}.{}.generated))", - proof_modules.join(" "), extra_theories.join(" "), self.coq_path_prefix, stem).unwrap(); + proof_modules.join(" "), extra_theories.join(" "), self.coq_path_prefix, stem).unwrap(); } } @@ -713,7 +717,7 @@ fn register_shims<'rcx, 'tcx>(vcx: &mut VerificationCtxt<'tcx, 'rcx>) -> Result< shim.name.to_string(), function_body::ProcedureMode::Shim, ); - vcx.procedure_registry.register_function(&did, meta); + vcx.procedure_registry.register_function(&did, meta)?; }, _ => { println!("Warning: cannot find defid for shim {:?}, skipping", shim.path); @@ -772,7 +776,7 @@ fn get_most_restrictive_function_mode<'tcx, 'rcx>( } /// Register functions of the crate in the procedure registry. -fn register_functions<'rcx, 'tcx>(vcx: &mut VerificationCtxt<'tcx, 'rcx>) { +fn register_functions<'rcx, 'tcx>(vcx: &mut VerificationCtxt<'tcx, 'rcx>) -> Result<(), String> { for &f in vcx.functions { let mut mode = get_most_restrictive_function_mode(vcx, f.to_def_id()); @@ -793,7 +797,7 @@ fn register_functions<'rcx, 'tcx>(vcx: &mut VerificationCtxt<'tcx, 'rcx>) { annot.code_name, function_body::ProcedureMode::Shim, ); - vcx.procedure_registry.register_function(&f.to_def_id(), meta); + vcx.procedure_registry.register_function(&f.to_def_id(), meta)?; continue; } @@ -812,8 +816,9 @@ fn register_functions<'rcx, 'tcx>(vcx: &mut VerificationCtxt<'tcx, 'rcx>) { let meta = function_body::ProcedureMeta::new(spec_name, fname, mode); - vcx.procedure_registry.register_function(&f.to_def_id(), meta); + vcx.procedure_registry.register_function(&f.to_def_id(), meta)?; } + Ok(()) } fn propagate_attr_from_impl(it: &rustc_ast::ast::AttrItem) -> bool { @@ -860,6 +865,7 @@ fn translate_functions<'rcx, 'tcx>(vcx: &mut VerificationCtxt<'tcx, 'rcx>) { &filtered_attrs, &vcx.type_translator, &vcx.procedure_registry, + &vcx.const_registry, ); if mode.is_only_spec() { @@ -953,6 +959,44 @@ pub fn get_filtered_functions<'tcx>(env: &Environment<'tcx>) -> Vec<LocalDefId> functions_with_spec } +/// Get constants in the current scope. +pub fn register_consts<'rcx, 'tcx>(vcx: &mut VerificationCtxt<'tcx, 'rcx>) -> Result<(), String> { + let statics = vcx.env.get_statics(); + + for s in statics.iter() { + let ty: ty::EarlyBinder<ty::Ty<'tcx>> = vcx.env.tcx().type_of(s.to_def_id()); + + let const_attrs = utils::filter_tool_attrs(vcx.env.get_attributes(s.to_def_id())); + if const_attrs.is_empty() { + continue; + } + + let ty = ty.skip_binder(); + match vcx.type_translator.translate_type(&ty).map_err(|x| format!("{:?}", x)) { + Ok(translated_ty) => { + let full_name = type_translator::strip_coq_ident(&vcx.env.get_item_name(s.to_def_id())); + + let mut const_parser = const_parser::VerboseConstAttrParser::new(); + let const_spec = const_parser.parse_const_attrs(*s, &const_attrs)?; + + let name = const_spec.name; + let loc_name = format!("{name}_loc"); + + let meta = radium::StaticMeta { + ident: name, + loc_name, + ty: translated_ty, + }; + vcx.const_registry.statics.insert(s.to_def_id(), meta); + }, + Err(e) => { + println!("Warning: static {:?} has unsupported type, skipping: {:?}", s, e); + }, + } + } + Ok(()) +} + /// Get and parse all module attributes. pub fn get_module_attributes<'tcx>( env: &Environment<'tcx>, @@ -1060,6 +1104,7 @@ where // add includes to the shim registry let library_load_paths = rrconfig::lib_load_paths(); + info!("Loading libraries from {:?}", library_load_paths); let found_libs = scan_loadpaths(&library_load_paths).map_err(|e| e.to_string())?; info!("Found the following RefinedRust libraries in the loadpath: {:?}", found_libs); for incl in includes.iter() { @@ -1089,12 +1134,17 @@ where extra_imports: imports.into_iter().map(|x| (x, false)).collect(), coq_path_prefix: path_prefix, shim_registry, + const_registry: ConstScope { + statics: HashMap::new(), + }, }; - register_functions(&mut vcx); + register_functions(&mut vcx)?; register_shims(&mut vcx)?; + register_consts(&mut vcx)?; + translate_functions(&mut vcx); continuation(vcx); diff --git a/rr_frontend/translation/src/spec_parsers/const_attr_parser.rs b/rr_frontend/translation/src/spec_parsers/const_attr_parser.rs new file mode 100644 index 0000000000000000000000000000000000000000..26356948a706af35dedd5031e082da39e5b35c3d --- /dev/null +++ b/rr_frontend/translation/src/spec_parsers/const_attr_parser.rs @@ -0,0 +1,79 @@ +// © 2023, The RefinedRust Developers and Contributors +// +// This Source Code Form is subject to the terms of the BSD-3-clause License. +// If a copy of the BSD-3-clause license was not distributed with this +// file, You can obtain one at https://opensource.org/license/bsd-3-clause/. + +use attribute_parse as parse; +use radium::specs; +use rustc_ast::ast::AttrItem; +use rustc_hir::def_id::{DefId, LocalDefId}; + +use crate::spec_parsers::parse_utils; + +/// Parse attributes on a const. +/// Permitted attributes: +/// - rr::name("x"), which will introduce the name x to refer to the const in other specs +pub trait ConstAttrParser { + fn parse_const_attrs<'a>( + &'a mut self, + did: LocalDefId, + attrs: &'a [&'a AttrItem], + ) -> Result<ConstAttrs, String>; +} + +#[derive(Debug, Clone)] +pub struct ConstAttrs { + pub name: String, +} + +pub struct VerboseConstAttrParser {} + +impl VerboseConstAttrParser { + pub fn new() -> Self { + VerboseConstAttrParser {} + } +} + +impl ConstAttrParser for VerboseConstAttrParser { + fn parse_const_attrs<'a>( + &'a mut self, + _did: LocalDefId, + attrs: &'a [&'a AttrItem], + ) -> Result<ConstAttrs, String> { + fn str_err(e: parse::ParseError) -> String { + format!("{:?}", e) + } + + let meta = (); + let mut name: Option<String> = None; + + for &it in attrs.iter() { + let ref path_segs = it.path.segments; + let ref args = it.args; + + if let Some(seg) = path_segs.get(1) { + let buffer = parse::ParseBuffer::new(&it.args.inner_tokens()); + match &*seg.ident.name.as_str() { + "name" => { + let parsed_name: parse::LitStr = buffer.parse(&meta).map_err(str_err)?; + if name.is_some() { + return Err(format!("name attribute has already been specified")); + } + name = Some(parsed_name.value()); + }, + _ => { + return Err(format!("unknown attribute for const specification: {:?}", args)); + }, + } + } + } + if name.is_none() { + Err(format!("no name attribute specified on const")) + } else { + Ok(ConstAttrs { + name: name.unwrap(), + }) + } + } +} diff --git a/rr_frontend/translation/src/spec_parsers/mod.rs b/rr_frontend/translation/src/spec_parsers/mod.rs index 318330ed3e67a08150e574e79ef715acd7f9a9af..3135ad62c0792ef7465d76ad6c8e0c0c94807db8 100644 --- a/rr_frontend/translation/src/spec_parsers/mod.rs +++ b/rr_frontend/translation/src/spec_parsers/mod.rs @@ -1,3 +1,4 @@ +pub mod const_attr_parser; pub mod crate_attr_parser; pub mod enum_spec_parser; pub mod module_attr_parser; diff --git a/rr_frontend/translation/src/spec_parsers/parse_utils.rs b/rr_frontend/translation/src/spec_parsers/parse_utils.rs index f6cb72c64edd06884d1d7ac14d0f178f85ba8b90..fc147eb371fe47d25ab3f8a14ab7e0d9bad6aed0 100644 --- a/rr_frontend/translation/src/spec_parsers/parse_utils.rs +++ b/rr_frontend/translation/src/spec_parsers/parse_utils.rs @@ -233,6 +233,14 @@ impl<'a> parse::Parse<ParseMeta<'a>> for RRCoqContextItem { pub type ParseMeta<'a> = (&'a [specs::LiteralTyParam], &'a [(Option<String>, specs::Lft)]); +/// Handle escape sequences in the given string. +pub(crate) fn handle_escapes(s: &str) -> String { + let s = String::from(s); + let s = s.replace("\\\"", "\""); + + s +} + /// Processes a literal Coq term annotated via an attribute. /// In particular, processes escapes `{...}` and replaces them via their interpretation, see /// below for supported escape sequences. @@ -251,6 +259,8 @@ pub(crate) fn process_coq_literal(s: &str, meta: ParseMeta<'_>) -> (String, spec let mut literal_lfts: HashSet<String> = HashSet::new(); let mut literal_tyvars: HashSet<specs::LiteralTyParam> = HashSet::new(); + let s = handle_escapes(s); + /* regexes: * - '{\s*rt_of\s+([[:alpha:]])\s*}' replace by lookup of the refinement type name * - '{\s*st_of\s+([[:alpha:]])\s*}' replace by lookup of the syntype name @@ -280,7 +290,7 @@ pub(crate) fn process_coq_literal(s: &str, meta: ParseMeta<'_>) -> (String, spec return None; }; - let cs = s; + let cs = &s; let cs = RE_RT_OF.replace_all(cs, |c: &Captures<'_>| { let t = &c[2]; let param = specs::lookup_ty_param(t, params); diff --git a/stdlib/option/extra_specs.v b/stdlib/option/extra_specs.v index aadd2c489e0280bc6b0edddd6bea9ae2968b704a..2470f41a8970663ea98f542db4ccb76654626726 100644 --- a/stdlib/option/extra_specs.v +++ b/stdlib/option/extra_specs.v @@ -1,11 +1,8 @@ -Section subtype. - Context `{!typeGS Σ}. - (* NOTE: variance proofs are currently not automatically generated by the frontend *) - Lemma Option_ty_weak_subtype E L {T_rt1 T_rt2} (T_ty1 : type T_rt1) (T_ty2 : type T_rt2) r1 r2 T : - (∃ r2', ⌜ r2 = Some (#r2')⌠∗ weak_subtype E L r1 r2' T_ty1 T_ty2 T) ⊢ - weak_subtype E L (Some (#r1)) r2 (Option_ty T_ty1) (Option_ty T_ty2) T. - Proof. - Admitted. - Global Instance Option_ty_weak_subtype_inst E L {T_rt1 T_rt2} (T_ty1 : type T_rt1) (T_ty2 : type T_rt2) r1 r2 : - Subtype E L (Some (#r1)) r2 (Option_ty T_ty1) (Option_ty T_ty2) := λ T, i2p (Option_ty_weak_subtype E L T_ty1 T_ty2 r1 r2 T). -End subtype. +(* NOTE: variance proofs are currently not automatically generated by the frontend *) +Lemma Option_ty_weak_subtype E L {T_rt1 T_rt2} (T_ty1 : type T_rt1) (T_ty2 : type T_rt2) r1 r2 T : + (∃ r2', ⌜ r2 = Some (#r2')⌠∗ weak_subtype E L r1 r2' T_ty1 T_ty2 T) ⊢ + weak_subtype E L (Some (#r1)) r2 (Option_ty T_ty1) (Option_ty T_ty2) T. +Proof. +Admitted. +Global Instance Option_ty_weak_subtype_inst E L {T_rt1 T_rt2} (T_ty1 : type T_rt1) (T_ty2 : type T_rt2) r1 r2 : +Subtype E L (Some (#r1)) r2 (Option_ty T_ty1) (Option_ty T_ty2) := λ T, i2p (Option_ty_weak_subtype E L T_ty1 T_ty2 r1 r2 T). diff --git a/stdlib/result/extra_specs.v b/stdlib/result/extra_specs.v index 1c0cf50a0cb06aa4fa5488cf9c6521a36bfc43c5..01dc49880da3e56c40c4bc642695469e58eec8c0 100644 --- a/stdlib/result/extra_specs.v +++ b/stdlib/result/extra_specs.v @@ -1,17 +1,17 @@ (* NOTE: variance proofs are currently not automatically generated by the frontend *) -Lemma core_result_Result_ty_weak_subtype_Ok E L {T_rt1 T_rt2 U_rt} (T_ty1 : type T_rt1) (T_ty2 : type T_rt2) (U_ty1 : type U_rt) (U_ty2 : type U_rt) r1 r2 T : +Lemma Result_ty_weak_subtype_Ok E L {T_rt1 T_rt2 U_rt} (T_ty1 : type T_rt1) (T_ty2 : type T_rt2) (U_ty1 : type U_rt) (U_ty2 : type U_rt) r1 r2 T : weak_subtype E L r1 r2 T_ty1 T_ty2 (mut_subtype E L U_ty1 U_ty2 T) ⊢ - weak_subtype E L (Ok (#r1)) (Ok (#r2)) (core_result_Result_ty T_ty1 U_ty1) (core_result_Result_ty T_ty2 U_ty2) T. + weak_subtype E L (Ok (#r1)) (Ok (#r2)) (Result_ty T_ty1 U_ty1) (Result_ty T_ty2 U_ty2) T. Proof. Admitted. -Global Instance core_result_Result_ty_weak_subtype_Ok_inst E L {T_rt1 T_rt2 U_rt} (T_ty1 : type T_rt1) (T_ty2 : type T_rt2) (U_ty1 U_ty2 : type U_rt) r1 r2 : -Subtype E L (Ok (#r1)) (Ok (#r2)) (core_result_Result_ty T_ty1 U_ty1) (core_result_Result_ty T_ty2 U_ty2) := λ T, i2p (core_result_Result_ty_weak_subtype_Ok E L T_ty1 T_ty2 U_ty1 U_ty2 r1 r2 T). +Global Instance Result_ty_weak_subtype_Ok_inst E L {T_rt1 T_rt2 U_rt} (T_ty1 : type T_rt1) (T_ty2 : type T_rt2) (U_ty1 U_ty2 : type U_rt) r1 r2 : +Subtype E L (Ok (#r1)) (Ok (#r2)) (Result_ty T_ty1 U_ty1) (Result_ty T_ty2 U_ty2) := λ T, i2p (Result_ty_weak_subtype_Ok E L T_ty1 T_ty2 U_ty1 U_ty2 r1 r2 T). -Lemma core_result_Result_ty_weak_subtype_Err E L {T_rt U_rt1 U_rt2} (T_ty1 T_ty2 : type T_rt) (U_ty1 : type U_rt1) (U_ty2 : type U_rt2) r1 r2 T : +Lemma Result_ty_weak_subtype_Err E L {T_rt U_rt1 U_rt2} (T_ty1 T_ty2 : type T_rt) (U_ty1 : type U_rt1) (U_ty2 : type U_rt2) r1 r2 T : mut_subtype E L T_ty1 T_ty2 (weak_subtype E L r1 r2 U_ty1 U_ty2 T) ⊢ - weak_subtype E L (Err (#r1)) (Err (#r2)) (core_result_Result_ty T_ty1 U_ty1) (core_result_Result_ty T_ty2 U_ty2) T. + weak_subtype E L (Err (#r1)) (Err (#r2)) (Result_ty T_ty1 U_ty1) (Result_ty T_ty2 U_ty2) T. Proof. Admitted. -Global Instance core_result_Result_ty_weak_subtype_Err_inst E L {T_rt U_rt1 U_rt2} (T_ty1 T_ty2 : type T_rt) (U_ty1 : type U_rt1) (U_ty2 : type U_rt2) r1 r2 : -Subtype E L (Err (#r1)) (Err (#r2)) (core_result_Result_ty T_ty1 U_ty1) (core_result_Result_ty T_ty2 U_ty2) := λ T, i2p (core_result_Result_ty_weak_subtype_Err E L T_ty1 T_ty2 U_ty1 U_ty2 r1 r2 T). +Global Instance Result_ty_weak_subtype_Err_inst E L {T_rt U_rt1 U_rt2} (T_ty1 T_ty2 : type T_rt) (U_ty1 : type U_rt1) (U_ty2 : type U_rt2) r1 r2 : +Subtype E L (Err (#r1)) (Err (#r2)) (Result_ty T_ty1 U_ty1) (Result_ty T_ty2 U_ty2) := λ T, i2p (Result_ty_weak_subtype_Err E L T_ty1 T_ty2 U_ty1 U_ty2 r1 r2 T). diff --git a/stdlib/result/src/lib.rs b/stdlib/result/src/lib.rs index 9db7f1400ee4d34488e95d68a322a827387881c8..408ee0afbba375573f988e4c293eed55aa22ac1a 100644 --- a/stdlib/result/src/lib.rs +++ b/stdlib/result/src/lib.rs @@ -8,13 +8,13 @@ use std::fmt; #[rr::export_as(core::result::Result)] -#[rr::refined_by("result {rt_of T} {rt_of E}")] +#[rr::refined_by("result (place_rfn {rt_of T}) (place_rfn {rt_of E})")] pub enum Result<T, E> { #[rr::pattern("Ok" $ "x")] - #[rr::refinement("-[#x]")] + #[rr::refinement("-[x]")] Ok(T), #[rr::pattern("Err" $ "x")] - #[rr::refinement("-[#x]")] + #[rr::refinement("-[x]")] Err(E), } @@ -37,7 +37,7 @@ impl<T, E> Result<T, E> { } #[rr::params("x")] - #[rr::args("Ok x")] + #[rr::args("Ok (#x)")] #[rr::returns("x")] pub fn unwrap(self) -> T where E: fmt::Debug { unimplemented!(); diff --git a/stdlib/result/theories/result.v b/stdlib/result/theories/result.v index 778fe193970ddd46a45aa09214e6df9ae9430f2f..45a5e30eb41f58a69f04b63932bc01842be99c38 100644 --- a/stdlib/result/theories/result.v +++ b/stdlib/result/theories/result.v @@ -27,3 +27,30 @@ Proof. - left. eexists _. done. Defined. + +Definition if_Ok {A B} (x : result A B) (Ï• : A → Prop) : Prop := + match x with + | Ok x => Ï• x + | _ => True + end. +Definition if_Err {A B} (x : result A B) (Ï• : B → Prop) : Prop := + match x with + | Err x => Ï• x + | _ => True + end. + +(** The same for Iris *) +Section iris. +Context `{!typeGS Σ}. + +Definition if_iOk {A B} (x : result A B) (Ï• : A → iProp Σ) : iProp Σ := + match x with + | Ok x => Ï• x + | _ => True + end. +Definition if_iErr {A B} (x : result A B) (Ï• : B → iProp Σ) : iProp Σ := + match x with + | Err x => Ï• x + | _ => True + end. +End iris. diff --git a/stdlib/spin/theories/once/once_ghost_state.v b/stdlib/spin/theories/once/once_ghost_state.v index 66b948eba3e420589df6d90581e1c2bf1e7880d8..603dc06932f785453f8684873bfd7ce77c0991b9 100644 --- a/stdlib/spin/theories/once/once_ghost_state.v +++ b/stdlib/spin/theories/once/once_ghost_state.v @@ -19,20 +19,13 @@ Section once. Context `{onceG Σ A}. Definition once_uninit_tok_def γ := own γ (Cinl (1/2)%Qp). - Definition once_uninit_tok_aux : seal (@once_uninit_tok_def). Proof. by eexists. Qed. - Definition once_uninit_tok := once_uninit_tok_aux.(unseal). - Definition once_uninit_tok_eq : @once_uninit_tok = @once_uninit_tok_def := once_uninit_tok_aux.(seal_eq). - Definition once_init_tok_def γ (a : A) := own γ (Cinr (to_agree (a : leibnizO A))). - Definition once_init_tok_aux : seal (@once_init_tok_def). Proof. by eexists. Qed. - Definition once_init_tok := once_init_tok_aux.(unseal). - Definition once_init_tok_eq : @once_init_tok = @once_init_tok_def := once_init_tok_aux.(seal_eq). Definition once_status_tok_def γ (a : option A) := match a with - | None => once_uninit_tok γ - | Some a => once_init_tok γ a + | None => once_uninit_tok_def γ + | Some a => once_init_tok_def γ a end. Definition once_status_tok_aux : seal (@once_status_tok_def). Proof. by eexists. Qed. Definition once_status_tok := once_status_tok_aux.(unseal). @@ -40,18 +33,18 @@ Section once. Lemma once_uninit_tok_alloc : - ⊢ |==> ∃ γ, once_uninit_tok γ ∗ once_uninit_tok γ. + ⊢ |==> ∃ γ, once_status_tok γ None ∗ once_status_tok γ None. Proof. - rewrite once_uninit_tok_eq /once_uninit_tok_def. + rewrite once_status_tok_eq /once_status_tok_def. setoid_rewrite <-own_op. rewrite -Cinl_op frac_op Qp.half_half. iApply own_alloc. done. Qed. Lemma once_uninit_tok_init γ a : - once_uninit_tok γ -∗ once_uninit_tok γ -∗ |==> once_init_tok γ a. + once_status_tok γ None -∗ once_status_tok γ None -∗ |==> once_status_tok γ (Some a). Proof. - rewrite once_uninit_tok_eq once_init_tok_eq. + rewrite once_status_tok_eq. iIntros "Ha Hb". iCombine "Ha Hb" as "Ha". rewrite -Cinl_op frac_op Qp.half_half. @@ -59,114 +52,74 @@ Section once. by apply cmra_update_exclusive. Qed. - Global Instance once_init_tok_persistent γ a : Persistent (once_init_tok γ a). - Proof. rewrite once_init_tok_eq. apply _. Qed. Global Instance once_status_tok_persistent γ a : Persistent (once_status_tok γ (Some a)). Proof. rewrite once_status_tok_eq. apply _. Qed. Lemma once_uninit_init_tok_False γ a : - once_uninit_tok γ -∗ once_init_tok γ a -∗ False. + once_status_tok γ None -∗ once_status_tok γ (Some a) -∗ False. Proof. - iIntros "H1 H2". rewrite once_uninit_tok_eq once_init_tok_eq. + iIntros "H1 H2". rewrite once_status_tok_eq. iDestruct (own_valid_2 with "H1 H2") as %Hv. done. Qed. Lemma once_uninit_uninit_tok_False γ : - once_uninit_tok γ -∗ once_uninit_tok γ -∗ once_uninit_tok γ -∗ False. + once_status_tok γ None -∗ once_status_tok γ None -∗ once_status_tok γ None -∗ False. Proof. - iIntros "H1 H2 H3". rewrite once_uninit_tok_eq. + iIntros "H1 H2 H3". rewrite once_status_tok_eq. iDestruct (own_valid_3 with "H1 H2 H3") as %Hv. done. Qed. Lemma once_init_tok_agree γ a b : - once_init_tok γ a -∗ once_init_tok γ b -∗ ⌜a = bâŒ. + once_status_tok γ (Some a) -∗ once_status_tok γ (Some b) -∗ ⌜a = bâŒ. Proof. - iIntros "H1 H2". rewrite once_init_tok_eq. + iIntros "H1 H2". rewrite once_status_tok_eq. iDestruct (own_valid_2 with "H1 H2") as %Hv. iPureIntro. by apply to_agree_op_inv_L in Hv. Qed. - Global Instance once_init_tok_timeless γ a : Timeless (once_init_tok γ a). - Proof. rewrite once_init_tok_eq. apply _. Qed. - Global Instance once_uninit_tok_timeless γ : Timeless (once_uninit_tok γ). - Proof. rewrite once_uninit_tok_eq. apply _. Qed. + Global Instance once_init_tok_timeless γ a : Timeless (once_status_tok γ a). + Proof. rewrite once_status_tok_eq; destruct a; apply _. Qed. End once. +Notation once_uninit_tok γ := (once_status_tok γ None). +Notation once_init_tok γ a := (once_status_tok γ (Some a)). + Section typing. Context {A} `{!typeGS Σ} `{!onceG Σ A}. - Lemma subsume_once_status γ a b T : + Lemma subsume_once_status_tok γ a b T : subsume (once_status_tok γ a) (once_status_tok γ b) T :- exhale ⌜a = bâŒ; return T. Proof. iIntros "(-> & HT)". iIntros "$"; done. Qed. - Definition subsume_once_status_inst := [instance subsume_once_status]. - Global Existing Instance subsume_once_status_inst. + Definition subsume_once_status_tok_inst := [instance subsume_once_status_tok]. + Global Existing Instance subsume_once_status_tok_inst. - Definition FindOnceStatus γ : find_in_context_info := + Definition FindOnceStatusTok γ : find_in_context_info := {| fic_A := option A; fic_Prop a := once_status_tok γ a |}. - Global Instance once_status_related γ a : RelatedTo (once_status_tok γ a) := {| rt_fic := FindOnceStatus γ |}. + Global Instance once_status_tok_related γ a : RelatedTo (once_status_tok γ a) := {| rt_fic := FindOnceStatusTok γ |}. +End typing. - (* - Lemma subsume_once_init γ a b T : - subsume (once_init_tok γ a) (once_init_tok γ b) T :- - exhale ⌜a = bâŒ; return T. - Proof. - iIntros "(-> & HT)". - iIntros "$"; done. - Qed. - Definition subsume_once_init_inst := [instance subsume_once_init]. - Global Existing Instance subsume_once_init_inst. +(** Since a frequent use case of once is in conjunction with static variables, we provide some extra support for that *) +Section statics. + Context {A} `{!typeGS Σ} `{!staticGS Σ} `{!onceG Σ A}. - Lemma subsume_once_init_status γ a b T : - subsume (once_init_tok γ a) (once_status_tok γ b) T :- - exhale ⌜b = Some aâŒ; return T. - Proof. - iIntros "(-> & HT)". - rewrite once_status_tok_eq/=. - iIntros "$"; done. - Qed. - Definition subsume_once_init_status_inst := [instance subsume_once_init_status]. - Global Existing Instance subsume_once_init_status_inst. + Definition once_status Ï€ (s : string) (a : option A) : iProp Σ := + ∃ γ, once_status_tok γ a ∗ initialized Ï€ s γ. + Global Typeclasses Opaque once_status. - Lemma subsume_once_uninit γ T : - subsume (once_uninit_tok γ) (once_uninit_tok γ) T :- - return T. - Proof. - iIntros "HT $"; done. - Qed. - Definition subsume_once_uninit_inst := [instance subsume_once_uninit]. - Global Existing Instance subsume_once_uninit_inst. - - Lemma subsume_once_uninit_status γ b T : - subsume (once_uninit_tok γ) (once_status_tok γ b) T :- - exhale ⌜b = NoneâŒ; return T. + Definition FindOnceStatus Ï€ s : find_in_context_info := + {| fic_A := option A; fic_Prop a := once_status Ï€ s a |}. + Global Instance once_status_related Ï€ s a : RelatedTo (once_status Ï€ s a) := {| rt_fic := FindOnceStatus Ï€ s |}. + Lemma subsume_once_status Ï€ s a b T : + subsume (once_status Ï€ s a) (once_status Ï€ s b) T :- + exhale ⌜a = bâŒ; return T. Proof. iIntros "(-> & HT)". - rewrite once_status_tok_eq/=. iIntros "$"; done. Qed. - Definition subsume_once_uninit_status_inst := [instance subsume_once_uninit_status]. - Global Existing Instance subsume_once_uninit_status_inst. - - Definition FindOnceInit γ : find_in_context_info := - {| fic_A := A; fic_Prop a := once_init_tok γ a |}. - Global Instance once_init_related γ a : RelatedTo (once_init_tok γ a) := {| rt_fic := FindOnceInit γ |}. - - Definition FindOnceUninit γ : find_in_context_info := - {| fic_A := unit; fic_Prop a := once_uninit_tok γ |}. - Global Instance once_uninit_related γ : RelatedTo (once_uninit_tok γ) := {| rt_fic := FindOnceUninit γ |}. - - Definition simplify_hyp_once_status_init : - simplify_hyp - *) - - (* TODO: first add infrastructure for associating ghost state with locations - Definition once_status (l : loc) (x : option A) := - ∃ γ, ghost_loc_map l γ ∗ once_status_tok γ x. - *) -End typing. +End statics. diff --git a/theories/rust_typing/owned_ptr.v b/theories/rust_typing/owned_ptr.v index 5e6893d361ae14cbc11ec887bd8aa64bf527cfa2..3e11ead5889b807cc5ce88806a1ba72725ee11c4 100644 --- a/theories/rust_typing/owned_ptr.v +++ b/theories/rust_typing/owned_ptr.v @@ -154,6 +154,24 @@ Section owned_ptr. End owned_ptr. +Section ofty. + Context `{!typeGS Σ}. + + (** A very fundamental equivalence that should hold. *) + Lemma owned_ptr_ofty_owned_equiv {rt} (ty : type rt) Ï€ l r : + l â—â‚—[Ï€, Owned true] #r @ (â— ty) ⊣⊢ l â—áµ¥{Ï€} (#r, l) @ owned_ptr ty. + Proof. + rewrite ltype_own_ofty_unfold/lty_of_ty_own {2}/ty_own_val/=. + iSplit. + - iIntros "(%ly & %Hst & %Hly & #Hsc & #Hlb & (? & ?) & %r' & <- & Hb)". + iExists _. iR. iR. iR. iFrame "# ∗". iExists _. iR. iFrame. + - iIntros "(%ly & %Hl & % & % & #Hlb & #Hsc & ? & ? & %r' & -> & Hb)". + apply val_of_loc_inj in Hl. subst. + iExists _. iR. iR. iFrame "# ∗". + iExists _. iR. done. + Qed. +End ofty. + Section subltype. Context `{!typeGS Σ}. diff --git a/theories/rust_typing/references.v b/theories/rust_typing/references.v index 45c7ca9276cb2d4b6036951bf2a8ee3e487b0497..3cd348249aafbd5cff3d717e967bb08822200ca1 100644 --- a/theories/rust_typing/references.v +++ b/theories/rust_typing/references.v @@ -199,6 +199,23 @@ Section mut_ref. Qed. End mut_ref. +Section ofty. + Context `{!typeGS Σ}. + + (** A very fundamental equivalence that should hold. *) + Lemma mut_ref_ofty_uniq_equiv {rt} (ty : type rt) Ï€ κ l r γ : + l â—â‚—[Ï€, Uniq κ γ] #r @ (â— ty) ⊣⊢ l â—áµ¥{Ï€} (#r, γ) @ mut_ref ty κ. + Proof. + rewrite ltype_own_ofty_unfold/lty_of_ty_own {3}/ty_own_val/=. + iSplit. + - iIntros "(%ly & %Hst & %Hly & #Hsc & #Hlb & Hc & Hobs & Hb)". + iExists _, _. iR. iR. iR. iFrame "# ∗". + -iIntros "(%l' & %ly & %Hl & % & % & #Hlb & #Hsc & Hobs & Hc & Hb)". + apply val_of_loc_inj in Hl. subst. + iExists _. iR. iR. iFrame "# ∗". + Qed. +End ofty. + Section subtype. Context `{!typeGS Σ}. @@ -1768,6 +1785,23 @@ Section shr_ref. Qed. End shr_ref. +Section ofty. + Context `{!typeGS Σ}. + + (** A very fundamental equivalence that should hold *) + Lemma shr_ref_ofty_shared_equiv {rt} (ty : type rt) Ï€ κ l r : + l â—â‚—[Ï€, Shared κ] #r @ (â— ty) ⊣⊢ l â—áµ¥{Ï€} #r @ shr_ref ty κ. + Proof. + rewrite ltype_own_ofty_unfold/lty_of_ty_own /ty_own_val/=. + iSplit. + - iIntros "(%ly & %Hst & %Hly & #Hsc & #Hlb & %r' & <- & #Ha)". + iExists _, _, _. iR. iR. iR. iFrame "#". done. + -iIntros "(%l' & %ly & %r' & %Hl & % & % & #Hsc & #Hlb & <- & #Ha)". + apply val_of_loc_inj in Hl. subst. + iExists _. iR. iR. iFrame "#". iExists _. iR. done. + Qed. +End ofty. + Section subtype. Context `{typeGS Σ}. diff --git a/theories/rust_typing/static.v b/theories/rust_typing/static.v new file mode 100644 index 0000000000000000000000000000000000000000..a963676da0b087260599202834e0236f74df13d7 --- /dev/null +++ b/theories/rust_typing/static.v @@ -0,0 +1,106 @@ +From refinedrust Require Import base type ltypes programs references. +From iris.base_logic Require Import ghost_map. + +(* TODO: should require that type is Send? *) +Class staticGS `{!typeGS Σ} := { + static_locs : gmap string loc; + static_types : gmap string (sigT type); +}. +Global Arguments staticGS _ {_}. + + +Section statics. + Context `{!typeGS Σ} `{!staticGS Σ}. + + (** Assertion stating that the static with name [x] has been registered for location [l] and type [ty]. *) + (** We assume registration for the expected type and the location parameter in the context where we verify our code *) + Definition static_is_registered (x : string) (l : loc) (ty : sigT type) := + static_locs !! x = Some l ∧ static_types !! x = Some ty. + + Import EqNotations. + + (* The global variable "name" has been initialized with refinement "r" *) + Definition initialized {rt} (Ï€ : thread_id) (name : string) (r : rt) : iProp Σ := + ∃ (l : loc) (ty : sigT type), ⌜static_is_registered name l ty⌠∗ + ∃ (Heq : rt = projT1 ty), + (l â—áµ¥{Ï€} (rew Heq in #r) @ shr_ref (projT2 ty) static)%I. + + Global Instance initialized_persistent {rt} (Ï€ : thread_id) (name : string) (r : rt) : + Persistent (initialized Ï€ name r). + Proof. apply _. Qed. + + Global Instance initialized_intro_persistent {rt} (Ï€ : thread_id) name (r : rt) : + IntroPersistent (initialized Ï€ name r) (initialized Ï€ name r). + Proof. constructor. iIntros "#$". Qed. + + (* On introduction of `initialized`, destruct it *) + Lemma simplify_initialized_hyp {rt} Ï€ (x : rt) name ty l + `{!TCFastDone (static_is_registered name l ty)} T: + (∃ (Heq : rt = projT1 ty), l â—áµ¥{Ï€} (rew Heq in #x) @ shr_ref (projT2 ty) static -∗ T) + ⊢ simplify_hyp (initialized Ï€ name x) T. + Proof. + unfold TCFastDone in *. destruct ty as [rt' ty]. + iDestruct 1 as (?) "HT". subst; simpl in *. + iIntros "Hinit". + iDestruct "Hinit" as "(%l' & %ty' & %Hlook1' & %Heq & Hl)". + destruct ty' as (rt & ty'). subst. simpl in *. + repeat match goal with | H : static_is_registered _ _ _ |- _ => destruct H end. + simplify_eq. + match goal with | H : existT _ _ = existT _ _ |- _ => apply existT_inj in H end. + subst. iApply ("HT" with "Hl"). + Qed. + Definition simplify_initialized_hyp_inst := [instance @simplify_initialized_hyp with 0%N]. + Global Existing Instance simplify_initialized_hyp_inst. + + Lemma initialized_intro {rt} Ï€ ty name l (x : rt) : + static_is_registered name l ty → + (∃ (Heq : rt = projT1 ty), l â—áµ¥{Ï€} (rew Heq in #x) @ shr_ref (projT2 ty) static) -∗ + initialized Ï€ name x. + Proof. iIntros (?) "Hl". iExists _, _. by iFrame. Qed. + + Lemma simplify_initialized_goal {rt} Ï€ (x : rt) name l ty + `{!TCFastDone (static_is_registered name l ty)} T: + (∃ (Heq : rt = projT1 ty), l â—áµ¥{Ï€} (rew Heq in #x) @ shr_ref (projT2 ty) static ∗ T) + ⊢ simplify_goal (initialized Ï€ name x) T. + Proof. + unfold TCFastDone in *. iIntros "[% [? $]]". subst. + iApply initialized_intro; [done..|]. by iExists _. + Qed. + Definition simplify_initialized_goal_inst := [instance @simplify_initialized_goal with 0%N]. + Global Existing Instance simplify_initialized_goal_inst. + + (** Subsumption *) + Definition FindInitialized (Ï€ : thread_id) (rt : Type) (name : string) := + {| fic_A := rt; fic_Prop r := (initialized Ï€ name r); |}. + Global Instance related_to_initialized (Ï€ : thread_id) {rt} name (r : rt) : + RelatedTo (initialized Ï€ name r) := + {| rt_fic := FindInitialized Ï€ rt name|}. + + Set Printing Universes. + Lemma find_in_context_initialized Ï€ name rt (T : rt → iProp Σ): + (∃ x, initialized Ï€ name x ∗ T x) + ⊢ find_in_context (FindInitialized Ï€ rt name) T. + Proof. iDestruct 1 as (x) "[Hinit HT]". iExists _. iFrame. Qed. + Definition find_in_context_initialized_inst := + [instance find_in_context_initialized with FICSyntactic]. + Global Existing Instance find_in_context_initialized_inst | 1. + + Lemma subsume_initialized Ï€ {rt} name (r1 r2 : rt) T: + (⌜r1 = r2⌠∗ T) + ⊢ subsume (initialized Ï€ name r1) (initialized Ï€ name r2) T. + Proof. iIntros "(-> & HT) ?". iFrame. Qed. + Definition subsume_initialized_inst := [instance subsume_initialized]. + Global Existing Instance subsume_initialized_inst. +End statics. +Global Typeclasses Opaque initialized. + +(* After calling adequacy: + we need to create initialized things. + then we can provide them to the proof. + + Users of initialized should unpack that hypothesis to get access to the type assignment. + This type assignment then allows us to call methods etc on the global variable. + + *) + + diff --git a/theories/rust_typing/typing.v b/theories/rust_typing/typing.v index b674dacaead5ad0a4e3c2442ab697aefc53c8dea..452621045e5410c4e3003c7b77e09b8f0ef132e8 100644 --- a/theories/rust_typing/typing.v +++ b/theories/rust_typing/typing.v @@ -1,6 +1,26 @@ -From refinedrust Require Export type program_rules int int_rules products references functions uninit box programs enum maybe_uninit alias_ptr existentials arrays value. +From refinedrust Require Export static type program_rules int int_rules products references functions uninit box programs enum maybe_uninit alias_ptr existentials arrays value. From refinedrust Require Export automation.loc_eq manual automation. Global Open Scope Z_scope. Notation Obs := gvar_pobs. + +(** Bundle for all ghost state we need *) +Class refinedrustGS Σ := { + refinedrust_typeGS :: typeGS Σ; + refinedrust_staticGS :: staticGS Σ; +}. + +Ltac instantiate_benign_universals term ::= + lazymatch type of term with + | ∀ (_ : gFunctors) (_ : refinedrustGS _), _ => + instantiate_benign_universals uconstr:(term _ _) + | ∀ _ : typeGS _, _ => + instantiate_benign_universals uconstr:(term ltac:(refine _)) + | ∀ _ : staticGS _, _ => + instantiate_benign_universals uconstr:(term ltac:(refine _)) + | ∀ _ : refinedrustGS _, _ => + instantiate_benign_universals uconstr:(term ltac:(refine _)) + | _ => + constr:(term) + end.