diff --git a/case_studies/tests/src/lib.rs b/case_studies/tests/src/lib.rs
index f055b343572197b56d92a6bd6b0f8f220c6ead6e..ba2ad52eea965a0d5b00b018d39f0ebb4dd4dde9 100644
--- a/case_studies/tests/src/lib.rs
+++ b/case_studies/tests/src/lib.rs
@@ -14,4 +14,4 @@ mod mixed;
mod closures;
mod references;
//
-//mod option;
+mod option;
diff --git a/case_studies/tests/src/option.rs b/case_studies/tests/src/option.rs
index 4ffe5cea57dd8ef2e42f2f55de4a1dbf55104dae..86599f3433f725a17ec89939bcf5fcf1215e764f 100644
--- a/case_studies/tests/src/option.rs
+++ b/case_studies/tests/src/option.rs
@@ -1,9 +1,12 @@
+#![rr::include("option")]
pub trait Bla {
fn bla(&self);
}
impl<T> Bla for Option<T> {
+ #[rr::params("x")]
+ #[rr::args("#x")]
#[rr::returns("()")]
fn bla(&self) {
diff --git a/rr_frontend/radium/src/coq.rs b/rr_frontend/radium/src/coq.rs
index 61e533903008b6af9714a6e02b7c95ce722479d4..7167e079d3fdc021a01569968e5cb6a61eb2b110 100644
--- a/rr_frontend/radium/src/coq.rs
+++ b/rr_frontend/radium/src/coq.rs
@@ -399,9 +399,55 @@ impl Display for CoqDefBody {
}
}
+#[derive(Debug, Clone)]
+pub enum CoqAttribute {
+ Global,
+ Local,
+}
+impl Display for CoqAttribute {
+ fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
+ match self {
+ Self::Global => write!(f, "global"),
+ Self::Local => write!(f, "local"),
+ }
+ }
+}
+
+#[derive(Debug, Clone)]
+pub struct CoqAttributes {
+ attrs: Vec<CoqAttribute>,
+}
+impl CoqAttributes {
+ pub fn empty() -> Self {
+ Self { attrs: vec![] }
+ }
+
+ pub fn new(attrs: Vec<CoqAttribute>) -> Self {
+ Self { attrs }
+ }
+}
+impl Display for CoqAttributes {
+ fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
+ if !self.attrs.is_empty() {
+ write!(f, "#[ ")?;
+ let mut needs_sep = false;
+ for attr in self.attrs.iter() {
+ if needs_sep {
+ write!(f, ", ")?;
+ }
+ needs_sep = true;
+ write!(f, "{}", attr)?;
+ }
+ write!(f, "]")?;
+ }
+ Ok(())
+ }
+}
+
/// A Coq typeclass instance declaration
#[derive(Debug, Clone)]
pub struct CoqInstanceDecl {
+ pub attrs: CoqAttributes,
pub name: Option<String>,
pub params: CoqParamList,
pub ty: CoqType,
@@ -411,8 +457,10 @@ pub struct CoqInstanceDecl {
impl Display for CoqInstanceDecl {
fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
match self.name {
- Some(ref name) => write!(f, "Instance {} {} : {}{}", name, self.params, self.ty, self.body),
- None => write!(f, "Instance {} : {}{}", self.params, self.ty, self.body),
+ Some(ref name) => {
+ write!(f, "{} Instance {} {} : {}{}", self.attrs, name, self.params, self.ty, self.body)
+ },
+ None => write!(f, "{} Instance {} : {}{}", self.attrs, self.params, self.ty, self.body),
}
}
}
diff --git a/rr_frontend/radium/src/specs.rs b/rr_frontend/radium/src/specs.rs
index 337dce8a66d80afdca7203ff2b2dd2d7e7458f69..98c36c1bd539a608e60b78c0cc17cb0730085b7a 100644
--- a/rr_frontend/radium/src/specs.rs
+++ b/rr_frontend/radium/src/specs.rs
@@ -1348,7 +1348,7 @@ impl<'def> AbstractVariant<'def> {
write!(out, "{}Definition {} : type ({}).\n", indent, self.plain_ty_name, self.rfn_type).unwrap();
write!(
out,
- "{indent}Proof using {}. exact ({}). Defined.\n",
+ "{indent}Proof using {} Type*. exact ({}). Defined.\n",
ty_params.iter().map(|x| x.type_term.clone()).collect::<Vec<_>>().join(" "),
self.generate_coq_type_term(sls_app)
)
@@ -1375,7 +1375,7 @@ impl<'def> AbstractVariant<'def> {
/// Generate a Coq definition for the struct type alias.
/// TODO: maybe we should also generate a separate alias def for the refinement type to make
/// things more readable?
- pub fn generate_coq_type_def(&self, ty_params: &[LiteralTyParam]) -> String {
+ pub fn generate_coq_type_def(&self, ty_params: &[LiteralTyParam], extra_context: &[CoqParam]) -> String {
let mut out = String::with_capacity(200);
let indent = " ";
// the write_str impl will always return Ok.
@@ -1399,6 +1399,17 @@ impl<'def> AbstractVariant<'def> {
}
out.push_str("\n");
+ // write coq parameters
+ write!(out, "{} (* Additional parameters *)\n", indent).unwrap();
+ if !extra_context.is_empty() {
+ write!(out, "{}Context", indent).unwrap();
+ for param in extra_context.iter() {
+ write!(out, " {}", param).unwrap();
+ }
+ write!(out, ".\n").unwrap();
+ }
+ write!(out, "\n").unwrap();
+
write!(out, "{}", self.generate_coq_type_def_core(ty_params)).unwrap();
write!(out, "End {}.\n", self.plain_ty_name).unwrap();
@@ -1490,10 +1501,10 @@ impl<'def> AbstractStruct<'def> {
}
/// Generate a Coq definition for the struct type alias.
- /// TODO: maybe we should also generate a separate alias def for the refinement type to make
- /// things more readable?
pub fn generate_coq_type_def(&self) -> String {
- self.variant_def.generate_coq_type_def(&self.ty_params)
+ let extra_context = if let Some(ref inv) = self.invariant { inv.coq_params.as_slice() } else { &[] };
+
+ self.variant_def.generate_coq_type_def(&self.ty_params, extra_context)
}
/// Generate an optional definition for the invariant of this type, if one has been specified.
@@ -2122,6 +2133,7 @@ impl<'def> AbstractEnum<'def> {
assertions.push(CoqTopLevelAssertion::InductiveDecl(ind.clone()));
// prove that it is inhabited
let instance_decl = CoqInstanceDecl {
+ attrs: CoqAttributes::new(vec![CoqAttribute::Global]),
name: None,
params: CoqParamList::empty(),
ty: CoqType::Literal(format!("Inhabited {}", ind.name)),
diff --git a/rr_frontend/translation/src/lib.rs b/rr_frontend/translation/src/lib.rs
index 907e9e5818e0827b19a3cddfd7f3ac3695c805eb..3be96a75965e171ff5630544b4ea4ffa7a7c8814 100644
--- a/rr_frontend/translation/src/lib.rs
+++ b/rr_frontend/translation/src/lib.rs
@@ -107,6 +107,8 @@ pub struct VerificationCtxt<'tcx, 'rcx> {
functions: &'rcx [LocalDefId],
/// the second component determines whether to include it in the code file as well
extra_imports: HashSet<(radium::CoqPath, bool)>,
+ /// extra Coq module dependencies
+ extra_dependencies: HashSet<String>,
coq_path_prefix: String,
dune_package: Option<String>,
shim_registry: shim_registry::ShimRegistry<'rcx>,
@@ -260,11 +262,23 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
}
}
+ let mut module_dependencies: Vec<_> =
+ self.extra_imports.iter().filter_map(|(x, _)| x.path.clone()).collect();
+ module_dependencies.extend(self.extra_dependencies.iter().cloned());
+
info!("Generated module summary ADTs: {:?}", adt_shims);
info!("Generated module summary functions: {:?}", function_shims);
let interface_file = File::create(path).unwrap();
- shim_registry::write_shims(interface_file, module_path, module, name, adt_shims, function_shims);
+ shim_registry::write_shims(
+ interface_file,
+ module_path,
+ module,
+ name,
+ &module_dependencies,
+ adt_shims,
+ function_shims,
+ );
}
/// Write specifications of a verification unit.
@@ -561,7 +575,8 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
fs::create_dir_all(base_dir_path.as_path()).unwrap();
}
- let coq_module_path = format!("{}.{}", self.coq_path_prefix, stem);
+ let toplevel_module_path = self.coq_path_prefix.to_string();
+ let coq_module_path = format!("{}.{}", toplevel_module_path, stem);
let generated_module_path = format!("{}.generated", coq_module_path);
let proof_module_path = format!("{}.proofs", coq_module_path);
@@ -623,8 +638,11 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
// write dune meta file
let mut dune_file = io::BufWriter::new(fs::File::create(generated_dune_path.as_path()).unwrap());
- let extra_theories: Vec<_> =
+ let mut extra_theories: HashSet<_> =
self.extra_imports.iter().filter_map(|(path, _)| path.path.clone()).collect();
+ extra_theories.extend(self.extra_dependencies.iter().cloned());
+ let extra_theories: Vec<_> = extra_theories.into_iter().collect();
+
let dune_package = if let Some(ref dune_package) = self.dune_package {
format!("(package {dune_package})\n")
} else {
@@ -752,6 +770,8 @@ fn register_shims<'rcx, 'tcx>(vcx: &mut VerificationCtxt<'tcx, 'rcx>) -> Result<
// add the extra imports
vcx.extra_imports
.extend(vcx.shim_registry.get_extra_imports().iter().map(|x| (x.clone(), true)));
+ // add the extra dependencies
+ vcx.extra_dependencies.extend(vcx.shim_registry.get_extra_dependencies().iter().cloned());
Ok(())
}
@@ -762,19 +782,18 @@ fn get_most_restrictive_function_mode<'tcx, 'rcx>(
) -> function_body::ProcedureMode {
let mut mode = function_body::ProcedureMode::Prove;
- let attrs = vcx.env.get_attributes(did);
- let v = crate::utils::filter_tool_attrs(attrs);
+ let attrs = get_attributes_of_function(&vcx.env, did);
// check if this is a purely spec function; if so, skip.
- if crate::utils::has_tool_attr(attrs, "shim") {
+ if crate::utils::has_tool_attr_filtered(attrs.as_slice(), "shim") {
mode = function_body::ProcedureMode::Shim;
}
- if crate::utils::has_tool_attr(attrs, "trust_me") {
+ if crate::utils::has_tool_attr_filtered(attrs.as_slice(), "trust_me") {
mode = function_body::ProcedureMode::TrustMe;
- } else if crate::utils::has_tool_attr(attrs, "only_spec") {
+ } else if crate::utils::has_tool_attr_filtered(attrs.as_slice(), "only_spec") {
mode = function_body::ProcedureMode::OnlySpec;
- } else if crate::utils::has_tool_attr(attrs, "ignore") {
+ } else if crate::utils::has_tool_attr_filtered(attrs.as_slice(), "ignore") {
info!("Function {:?} will be ignored", did);
mode = function_body::ProcedureMode::Ignore;
}
@@ -839,6 +858,18 @@ fn propagate_attr_from_impl(it: &rustc_ast::ast::AttrItem) -> bool {
}
}
+fn get_attributes_of_function<'a>(env: &'a Environment, did: DefId) -> Vec<&'a rustc_ast::ast::AttrItem> {
+ let attrs = env.get_attributes(did);
+ let mut filtered_attrs = crate::utils::filter_tool_attrs(attrs);
+ // also add selected attributes from the surrounding impl
+ if let Some(impl_did) = env.tcx().impl_of_method(did) {
+ let impl_attrs = env.get_attributes(impl_did);
+ let filtered_impl_attrs = crate::utils::filter_tool_attrs(impl_attrs);
+ filtered_attrs.extend(filtered_impl_attrs.into_iter().filter(|x| propagate_attr_from_impl(x)));
+ }
+ filtered_attrs
+}
+
/// Translate functions of the crate, assuming they were previously registered.
fn translate_functions<'rcx, 'tcx>(vcx: &mut VerificationCtxt<'tcx, 'rcx>) {
for &f in vcx.functions {
@@ -846,14 +877,7 @@ fn translate_functions<'rcx, 'tcx>(vcx: &mut VerificationCtxt<'tcx, 'rcx>) {
let fname = vcx.env.get_item_name(f.to_def_id());
let meta = vcx.procedure_registry.lookup_function(&f.to_def_id()).unwrap();
- let attrs = vcx.env.get_attributes(f.to_def_id());
- let mut filtered_attrs = crate::utils::filter_tool_attrs(attrs);
- // also add selected attributes from the surrounding impl
- if let Some(impl_did) = vcx.env.tcx().impl_of_method(f.to_def_id()) {
- let impl_attrs = vcx.env.get_attributes(impl_did);
- let filtered_impl_attrs = crate::utils::filter_tool_attrs(impl_attrs);
- filtered_attrs.extend(filtered_impl_attrs.into_iter().filter(|x| propagate_attr_from_impl(x)));
- }
+ let filtered_attrs = get_attributes_of_function(&vcx.env, f.to_def_id());
let mode = meta.get_mode();
if mode.is_shim() {
@@ -1165,6 +1189,7 @@ where
type_translator: &type_translator,
procedure_registry,
extra_imports: imports.into_iter().map(|x| (x, false)).collect(),
+ extra_dependencies: HashSet::new(),
coq_path_prefix: path_prefix,
shim_registry,
dune_package: package,
diff --git a/rr_frontend/translation/src/shim_registry.rs b/rr_frontend/translation/src/shim_registry.rs
index d2b88b5ff6ad7cb1ecd6cdf51b9bea6f18cb75db..0f30153a3d9f933c368f9763e09578f840fc462a 100644
--- a/rr_frontend/translation/src/shim_registry.rs
+++ b/rr_frontend/translation/src/shim_registry.rs
@@ -109,6 +109,8 @@ pub struct ShimRegistry<'a> {
adt_shims: Vec<AdtShim<'a>>,
/// extra imports
imports: Vec<radium::specs::CoqPath>,
+ /// extra module dependencies
+ depends: Vec<String>,
}
impl<'a> ShimRegistry<'a> {
@@ -139,6 +141,7 @@ impl<'a> ShimRegistry<'a> {
function_shims: Vec::new(),
adt_shims: Vec::new(),
imports: Vec::new(),
+ depends: Vec::new(),
}
}
@@ -186,6 +189,19 @@ impl<'a> ShimRegistry<'a> {
};
self.imports.push(coq_path);
+ let depends = obj
+ .get("module_dependencies")
+ .ok_or(format!("Missing attribute \"module_dependencies\""))?;
+ let depends = depends
+ .as_array()
+ .ok_or(format!("Expected array for \"module_dependencies\" attribute"))?;
+ for el in depends.iter() {
+ let module = el
+ .as_str()
+ .ok_or(format!("Expected string for element of \"module_dependencies\" array"))?;
+ self.depends.push(module.to_string());
+ }
+
let arr = obj.get("items").ok_or(format!("Missing attribute \"items\""))?;
let arr = arr.as_array().ok_or(format!("Expected array for \"items\" attribute"))?;
v = arr.clone();
@@ -237,6 +253,10 @@ impl<'a> ShimRegistry<'a> {
pub fn get_extra_imports(&self) -> &[radium::specs::CoqPath] {
&self.imports
}
+
+ pub fn get_extra_dependencies(&self) -> &[String] {
+ &self.depends
+ }
}
/// Write serialized representation of shims to a file.
@@ -245,6 +265,7 @@ pub fn write_shims<'a>(
load_path: &str,
load_module: &str,
name: &str,
+ module_dependencies: &[String],
adt_shims: Vec<AdtShim<'a>>,
function_shims: Vec<FunctionShim<'a>>,
) {
@@ -268,6 +289,7 @@ pub fn write_shims<'a>(
"refinedrust_path": load_path,
"refinedrust_module": load_module,
"refinedrust_name": name,
+ "module_dependencies": module_dependencies,
"items": array_val
});
diff --git a/rr_frontend/translation/src/spec_parsers/crate_attr_parser.rs b/rr_frontend/translation/src/spec_parsers/crate_attr_parser.rs
index fa30039346372140661a17775873301a0b1d6a1c..5c1c6c242e23eab1b3694c9865c27064063eb85a 100644
--- a/rr_frontend/translation/src/spec_parsers/crate_attr_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/crate_attr_parser.rs
@@ -23,6 +23,7 @@ pub struct CrateAttrs {
pub prefix: Option<String>,
pub includes: Vec<String>,
pub package: Option<String>,
+ pub context_params: Vec<specs::CoqParam>,
}
pub struct VerboseCrateAttrParser {}
@@ -44,6 +45,7 @@ impl CrateAttrParser for VerboseCrateAttrParser {
let mut includes: Vec<String> = Vec::new();
let mut prefix: Option<String> = None;
let mut package: Option<String> = None;
+ let mut context_params = Vec::new();
for &it in attrs.iter() {
let ref path_segs = it.path.segments;
@@ -74,6 +76,15 @@ impl CrateAttrParser for VerboseCrateAttrParser {
}
package = Some(path.value().to_string());
},
+ "context" => {
+ let param: parse_utils::RRGlobalCoqContextItem =
+ buffer.parse(&meta).map_err(str_err)?;
+ context_params.push(specs::CoqParam::new(
+ specs::CoqName::Unnamed,
+ specs::CoqType::Literal(param.item),
+ true,
+ ));
+ },
_ => {
return Err(format!("unknown attribute for crate specification: {:?}", args));
},
@@ -85,6 +96,7 @@ impl CrateAttrParser for VerboseCrateAttrParser {
prefix,
includes,
package,
+ context_params,
})
}
}
diff --git a/rr_frontend/translation/src/spec_parsers/module_attr_parser.rs b/rr_frontend/translation/src/spec_parsers/module_attr_parser.rs
index b4ee618efe13a8b1a80e2b5e2be72bf906880841..b89f23fda8c3f7be9414475ebe2f1f79a178d695 100644
--- a/rr_frontend/translation/src/spec_parsers/module_attr_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/module_attr_parser.rs
@@ -26,6 +26,7 @@ pub trait ModuleAttrParser {
pub struct ModuleAttrs {
pub imports: Vec<specs::CoqPath>,
pub includes: Vec<String>,
+ pub context_params: Vec<specs::CoqParam>,
}
pub struct VerboseModuleAttrParser {}
@@ -49,6 +50,7 @@ impl ModuleAttrParser for VerboseModuleAttrParser {
let meta = ();
let mut imports: Vec<specs::CoqPath> = Vec::new();
let mut includes: Vec<String> = Vec::new();
+ let mut context_params = Vec::new();
for &it in attrs.iter() {
let ref path_segs = it.path.segments;
@@ -65,12 +67,25 @@ impl ModuleAttrParser for VerboseModuleAttrParser {
let name: parse::LitStr = buffer.parse(&meta).map_err(str_err)?;
includes.push(name.value());
},
+ "context" => {
+ let param: parse_utils::RRGlobalCoqContextItem =
+ buffer.parse(&meta).map_err(str_err)?;
+ context_params.push(specs::CoqParam::new(
+ specs::CoqName::Unnamed,
+ specs::CoqType::Literal(param.item),
+ true,
+ ));
+ },
_ => {
return Err(format!("unknown attribute for module specification: {:?}", args));
},
}
}
}
- Ok(ModuleAttrs { imports, includes })
+ Ok(ModuleAttrs {
+ imports,
+ includes,
+ context_params,
+ })
}
}
diff --git a/rr_frontend/translation/src/spec_parsers/parse_utils.rs b/rr_frontend/translation/src/spec_parsers/parse_utils.rs
index fc147eb371fe47d25ab3f8a14ab7e0d9bad6aed0..123c9c9899c597597af6c17a75575d5f15624d7b 100644
--- a/rr_frontend/translation/src/spec_parsers/parse_utils.rs
+++ b/rr_frontend/translation/src/spec_parsers/parse_utils.rs
@@ -231,6 +231,19 @@ impl<'a> parse::Parse<ParseMeta<'a>> for RRCoqContextItem {
}
}
+/// a variant of `RRCoqContextItem` for module/crate scope
+#[derive(Debug)]
+pub struct RRGlobalCoqContextItem {
+ pub item: String,
+}
+impl<U> parse::Parse<U> for RRGlobalCoqContextItem {
+ fn parse(input: parse::ParseStream, meta: &U) -> parse::ParseResult<Self> {
+ let item: parse::LitStr = input.parse(meta)?;
+
+ Ok(RRGlobalCoqContextItem { item: item.value() })
+ }
+}
+
pub type ParseMeta<'a> = (&'a [specs::LiteralTyParam], &'a [(Option<String>, specs::Lft)]);
/// Handle escape sequences in the given string.
diff --git a/rr_frontend/translation/src/utils.rs b/rr_frontend/translation/src/utils.rs
index 82abb1136fc35c71d07e0881787a77884180965f..59152de11578f810b3c2d07c0422b02423611732 100644
--- a/rr_frontend/translation/src/utils.rs
+++ b/rr_frontend/translation/src/utils.rs
@@ -345,6 +345,16 @@ pub fn has_tool_attr(attrs: &[ast::Attribute], name: &str) -> bool {
})
}
+/// Check if `<tool>::name` is among the filtered attributes.
+pub fn has_tool_attr_filtered(attrs: &[&ast::AttrItem], name: &str) -> bool {
+ attrs.iter().any(|item| {
+ let segments = &item.path.segments;
+ segments.len() == 2
+ && segments[0].ident.as_str() == config::spec_hotword().as_str()
+ && segments[1].ident.as_str() == name
+ })
+}
+
/// Check if any attribute starting with `<tool>` is among the attributes.
pub fn has_any_tool_attr(attrs: &[ast::Attribute]) -> bool {
attrs.iter().any(|attr| match &attr.kind {