diff --git a/SPEC_FORMAT.md b/SPEC_FORMAT.md
index fffb1c22007c4d9bcad37ee1bdf2dc1e1b4893c6..25ac7ca0124f6f23c3be220cd5bbc88c3c26f34f 100644
--- a/SPEC_FORMAT.md
+++ b/SPEC_FORMAT.md
@@ -37,6 +37,7 @@ Finally, the `returns` clause specifies a refinement (and optionally, a type) fo
| `ensures` | specify a postcondition | multiple | `#[rr::ensures("x > y")]` |
| `exists` | specify an existential for the postcondition | multiple | `#[rr::exists("x" : "Z")]` |
| `observe` | shortcut for specifying observations on ghost variables | single | `#[rr::observe("γ": "x + 2")]` |
+| `context` | add an unnamed implicit parameter to the context | single | `#[rr::context("ghost_varG Σ Z")]` |
There are further attributes that influence the proof-checking behaviour:
| Keyword | Purpose | Properties | Example |
@@ -54,6 +55,7 @@ The following attributes are also available on impls and then influence all func
| `trust_me` | generate and type-check the specifications and code, but do not generate proofs | none | `#[rr::trust_me]` |
| `only_spec` | only generate and type-check the specifications, but do not generate the code | none | `#[rr::only_spec]` |
| `skip` | ignore this block completely | none | `#[rr::skip]` |
+| `context` | add an unnamed implicit parameter to the context | single | `#[rr::context("ghost_varG Σ Z")]` |
## Struct attributes
@@ -65,6 +67,7 @@ The following attributes are also available on impls and then influence all func
| `refines` | Optionally specify the refinement of the raw struct type (can only be used when no refinements are specified via `field` attributes on the struct's fields) | single | `#[rr::refines("-[a; b]")]` |
| `mode` | Specifies the sharing mode of the defined type: either `plain` (the default, invariants are shared on a best-effort basis for the sharing invariant) or `persistent` (all invariants need to be shareable) | `#[rr::mode("plain")]` |
| `export_as` | influence the exported path in the generated RefinedRust library interface for import in other proofs | a Rust path | `#[rr::export_as(std::vec::Vec)]` |
+| `context` | add an unnamed implicit parameter to the context in which the invariant is declared | single | `#[rr::context("ghost_varG Σ Z")]` |
Invariants on structs can be prefixed by `#own` or `#shr` to only include the invariant in the struct's ownership or sharing predicate, respectively, e.g.: `#[rr::invariant(#own "freeable l len")]`.
diff --git a/rr_frontend/radium/src/code.rs b/rr_frontend/radium/src/code.rs
index 9ea7051b5672b9c427cece7ea936e7c3753c01fa..8d5d25982667b5253f7bcc882ed8076ad93573fd 100644
--- a/rr_frontend/radium/src/code.rs
+++ b/rr_frontend/radium/src/code.rs
@@ -986,12 +986,14 @@ impl<'def> Function<'def> {
// write coq parameters
if !self.spec.coq_params.is_empty() || !self.other_functions.is_empty() {
write!(f, "∀ ")?;
- for (n, ty, imp) in self.spec.coq_params.iter() {
- if !imp {
- write!(f, "({n} : {ty}) ")?;
+ for param in self.spec.coq_params.iter() {
+ // TODO use CoqParam::format instead
+ if param.implicit {
+ write!(f, "`({})", param.ty)?;
} else {
- write!(f, "`({ty}) ")?;
+ write!(f, "({} : {})", param.name, param.ty)?;
}
+ write!(f, " ")?;
}
// assume locations for other functions
@@ -1060,9 +1062,9 @@ impl<'def> Function<'def> {
write!(f, "] (type_of_{} ", self.name())?;
// write type args (passed to the type definition)
- for (n, _, imp) in self.spec.coq_params.iter() {
- if !imp {
- write!(f, "{} ", n)?;
+ for param in self.spec.coq_params.iter() {
+ if !param.implicit {
+ write!(f, "{} ", param.name)?;
}
}
@@ -1085,9 +1087,9 @@ impl<'def> Function<'def> {
// intros spec params
if !self.spec.coq_params.is_empty() {
write!(f, "intros")?;
- for (n, _, imp) in self.spec.coq_params.iter() {
- if !imp {
- write!(f, " {n}")?;
+ for param in self.spec.coq_params.iter() {
+ if !param.implicit {
+ write!(f, " {}", param.name)?;
} else {
write!(f, " ?")?;
}
diff --git a/rr_frontend/radium/src/specs.rs b/rr_frontend/radium/src/specs.rs
index 3f5eeb9e1659f2eae50081ed0896d748054dcf18..e1f84f5e6e199561e08b5e15472c7f0ac2b5475e 100644
--- a/rr_frontend/radium/src/specs.rs
+++ b/rr_frontend/radium/src/specs.rs
@@ -345,6 +345,10 @@ pub struct TypeAnnotMeta {
}
impl TypeAnnotMeta {
+ pub fn is_empty(&self) -> bool {
+ self.escaped_lfts.is_empty() && self.escaped_tyvars.is_empty()
+ }
+
pub fn empty() -> TypeAnnotMeta {
TypeAnnotMeta {
escaped_lfts: HashSet::new(),
@@ -798,6 +802,8 @@ pub struct InvariantSpec {
/// the specification of the abstracted refinement under a context where rfn_pat is bound
abstracted_refinement: Option<CoqPattern>,
// TODO add stuff for non-atomic/atomic invariants
+ /// name, type, implicit or not
+ coq_params: Vec<CoqParam>,
}
impl InvariantSpec {
@@ -811,6 +817,7 @@ impl InvariantSpec {
invariants: Vec<(IProp, InvariantMode)>,
ty_own_invariants: Vec<TyOwnSpec>,
abstracted_refinement: Option<CoqPattern>,
+ coq_params: Vec<CoqParam>,
) -> Self {
match flags {
InvariantSpecFlags::Persistent => {
@@ -830,6 +837,7 @@ impl InvariantSpec {
invariants,
ty_own_invariants,
abstracted_refinement,
+ coq_params,
}
}
@@ -1091,7 +1099,17 @@ impl InvariantSpec {
}
out.push_str(".\n");
}
- out.push_str("\n");
+
+ // write coq parameters
+ write!(out, "{} (* Additional parameters *)\n", indent).unwrap();
+ if !self.coq_params.is_empty() {
+ write!(out, "{}Context", indent).unwrap();
+ for param in self.coq_params.iter() {
+ write!(out, " {}", param).unwrap();
+ }
+ write!(out, ".\n").unwrap();
+ }
+ write!(out, "\n").unwrap();
// get the applied base_rfn_type
let rfn_instantiations: Vec<String> =
@@ -2545,13 +2563,45 @@ pub struct LoopSpec {
pub func_predicate: IPropPredicate,
}
+#[derive(Clone, Debug, PartialEq)]
+pub struct CoqParam {
+ pub name: CoqName,
+ pub ty: CoqType,
+ pub implicit: bool,
+}
+
+impl CoqParam {
+ pub fn new(name: CoqName, ty: CoqType, implicit: bool) -> Self {
+ Self { name, ty, implicit }
+ }
+
+ pub fn format(&self, f: &mut Formatter, make_implicits: bool) -> fmt::Result {
+ if self.implicit {
+ if make_implicits {
+ write!(f, "`{{{}}}", self.ty)
+ }
+ else {
+ write!(f, "`({})", self.ty)
+ }
+ } else {
+ write!(f, "({} : {})", self.name, self.ty)
+ }
+ }
+}
+
+impl Display for CoqParam {
+ fn fmt(&self, f: &mut Formatter) -> fmt::Result {
+ self.format(f, true)
+ }
+}
+
/**
* A Caesium function specification.
*/
#[derive(Debug)]
pub struct FunctionSpec<'def> {
/// Coq-level parameters the typing statement needs (bool is for implicit or not)
- pub coq_params: Vec<(CoqName, CoqType, bool)>,
+ pub coq_params: Vec<CoqParam>,
/// Function name
pub function_name: String,
/// The name of the spec
@@ -2598,15 +2648,11 @@ impl<'def> FunctionSpec<'def> {
if self.coq_params.len() == 0 {
} else {
let mut need_sep = false;
- for (name, t, implicit) in self.coq_params.iter() {
+ for param in self.coq_params.iter() {
if need_sep {
out.push_str(" ");
}
- if *implicit {
- out.push_str(format!("`{{{}}}", t).as_str());
- } else {
- out.push_str(format!("({} : {})", name, t).as_str());
- }
+ out.push_str(format!("{}", param).as_str());
need_sep = true;
}
}
@@ -2712,7 +2758,8 @@ impl<'def> Display for FunctionSpec<'def> {
#[derive(Debug)]
pub struct FunctionSpecBuilder<'def> {
/// Coq-level parameters the typing statement needs, bool is true if implicit
- coq_params: Vec<(CoqName, CoqType, bool)>,
+ coq_params: Vec<CoqParam>,
+ late_coq_params: Vec<CoqParam>,
lifetimes: Vec<Lft>,
params: Vec<(CoqName, CoqType)>,
@@ -2734,6 +2781,7 @@ impl<'def> FunctionSpecBuilder<'def> {
pub fn new() -> Self {
Self {
coq_params: Vec::new(),
+ late_coq_params: Vec::new(),
lifetimes: Vec::new(),
params: Vec::new(),
ty_params: Vec::new(),
@@ -2810,16 +2858,28 @@ impl<'def> FunctionSpecBuilder<'def> {
Ok(())
}
- /// Add a Coq-level param.
+ /// Add a Coq-level param that comes before the type parameters.
pub fn add_coq_param(&mut self, name: CoqName, t: CoqType, implicit: bool) -> Result<(), String> {
self.ensure_coq_not_bound(&name)?;
- self.coq_params.push((name, t, implicit));
+ self.coq_params.push(CoqParam::new(name, t, implicit));
+ Ok(())
+ }
+
+ /// Add a Coq-level param that comes after the type parameters.
+ pub fn add_late_coq_param(&mut self, name: CoqName, t: CoqType, implicit: bool) -> Result<(), String> {
+ self.ensure_coq_not_bound(&name)?;
+ self.late_coq_params.push(CoqParam::new(name, t, implicit));
Ok(())
}
/// Variant of [add_coq_param] that can never fail and makes the parameter anonymous.
pub fn add_unnamed_coq_param(&mut self, t: CoqType, implicit: bool) {
- self.coq_params.push((CoqName::Unnamed, t, implicit));
+ self.coq_params.push(CoqParam::new(CoqName::Unnamed, t, implicit));
+ }
+
+ /// Variant of [add_late_coq_param] that can never fail and makes the parameter anonymous.
+ pub fn add_unnamed_late_coq_param(&mut self, t: CoqType, implicit: bool) {
+ self.late_coq_params.push(CoqParam::new(CoqName::Unnamed, t, implicit));
}
/// Add a new universal lifetime constraint.
@@ -2901,7 +2961,8 @@ impl<'def> FunctionSpecBuilder<'def> {
/// `name` is the designated name of the function.
/// `code_params` are the parameters the code body needs to be provided (e.g., locations of
/// other functions).
- pub fn into_function_spec(self, name: &str, spec_name: &str) -> FunctionSpec<'def> {
+ pub fn into_function_spec(mut self, name: &str, spec_name: &str) -> FunctionSpec<'def> {
+ self.coq_params.extend(self.late_coq_params.into_iter());
let ret = self.ret.unwrap_or(TypeWithRef::make_unit());
FunctionSpec {
function_name: name.to_string(),
diff --git a/rr_frontend/translation/src/function_body.rs b/rr_frontend/translation/src/function_body.rs
index a6e0eac34311cd76e02ec404c1a3c822ee652917..901de3686c154757c7ec255280d4561f527be156 100644
--- a/rr_frontend/translation/src/function_body.rs
+++ b/rr_frontend/translation/src/function_body.rs
@@ -185,7 +185,7 @@ pub struct FunctionTranslator<'a, 'def, 'tcx> {
/// registry of other procedures
procedure_registry: &'a ProcedureScope<'def>,
/// attributes on this function
- attrs: &'a [Attribute],
+ attrs: &'a [&'a rustc_ast::ast::AttrItem],
/// polonius info for this function
info: &'a PoloniusInfo<'a, 'tcx>,
/// translator for types
@@ -204,7 +204,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> FunctionTranslator<'a, 'def, 'tcx> {
env: &'def Environment<'tcx>,
meta: ProcedureMeta,
proc: Procedure<'tcx>,
- attrs: &'a [Attribute],
+ attrs: &'a [&'a rustc_ast::ast::AttrItem],
ty_translator: &'def TypeTranslator<'def, 'tcx>,
proc_registry: &'a ProcedureScope<'def>,
) -> Result<Self, TranslationError> {
@@ -410,8 +410,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> FunctionTranslator<'a, 'def, 'tcx> {
/// Parse and process attributes of this function.
fn process_attrs(&mut self) -> Result<(), TranslationError> {
- let a = self.attrs;
- let v = crate::utils::filter_tool_attrs(a);
+ let v = self.attrs;
let inputs = &self.inputs;
let output = &self.output;
@@ -436,7 +435,7 @@ impl<'a, 'def: 'a, 'tcx: 'def> FunctionTranslator<'a, 'def, 'tcx> {
ty_translator.intern_literal(lit)
});
parser
- .parse_function_spec(v.as_slice(), &mut self.translated_fn)
+ .parse_function_spec(v, &mut self.translated_fn)
.map_err(|e| TranslationError::AttributeError(e))?;
Ok(())
},
@@ -642,7 +641,7 @@ struct BodyTranslator<'a, 'def, 'tcx> {
/// registry of other procedures
procedure_registry: &'a ProcedureScope<'def>,
/// attributes on this function
- attrs: &'a [Attribute],
+ attrs: &'a [&'a rustc_ast::ast::AttrItem],
/// polonius info for this function
info: &'a PoloniusInfo<'a, 'tcx>,
/// local lifetimes: the LHS is the lifetime name, the RHS are the super lifetimes
diff --git a/rr_frontend/translation/src/lib.rs b/rr_frontend/translation/src/lib.rs
index d66d99dd513d721310c1e9a587ee28e1359ade26..c67475de4740062a91ca155632c2a7b87bfea9ab 100644
--- a/rr_frontend/translation/src/lib.rs
+++ b/rr_frontend/translation/src/lib.rs
@@ -829,6 +829,17 @@ fn register_functions<'rcx, 'tcx>(vcx: &mut VerificationCtxt<'tcx, 'rcx>) {
}
}
+fn propagate_attr_from_impl(it: &rustc_ast::ast::AttrItem) -> bool {
+ if let Some(ident) = it.path.segments.get(1) {
+ match ident.ident.as_str() {
+ "context" => true,
+ _ => false,
+ }
+ } else {
+ false
+ }
+}
+
/// 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 {
@@ -837,6 +848,13 @@ fn translate_functions<'rcx, 'tcx>(vcx: &mut VerificationCtxt<'tcx, 'rcx>) {
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 mode = meta.get_mode();
if mode.is_shim() {
@@ -852,7 +870,7 @@ fn translate_functions<'rcx, 'tcx>(vcx: &mut VerificationCtxt<'tcx, 'rcx>) {
&vcx.env,
meta,
proc,
- attrs,
+ &filtered_attrs,
&vcx.type_translator,
&vcx.procedure_registry,
);
diff --git a/rr_frontend/translation/src/spec_parsers/parse_utils.rs b/rr_frontend/translation/src/spec_parsers/parse_utils.rs
index 9897cdff92ff6e1088eb018aacc7950076eabf60..f6cb72c64edd06884d1d7ac14d0f178f85ba8b90 100644
--- a/rr_frontend/translation/src/spec_parsers/parse_utils.rs
+++ b/rr_frontend/translation/src/spec_parsers/parse_utils.rs
@@ -204,6 +204,33 @@ impl<'a, U> Parse<U> for CoqPath {
}
}
+/// Parse an assumed Coq context item, e.g.
+/// `"`{ghost_mapG Σ Z Z}"`.
+#[derive(Debug)]
+pub struct RRCoqContextItem {
+ pub item: String,
+ /// true if this should be put at the end of the dependency list, e.g. if it depends on type
+ /// parameters
+ pub at_end: bool,
+}
+impl<'a> parse::Parse<ParseMeta<'a>> for RRCoqContextItem {
+ fn parse(input: parse::ParseStream, meta: &ParseMeta<'a>) -> parse::ParseResult<Self> {
+ let item: parse::LitStr = input.parse(meta)?;
+ let (item_str, annot_meta) = process_coq_literal(&item.value(), *meta);
+
+ let mut at_end = false;
+ if !annot_meta.is_empty() {
+ at_end = true;
+ }
+
+ //annot_meta.
+ Ok(RRCoqContextItem {
+ item: item_str,
+ at_end,
+ })
+ }
+}
+
pub type ParseMeta<'a> = (&'a [specs::LiteralTyParam], &'a [(Option<String>, specs::Lft)]);
/// Processes a literal Coq term annotated via an attribute.
diff --git a/rr_frontend/translation/src/spec_parsers/struct_spec_parser.rs b/rr_frontend/translation/src/spec_parsers/struct_spec_parser.rs
index a2973426b1496f9ea7063b6349fcc16e25d7c222..add95b4a8a624307ce2397d7fd591424144574fe 100644
--- a/rr_frontend/translation/src/spec_parsers/struct_spec_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/struct_spec_parser.rs
@@ -23,6 +23,7 @@ pub trait InvariantSpecParser {
/// - rr::exists
/// - rr::invariant
/// - rr::refines for the inner refinement
+ /// - rr::context for context items that are required to be available in the definition
///
/// Returns whether a Boolean stating whether a rr::refines attribute was included.
fn parse_invariant_spec<'a>(
@@ -203,6 +204,8 @@ impl InvariantSpecParser for VerboseInvariantSpecParser {
// use Plain as the default
let mut inv_flags = specs::InvariantSpecFlags::Plain;
+ let mut params: Vec<specs::CoqParam> = Vec::new();
+
for &it in attrs.iter() {
let ref path_segs = it.path.segments;
let ref args = it.args;
@@ -256,6 +259,14 @@ impl InvariantSpecParser for VerboseInvariantSpecParser {
abstracted_refinement = Some(term.to_string());
}
},
+ "context" => {
+ let param = RRCoqContextItem::parse(&buffer, &meta).map_err(str_err)?;
+ params.push(specs::CoqParam::new(
+ specs::CoqName::Unnamed,
+ specs::CoqType::Literal(param.item),
+ true,
+ ));
+ },
_ => {
//skip, this may be part of an enum spec
()
@@ -276,6 +287,7 @@ impl InvariantSpecParser for VerboseInvariantSpecParser {
invariants,
type_invariants,
abstracted_refinement,
+ params,
);
Ok((spec, refinement_included))
diff --git a/rr_frontend/translation/src/spec_parsers/verbose_function_spec_parser.rs b/rr_frontend/translation/src/spec_parsers/verbose_function_spec_parser.rs
index df4900be8813c8d95419daeb545eaec1c602a443..9aaba8831581e9ec0287d9738c8707df4fec8c38 100644
--- a/rr_frontend/translation/src/spec_parsers/verbose_function_spec_parser.rs
+++ b/rr_frontend/translation/src/spec_parsers/verbose_function_spec_parser.rs
@@ -23,22 +23,6 @@ pub trait FunctionSpecParser<'def> {
) -> Result<(), String>;
}
-/// Parse an assumed Coq context item, e.g.
-/// `"`{ghost_mapG Σ Z Z}"`.
-#[derive(Debug)]
-struct RRCoqContextItem {
- item: String,
-}
-impl<U> parse::Parse<U> for RRCoqContextItem
-where
- U: ?Sized,
-{
- fn parse(input: parse::ParseStream, meta: &U) -> parse::ParseResult<Self> {
- let item: parse::LitStr = input.parse(meta)?;
- Ok(RRCoqContextItem { item: item.value() })
- }
-}
-
/// A sequence of refinements with optional types, e.g.
/// `"42" @ "int i32", "1337", "(a, b)"`
#[derive(Debug)]
@@ -316,12 +300,19 @@ where
},
"context" => {
let context_item = RRCoqContextItem::parse(&buffer, &meta).map_err(str_err)?;
- builder.spec.add_coq_param(
- specs::CoqName::Unnamed,
- specs::CoqType::Literal(context_item.item),
- true,
- )?;
- //spec.add_coq_context_item(context_item.item);
+ if context_item.at_end {
+ builder.spec.add_late_coq_param(
+ specs::CoqName::Unnamed,
+ specs::CoqType::Literal(context_item.item),
+ true,
+ )?;
+ } else {
+ builder.spec.add_coq_param(
+ specs::CoqName::Unnamed,
+ specs::CoqType::Literal(context_item.item),
+ true,
+ )?;
+ }
},
_ => {
info!("ignoring function attribute: {:?}", args);