From 306faeba9889efd3048e5e44134f306361d7a024 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Mon, 24 Jul 2023 12:29:20 -0700 Subject: [PATCH 01/36] Function contract RFC first draft --- rfc/src/rfcs/0008-function-contracts.md | 435 ++++++++++++++++++++++++ 1 file changed, 435 insertions(+) create mode 100644 rfc/src/rfcs/0008-function-contracts.md diff --git a/rfc/src/rfcs/0008-function-contracts.md b/rfc/src/rfcs/0008-function-contracts.md new file mode 100644 index 000000000000..d0cb4e5af99c --- /dev/null +++ b/rfc/src/rfcs/0008-function-contracts.md @@ -0,0 +1,435 @@ +- **Feature Name:** Function Contracts +- **Feature Request Issue:** *Link to issue* +- **RFC PR:** *Link to original PR* +- **Status:** Under Review +- **Version:** 0 [0-9]\* *Increment this version whenever you open a new PR to update the RFC (not at every revision). + Start with 0.* +- **Proof-of-concept:** [features/contracts](https://github.com/model-checking/kani/tree/features/contracts) + +------------------- + +## Summary + +Contracts are a powerful tool for verification. They are both a convenient way +to write specifications as well as allowing users to soundly approximate the +behavior of units of code. The verification tool then leverages these +approximations for modular verification which affords both scalability, but also +allows for verifying unbounded loops and recursion. + +## User Impact + +Enabling function contracts is a non-invasive change. While it contains a new +API, that API is strictly additive for users. All prior operations are unchanged. + +The proposal in this RFC lays the ground work for two important goals. The +following describes those goals and any residual challenges to overcome to +achieve them. + +- **Scalability:** Function contracts are sound (over)abstractions of function + behavior. By verifiying the contract against its implemetation and + subsequently performing caller verification against the (cheaper) abstraction + verification can be modularized, cached and thus scaled. + + This proposal would yield those benefits within a single verification session, + but would still re-verify the contract every session. With a suitable caching + mechanism this could be avoided in future. +- **Unbounded Verification:** Contracts can be reasoned over inductively and + thus verify recursive functions. + + This proposal adds basic function contract functionality, but does not add an + indictive reasoning framework. + +## User Experience + +This proposal introduces 4 new annotations. + +- `#[kani::requires(CONDITION)]` and `#[kani::ensures(CONDITION)]` are + annotations for non-harness functions (lets use `f` for an example) and encode + pre- and postconditions respectively. + + Preconditions are a refinement (beyhond the type) of the domain of the + `f`. + + Postconditions are a refinement (beyond the type) of the codomain of the + `f`. + + `CONDITION`s are arbitrary boolean Rust expressions[^side-effects]. They may + reference the arguments of `f`. In the case of preconditions the value of + those arguments will be the value they have before `f` is called, in the case + of postconditions the value after the call to `f` returns. Additionally the + postcondition has access to the result of `f` in a variable called `result`. + (see [Open Questions](#open-questions) for a discussion on the `result` + variable.) + + A postcondition may also use the special builtin `old` pseudo function. + `old(EXPR)` evaluates `EXPR` in the context *before* the call to `f`, e.g. + like a precondition. + + A function may be annotated with multiple `requires` and `ensures` clauses + that are implicitly conjoined. The sum total of the clauses and the assigns + clause (see below) comprise the function contract. + +- `#[kani::for_contract(PATH)]` is a harness annotation which designates that + this harness is especially designed for verifying that function `PATH` obeys + it's contract. As an example assume `PATH` is `f`. + + The harness itself is implemented as usual by the user and verified the same + way as any other, including admitting other verification features like + stubbing. However additionally the preconditions of `f` id `kani::assume`'d + before every call to `f` and the postconditions are `kani::asssert`'ed after + it returns. + + Kani checks that `f` is in the call chain of this harness, but no further + checks are performed whether this harness is suitable for verifying the + contract of `f`, see also [Open Questions](#open-questions). + + Only one `for_contract` annotation is permitted per harness. + +- `#[kani::use_contract(PATH)]` is a harness annotation which instructs the + verifier to use the contract of `PATH` during verification instead of it's + body. + + `use_contract(f)` is only safe if a `for_contract(f)` harness has previously + been verified. See [Future possibilities](#future-possibilities) for a + discussion on automatic enforcement mechanisms of this requirement. + + Multiple `use_contract` annotations are permitted for a single harness. + +[^side-effects]: Contract conditions are required to be side effect free, e.g. perform no I/O perform no memory mutation and allocate/free no heap memory. See also the side effect discussion in [Open Questions](#open-questions). + + +For correct functionality contracts further require reasoning about memory. To +keep the burden on users user lower we propose to leverage the rust type +information to overapproximate the memory a function may modify. This allows +correct havocing without additional user interaction. Inference of memory +clauses considers any `mut` reachable memory to be potentially freed, +reallocated or reassigned. In addition any reachable `static` variables are +considered modified. See [future possibilities](#future-possibilities) for a +discussion on explicit assigns clauses. + +This proposal also introduces a new hidden builtin `kani::unchecked_deref`. The necessity for this builtin is explained [later](#dealing-with-mutable-borrows). + +--- + +What is the scope of this RFC? Which use cases do you have in mind? Explain how users will interact with it. Also +please include: + +- How would you teach this feature to users? What changes will be required to the user documentation? +- If the RFC is related to architectural changes and there are no visible changes to UX, please state so. + + +## Detailed Design + +Let us consider a complete example: + +```rs +#[kani::requires(divisor != 0)] +#[kani::ensures(result < dividend)] +fn my_div(dividend: u32, divisor: u32) -> u32 { + dividend / divisor +} + +#[kani::proof] +#[kani::for_contract(my_div)] +fn my_div_harness() { + my_div(kani::any(), kani::any()) +} + +#[kani::proof] +#[kani::use_contract] +fn use_div() { + let v = vec![...]; + let some_idx = my_div(v.len() - 1, 3); + v[some_idx]; +} +``` + +The following subsections describe the Kani pipeline for this example in order. + +### Code generation in `kani_macros` + +The `requires` and `ensures` macros generate new sibling functions to e.g. `my_div` +(see also discussion in [alternatives](#rationale-and-alternatives)). One +function is generated which corresponds to checking the contract holds for the +implementation. One function is generated which corresponds to approximating the +function behavior when called with the same arguments. + +The complete code generated for the example is shown below and followed by an explanation of each component. + +```rs +fn my_div_copy_965916(dividend: u32, divisor: u32) -> u32 { dividend / divisor } + +#[kanitool::checked_with = "my_div_check_5e3713"] +#[kanitool::replaced_with = "my_div_replace_5e3713"] +fn my_div(dividend: u32, divisor: u32) -> u32 { dividend / divisor } + +fn my_div_check_5e3713(dividend: u32, divisor: u32) -> u32 { + let dividend_renamed = kani::untracked_deref(÷nd); + let divisor_renamed = kani::untracked_deref(&divisor); + let result = my_div_check_965916(dividend, divisor); + kani::assert(result <= dividend_renamed, "result <= dividend"); + result +} + +fn my_div_replace_5e3713(dividend: u32, divisor: u32) -> u32 { + let dividend_renamed = kani::untracked_deref(÷nd); + let divisor_renamed = kani::untracked_deref(&divisor); + let result = my_div_replace_965916(dividend, divisor); + kani::assume(result <= dividend_renamed); + result +} + +fn my_div_check_965916(dividend: u32, divisor: u32) -> u32 { + kani::assume(divisor != 0); + my_div_copy_965916(dividend, divisor) +} + +fn my_div_replace_965916(dividend: u32, divisor: u32) -> u32 { + kani::assert(divisor != 0, "divisor != 0"); + kani::any() +} +``` + + +To support mutiple clauses while performing all code generation at macro +expansion time each clause separately generates both a checking and a +replacement function, wrapping like onion layers around any prior checks. Both +the generated check and replace function is attached to the annotated function +using `kanitool::{checked,replaced}_with` annotations. When the item is +reemitted from the clause macro, the `kanitool` annotation is placed last in +the attribute sequence, so that clauses expanded later can see it. Those +subsequently expanded clauses use the `kanittol` annotations to determine which +function to call inside them next. If no prior `kanitool` annotation is present +the original `my_div` or a copy of it is called instead. The copy is called in case +of the `check` function, since the compiler will later substitute all +occurrences of `my_div` with the `check` function which would also apply here and +cause an infinite recursion and make the original `my_div` body inaccessible. + +Each generated function is named `_{replace,check,copy}_`, where +`hash` is a hash of the original "function item" ast, in this case `my_div`, +including any attributes, such as `#[kanitool::checked_with = +"my_div_check_5e3713"]` from clauses expanded earlier, which guarantees the hash is +unique for each clause expansion. + +Type signatures of the generated functions are always identical to the type +signature of the contracted function, including type parameters and lifetimes. + + +### Dealing with mutable borrows + +Preconditions (`requires`) are emitted as-is into the generated function, +providing access to the function arguments directly. This is safe because they +are required to be side-effect free[^side-effects]. + +Postconditions (`ensures`) have to be handled specially. They can reference the +arguments of the function, though not modify them. However this is problematic +even without modification if part of an input is borrowed mutably as would be +the case in the following example of the `Vec::split_at_mut` function. + +```rs +impl Vec { + #[ensures(self.len() == result.0.len() + result.1.len())] + fn split_at_mut(&mut self, i: usize) -> (&mut [T], &mut [T]) { + ... + } +} +``` + +This contract refers simultaneously to `self` and the result. Since the method however borrows `self` mutably, the borrow checker would not allow the following simplistic code generation: + +```rs +impl Vec { + fn split_at_mut_check_(&mut self, i: usize) -> (&mut [T], &mut [T]) { + let result = self.split_at_mut(i); + kani::assert(self.len() == result.0.len() + result.1.len()); + result + } +} +``` + +`self` would not be permitted to be used here until `result` goes out of scope +and releasese the borrow. To avoid this issue we break the borrowchecker +guarantee with a new biltin `fn kani::unsafe_deref(t: &T) -> T`. The +implementation of this function is simply a CBMC level `*` (deref). In Rust this +implementation would be illegal without the `Copy` trait (which generates a +copy) but in CBMC this is acceptable. Breaking the borrow checker this way is safe for 2 reasons: + +1. Postconditions are not allowed perform mutation[^side-effects] and +2. Post conditions are of type `bool`, meaning they cannot leak references to + the arguments and cause race conditions. + +Circumventing the borrow checker is facilitated with a visit over the initial +postcondition expression that renames every occurrence of the arguments to a +fresh identifier and then generates a call `let i = unsafe_deref(&a)` for each +argument `a` and fresh identifier `i` **before** the call to the contracted +function. Because `unsafe_deref` creates shallow copies, they will witness any +modifications of memory they point to. + +Shadowing. + +### `old` + +The special `old` builtin function is implemented as an AST rewrite. Consider the below example: + +```rs +impl Vec { + #[kani::ensures(self.is_empty() || self.len() == old(self.len()) - 1)] + fn pop(&mut self) -> Option { + ... + } +} +``` + +`old` gives the user access to `self.len()`, evaluated before `pop` to be able +to compare it to `self.len()` after `pop` mutates `self`. + +While `old` might appear like a function it is not. The implementation lifts the +argument expression to old via AST rewrite to before the call to `pop` and binds +it to a temporary variable. This makes `old` syntax rather than a function, but +also makes it very powerful as any expression is allowed in `old` including +calculations, function calls etc. Our example would generate the code below: + +```rs +impl Vec { + fn pop_check_(&mut self) -> Option { + let old_1 = self.len(); + let result = Self::pop_copy_(self); + kani::assert(self.is_empty() || self.len() == old_1 - 1) + } +} +``` + +Note that unlike for arguments for postconditions, we do not use `unsafe_deref` +to break the borrowing rules. Unlike for those arguments, which must witness +mutations, the expression in `old` is supposed to reflect the state *before* the +function call and must therefore not observe mutations performed by e.g. `pop`. +We can use the borrowchecker to enforce this for safe Rust[^old-safety]. The +borrow checker will ensure that none of the temporary variables created borrow +from any mutable arguments and thus guarantee that they cannot witness mutations +in e.g. `pop`. To use e.g. `old(self)` in such a case the user can create copies +with the usual mechanism, such as `clone`, e.g. `old(self.clone())`. + +[^old-safety]: For unsafe rust we need additional protections which are not part + of this proposal. + +### Substitution with `kani_compiler` + +Harnesses annotated with `for_contract` or `use_contract` are subject to +substitution. Only one `for_contract(f)` annotation is allowed per harness and +it triggers substitution of the target function `f` with the check function in +the `#[kanitool::checked_with = ...]` annotation on `f`. Multiple +`use_contract(g)` annotations are allowed on each harness, including on +`for_contract` harnesses, though the simultaneous presence of `for_contract` and +`use_contract` for the same target function is not permissible. + +If the target function (`f` or `g`) does not have a `checked_with` or +`replaced_with` attribute (respectively) an error is thrown. + +### Invoking `goto-instrument` from `kani-driver` + +In addition to the Kani side substitiution we also perform instrumentation on +the CBMC because we rely on it's support for memory predicates. The +generated memory predicates are emitted from the compiler as CBMC contracts. To +enforce the memory contract `goto-instrument` has to be invoked with the correct +functions name. Since this is after lowering into GOTO-C the name provided has +to be the mangled name of the monomorphized instances. The compiler determines +which monomorphized version of the contracted functions are used in a +reachability pass. Those names are passed to the driver (as the component that +invokes `goto-instrument`) via the `HarnessAttributes` struct, using an `Option` +to represent a possible contract to enforce and a `Vec` as the contracts which +are used as abstractions. + +This is the technical portion of the RFC. Please provide high level details of the implementation you have in mind: + + + +## Rationale and alternatives + + + + +- **Kani-side implementation vs CBMC** Instead of generating check and replace + functions in Kani, we could use the contract instrumentation provided by CBMC. + We tried this earlier but came up short, because it is difficult to implement, + while supporting arbitrary Rust syntax. We exported the conditions into + functions so that Rust would do the parsing/type checking/lowering for us and + then call the lowered function in the CBMC contract. The trouble is that + CBMC's `old` is only supported directly in the contract, not in functions + called from the contract. This means we either need to inline the contract + function body, which is brittle in the presence if control flow, or we must + extract the `old` expressions, evaluate them in the contract directly and pass + the results to the check function. However this means we must restrict the + expressions in `old`, because we now need to lower those by hand and even if + we could let rustc do it, CBMC's old has no support for function calls in its + argument expression. +- **Expanding all contract macros at the same time** Instead of expanding + contract macros one-at-a-atime and creating the onion layer structure we could + expand all subsequent one's with the outermost one, creating only one check + and replace function each. This is however brittle with respect to renaming. + If a user does `use kani::requires as my_requires` and then does multiple + `#[my_requires(condition)]` macro would not collect them properly since it can + only mathc syntactically and it does not know about the `use` and neither can + we restrict this kind if use or warn the user. By contrast the collection with + `kanitool::checked_with` is safe, because that attribute is generated by our + macro itself, so we can rely on the fact that it uses then canonical + representation. +- **Generating nested functions instead of siblings** Instead of generating the + `check` and `replace` functions as siblings to the contracted function we + could nest them like so + + ```rs + fn my_div(dividend: u32, divisor: u32) -> u32 { + fn my_div_check_5e3713(dividend: u32, divisor: u32) -> u32 { + ... + } + ... + } + ``` + + This could be beneficial if we want to be able to allow contracts on trait + impl items, in which case generating sibling functions is not allowed. The + only thing required to make this work is an additional pass over the condition + that replaces every `self` with a fresh identifier that now becomes the first + argument of the function. + + +## Open questions + +- We assume here entirely derived assigns clauses, instead of explicit one's. +- Semantics of arguments in postconditions: Shold they reflect changes to `mut` + arguments, e.g. a `mut i: u32`? I think that even in other tools (e.g. CBMC) + the actual value of arguments is copied into the function and therefore + changes to it are not reflected. +- Traits +- Our handling of `impl` in `reuqires` and `ensures` macros is brittle, though + probably can't be improved. If the contracted function is an `impl` item, then + the call to the next onion layer has to be `Self::()` instead of + `()`. However we have no reliable way of knowing when we are in an + `impl` fn. The macro uses a heuristic (is `self` or `Self` present) but in + theory a user can declare an `impl` fn that never uses either `Self` or `self` + in which case we generate broken code that throws cryptic error messages. + + + + +## Future possibilities + +- Enforcing contract checking before substitution +- Quantifiers +- Side effect freedom is currently enforced by CBMC. This means that the error originates there and is likely not legible. Intead Kani should perform a reachability analysis from the contract expressions and determine whether side effects are possible, throwing a graceful error. + +What are natural extensions and possible improvements that you predict for this feature that is out of the +scope of this RFC? Feel free to brainstorm here. \ No newline at end of file From b027ccef8cef98c1d03947db2d72b90a3e02db3f Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Tue, 25 Jul 2023 15:17:27 -0700 Subject: [PATCH 02/36] Minor Fixes --- rfc/src/rfcs/0008-function-contracts.md | 51 +++++++++++++++---------- 1 file changed, 31 insertions(+), 20 deletions(-) diff --git a/rfc/src/rfcs/0008-function-contracts.md b/rfc/src/rfcs/0008-function-contracts.md index d0cb4e5af99c..cd18175f4c74 100644 --- a/rfc/src/rfcs/0008-function-contracts.md +++ b/rfc/src/rfcs/0008-function-contracts.md @@ -157,7 +157,8 @@ function behavior when called with the same arguments. The complete code generated for the example is shown below and followed by an explanation of each component. ```rs -fn my_div_copy_965916(dividend: u32, divisor: u32) -> u32 { dividend / divisor } +fn my_div_check_copy_965916(dividend: u32, divisor: u32) -> u32 { dividend / divisor } +fn my_div_replace_copy_965916(dividend: u32, divisor: u32) -> u32 { kani::any() } #[kanitool::checked_with = "my_div_check_5e3713"] #[kanitool::replaced_with = "my_div_replace_5e3713"] @@ -186,7 +187,7 @@ fn my_div_check_965916(dividend: u32, divisor: u32) -> u32 { fn my_div_replace_965916(dividend: u32, divisor: u32) -> u32 { kani::assert(divisor != 0, "divisor != 0"); - kani::any() + my_div_replace_copy_965916(dividend, divisor) } ``` @@ -200,16 +201,20 @@ reemitted from the clause macro, the `kanitool` annotation is placed last in the attribute sequence, so that clauses expanded later can see it. Those subsequently expanded clauses use the `kanittol` annotations to determine which function to call inside them next. If no prior `kanitool` annotation is present -the original `my_div` or a copy of it is called instead. The copy is called in case -of the `check` function, since the compiler will later substitute all -occurrences of `my_div` with the `check` function which would also apply here and -cause an infinite recursion and make the original `my_div` body inaccessible. - -Each generated function is named `_{replace,check,copy}_`, where -`hash` is a hash of the original "function item" ast, in this case `my_div`, -including any attributes, such as `#[kanitool::checked_with = -"my_div_check_5e3713"]` from clauses expanded earlier, which guarantees the hash is -unique for each clause expansion. +then the check function calls a copy of `my_div`instead. The copy is called in +case of the `check` function, since the compiler will later substitute all +occurrences of `my_div` with the `check` function which would also apply here +and cause an infinite recursion and make the original `my_div` body +inaccessible. The replace function also makes a copy, the body of which is a +`kani::any()` non-determinstic value and this copy carries any memory predicates +which will be havoced by CBMC. + +Each generated function is named +`_{replace,check,reaplace_copy,check_copy}_`, where `hash` +is a hash of the original "function item" ast, in this case `my_div`, including +any attributes, such as `#[kanitool::checked_with = "my_div_check_5e3713"]` from +clauses expanded earlier, which guarantees the hash is unique for each clause +expansion. Type signatures of the generated functions are always identical to the type signature of the contracted function, including type parameters and lifetimes. @@ -267,7 +272,7 @@ modifications of memory they point to. Shadowing. -### `old` +### History Variables The special `old` builtin function is implemented as an AST rewrite. Consider the below example: @@ -284,10 +289,11 @@ impl Vec { to compare it to `self.len()` after `pop` mutates `self`. While `old` might appear like a function it is not. The implementation lifts the -argument expression to old via AST rewrite to before the call to `pop` and binds -it to a temporary variable. This makes `old` syntax rather than a function, but -also makes it very powerful as any expression is allowed in `old` including -calculations, function calls etc. Our example would generate the code below: +argument expression to old via AST rewrite in the `ensures` macro to before the +call to `pop` and binds it to a temporary variable. This makes `old` syntax +rather than a function, but also makes it very powerful as any expression is +allowed in `old` including calculations, function calls etc. Our example would +generate the code below: ```rs impl Vec { @@ -310,7 +316,8 @@ in e.g. `pop`. To use e.g. `old(self)` in such a case the user can create copies with the usual mechanism, such as `clone`, e.g. `old(self.clone())`. [^old-safety]: For unsafe rust we need additional protections which are not part - of this proposal. + of this proposal but are similar to the side effect freedom checks discussed + in the [future section](#future-possibilities) ### Substitution with `kani_compiler` @@ -339,9 +346,11 @@ invokes `goto-instrument`) via the `HarnessAttributes` struct, using an `Option` to represent a possible contract to enforce and a `Vec` as the contracts which are used as abstractions. -This is the technical portion of the RFC. Please provide high level details of the implementation you have in mind: +We call `goto-instrument --enforce-contract --replace-call-with-contract ` ## Detailed Design -Let us consider a complete example: +The lifecycle of a contract is split roughly into three phases. Let us consider +as an example this function: ```rs -#[kani::requires(divisor != 0)] -#[kani::ensures(result < dividend)] fn my_div(dividend: u32, divisor: u32) -> u32 { dividend / divisor } +``` + +1. Specifying the contract + + The user provides a specification (some combination of `requires`, `ensures`, + `assigns`, ...). In our case this may look like so: + + ```rs + #[kani::requires(divisor != 0)] + #[kani::ensures(result <= dividend)] + fn my_div(dividend: u32, divisor: u32) -> u32 { + dividend / divisor + } + ``` + + Any absent clause defaults to `true` (no constraints on input, output or + memory). + + +2. Checking the contract + + It is important that the combination of clauses is an + overapproximation of the function's behavior. This means the domain of the + function described (by the `requires`) clause is *at most* as large as the + actual function domain (the input space for which it's behavior is well + defined) and the codomain (described by `ensures`, `assigns` and `frees`) is + *at least* as large as the actual space of outputs a function may produce. + + For example in this case it would be permissible to use + `#[kani::requires(divisor > 100)]` (smaller permissible input domain) or + `#[kani::ensures(result < dividend + divisor)]` (larger possible output + domain), but e.g. `#[kani::ensures(result < dividend)]` is not allowed. + + The verifyer must check that this overapproximation property holds. To do so + it requires a suitably generic environment in which to test pre and + postconditions. The choice of environment has implications on soundness and + ideally the verifier can create an environment automatically. This is a + difficult problem due to heaps and part of [future + possibilities](#future-possibilities). For the purposes of this proposal the + user must provide a suitable harness as checking environment. This is done + with the `for_contract` annotation (below). + + ```rs + #[kani::proof] + #[kani::for_contract(my_div)] + fn my_div_harness() { + my_div(kani::any(), kani::any()) + } + ``` + + To facilitate contract checking against the implementation of `my_div` the + verifier performs code generation which turns preconditions (`requires`) into + `kani::assume` calls before function execution. This restricts the arbitrary + (`kani::any`) input domain from the harness to the one claimed by the + precondition. We also turn postconditions (`ensures`, `assigns`...) into + `kani::assert` calls *after* the function execution verifying the integrity + of the codomain. + + ... Done like stubbing + +- Substituting the contract + +Let us consider a complete example: + +```rs -#[kani::proof] -#[kani::for_contract(my_div)] -fn my_div_harness() { - my_div(kani::any(), kani::any()) -} #[kani::proof] #[kani::use_contract] @@ -319,6 +406,13 @@ with the usual mechanism, such as `clone`, e.g. `old(self.clone())`. of this proposal but are similar to the side effect freedom checks discussed in the [future section](#future-possibilities) +### Assigns Clauses + +- Inference +- Lvalue tracking +- Code generation for conditions +- Code generation for slice patterns + ### Substitution with `kani_compiler` Harnesses annotated with `for_contract` or `use_contract` are subject to @@ -440,7 +534,10 @@ This is the technical portion of the RFC. Please provide high level details of t - Enforcing contract checking before substitution - Quantifiers -- Side effect freedom is currently enforced by CBMC. This means that the error originates there and is likely not legible. Intead Kani should perform a reachability analysis from the contract expressions and determine whether side effects are possible, throwing a graceful error. +- Side effect freedom is currently enforced by CBMC. This means that the error + originates there and is likely not legible. Intead Kani should perform a + reachability analysis from the contract expressions and determine whether side + effects are possible, throwing a graceful error. What are natural extensions and possible improvements that you predict for this feature that is out of the scope of this RFC? Feel free to brainstorm here. \ No newline at end of file From 10707b6c31540aee5d7c03c2ca4ef676efad6866 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Wed, 26 Jul 2023 18:17:50 -0700 Subject: [PATCH 04/36] User experience Section rewrite --- rfc/src/rfcs/0008-function-contracts.md | 417 +++++++++++++++--------- 1 file changed, 258 insertions(+), 159 deletions(-) diff --git a/rfc/src/rfcs/0008-function-contracts.md b/rfc/src/rfcs/0008-function-contracts.md index f1893bd526c9..adb57dd594ce 100644 --- a/rfc/src/rfcs/0008-function-contracts.md +++ b/rfc/src/rfcs/0008-function-contracts.md @@ -16,222 +16,304 @@ behavior of units of code. The verification tool then leverages these approximations for modular verification which affords both scalability, but also allows for verifying unbounded loops and recursion. + + ## User Impact -Enabling function contracts is a non-invasive change. While it contains a new -API, that API is strictly additive for users. All prior operations are unchanged. + -The proposal in this RFC lays the ground work for two important goals. The -following describes those goals and any residual challenges to overcome to -achieve them. +Function contracts are a mechanism for a stubbing-like abstraction of concrete +implementations but with a significantly reduced threat to soundness. It also +lays the ground work for the following two ambitious goals. - **Scalability:** Function contracts are sound (over)abstractions of function behavior. By verifiying the contract against its implemetation and subsequently performing caller verification against the (cheaper) abstraction verification can be modularized, cached and thus scaled. - - This proposal would yield those benefits within a single verification session, - but would still re-verify the contract every session. With a suitable caching - mechanism this could be avoided in future. - **Unbounded Verification:** Contracts can be reasoned over inductively and thus verify recursive functions. - This proposal adds basic function contract functionality, but does not add an - indictive reasoning framework. - -## User Experience +Enabling function contracts is a non-invasive change. While it contains a new +API, that API is strictly additive for users. All prior operations are unchanged. -This proposal introduces 6 new annotations. +A `-Zcontracts` guard will be added wich is necessary to access any of the +contract functionality (attributes) described below. Any use of such attributes +without `-Zcontracts` is a compile time error. -- `#[kani::requires(CONDITION)]` and `#[kani::ensures(CONDITION)]` are - annotations for non-harness functions (lets use `f` for an example) and encode - pre- and postconditions respectively. +### Caveats - Preconditions are a refinement (beyhond the type) of the domain of the - `f`. +This proposal focuses on scalability benefits within a single verification session, +caching strategies for cross-session speedup are left to future work. - Postconditions are a refinement (beyond the type) of the codomain of the - `f`. +We add function contract functionality, but do not add the indictive reasoning +support needed for many unbounded problems, such as "deacreases" measures and +inductive lemmas. - `CONDITION`s are arbitrary boolean Rust expressions[^side-effects]. They may - reference the arguments of `f`. In the case of preconditions the value of - those arguments will be the value they have before `f` is called, in the case - of postconditions the value after the call to `f` returns. Additionally the - postcondition has access to the result of `f` in a variable called `result`. - (see [Open Questions](#open-questions) for a discussion on the `result` - variable.) +## User Experience - A postcondition may also use the special builtin `old` pseudo function. - `old(EXPR)` evaluates `EXPR` in the context *before* the call to `f`, e.g. - like a precondition. +Function contracts provide a way to approximate function behavior, verify the +approximation and subsequently use the approximation instead if the (possibly +costly) implementation. The lifecycle of a contract is split roughly into three +phases. Which we will explore on this simple example: - A function may be annotated with multiple `requires` and `ensures` clauses - that are implicitly conjoined. The sum total of the clauses and the assigns - clause (see below) comprise the function contract. +```rs +fn my_div(dividend: u32, divisor: u32) -> u32 { + dividend / divisor +} +``` -- `#[kani::for_contract(PATH)]` is a harness annotation which designates that - this harness is especially designed for verifying that function `PATH` obeys - it's contract. As an example assume `PATH` is `f`. +1. In the first phase we **specify** the approximation. Kani provides two new + annotations: `requires` (preconditions) to describe the expectations this + function has as to the calling context and `ensures` (postconditions) which + approximates function outputs in terms of function inputs. - The harness itself is implemented as usual by the user and verified the same - way as any other, including admitting other verification features like - stubbing. However additionally the preconditions of `f` id `kani::assume`'d - before every call to `f` and the postconditions are `kani::asssert`'ed after - it returns. + ```rs + #[kani::requires(divisor != 0)] + #[kani::ensures(result <= dividend)] + fn my_div(dividend: u32, divisor: u32) -> u32 { + dividend / divisor + } + ``` - Kani checks that `f` is in the call chain of this harness, but no further - checks are performed whether this harness is suitable for verifying the - contract of `f`, see also [Open Questions](#open-questions). - - Only one `for_contract` annotation is permitted per harness. - -- `#[kani::use_contract(PATH)]` is a harness annotation which instructs the - verifier to use the contract of `PATH` during verification instead of it's - body. + `requires` here indicates this function expects its `divisor` input to never + be 0, or it will not execute correctly (i.e. panic). - `use_contract(f)` is only safe if a `for_contract(f)` harness has previously - been verified. See [Future possibilities](#future-possibilities) for a - discussion on automatic enforcement mechanisms of this requirement. + `ensures` puts a bound on the output, relative to the `dividend` input. - Multiple `use_contract` annotations are permitted for a single harness. + Conditions in contracts are plain Rust expressions which can reference the + function arguments and, in case of `ensures`, the `result`[^result-naming] + result of the function. Syntactically Kani supports any Rust expression, + including function calls, defining types etc, however they must be + side-effect free[^side-effects]. -- The memory predicate family `#[kani::assigns(CONDITION, ASSIGN_RANGE...)]`, - `#[kani::frees(CONDITION, LVALUE...)]` expresses manual contraints on which - parts of an object the annotated function may assigned/freed. + [^result-naming]: See [open questions](#open-questions) for a discussion + about naming of the result variable. - In both cases the `CONDITION`s limit the applicability of the clause, may - reference the arguments of the function and can be omitted in which case they - default to `true`. +2. Checking the Contract - `LVALUE` are simple expressions permissible on the left hand side of an - assignment. They compose of the name of one function argument and zero or more - projections (dereference `*`, field access `.x`, slice indexing `[1]`). + Next Kani must make sure that the approximation we specified actually holds. + This is in opposition to the related "stubbing" mechanism, where the + approximation is not checked but always trusted. - The `ASSIGN_RANGE` permits any `LVALUE` but additionally permits more complex - slice expressions as the last projection and applies to pointer values. `[..]` - denotes the entirety of an allocation, `[i..]`, `[..j]` and `[i..j]` are - ranges of pointer offsets. A slicing syntax `p[i..j]` only applies if `p` is a - `*mut T` and points to an array allocation. The slice indices are offsets with - sizing `T`, e.g. in Rust `p[i..j]` would be equivalent to - `std::slice::from_raw_parts(p.offset(i), i - j)`. `i` must be smaller or equal - than `j`. + Kani must check that contract overapproximates the function to guarantee + soundness. Specifically the domain (inputs) of the function described (by the + `requires` clause) must be *at most* as large as the input space for which + the function's behavior is well defined, and the codomain (outputs, described + by `ensures`) must be *at least* as large as the actual space of outputs the + function may produce. - Because lvalues are restricted to using fields we break encapsulation here. - You may, if need be, reference fields that are usually hidden without an error - from the compiler. - - See also discussion on conditions in assigns clauses in - [Rationale](#rationale-and-alternatives) - -- To reduce developer burden we additionally propose to leverage the rust type - information to overapproximate the memory a function may modify. This allows - sound havocing in the absence of an `assigns` or `frees`. Inference of memory - clauses considers any `mut` reachable memory to be potentially freed, - reallocated or reassigned for any execution of the function. In addition any - reachable `static` variables are considered modified. - -[^side-effects]: Contract conditions are required to be side effect free, e.g. - perform no I/O perform no memory mutation and allocate/free no heap memory. - See also the side effect discussion in [Open Questions](#open-questions). + For example in our case it would be permissible to use + `#[kani::requires(divisor > 100)]` (smaller permissible input domain) or + `#[kani::ensures(result < dividend + divisor)]` (larger possible output + domain), but e.g. `#[kani::ensures(result < dividend)]` (small output) is not + allowed. -This proposal also introduces a new hidden builtin `kani::unchecked_deref`. The -necessity for this builtin is explained [later](#dealing-with-mutable-borrows). + To facilitate the check Kani needs a suitable environment to verify our + function in. For this proposal the environment must be provided by us (the + users). See [future possibilities](#future-possibilities) for a discussion + about the arising soundness issues and their remedies. - + ```rs + #[kani::proof_for_contract(my_div)] + fn my_div_harness() { + my_div(kani::any(), kani::any()) + } + ``` + Similar to a unit-test harness for any other function we are supposed to + create inputs for the function that are as generic/abstract as possible to + make sure we catch all edge cases, then call the function at least once with + those abstract inputs. If we forget to call `my_div` Kani would report an + error. + + Unlike a unit-test we can however elide any checks of the output and + post-call state. Instead Kani uses the conditions we specified in the + contract as checks. It inserts the preconditions (`requires`) of `my_div` as + `kani::assume` *before* the call to `my_div`, to ensure it only tests the + function on inputs it is actually defined for. Postconditions (`ensures`) are + inserted as `kani::assert` checks *after* the call to `my_div`. + + The expanded version of our harness and function is equivalent to the following: -## Detailed Design + ```rs + #[kani::proof] + fn my_div_harness() { + let dividend = kani::any(); + let divisor = kani::any(); + kani::assume(divisor != 0); + let result = my_div(dividend, divisor); + kani::assert(result <= dividend); + } + ``` -The lifecycle of a contract is split roughly into three phases. Let us consider -as an example this function: + This expanded harness is then verified like any other harness but also gives + the green light for the next step: verified stubbing. -```rs -fn my_div(dividend: u32, divisor: u32) -> u32 { - dividend / divisor -} -``` +3. In the last phase the **verified** contract is ready for us to use to + **stub** in other harnesses. -1. Specifying the contract + Unlike in regular stubbing Kani there to be at least one associated + `proof_for_contract` harness for each function to stub *and* it requires all + such harnesses to pass verification before attempting verification of any + harnesses that use it as a stub. - The user provides a specification (some combination of `requires`, `ensures`, - `assigns`, ...). In our case this may look like so: + A possible harness that uses our `my_div` contract could be the following: ```rs - #[kani::requires(divisor != 0)] - #[kani::ensures(result <= dividend)] - fn my_div(dividend: u32, divisor: u32) -> u32 { - dividend / divisor + #[kani::proof] + #[kani::stub_verified(my_div)] + fn use_div() { + let v = vec![...]; + let some_idx = my_div(v.len() - 1, 3); + v[some_idx]; } ``` - Any absent clause defaults to `true` (no constraints on input, output or - memory). - - -2. Checking the contract - - It is important that the combination of clauses is an - overapproximation of the function's behavior. This means the domain of the - function described (by the `requires`) clause is *at most* as large as the - actual function domain (the input space for which it's behavior is well - defined) and the codomain (described by `ensures`, `assigns` and `frees`) is - *at least* as large as the actual space of outputs a function may produce. - - For example in this case it would be permissible to use - `#[kani::requires(divisor > 100)]` (smaller permissible input domain) or - `#[kani::ensures(result < dividend + divisor)]` (larger possible output - domain), but e.g. `#[kani::ensures(result < dividend)]` is not allowed. - - The verifyer must check that this overapproximation property holds. To do so - it requires a suitably generic environment in which to test pre and - postconditions. The choice of environment has implications on soundness and - ideally the verifier can create an environment automatically. This is a - difficult problem due to heaps and part of [future - possibilities](#future-possibilities). For the purposes of this proposal the - user must provide a suitable harness as checking environment. This is done - with the `for_contract` annotation (below). + To use the contract as a stub Kani must first ensure the calling context is + safe. It a `kani::assert` for the preconditions (`requires`) of `my_div` + before the call. Then it replaces the result of `my_div` with a + non-deterministic value (see [havocing](#memory-predicates-and-havocing) for + the equivalent for mutable memory), constrained by a `kani::assume` of + `'my_div`'s postconditions (`ensures`). + And the expanded version is equivalent to this: + ```rs #[kani::proof] - #[kani::for_contract(my_div)] - fn my_div_harness() { - my_div(kani::any(), kani::any()) + #[kani::stub_verified(my_div)] + fn use_div() { + let v = vec![...]; + let dividend = v.len() - 1; + let divisor = 3; + kani::assert(divisor != 0); + let result = kani::any(); + kani::assume(result <= dividend); + let some_idx = result; + v[some_idx]; } ``` - To facilitate contract checking against the implementation of `my_div` the - verifier performs code generation which turns preconditions (`requires`) into - `kani::assume` calls before function execution. This restricts the arbitrary - (`kani::any`) input domain from the harness to the one claimed by the - precondition. We also turn postconditions (`ensures`, `assigns`...) into - `kani::assert` calls *after* the function execution verifying the integrity - of the codomain. + Notice that this performs no actual computation for `my_div` (other than the + conditions) which allows us to avoid something potentially costly. + +Also notice that Kani was able to express both contract checking and stubbing +with existing capabilities, the important feature is the enforcement. The +checking is, by construction, performed **against the same condition** that is +later used as stub, which ensures soundness (see discussion on lingering threats +to soundness in the [future](#future-possibilities) section) and guards against +stubs diverging from their checks. - ... Done like stubbing +### History Variables -- Substituting the contract +Kani's contract language contains additional support for reasoning about changes +to memory. One case where this is necessary is whenever `ensures` needs to +reason about state before the function call. By default it only has access to +state after the call completes, which will be different if the call mutates +memory. -Let us consider a complete example: +Consider the `Vec::pop` function ```rs +impl Vec { + fn pop(&mut self) -> Option { + ... + } +} +``` +If we want to describe in which case the result is `Some`, we need to know +whether `self` is empty *before* `pop` is called. To do this Kani provides the +`old(EXPR)` pseudo function, which evaluates `EXPR` before the call (e.g. to +`pop`) and makes the result available to `ensures`. it would be used like so -#[kani::proof] -#[kani::use_contract] -fn use_div() { - let v = vec![...]; - let some_idx = my_div(v.len() - 1, 3); - v[some_idx]; +```rs +impl Vec { + #[kani::ensures(old(self.is_empty()) || result.is_some())] + fn pop(&mut self) -> Option { + ... + } } ``` -The following subsections describe the Kani pipeline for this example in order. +`old` allows evaluating any (side-effect free[^side-effects]) Rust expression +but Rust enforces that it does not borrow so as to observe the mutations from +e.g. `pop`, as that would defeat the purpose. Instead Kani encourages us to make +copies (using e.g. `clone()`) if necessary. + +Note also that `old` is syntax, not a function and implemented as an extraction +and lifting during code generation. It can reference e.g. `pop`'s arguments but +not local variables. Compare the following + +**Invalid ❌:** `#[kani::ensures({ let x = self.is_empty(); old(x) } || result.is_some())]` +**Valid ✅:** `#[kani::ensures(old({ let x = self.is_empty(); x }) || result.is_some())]` + +And it will only be recognized as `old(...)`, not as `let old1 = old; old1(...)` etc. + +### Memory Predicates and Havocing + +The last new feature added are predicates to refine a function's access to heap +memory. A memory footprint is used by the verifier to perform "havocing" during +contract stubbing. Recall that stubbing replaces the result value with a +non-deterministic `kani::any()`, havocing is the equivalent memory regions +touched by the function. Any memory regions in the footprint are "havoced" by +the verifier, that is replaced by a non-deterministic value (subject to type +constraints). + +By default Kani infers a memory footprint as all memory reachable from a `&mut` +input or any `static` global referenced, directly or transitively, by the +function. While the inferred footprint is sound and enough for successful +contract checking[^inferred-footprint] it can easily turn large section of +memory to non-deterministic values, invalidate invariants of your program and +cause the verification to fail when the contract is used as a stub. + +[^inferred-footprint]: While inferred memory footprints are sound for both safe + and unsafe rust certain features in unsafe rust (e.g. `RefCell`) get + inferred incorrectly and will lead to a failing contract check. + +To reduce the scope of havocing Kani provides the `#[kani::assigns(CONDITION, +ASSIGN_RANGE...)]` and `#[kani::frees(CONDITION, LVALUE...)]` attributes. When +these attributes are provided Kani will only havoc the location mentioned in +`ASSIGN_RANGE` and `LVALUE` instead of the inferred footprint. Additionally Kani +verifies during checking that only the mentioned memory regions are touched and +only under the mentioned conditions. + +`CONDITION`s limit when the clause applies, may reference the arguments of the +function and can be omitted. + +`LVALUE` are simple expressions permissible on the left hand side of an +assignment. They compose of the name of one function argument and zero or more +projections (dereference `*`, field access `.x`, slice indexing `[1]`). + +The `ASSIGN_RANGE` permits any `LVALUE` but additionally permits more complex +slice expressions as the last projection and applies to pointer values. `[..]` +denotes the entirety of an allocation, `[i..]`, `[..j]` and `[i..j]` are +ranges of pointer offsets. A slicing syntax `p[i..j]` only applies if `p` is a +`*mut T` and points to an array allocation. The slice indices are offsets with +sizing `T`, e.g. in Rust `p[i..j]` would be equivalent to +`std::slice::from_raw_parts(p.offset(i), i - j)`. `i` must be smaller or equal +than `j`. + +Because lvalues are restricted to using projections only Kani must break +encapsulation here. If need be we may reference fields that are usually hidden, +without an error from the compiler. + +See also discussion on conditions in assigns clauses in + +[^side-effects]: Code used in contracts is required to be side effect free which + means it must not perform I/O, mutate memory (`&mut` vars and such) and + (de)allocate heap memory. This is enforced by the verifier, see the + discussion in the [future](#future-possibilities) section. + +What is the scope of this RFC? Which use cases do you have in mind? Explain how users will interact with it. Also +please include: + +## Detailed Design + + + ### Code generation in `kani_macros` @@ -338,6 +420,9 @@ impl Vec { } } ``` +This proposal also introduces a new hidden builtin `kani::unchecked_deref`. The +necessity for this builtin is explained [later](#dealing-with-mutable-borrows). + `self` would not be permitted to be used here until `result` goes out of scope and releasese the borrow. To avoid this issue we break the borrowchecker @@ -454,6 +539,9 @@ This is the technical portion of the RFC. Please provide high level details of t ## Rationale and alternatives + + + + - We assume here entirely derived assigns clauses, instead of explicit one's. - Semantics of arguments in postconditions: Shold they reflect changes to `mut` arguments, e.g. a `mut i: u32`? I think that even in other tools (e.g. CBMC) @@ -523,6 +613,11 @@ This is the technical portion of the RFC. Please provide high level details of t `impl` fn. The macro uses a heuristic (is `self` or `Self` present) but in theory a user can declare an `impl` fn that never uses either `Self` or `self` in which case we generate broken code that throws cryptic error messages. +- Making result special. Should we use special syntax here like `@result` or + `kani::result()`, though with the latter I worry that people may get confused + because it is syntactic and not subject to usual `use` renaming and import + semantics. Alternatively we can let the user pick the name with an additional + argument to `ensures`, e.g. `ensures(my_result_var, CONDITION)` + - Enforcing contract checking before substitution - Quantifiers - Side effect freedom is currently enforced by CBMC. This means that the error originates there and is likely not legible. Intead Kani should perform a reachability analysis from the contract expressions and determine whether side effects are possible, throwing a graceful error. +- Soundness issues with harnesses and remedies that are in the works +- What about mutable trait inputs (wrt memory access patters), e.g. a `mut impl AccessMe` What are natural extensions and possible improvements that you predict for this feature that is out of the scope of this RFC? Feel free to brainstorm here. \ No newline at end of file From 7d837ef48ff2abd7bf980707bb6a8373f7fb5bbd Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 27 Jul 2023 11:08:45 -0700 Subject: [PATCH 05/36] Work on design section --- rfc/src/rfcs/0008-function-contracts.md | 45 ++++++++++++++++++++++++- 1 file changed, 44 insertions(+), 1 deletion(-) diff --git a/rfc/src/rfcs/0008-function-contracts.md b/rfc/src/rfcs/0008-function-contracts.md index adb57dd594ce..7e439a1c6805 100644 --- a/rfc/src/rfcs/0008-function-contracts.md +++ b/rfc/src/rfcs/0008-function-contracts.md @@ -314,10 +314,53 @@ please include: +Kani implements the functionality of function contracts in two places. + +1. Code generation in the `requires` and `ensures` macros. +2. GOTO level contracts using CBMC's contract language generated in + `kani-compiler` for handling memory predicates. + +With some additional plumbing in the compiler and the driver. ### Code generation in `kani_macros` -The `requires` and `ensures` macros generate new sibling functions to e.g. `my_div` +The `requires` and `ensures` macros perform code generation in the macro, +creating a `check` and a `replace` function which use `assert` and `assume` as +described in the [user expersection](#user-experience) section. Both are +attached via a `kanitool` attribute to the function which they are checking and +replacing respectively. + +The code generation in the macros is straightforward, save two features: `old` +and the borrow checker. + +The special `old` builtin function is implemented as an AST rewrite. Consider +the below example: + +```rs +impl Vec { + #[kani::ensures(self.is_empty() || self.len() == old(self.len()) - 1)] + fn pop(&mut self) -> Option { + ... + } +} +``` + +The `ensures` macro performs an AST rewrite constiting of an extraction of the +expressions in `old` and a replacement with a fresh local variable, creating the +following: + +```rs +impl Vec { + fn check_pop(&mut self) -> Option { + let old_1 = self.len(); + let result = Self::pop(self); + kani::assert(self.is_empty() || self.len() == old_1 - 1) + } +} +``` + +The expression inse + (see also discussion in [alternatives](#rationale-and-alternatives)). One function is generated which corresponds to checking the contract holds for the implementation. One function is generated which corresponds to approximating the From eeaa4e4bcb6dbff91e20f266b2cda1934f5c2120 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 27 Jul 2023 13:48:06 -0700 Subject: [PATCH 06/36] Pass over design --- rfc/src/rfcs/0008-function-contracts.md | 232 ++++-------------------- 1 file changed, 39 insertions(+), 193 deletions(-) diff --git a/rfc/src/rfcs/0008-function-contracts.md b/rfc/src/rfcs/0008-function-contracts.md index 7e439a1c6805..fb0288c81a84 100644 --- a/rfc/src/rfcs/0008-function-contracts.md +++ b/rfc/src/rfcs/0008-function-contracts.md @@ -84,7 +84,8 @@ fn my_div(dividend: u32, divisor: u32) -> u32 { function arguments and, in case of `ensures`, the `result`[^result-naming] result of the function. Syntactically Kani supports any Rust expression, including function calls, defining types etc, however they must be - side-effect free[^side-effects]. + side-effect free[^side-effects]. Multiple `requires` and `ensrues` clauses + are allowed on the same function, they are implicitly logically conjoined. [^result-naming]: See [open questions](#open-questions) for a discussion about naming of the result variable. @@ -328,9 +329,10 @@ The `requires` and `ensures` macros perform code generation in the macro, creating a `check` and a `replace` function which use `assert` and `assume` as described in the [user expersection](#user-experience) section. Both are attached via a `kanitool` attribute to the function which they are checking and -replacing respectively. +replacing respectively. See also the [discussion](#rationale-and-alternatives) +about why we decided to generate check and replace functions like this. -The code generation in the macros is straightforward, save two features: `old` +The code generation in the macros is straightforward, save two aspects: `old` and the borrow checker. The special `old` builtin function is implemented as an AST rewrite. Consider @@ -359,89 +361,23 @@ impl Vec { } ``` -The expression inse +Nested invocations of `old` are prohibited (Kani throws an error) and the +expression inside may only refer to the function arguments and not other local +variables in the contract (Rust will report those variables as not being in +scope). -(see also discussion in [alternatives](#rationale-and-alternatives)). One -function is generated which corresponds to checking the contract holds for the -implementation. One function is generated which corresponds to approximating the -function behavior when called with the same arguments. +The borrow checker also ensures for us that none of the temporary variables +borrow in a way that would be able to observe the moditication in `pop` which +would occur for instance if the user wrote `old(self)`. Instead of borrowing +copies should be created (e.g. `old(self.clone())`). This is only enforced for +safe rust though. -The complete code generated for the example is shown below and followed by an explanation of each component. - -```rs -fn my_div_check_copy_965916(dividend: u32, divisor: u32) -> u32 { dividend / divisor } -fn my_div_replace_copy_965916(dividend: u32, divisor: u32) -> u32 { kani::any() } - -#[kanitool::checked_with = "my_div_check_5e3713"] -#[kanitool::replaced_with = "my_div_replace_5e3713"] -fn my_div(dividend: u32, divisor: u32) -> u32 { dividend / divisor } - -fn my_div_check_5e3713(dividend: u32, divisor: u32) -> u32 { - let dividend_renamed = kani::untracked_deref(÷nd); - let divisor_renamed = kani::untracked_deref(&divisor); - let result = my_div_check_965916(dividend, divisor); - kani::assert(result <= dividend_renamed, "result <= dividend"); - result -} - -fn my_div_replace_5e3713(dividend: u32, divisor: u32) -> u32 { - let dividend_renamed = kani::untracked_deref(÷nd); - let divisor_renamed = kani::untracked_deref(&divisor); - let result = my_div_replace_965916(dividend, divisor); - kani::assume(result <= dividend_renamed); - result -} - -fn my_div_check_965916(dividend: u32, divisor: u32) -> u32 { - kani::assume(divisor != 0); - my_div_copy_965916(dividend, divisor) -} - -fn my_div_replace_965916(dividend: u32, divisor: u32) -> u32 { - kani::assert(divisor != 0, "divisor != 0"); - my_div_replace_copy_965916(dividend, divisor) -} -``` - - -To support mutiple clauses while performing all code generation at macro -expansion time each clause separately generates both a checking and a -replacement function, wrapping like onion layers around any prior checks. Both -the generated check and replace function is attached to the annotated function -using `kanitool::{checked,replaced}_with` annotations. When the item is -reemitted from the clause macro, the `kanitool` annotation is placed last in -the attribute sequence, so that clauses expanded later can see it. Those -subsequently expanded clauses use the `kanittol` annotations to determine which -function to call inside them next. If no prior `kanitool` annotation is present -then the check function calls a copy of `my_div`instead. The copy is called in -case of the `check` function, since the compiler will later substitute all -occurrences of `my_div` with the `check` function which would also apply here -and cause an infinite recursion and make the original `my_div` body -inaccessible. The replace function also makes a copy, the body of which is a -`kani::any()` non-determinstic value and this copy carries any memory predicates -which will be havoced by CBMC. - -Each generated function is named -`_{replace,check,reaplace_copy,check_copy}_`, where `hash` -is a hash of the original "function item" ast, in this case `my_div`, including -any attributes, such as `#[kanitool::checked_with = "my_div_check_5e3713"]` from -clauses expanded earlier, which guarantees the hash is unique for each clause -expansion. - -Type signatures of the generated functions are always identical to the type -signature of the contracted function, including type parameters and lifetimes. - - -### Dealing with mutable borrows - -Preconditions (`requires`) are emitted as-is into the generated function, -providing access to the function arguments directly. This is safe because they -are required to be side-effect free[^side-effects]. - -Postconditions (`ensures`) have to be handled specially. They can reference the -arguments of the function, though not modify them. However this is problematic -even without modification if part of an input is borrowed mutably as would be -the case in the following example of the `Vec::split_at_mut` function. +The second part relevant for the implementation is how we deal with the borrow +checker. Postconditions (`ensures`) reference the arguments of the function, +though don't modify them. However this is problematic even without modification +if part of an input is borrowed mutably in the return value. For instance the +`Vec::split_at_mut` function does this and a sensible contract for it might look +as follows: ```rs impl Vec { @@ -452,123 +388,33 @@ impl Vec { } ``` -This contract refers simultaneously to `self` and the result. Since the method however borrows `self` mutably, the borrow checker would not allow the following simplistic code generation: - -```rs -impl Vec { - fn split_at_mut_check_(&mut self, i: usize) -> (&mut [T], &mut [T]) { - let result = self.split_at_mut(i); - kani::assert(self.len() == result.0.len() + result.1.len()); - result - } -} -``` -This proposal also introduces a new hidden builtin `kani::unchecked_deref`. The -necessity for this builtin is explained [later](#dealing-with-mutable-borrows). - - -`self` would not be permitted to be used here until `result` goes out of scope -and releasese the borrow. To avoid this issue we break the borrowchecker -guarantee with a new biltin `fn kani::unsafe_deref(t: &T) -> T`. The -implementation of this function is simply a CBMC level `*` (deref). In Rust this -implementation would be illegal without the `Copy` trait (which generates a -copy) but in CBMC this is acceptable. Breaking the borrow checker this way is safe for 2 reasons: +This contract refers simultaneously to `self` and the result. Since the method +however borrows `self` mutably, the borrow checker would complain about a simple +`assert` of the postcondition. To work around this we strategically break the +borrowing rules using a new hidden builtin `kani::unckecked_deref` with the type +signature `for fn (&T) -> T` which is essentially a C-style dereference +operation. Breaking the borrow checker like this is safe for 2 reasons: 1. Postconditions are not allowed perform mutation[^side-effects] and 2. Post conditions are of type `bool`, meaning they cannot leak references to the arguments and cause race conditions. -Circumventing the borrow checker is facilitated with a visit over the initial -postcondition expression that renames every occurrence of the arguments to a -fresh identifier and then generates a call `let i = unsafe_deref(&a)` for each -argument `a` and fresh identifier `i` **before** the call to the contracted -function. Because `unsafe_deref` creates shallow copies, they will witness any -modifications of memory they point to. +The "copies" of arguments created by by `unsafe_deref` are stored as fresh local +variables and their occurrence in the postcondition is renamed. -Shadowing. +### Changes to Other Components -### History Variables - -The special `old` builtin function is implemented as an AST rewrite. Consider the below example: - -```rs -impl Vec { - #[kani::ensures(self.is_empty() || self.len() == old(self.len()) - 1)] - fn pop(&mut self) -> Option { - ... - } -} -``` - -`old` gives the user access to `self.len()`, evaluated before `pop` to be able -to compare it to `self.len()` after `pop` mutates `self`. - -While `old` might appear like a function it is not. The implementation lifts the -argument expression to old via AST rewrite in the `ensures` macro to before the -call to `pop` and binds it to a temporary variable. This makes `old` syntax -rather than a function, but also makes it very powerful as any expression is -allowed in `old` including calculations, function calls etc. Our example would -generate the code below: - -```rs -impl Vec { - fn pop_check_(&mut self) -> Option { - let old_1 = self.len(); - let result = Self::pop_copy_(self); - kani::assert(self.is_empty() || self.len() == old_1 - 1) - } -} -``` +Contract enforcement and replacement (`kani::proof_for_contract(f)`, +`kani::verified_stub(f)`) both dispats to the stubbing logic, replacing `f` with +the generated check and replace function respectively. If `f` has no contract, +an error is thrown. -Note that unlike for arguments for postconditions, we do not use `unsafe_deref` -to break the borrowing rules. Unlike for those arguments, which must witness -mutations, the expression in `old` is supposed to reflect the state *before* the -function call and must therefore not observe mutations performed by e.g. `pop`. -We can use the borrowchecker to enforce this for safe Rust[^old-safety]. The -borrow checker will ensure that none of the temporary variables created borrow -from any mutable arguments and thus guarantee that they cannot witness mutations -in e.g. `pop`. To use e.g. `old(self)` in such a case the user can create copies -with the usual mechanism, such as `clone`, e.g. `old(self.clone())`. - -[^old-safety]: For unsafe rust we need additional protections which are not part - of this proposal but are similar to the side effect freedom checks discussed - in the [future section](#future-possibilities) - -### Assigns Clauses - -- Inference -- Lvalue tracking -- Code generation for conditions -- Code generation for slice patterns - -### Substitution with `kani_compiler` - -Harnesses annotated with `for_contract` or `use_contract` are subject to -substitution. Only one `for_contract(f)` annotation is allowed per harness and -it triggers substitution of the target function `f` with the check function in -the `#[kanitool::checked_with = ...]` annotation on `f`. Multiple -`use_contract(g)` annotations are allowed on each harness, including on -`for_contract` harnesses, though the simultaneous presence of `for_contract` and -`use_contract` for the same target function is not permissible. - -If the target function (`f` or `g`) does not have a `checked_with` or -`replaced_with` attribute (respectively) an error is thrown. - -### Invoking `goto-instrument` from `kani-driver` - -In addition to the Kani side substitiution we also perform instrumentation on -the CBMC because we rely on it's support for memory predicates. The -generated memory predicates are emitted from the compiler as CBMC contracts. To -enforce the memory contract `goto-instrument` has to be invoked with the correct -functions name. Since this is after lowering into GOTO-C the name provided has -to be the mangled name of the monomorphized instances. The compiler determines -which monomorphized version of the contracted functions are used in a -reachability pass. Those names are passed to the driver (as the component that -invokes `goto-instrument`) via the `HarnessAttributes` struct, using an `Option` -to represent a possible contract to enforce and a `Vec` as the contracts which -are used as abstractions. - -We call `goto-instrument --enforce-contract --replace-call-with-contract ` +For memory predicates Kani relies on CBMC. Generated memory predicates (whether +derived from types of from explicit clauses) are emitted from the compiler as +GOTO contracts in the artifact. Then the driver invokes `goto-instrument` with +the name of the GOTO-level function names to enforce or replace the memory +contracts. The compiler communicates the names of the function via harness +metadata. -- We assume here entirely derived assigns clauses, instead of explicit one's. -- Semantics of arguments in postconditions: Shold they reflect changes to `mut` - arguments, e.g. a `mut i: u32`? I think that even in other tools (e.g. CBMC) - the actual value of arguments is copied into the function and therefore - changes to it are not reflected. -- Trait contracts - Is it really correct to return `kani::any()` from the replacement copy, even if it can be a pointer? - Our handling of `impl` in `reuqires` and `ensures` macros is brittle, though @@ -518,14 +508,29 @@ This is the technical portion of the RFC. Please provide high level details of t -- Enforcing contract checking before substitution -- Quantifiers -- Side effect freedom is currently enforced by CBMC. This means that the error +- **Quantifiers:** Quantifiers are like logic-level loops and a powerful + reasoning helper. CBMC has support for both `exists` and `forall`, but the + code generation is difficult. The most ergonomic and easy way to implement + quantifiers on the Rust side is as higher-order functions taking `Fn(T) -> + bool`, where `T` is some arbitrary type that can be quantified over. This + interface is familiar to developers, but the code generation is tricky, as + CBMC level quantifiers only allow certain kinds of expressions. This + necessiates a rewrite of the `Fn` closure to a compliant expression. +- **Side effect** freedom is currently enforced by CBMC. This means that the error originates there and is likely not legible. Intead Kani should perform a reachability analysis from the contract expressions and determine whether side effects are possible, throwing a graceful error. -- Soundness issues with harnesses and remedies that are in the works +- Letting the user supply the **harnesses for checking contracts** is a source of + unsoundness, if corner cases are not adequately covered. Ideally Kani would + generate the check harness automatically, but this is difficult both because + heap datastructures are potentially infinite, and also because it must observe + user-level invariants. - What about mutable trait inputs (wrt memory access patters), e.g. a `mut impl AccessMe` - -What are natural extensions and possible improvements that you predict for this feature that is out of the -scope of this RFC? Feel free to brainstorm here. \ No newline at end of file +- **Trait contracts:** Ous proposal could be extended easily to handle simple + trait contracts. The macros would generate new trait methods with default + implementation, similar to the functions it generates today. Using sealed + types we can prevent the user from overwriting the generated contract methods. + Contracts for the trait and contracts on it's impls are combined by stubbing + the original method depending on context. The occurrence inside the contract + generated from the trait method is replaced by the impl contract. Any other + occurrence is replaced by the just altered trait method contract. From 6a79ca1ebc2cdbe0cc98047e80d569cd66d80f1e Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 27 Jul 2023 15:12:09 -0700 Subject: [PATCH 08/36] Conversation fixes --- rfc/src/rfcs/0008-function-contracts.md | 66 ++++++++++++++++++++----- 1 file changed, 55 insertions(+), 11 deletions(-) diff --git a/rfc/src/rfcs/0008-function-contracts.md b/rfc/src/rfcs/0008-function-contracts.md index b6a88da709d6..bd4186f20cb4 100644 --- a/rfc/src/rfcs/0008-function-contracts.md +++ b/rfc/src/rfcs/0008-function-contracts.md @@ -9,21 +9,26 @@ ## Summary -Contracts are a powerful tool for verification. They are both a convenient way -to write specifications as well as allowing users to soundly approximate the -behavior of units of code. The verification tool then leverages these -approximations for modular verification which affords both scalability, but also -allows for verifying unbounded loops and recursion. +Function contracts are a mechanism for a stubbing-like abstraction of concrete +implementations but with a significantly reduced threat to soundness[^simple-unsoundness]. +Lays the ground work for modular verification. ## User Impact -Function contracts are a mechanism for a stubbing-like abstraction of concrete -implementations but with a significantly reduced threat to soundness. It also -lays the ground work for the following two ambitious goals. +Function contracts provide an interface for verified abstraction, a mechanism +similar to stubbing, but sound[^simple-unsoundness]. It also paves the way for +the following two ambitious goals. + +[^simple-unsoundness]: The main remaining threat to soundness in the use of + contracts, as defined in this proposal, is the reliance on user-supplied + harnesses for contract checking (explained in bulled 2 of [user + experience](#user-experience)). A more thorough discussion on the dangers + and potential remedies can be found in the [future](#future-possibilities) + section. - **Scalability:** Function contracts are sound (over)abstractions of function behavior. By verifiying the contract against its implemetation and @@ -45,7 +50,7 @@ This proposal focuses on scalability benefits within a single verification sessi caching strategies for cross-session speedup are left to future work. We add function contract functionality, but do not add the inductive reasoning -support needed for many unbounded problems, such as "deacreases" measures and +support needed for many unbounded problems, such as "decreases" measures and inductive lemmas. ## User Experience @@ -302,11 +307,50 @@ encapsulation here. If need be we can reference fields that are usually hidden, without an error from the compiler. [^side-effects]: Code used in contracts is required to be side effect free which - means it must not perform I/O, mutate memory (`&mut` vars and such) and + means it must not perform I/O, mutate memory (`&mut` vars and such) or (de)allocate heap memory. This is enforced by the verifier, see the discussion in the [future](#future-possibilities) section. +### Detailed Attribute Contraints Overview + +Any violation of the following constraints constitutes a compile-time error. + +- A function may have any number of `requires`, `ensures`, `assigns` and `frees` + attributes. Any function with at least one such annotation is considered as + "having a contract". + + Harnesses (general or for contract checking) may not have any such annotation. + +- A function may have one `proof_for_contract(TARGET)` annotation. `TARGET` must + "have a contract". Multiple functions may have `proof_for_contract` + annotations with the same `TARGET`. All such harnesses must pass verification, + before `TARGET` may be used as a verified stub. + + A `proof_for_contract` harness may use both `stub` and `stub_verified`, though + the `TARGET` may not appear in either. + + Kani checks that `TARGET` is reachable from the `proof_for_contract` harness, + but it does not warn if stubbed functions use `TARGET`[^stubcheck]. + + A `proof_for_contract` function may not have the `kani::proof` attribute (it + is already implied by `proof_for_contract`). + +- A harness may have multiple `stub_verified(TARGET)` attributes. Each `TARGET` + must "have a contract". No `TARGET` may appear twice. + +- Harnesses may combine `stub(S_TARGET, ..)` and `stub_verified(V_TARGET)` + annotations, though no target may occur in `S_TARGET`s and `V_TARGET`s + simultaneously. + +- For mutually recursive functions using `stub_verified` kani will check their + contracts in non-deterministic order and assume each time the respective other + check succeeded. + +[^stubcheck]: Kani cannot report the occurrence of a contract function to check + in stubbed functions as errors, because the mechanism is needed to verify + mutually recursive functions. + ## Detailed Design @@ -401,7 +445,7 @@ variables and their occurrence in the postcondition is renamed. ### Changes to Other Components Contract enforcement and replacement (`kani::proof_for_contract(f)`, -`kani::verified_stub(f)`) both dispatch to the stubbing logic, stubbing `f` with +`kani::stub_verified(f)`) both dispatch to the stubbing logic, stubbing `f` with the generated check and replace function respectively. If `f` has no contract, an error is thrown. From b4a3d8c0e1494c95c10f38ea742f4bf348f9c627 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Tue, 1 Aug 2023 16:11:42 -0700 Subject: [PATCH 09/36] Hopefully all non-assigns/mem-predicates comments --- rfc/src/rfcs/0008-function-contracts.md | 107 +++++++++++------------- 1 file changed, 51 insertions(+), 56 deletions(-) diff --git a/rfc/src/rfcs/0008-function-contracts.md b/rfc/src/rfcs/0008-function-contracts.md index bd4186f20cb4..e934c60ffbd4 100644 --- a/rfc/src/rfcs/0008-function-contracts.md +++ b/rfc/src/rfcs/0008-function-contracts.md @@ -1,27 +1,34 @@ - **Feature Name:** Function Contracts -- **Feature Request Issue:** - +- **Feature Request Issue:** [#2652](https://github.com/model-checking/kani/issues/2652) - **RFC PR:** [#2620](https://github.com/model-checking/kani/pull/2620) - **Status:** Under Review - **Version:** 0 - **Proof-of-concept:** [features/contracts](https://github.com/model-checking/kani/tree/features/contracts) +- **Gate:** `-Zcontracts`, enforced by compile time error[^gate] + +[^gate]: Enforced gates means all uses of constructs (functions, annotations, + macros) in this RFC are an error. ------------------- ## Summary -Function contracts are a mechanism for a stubbing-like abstraction of concrete +Function contracts are a mechanism for a [stubbing]-like abstraction of concrete implementations but with a significantly reduced threat to soundness[^simple-unsoundness]. Lays the ground work for modular verification. +[stubbing]: https://model-checking.github.io/kani/rfc/rfcs/0002-function-stubbing.html + ## User Impact Function contracts provide an interface for verified abstraction, a mechanism -similar to stubbing, but sound[^simple-unsoundness]. It also paves the way for -the following two ambitious goals. +similar to [stubbing], but sound[^simple-unsoundness]. This kind of verified +stubbing allows for modular verification, which paves the way for the +following two ambitious goals. [^simple-unsoundness]: The main remaining threat to soundness in the use of contracts, as defined in this proposal, is the reliance on user-supplied @@ -40,25 +47,22 @@ the following two ambitious goals. Enabling function contracts is a non-invasive change. While it contains a new API, that API is strictly additive for users. All prior operations are unchanged. -A `-Zcontracts` guard will be added which is necessary to access any of the -contract functionality described below. Any use of the contracts API, such as attributes, -without `-Zcontracts` is a compile time error. - ### Caveats -This proposal focuses on scalability benefits within a single verification session, -caching strategies for cross-session speedup are left to future work. - We add function contract functionality, but do not add the inductive reasoning -support needed for many unbounded problems, such as "decreases" measures and -inductive lemmas. +support needed for many unbounded problems, such as ["decreases" +measures](https://diffblue.github.io/cbmc/contracts-decreases.html) and +inductive lemmas (for instance in [ACSL](https://frama-c.com/download/acsl.pdf) +section 2.6.3 "inductive predicates"). ## User Experience -Function contracts provide a way to approximate function behavior, verify the -approximation and subsequently use the approximation instead if the (possibly -costly) implementation. The lifecycle of a contract is split roughly into three -phases. Which we will explore on this simple example: +Function contract provide a verifiable way to specify function behavior. In +addition the specified behavior can subsequently be used as an abstraction of +the functions behavior at call sites. + +The lifecycle of a contract is split roughly into three phases. Which we will +explore on this simple example: ```rs fn my_div(dividend: u32, divisor: u32) -> u32 { @@ -86,7 +90,7 @@ fn my_div(dividend: u32, divisor: u32) -> u32 { Conditions in contracts are plain Rust expressions which can reference the function arguments and, in case of `ensures`, the result of the function as a - special `result`[^result-naming] varaible. Syntactically Kani supports any + special `result`[^result-naming] variable. Syntactically Kani supports any Rust expression, including function calls, defining types etc, however they must be side-effect free[^side-effects]. Multiple `requires` and `ensures` clauses are allowed on the same function, they are implicitly logically @@ -95,24 +99,11 @@ fn my_div(dividend: u32, divisor: u32) -> u32 { [^result-naming]: See [open questions](#open-questions) for a discussion about naming of the result variable. -2. Checking the Contract - - Next Kani must make sure that the approximation we specified actually holds. - This is in opposition to the related "stubbing" mechanism, where the - approximation is not checked but always trusted. +2. Next Kani must make sure that the approximation we specified actually holds + by **checking** the contract against the implementation. This is in contrast + to ["stubbing"][stubbing], where the approximation is blindly trusted. The contract must always overapproximate the function to guarantee soundness. - Specifically the domain (inputs) of the function described (by the `requires` - clause) must be *at most* as large as the input space for which the - function's behavior is well defined, and the codomain (outputs, described by - `ensures`) must be *at least* as large as the actual space of outputs the - function may produce. - - For example in our case it would be permissible to use - `#[kani::requires(divisor > 100)]` (smaller permissible input domain) or - `#[kani::ensures(result < dividend + divisor)]` (larger possible output - domain), but `#[kani::ensures(result < dividend)]` (small output) is not - allowed. To facilitate the check Kani needs a suitable environment to verify the function in. For this proposal the environment must be provided by us (the @@ -129,11 +120,10 @@ fn my_div(dividend: u32, divisor: u32) -> u32 { } ``` - Similar to a unit-test harness for any other function, we are supposed to - create inputs for the function that are as generic/abstract as possible to - make sure we catch all edge cases, then call the function at least once with - those abstract inputs. If we forget to call `my_div` Kani would report an - error. + Similar to a verification harness for any other function, we are supposed to + create all possible input combinations the function can encounter, then call + the function at least once with those abstract inputs. If we forget to call + `my_div` Kani reports an error. Unlike a unit-test we can however elide any checks of the output and post-call state. Instead Kani uses the conditions we specified in the @@ -187,20 +177,12 @@ fn my_div(dividend: u32, divisor: u32) -> u32 { Mutable memory is similarly made non-deterministic, discussed later in [havociing](#memory-predicates-and-havocing). - The expanded version is equivalent to this: + Stubbing `my_div` expands it similar to this: ```rs - #[kani::proof] - #[kani::stub_verified(my_div)] - fn use_div() { - let v = vec![...]; - let dividend = v.len() - 1; - let divisor = 3; - kani::assert(divisor != 0); - let result = kani::any(); - kani::assume(result <= dividend); - let some_idx = result; - v[some_idx]; + fn my_div_stub(dividend: u32, divisor: u32) -> u32 { + kani::assert(divisor != 0); // pre-condition + kani::any_where(|result| { /* post-condition */ result <= dividend }) } ``` @@ -323,12 +305,12 @@ Any violation of the following constraints constitutes a compile-time error. Harnesses (general or for contract checking) may not have any such annotation. - A function may have one `proof_for_contract(TARGET)` annotation. `TARGET` must - "have a contract". Multiple functions may have `proof_for_contract` - annotations with the same `TARGET`. All such harnesses must pass verification, - before `TARGET` may be used as a verified stub. + "have a contract". One or more `proof_for_contract` harnesses may have the + same `TARGET`. All such harnesses must pass verification, before `TARGET` may + be used as a verified stub. - A `proof_for_contract` harness may use both `stub` and `stub_verified`, though - the `TARGET` may not appear in either. + A `proof_for_contract` harness may use any harness attributes, including + `stub` and `stub_verified`, though the `TARGET` may not appear in either. Kani checks that `TARGET` is reachable from the `proof_for_contract` harness, but it does not warn if stubbed functions use `TARGET`[^stubcheck]. @@ -542,6 +524,8 @@ This is the technical portion of the RFC. Please provide high level details of t semantics. Alternatively we can let the user pick the name with an additional argument to `ensures`, e.g. `ensures(my_result_var, CONDITION)` + See [#2597](https://github.com/model-checking/kani/issues/2597) + [stubbing]: https://model-checking.github.io/kani/rfc/rfcs/0002-function-stubbing.html @@ -25,10 +26,9 @@ Lays the ground work for modular verification. -Function contracts provide an interface for verified abstraction, a mechanism -similar to [stubbing], but sound[^simple-unsoundness]. This kind of verified -stubbing allows for modular verification, which paves the way for the -following two ambitious goals. +Function contracts provide an interface for a verified, +sound[^simple-unsoundness] type of of [stubbing]. This allows for modular +verification, which paves the way for the following two ambitious goals. [^simple-unsoundness]: The main remaining threat to soundness in the use of contracts, as defined in this proposal, is the reliance on user-supplied @@ -51,12 +51,11 @@ newly introduced APIs are entirely backwards compatible. ## User Experience -Function contracts provide a verifiable way to specify function behavior. In -addition, the specified behavior can subsequently be used as an of -the function's behavior at call sites. +A function contracts approximates the behavior of a function. This approximation +can subsequently be used as a stub for the concrete implementation. -The lifecycle of a contract is split roughly into three phases: specification, -verification and stubbing. Which we will explore on this simple example: +The lifecycle of a contract is split into three phases: specification, +verification and stubbing, which we will explore on this example: ```rs fn my_div(dividend: u32, divisor: u32) -> u32 { @@ -82,12 +81,13 @@ fn my_div(dividend: u32, divisor: u32) -> u32 { `ensures` puts a bound on the output, relative to the `dividend` input. - Conditions in contracts are plain Rust expressions which can reference the - function arguments and, in case of `ensures`, the result of the function as a - special `result` variable (see [open questions](#open-questions) on a - discussion about (re)naming). Syntactically Kani supports any Rust - expression, including function calls, defining types etc. However they must - be side-effect free[^side-effects] or Kani will throw a compile error. + Conditions in contracts are plain Rust expressions which reference the + function arguments and, in case of `ensures`, the return value of the + function. The return value is a special variable called `result` (see [open + questions](#open-questions) on a discussion about (re)naming). Syntactically + Kani supports any Rust expression, including function calls, defining types + etc. However they must be side-effect free (see also side effects + [here](#changes-to-other-components)) or Kani will throw a compile error. Multiple `requires` and `ensures` clauses are allowed on the same function, they are implicitly logically conjoined. @@ -98,9 +98,10 @@ fn my_div(dividend: u32, divisor: u32) -> u32 { ["stubbing"][stubbing], where the approximation is trusted blindly. To facilitate this check Kani needs a suitable environment to verify the - function in. For this proposal the environment must be provided by us (the - users). See [future possibilities](#future-possibilities) for a discussion - about the arising soundness issues and their remedies. + function in. Kani demands of us, as the user, to provide this environment. + This is a limitation of this proposal, see also [future + possibilities](#future-possibilities) for a discussion about the arising + soundness issues and their remedies. We provide the checking environment for our contract with a `proof_for_contract` harness that specifies the contract it is supposed to @@ -189,11 +190,6 @@ later used as stub, which ensures soundness (see discussion on lingering threats to soundness in the [future](#future-possibilities) section) and guarding against stubs diverging from their checks. -[^side-effects]: Code used in contracts is required to be side effect free which - means it must not perform I/O, mutate memory (`&mut` vars and such) or - (de)allocate heap memory. This is enforced by the verifier, see the - discussion in the [future](#future-possibilities) section. - ### Write Sets and havocking A return value is only one way in which a function may communicate data. It can @@ -311,7 +307,7 @@ impl Vec { } ``` -`old` allows evaluating any (side-effect free[^side-effects]) Rust expression. +`old` allows evaluating any (side-effect free, see [here](#changes-to-other-components)) Rust expression. The borrow checker enforces the result of `old` cannot observe the mutations from e.g. `pop`, as that would defeat the purpose. If `your` expression in `old` returns borrowed content, make a copy instead (using e.g. `clone()`). @@ -461,9 +457,10 @@ using a new hidden builtin `kani::unckecked_deref` with the type signature `for fn (&T) -> T` which is essentially a C-style dereference operation. Breaking the borrow checker like this is safe for 2 reasons: -1. Postconditions are not allowed perform mutation[^side-effects] and +1. Postconditions are not allowed perform mutation and 2. Post conditions are of type `bool`, meaning they cannot leak references to - the arguments and cause race conditions. + the arguments and cause the race conditions the Rust type system tries to + prevent. The "copies" of arguments created by by `unsafe_deref` are stored as fresh local variables and their occurrence in the postcondition is renamed. @@ -495,8 +492,10 @@ fn recursion_wrapper(&mut self) { replace_pop(self) } else { unsafe { IS_ENTERED = true; } - check_pop(self) - } + let result = check_pop(self); + unsafe { IS_ENTERED = false; } + result + }; } ``` @@ -519,11 +518,14 @@ in the artifact. Then the driver invokes `goto-instrument` with the name of the GOTO-level function names to enforce or replace the memory contracts. The compiler communicates the names of the function via harness metadata. -**Side effect** freedom is enforced with an MIR traversal over all code -reachable from a contract expression. An error is thrown if known side-effecting -actions are performed such as `ptr::write`, `malloc` or `free` and reported as a -graceful compiler error. If the code calls out to C we rely on CBMC to catch the -violation dynamically, resulting in a less readable error. + +Code used in contracts is required to be **side effect** free which means it +must not perform I/O, mutate memory (`&mut` vars and such) or (de)allocate heap +memory. This is enforced in two layers. First with an MIR traversal over all +code reachable from a contract expression. An error is thrown if known +side-effecting actions are performed such as `ptr::write`, `malloc` or `free` in +a second layer we rely on CBMC to catch the violation dynamically if the code +calls out to C, ensuring soundness but causing less readable errors. [stubbing]: https://model-checking.github.io/kani/rfc/rfcs/0002-function-stubbing.html @@ -63,7 +63,7 @@ fn my_div(dividend: u32, divisor: u32) -> u32 { } ``` -1. In the first phase we **specify** the approximation. Kani provides two new +1. In the first phase we **specify** the contract. Kani provides two new annotations: `requires` (preconditions) to describe the expectations this function has as to the calling context and `ensures` (postconditions) which approximates function outputs in terms of function inputs. @@ -94,18 +94,21 @@ fn my_div(dividend: u32, divisor: u32) -> u32 { 2. Next, Kani makes sure that the contract we specified overapproximates the - implementation with a **check**. This is in contrast to - ["stubbing"][stubbing], where the approximation is trusted blindly. + implementation with a **check**. This is in contrast to a + ["stub"][stubbing], which is trusted blindly. To facilitate this check Kani needs a suitable environment to verify the - function in. Kani demands of us, as the user, to provide this environment. - This is a limitation of this proposal, see also [future - possibilities](#future-possibilities) for a discussion about the arising - soundness issues and their remedies. + function in. The environment consists mainly of the function arguments but + also of a valid heap that any pointers may refer to and properly initialized + `static` variables. + + Kani demands of us, as the user, to provide this environment; a limitation of + this proposal. See also [future possibilities](#future-possibilities) for a + discussion about the arising soundness issues and their remedies. We provide the checking environment for our contract with a - `proof_for_contract` harness that specifies the contract it is supposed to - check. + `proof_for_contract` harness that references the function for which the + contract is supposed to be checked. ```rs #[kani::proof_for_contract(my_div)] @@ -124,7 +127,7 @@ fn my_div(dividend: u32, divisor: u32) -> u32 { Kani inserts preconditions (`requires`) as `kani::assume` *before* the call to `my_div`, limiting inputs to those the function is actually defined for. It inserts postconditions (`ensures`) as `kani::assert` checks *after* the - call to `my_div` enforcing the contract. + call to `my_div`, enforcing the contract. The expanded version of our harness and function is equivalent to the following: @@ -139,7 +142,7 @@ fn my_div(dividend: u32, divisor: u32) -> u32 { } ``` - Kani verifies the expanded harness like any other harness which gives the + Kani verifies the expanded harness like any other harness, giving the green light for the next step: verified stubbing. 3. In the last phase the **verified** contract is ready for us to use to @@ -171,7 +174,7 @@ fn my_div(dividend: u32, divisor: u32) -> u32 { Mutable memory is similarly made non-deterministic, discussed later in [havocking](#memory-predicates-and-havocking). - Stubbing `my_div` expands it similar to this: + An expanded stubbing of `my_div` looks like this: ```rs fn my_div_stub(dividend: u32, divisor: u32) -> u32 { @@ -190,13 +193,13 @@ later used as stub, which ensures soundness (see discussion on lingering threats to soundness in the [future](#future-possibilities) section) and guarding against stubs diverging from their checks. -### Write Sets and havocking +### Write Sets and Havocking A return value is only one way in which a function may communicate data. It can also communicate data by modifying values stored behind mutable pointers. To simulate all possible modifications a function could apply to pointed-to data -the verifier "havocs" those regions, essentially replacing their content with +the verifier "havocks" those regions, essentially replacing their content with non-deterministic values. Let us consider a simple example of a `pop` method. @@ -214,20 +217,21 @@ what Kani will assume it does by default. It infers the "write set", that is the set of memory locations a function may modify, from the type system. As a result any data pointed to by a mutable reference or pointer is considered part of the write set. In addition a static analysis of the source code discovers any -`static mut` variables the function or it's dependencies reference and add all -pointed-to data to the write set also. During havocking all locations in the -write set are replaced by non-deterministic values by the verifier. +`static mut` variables the function or it's dependencies reference and adds all +pointed-to data to the write set also. During havocking the verifier replaces +all locations in the write set with non-deterministic values. While the inferred write set is sound and enough for successful contract -checking[^inferred-footprint] in many cases (such as `pop`) this inference is -too coarse grained. In this case every value in this vector will be made +checking[^inferred-footprint] in many cases this inference is too coarse +grained. In the caase of `pop` case every value in this vector will be made non-deterministic. -This proposal also adds an `modifies` and `frees` clause which limits the scope -of havocking. Both clauses represent an assertion that the function will modify -only the specified memory regions. Similar to requires/ensures the verifier -enforces the assertion in the checking stage to ensure soundness. When the -contract is used as a stub the modifies clause is used as the write set to havoc. +To address this the proposal also adds an `modifies` and `frees` clause which +limits the scope of havocking. Both clauses represent an assertion that the +function will modify only the specified memory regions. Similar to +requires/ensures the verifier enforces the assertion in the checking stage to +ensure soundness. When the contract is used as a stub the modifies clause is +used as the write set to havock. In our `pop` example the only modified memory location is the last element and only if the vector was not already empty, which would be specified thusly. @@ -272,7 +276,7 @@ impl Vec { ``` `[..]` denotes the entirety of an allocation, `[i..]`, `[..j]` and `[i..j]` are -ranges of pointer offsets[^slice-expr]. The slice indices are offsets with sizing `T`, e.g. +ranges of pointer offsets[^slice-exprs]. The slice indices are offsets with sizing `T`, e.g. in Rust `p[i..j]` would be equivalent to `std::slice::from_raw_parts(p.offset(i), i - j)`. `i` must be smaller or equal than `j`. @@ -286,17 +290,18 @@ memory that is deallocated. It does not admit slice syntax, only lvalues. ### History Variables -Kani's contract language contains additional support for reasoning about changes -to memory. One case where this is necessary is whenever `ensures` needs to -reason about state before the function call. By default it only has access to -state after the call completes, which will be different if the call mutates -memory. +Kani's contract language contains additional support for reasoning how the value +of mutable memory changes. One case where this is necessary is whenever +`ensures` needs to reason about state before the function call. By default it +only has access to state after the call completes, which will be different if +the call mutates memory. -Returning to out `pop` function from before we may wish to describe in which +Returning to our `pop` function from before we may wish to describe in which case the result is `Some`. However that depends on whether `self` is empty *before* `pop` is called. To do this Kani provides the `old(EXPR)` pseudo -function, which evaluates `EXPR` before the call (e.g. to `pop`) and makes the -result available to `ensures`. It is used like so: +function (see [this section](#open-questions) about a discussion on naming), +which evaluates `EXPR` before the call (e.g. to `pop`) and makes the result +available to `ensures`. It is used like so: ```rs impl Vec { @@ -463,18 +468,19 @@ the borrow checker like this is safe for 2 reasons: prevent. The "copies" of arguments created by by `unsafe_deref` are stored as fresh local -variables and their occurrence in the postcondition is renamed. +variables and their occurrence in the postcondition is renamed. In addition a +`mem::forget` is emitted for each copy to avoid a double free. ### Recursion -Kani verifies contractgs for recursive functions inductively. Reentry of the -function is detected with a static variable and in this case we use the -replacement of the contract instead of the function body. +Kani verifies contracts for recursive functions inductively. Reentry of the +function is detected with a function-specific static variable. Upon detecting +reentry we use the replacement of the contract instead of the function body. -Kani generates an additional wrapper around the function to add this detection. +Kani generates an additional wrapper around the function to add the detection. The additional wrapper is there so we can place the `modifies` contract on `check_pop` and `replace_pop` instead of `recursion_wrapper` which prevents CBMC -from triggering its recursion induction. +from triggering its recursion induction as this would skip our replacement checks. ```rs #[checked_with = "recursion_wrapper"] @@ -500,17 +506,17 @@ fn recursion_wrapper(&mut self) { ``` Note that this is insufficient to verify all types of recursive functions, as -the contract specification language has no support for inductive lemmas -inductive lemmas (for instance in [ACSL](https://frama-c.com/download/acsl.pdf) -section 2.6.3 "inductive predicates"). Inductive lemmas are usually needed for -recursive datastructures. +the contract specification language has no support for inductive lemmas (for +instance in [ACSL](https://frama-c.com/download/acsl.pdf) section 2.6.3 +"inductive predicates"). Inductive lemmas are usually needed for recursive +datastructures. ### Changes to Other Components Contract enforcement and replacement (`kani::proof_for_contract(f)`, `kani::stub_verified(f)`) both dispatch to the **stubbing logic**, stubbing `f` with the generated check and replace function respectively. If `f` has no -contract, an error is thrown. +contract, Kani throws an error. For **write sets** Kani relies on CBMC. `modifies` clauses (whether derived from types of from explicit clauses) are emitted from the compiler as GOTO contracts @@ -523,8 +529,8 @@ Code used in contracts is required to be **side effect** free which means it must not perform I/O, mutate memory (`&mut` vars and such) or (de)allocate heap memory. This is enforced in two layers. First with an MIR traversal over all code reachable from a contract expression. An error is thrown if known -side-effecting actions are performed such as `ptr::write`, `malloc` or `free` in -a second layer we rely on CBMC to catch the violation dynamically if the code +side-effecting actions are performed such as `ptr::write`, `malloc` or `free`. +In a second layer we rely on CBMC to catch the violation dynamically if the code calls out to C, ensuring soundness but causing less readable errors. -- **Kani-side implementation vs CBMC** Instead of generating check and replace - functions in Kani, we could use the contract instrumentation provided by CBMC. - We tried this earlier but came up short, because it is difficult to implement, - while supporting arbitrary Rust syntax. We exported the conditions into - functions so that Rust would do the parsing/type checking/lowering for us and - then call the lowered function in the CBMC contract. The trouble is that - CBMC's `old` is only supported directly in the contract, not in functions - called from the contract. This means we either need to inline the contract - function body, which is brittle in the presence if control flow, or we must - extract the `old` expressions, evaluate them in the contract directly and pass - the results to the check function. However this means we must restrict the - expressions in `old`, because we now need to lower those by hand and even if - we could let rustc do it, CBMC's old has no support for function calls in its - argument expression. -- **Expanding all contract macros at the same time** Instead of expanding - contract macros one-at-a-atime and creating the onion layer structure we could - expand all subsequent one's with the outermost one, creating only one check - and replace function each. This is however brittle with respect to renaming. - If a user does `use kani::requires as my_requires` and then does multiple - `#[my_requires(condition)]` macro would not collect them properly since it can - only mathc syntactically and it does not know about the `use` and neither can - we restrict this kind if use or warn the user. By contrast the collection with - `kanitool::checked_with` is safe, because that attribute is generated by our - macro itself, so we can rely on the fact that it uses then canonical - representation. -- **Generating nested functions instead of siblings** Instead of generating the - `check` and `replace` functions as siblings to the contracted function we - could nest them like so - - ```rs - fn my_div(dividend: u32, divisor: u32) -> u32 { - fn my_div_check_5e3713(dividend: u32, divisor: u32) -> u32 { - ... - } +### Kani-side implementation vs CBMC + +Instead of generating check and replace functions in Kani, we could use the contract instrumentation provided by CBMC. + +We tried this earlier but came up short, because it is difficult to implement, +while supporting arbitrary Rust syntax. We exported the conditions into +functions so that Rust would do the parsing/type checking/lowering for us and +then call the lowered function in the CBMC contract. + +The trouble is that CBMC's `old` is only supported directly in the contract, not +in functions called from the contract. This means we either need to inline the +contract function body, which is brittle in the presence if control flow, or we +must extract the `old` expressions, evaluate them in the contract directly and +pass the results to the check function. However this means we must restrict the +expressions in `old`, because we now need to lower those by hand and even if we +could let rustc do it, CBMC's old has no support for function calls in its +argument expression. + +### Expanding all contract macros at the same time + +Instead of expanding contract macros one-at-a-atime and layering the checks we +could expand all subsequent one's with the outermost one in one go. + +This is however brittle with respect to renaming. If a user does `use +kani::requires as my_requires` and then does multiple +`#[my_requires(condition)]` macro would not collect them properly since it can +only mathc syntactically and it does not know about the `use` and neither can we +restrict this kind if use or warn the user. By contrast the collection with +`kanitool::checked_with` is safe, because that attribute is generated by our +macro itself, so we can rely on the fact that it uses then canonical +representation. + +### Generating nested functions instead of siblings + +Instead of generating the `check` and `replace` functions as siblings to the +contracted function we could nest them like so + +```rs +fn my_div(dividend: u32, divisor: u32) -> u32 { + fn my_div_check_5e3713(dividend: u32, divisor: u32) -> u32 { ... } - ``` - - This could be beneficial if we want to be able to allow contracts on trait - impl items, in which case generating sibling functions is not allowed. The - only thing required to make this work is an additional pass over the condition - that replaces every `self` with a fresh identifier that now becomes the first - argument of the function. -- **Explicit command line checking/substitution vs attributes:** Instead of + ... +} +``` + +This could be beneficial if we want to be able to allow contracts on trait impl +items, in which case generating sibling functions is not allowed. On the other +hand this makes it harder to implement contracts on traits *definitions*, +because there is no body available which we could nest the function into. +Utimately we may require both so that we vcan support both. + + +What is required to make this work is an additional pass over the condition that +replaces every `self` with a fresh identifier that now becomes the first +argument of the function. In addition there are open questions as to how to +resolve the nested name inside the compiler. + +### Explicit command line checking/substitution vs attributes: + +Instead of adding a new special `proof_for_contact` attributes we could have instead done: 1. **Check contracts on the command line** like CBMC does. This makes contract From e37d23ebcaaa1947181c47d1d3475b6fd1c53d0a Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Tue, 15 Aug 2023 21:12:24 -0700 Subject: [PATCH 26/36] Spellcheck --- rfc/src/rfcs/0009-function-contracts.md | 38 ++++++++++++------------- 1 file changed, 19 insertions(+), 19 deletions(-) diff --git a/rfc/src/rfcs/0009-function-contracts.md b/rfc/src/rfcs/0009-function-contracts.md index f2a35c8df1ef..5635966a3957 100644 --- a/rfc/src/rfcs/0009-function-contracts.md +++ b/rfc/src/rfcs/0009-function-contracts.md @@ -38,7 +38,7 @@ verification, which paves the way for the following two ambitious goals. section. - **Scalability:** Function contracts are sound (over)abstractions of function - behavior. By verifiying the contract against its implemetation and + behavior. By verifying the contract against its implementation and subsequently performing caller verification against the (cheaper) abstraction, verification can be modularized, cached and thus scaled. - **Unbounded Verification:** The abstraction provided by the contract can be @@ -152,7 +152,7 @@ fn my_div(dividend: u32, divisor: u32) -> u32 { **stub** other harnesses. Kani requires that there has to be at least one associated - `proof_for_contract` harness for each function to stub, otherwise an eror is + `proof_for_contract` harness for each function to stub, otherwise an error is thrown. In addition, by default, it requires all `proof_for_contract` harnesses to pass verification before attempting verification of any harnesses that use the contract as a stub. @@ -170,7 +170,7 @@ fn my_div(dividend: u32, divisor: u32) -> u32 { ``` At a call site where the contract is used as a stub Kani `kani::assert`s the - preconditions (`requies`) and produces a nondeterministic value (`kani::any`) + preconditions (`requires`) and produces a nondeterministic value (`kani::any`) which satisfies the postconditions. Mutable memory is similarly made non-deterministic, discussed later in @@ -197,9 +197,9 @@ stubs diverging from their checks. ### Write Sets and Havocking -Functions can have side effects on data rechable through mutable refrences or +Functions can have side effects on data reachable through mutable references or pointers. To overapproximate all such modifications a function could apply to -pointed-to data the verifier "havocks" those regions, essentially replacing +pointed-to data the verifier "havocs" those regions, essentially replacing their content with non-deterministic values. Let us consider a simple example of a `pop` method. @@ -223,7 +223,7 @@ all locations in the write set with non-deterministic values. While the inferred write set is sound and enough for successful contract checking[^inferred-footprint] in many cases this inference is too coarse -grained. In the caase of `pop` case every value in this vector will be made +grained. In the case of `pop` case every value in this vector will be made non-deterministic. To address this the proposal also adds an `modifies` and `frees` clause which @@ -231,7 +231,7 @@ limits the scope of havocking. Both clauses represent an assertion that the function will modify only the specified memory regions. Similar to requires/ensures the verifier enforces the assertion in the checking stage to ensure soundness. When the contract is used as a stub the modifies clause is -used as the write set to havock. +used as the write set to havoc. In our `pop` example the only modified memory location is the last element and only if the vector was not already empty, which would be specified thusly. @@ -331,7 +331,7 @@ not local variables. Compare the following And it will only be recognized as `old(...)`, not as `let old1 = old; old1(...)` etc. -### Workflow and Attribute Contraints Overview +### Workflow and Attribute Constraints Overview 1. By default `kani` or `cargo kani` first verifies all contract harnesses (`proof_for_contract`) reachable from the file or in the local workspace @@ -423,7 +423,7 @@ impl Vec { } ``` -The `ensures` macro performs an AST rewrite constiting of an extraction of the +The `ensures` macro performs an AST rewrite consisting of an extraction of the expressions in `old` and a replacement with a fresh local variable, creating the following: @@ -443,7 +443,7 @@ variables in the contract (Rust will report those variables as not being in scope). The borrow checker also ensures for us that none of the temporary variables -borrow in a way that would be able to observe the moditication in `pop` which +borrow in a way that would be able to observe the modification in `pop` which would occur for instance if the user wrote `old(self)`. Instead of borrowing copies should be created (e.g. `old(self.clone())`). This is only enforced for safe rust though. @@ -466,7 +466,7 @@ impl Vec { This contract refers simultaneously to `self` and the result. Since the method however borrows `self` mutably, it would no longer be accessible in the postcondition. To work around this we strategically break the borrowing rules -using a new hidden builtin `kani::unckecked_deref` with the type signature `for +using a new hidden builtin `kani::unchecked_deref` with the type signature `for fn (&T) -> T` which is essentially a C-style dereference operation. Breaking the borrow checker like this is safe for 2 reasons: @@ -517,7 +517,7 @@ Note that this is insufficient to verify all types of recursive functions, as the contract specification language has no support for inductive lemmas (for instance in [ACSL](https://frama-c.com/download/acsl.pdf) section 2.6.3 "inductive predicates"). Inductive lemmas are usually needed for recursive -datastructures. +data structures. ### Changes to Other Components @@ -589,7 +589,7 @@ could expand all subsequent one's with the outermost one in one go. This is however brittle with respect to renaming. If a user does `use kani::requires as my_requires` and then does multiple `#[my_requires(condition)]` macro would not collect them properly since it can -only mathc syntactically and it does not know about the `use` and neither can we +only match syntactically and it does not know about the `use` and neither can we restrict this kind if use or warn the user. By contrast the collection with `kanitool::checked_with` is safe, because that attribute is generated by our macro itself, so we can rely on the fact that it uses then canonical @@ -613,7 +613,7 @@ This could be beneficial if we want to be able to allow contracts on trait impl items, in which case generating sibling functions is not allowed. On the other hand this makes it harder to implement contracts on traits *definitions*, because there is no body available which we could nest the function into. -Utimately we may require both so that we vcan support both. +Ultimately we may require both so that we can support both. What is required to make this work is an additional pass over the condition that @@ -653,7 +653,7 @@ Instead of semantics. Alternatively we can let the user pick the name with an additional argument to `ensures`, e.g. `ensures(my_result_var, CONDITION)` - Similar concers apply to `old`, which may be more appropriate to be special + Similar concerns apply to `old`, which may be more appropriate to be special syntax, e.g. `@old`. See [#2597](https://github.com/model-checking/kani/issues/2597) @@ -699,11 +699,11 @@ Instead of bool`, where `T` is some arbitrary type that can be quantified over. This interface is familiar to developers, but the code generation is tricky, as CBMC level quantifiers only allow certain kinds of expressions. This - necessiates a rewrite of the `Fn` closure to a compliant expression. + necessitates a rewrite of the `Fn` closure to a compliant expression. - Letting the user supply the **harnesses for checking contracts** is a source of unsoundness, if corner cases are not adequately covered. Ideally Kani would generate the check harness automatically, but this is difficult both because - heap datastructures are potentially infinite, and also because it must observe + heap data structures are potentially infinite, and also because it must observe user-level type invariants. A complete solution for this is not known to us but there are ongoing @@ -711,7 +711,7 @@ Instead of Environments that are non-inductive, safe Rust (e.g. no recursively defined data structures, no raw pointers) could be created from the type as the - safe Rust type contraints describe a finite space. + safe Rust type constraints describe a finite space. For dealing with pointers one applicable mechanism could be *memory predicates* to declaratively describe the state of the heap both before and @@ -721,7 +721,7 @@ Instead of This does not easily translate to Kani, since we handle pre/postconditions manually and mainly in proc-macros. There are multiple ways to bridge this gap, perhaps the easiest being to add memory predicates *separately* to Kani - instead of as part of pre/postcondtions, so they can be handled by forwarding + instead of as part of pre/postconditions, so they can be handled by forwarding them to CBMC. However this is also tricky, because memory predicates are used to describe pointers and pointers only. Meaning that if they are encapsulated in a structure (such as `Vec` or `RefCell`) there is no way of specifying the From 61f956a13dcba6f66e8ce5dfd865624f2dfeb88a Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Tue, 15 Aug 2023 21:42:08 -0700 Subject: [PATCH 27/36] Spell checks and suggestions --- rfc/src/rfcs/0009-function-contracts.md | 86 +++++++++++++++---------- 1 file changed, 52 insertions(+), 34 deletions(-) diff --git a/rfc/src/rfcs/0009-function-contracts.md b/rfc/src/rfcs/0009-function-contracts.md index 5635966a3957..4cb88d218838 100644 --- a/rfc/src/rfcs/0009-function-contracts.md +++ b/rfc/src/rfcs/0009-function-contracts.md @@ -14,8 +14,9 @@ ## Summary Function contracts are a mechanism, similar to [stubbing], which allows a -concrete implementations to be replaced by an overapproximation without losing -soundness[^simple-unsoundness]. +concrete implementations to be replaced by an abstraction without losing +soundness[^simple-unsoundness] by first validating the abstraction against the +implementation it will replace. This allows for a modular verification. @@ -27,8 +28,9 @@ This allows for a modular verification. Function contracts provide an interface for a verified, -sound[^simple-unsoundness] type of of [stubbing]. This allows for modular -verification, which paves the way for the following two ambitious goals. +sound[^simple-unsoundness] function abstraction. This is similar to [stubbing] +but with verification of the abstraction instead of blind trust. This allows for +modular verification, which paves the way for the following two ambitious goals. [^simple-unsoundness]: The main remaining threat to soundness in the use of contracts, as defined in this proposal, is the reliance on user-supplied @@ -37,26 +39,28 @@ verification, which paves the way for the following two ambitious goals. and potential remedies can be found in the [future](#future-possibilities) section. -- **Scalability:** Function contracts are sound (over)abstractions of function - behavior. By verifying the contract against its implementation and - subsequently performing caller verification against the (cheaper) abstraction, - verification can be modularized, cached and thus scaled. +- **Scalability:** A function contract is an abstraction (sound + overapproximation) of a function's behavior. By verifying the contract against + its implementation and subsequently performing caller verification against the + (cheaper) abstraction, verification can be modularized, cached and thus + scaled. - **Unbounded Verification:** The abstraction provided by the contract can be used instead of a recursive call, thus allowing verification of recursive functions. Function contracts are completely optional with no user impact if unused. The -newly introduced APIs are entirely backwards compatible. +newly introduced interface (attributes, macros, CLI) do not require any changes +to Kani's current interface. ## User Experience -A function contracts specifies the behavior of a function in a way that can be -both checked against the function and also used as a stub for the concrete -implementation. +A function contracts specifies the behavior of a function as a predicate that +can be checked against the function implementation and also used as an +abstraction of the implementation at the call sites. The lifecycle of a contract is split into three phases: specification, -verification and stubbing, which we will explore on this example: +verification and call abstraction, which we will explore on this example: ```rs fn my_div(dividend: u32, divisor: u32) -> u32 { @@ -146,16 +150,16 @@ fn my_div(dividend: u32, divisor: u32) -> u32 { ``` Kani verifies the expanded harness like any other harness, giving the - green light for the next step: verified stubbing. + green light for the next step: call abstraction. 3. In the last phase the **verified** contract is ready for us to use to - **stub** other harnesses. + abstract the function at its call sites. Kani requires that there has to be at least one associated - `proof_for_contract` harness for each function to stub, otherwise an error is + `proof_for_contract` harness for each abstracted function, otherwise an error is thrown. In addition, by default, it requires all `proof_for_contract` harnesses to pass verification before attempting verification of any - harnesses that use the contract as a stub. + harnesses that use the contract as an abstraction. A possible harness that uses our `my_div` contract could be the following: @@ -169,9 +173,9 @@ fn my_div(dividend: u32, divisor: u32) -> u32 { } ``` - At a call site where the contract is used as a stub Kani `kani::assert`s the - preconditions (`requires`) and produces a nondeterministic value (`kani::any`) - which satisfies the postconditions. + At a call site where the contract is used as an abstraction Kani + `kani::assert`s the preconditions (`requires`) and produces a + nondeterministic value (`kani::any`) which satisfies the postconditions. Mutable memory is similarly made non-deterministic, discussed later in [havocking](#memory-predicates-and-havocking). @@ -188,12 +192,12 @@ fn my_div(dividend: u32, divisor: u32) -> u32 { Notice that this performs no actual computation for `my_div` (other than the conditions) which allows us to avoid something potentially costly. -Also notice that Kani was able to express both contract checking and stubbing +Also notice that Kani was able to express both contract checking and abstracting with existing capabilities; the important feature is the enforcement. The checking is, by construction, performed **against the same condition** that is -later used as stub, which ensures soundness (see discussion on lingering threats -to soundness in the [future](#future-possibilities) section) and guarding against -stubs diverging from their checks. +later used as the abstraction, which ensures soundness (see discussion on +lingering threats to soundness in the [future](#future-possibilities) section) +and guarding against abstractions diverging from their checks. ### Write Sets and Havocking @@ -230,8 +234,8 @@ To address this the proposal also adds an `modifies` and `frees` clause which limits the scope of havocking. Both clauses represent an assertion that the function will modify only the specified memory regions. Similar to requires/ensures the verifier enforces the assertion in the checking stage to -ensure soundness. When the contract is used as a stub the modifies clause is -used as the write set to havoc. +ensure soundness. When the contract is used as an abstraction the modifies +clause is used as the write set to havoc. In our `pop` example the only modified memory location is the last element and only if the vector was not already empty, which would be specified thusly. @@ -357,13 +361,13 @@ Kani reports a compile time error if any of the following constraints are violat - A harness may have up to one `proof_for_contract(TARGET)` annotation where `TARGET` must "have a contract". One or more `proof_for_contract` harnesses may have the same `TARGET`. All such harnesses must pass verification, before `TARGET` may - be used as a verified stub. + be used as an abstraction. A `proof_for_contract` harness may use any harness attributes, including `stub` and `stub_verified`, though the `TARGET` may not appear in either. - Kani checks that `TARGET` is reachable from the `proof_for_contract` harness, - but it does not warn if stubbed functions use `TARGET`[^stubcheck]. + but it does not warn if abstracted functions use `TARGET`[^stubcheck]. A current limitation with how contracts are enforced means that if target is polymorphic, only one monomorphization of `TARGET` is permissible. @@ -383,7 +387,7 @@ Kani reports a compile time error if any of the following constraints are violat check succeeded. [^stubcheck]: Kani cannot report the occurrence of a contract function to check - in stubbed functions as errors, because the mechanism is needed to verify + in abstracted functions as errors, because the mechanism is needed to verify mutually recursive functions. ## Detailed Design @@ -669,7 +673,7 @@ Instead of - **With harness selection** (`--harness`) only those contracts which the selected harnesses depend on are checked. - **For high assurance** passing a `--paranoid` flag also checks contracts for - dependencies (other crates) when they are used in stubs. + dependencies (other crates) when they are used in abstractions. - **Per harness** the users can disable the checking for specific contracts via attribute, like `#[stub_verified(TARGET, trusted)]` or `#[stub_unverified(TARGET)]`. This also plays nicely with `cfg_attr`. @@ -682,7 +686,21 @@ Instead of Aside: I'm obviously having some fun here with the names, happy to change, it's really just about the semantics. - +- Can `old` accidentally break scope? The `old` function cannot reference local + variables. For instance `#[ensures({let x = ...; old(x)})]` cannot work as an + AST rewrite because the expression in `old` is lifted out of it's context into + one where the only bound variables are the function arguments (see also + [history variables](#history-variables)). In most cases this will be a + compiler error complaining that `x` is unbound, however it is possible that + *if* there is also a function argument `x`, then it may silently succeed the + code generation but confusingly fail verification. For instance `#[ensures({ + let x = 1; old(x) == x })]` on a function that has an argument named `x` would + *not* hold. + + To handle this correctly we would need an extra check that detects if `old` + references local variables. That would also enable us to provide a better + error message than the default "cannot find value `x` in this scope". + -- Is it really correct to return `kani::any()` from the replacement copy, even - if it can be a pointer? +- Returning `kani::any()` in a replacement isn't great, because it wouldn't work + for references as they can't have an `Arbitrary` implementation. Plus the + soundness then relies on a correct implementation of `Arbitrary`. Instead it + may be better to allow for the user to specify type invariants which can the + be used to generate correct values in replacement but also be checked as part + of the contract checking. - Making result special. Should we use special syntax here like `@result` or `kani::result()`, though with the latter I worry that people may get confused because it is syntactic and not subject to usual `use` renaming and import From e76d9e2501af9ff515aebf730195c783ee4fe25d Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Wed, 16 Aug 2023 18:16:25 -0700 Subject: [PATCH 30/36] More suggestions from review --- rfc/src/rfcs/0009-function-contracts.md | 53 +++++++++++++------------ 1 file changed, 27 insertions(+), 26 deletions(-) diff --git a/rfc/src/rfcs/0009-function-contracts.md b/rfc/src/rfcs/0009-function-contracts.md index e572b5a9c802..f4a9dcf5fbf4 100644 --- a/rfc/src/rfcs/0009-function-contracts.md +++ b/rfc/src/rfcs/0009-function-contracts.md @@ -48,9 +48,9 @@ modular verification, which paves the way for the following two ambitious goals. used instead of a recursive call, thus allowing verification of recursive functions. -Function contracts are completely optional with no user impact if unused. The -newly introduced interface (attributes, macros, CLI) do not require any changes -to Kani's current interface. +Function contracts are completely optional with no user impact if unused. This +RFC proposes the addition of new attributes, and functions, that shouldn't +interfere with existing functionalities. ## User Experience @@ -653,32 +653,33 @@ Instead of wants to the can just factor out the actual contents of the harness to reuse it. -### Misc +### Polymorphism during contract checking -- A current limitation with how contracts are enforced means that if the target - of a `proof_for_contract` is polymorphic, only one monomorphization is - permitted to occur in the harness. This does not limit the target to a single - occurrence, *but* to a single instantiation of its generic parameters. +A current limitation with how contracts are enforced means that if the target of +a `proof_for_contract` is polymorphic, only one monomorphization is permitted to +occur in the harness. This does not limit the target to a single occurrence, +*but* to a single instantiation of its generic parameters. - This is because we rely on CBMC for enforcing the `assigns` contract. At the - GOTO level all monomorphized instances are distinct functions *and* CBMC only - allows checking one function contract at a time, hence this restriction. +This is because we rely on CBMC for enforcing the `modifies` contract. At the +GOTO level all monomorphized instances are distinct functions *and* CBMC only +allows checking one function contract at a time, hence this restriction. -- We make the user supply the harnesses for checking contracts. This is our - major source of unsoundness, if corner cases are not adequately covered. - Having Kani generate the harnesses automatically is a non-trivial task - (because heaps are hard) and will be the subject of [future - improvements](#future-possibilities). +### User supplied harnesses - In limited cases we could generate harnesses, for instance if only bounded - types (integers, booleans, enums, tuples, structs, references and their - combinations) were used. We could restrict the use of contracts to cases where - only such types are involved in the function inputs and outputs, however this - would drastically limit the applicability, as even simple heap data structures - such as `Vec`, `String` and even `&[T]` and `&str` (slices) would be out of - scope. These data structures however are ubiquitous and users can avoid the - unsoundness with relative confidence by overprovisioning (generating inputs - that are several times larger than what they expect the function will touch). +We make the user supply the harnesses for checking contracts. This is our major +source of unsoundness, if corner cases are not adequately covered. Having Kani +generate the harnesses automatically is a non-trivial task (because heaps are +hard) and will be the subject of [future improvements](#future-possibilities). + +In limited cases we could generate harnesses, for instance if only bounded types +(integers, booleans, enums, tuples, structs, references and their combinations) +were used. We could restrict the use of contracts to cases where only such types +are involved in the function inputs and outputs, however this would drastically +limit the applicability, as even simple heap data structures such as `Vec`, +`String` and even `&[T]` and `&str` (slices) would be out of scope. These data +structures however are ubiquitous and users can avoid the unsoundness with +relative confidence by overprovisioning (generating inputs that are several +times larger than what they expect the function will touch). ## Open questions @@ -794,7 +795,7 @@ Instead of trait contracts. The macros would generate new trait methods with default implementations, similar to the functions it generates today. Using sealed types we can prevent the user from overwriting the generated contract methods. - Contracts for the trait and contracts on it's impls are combined by abstracting + Contracts for the trait and contracts on it's `impl`s are combined by abstracting the original method depending on context. The occurrence inside the contract generated from the trait method is replaced by the `impl` contract. Any other occurrence is replaced by the just altered trait method contract. From 728b2714b2e190431e719439c90c0f9d4c30824a Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Wed, 16 Aug 2023 18:17:26 -0700 Subject: [PATCH 31/36] Update rfc/src/rfcs/0009-function-contracts.md Co-authored-by: Celina G. Val --- rfc/src/rfcs/0009-function-contracts.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rfc/src/rfcs/0009-function-contracts.md b/rfc/src/rfcs/0009-function-contracts.md index f4a9dcf5fbf4..8440727f37cd 100644 --- a/rfc/src/rfcs/0009-function-contracts.md +++ b/rfc/src/rfcs/0009-function-contracts.md @@ -703,7 +703,7 @@ times larger than what they expect the function will touch). See [#2597](https://github.com/model-checking/kani/issues/2597) - How to check the right contracts at the right time. By default `kani` and - `cargo kani` check all contracts in a file/workspace. This represents the + `cargo kani` check all contracts in a crate/workspace. This represents the safest option for the user but may be too costly in some cases. The user should be provided with options to disable contract checking for the From 333ae997703c8e8af750f2bf0168ffaf24976d1a Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 17 Aug 2023 14:16:40 -0700 Subject: [PATCH 32/36] Add the two concerns raised by celina --- rfc/src/rfcs/0009-function-contracts.md | 27 ++++++++++++++++--------- 1 file changed, 18 insertions(+), 9 deletions(-) diff --git a/rfc/src/rfcs/0009-function-contracts.md b/rfc/src/rfcs/0009-function-contracts.md index f4a9dcf5fbf4..f9e9099b42ef 100644 --- a/rfc/src/rfcs/0009-function-contracts.md +++ b/rfc/src/rfcs/0009-function-contracts.md @@ -400,14 +400,14 @@ Kani reports a compile time error if any of the following constraints are violat -Kani implements the functionality of function contracts in two places. +Kani implements the functionality of function contracts in three places. 1. Code generation in the `requires` and `ensures` macros (`kani_macros`). 2. GOTO level contracts using CBMC's contract language generated in `kani-compiler` for `modifies` clauses. -3. Dependencies and ordering among harnesses in the driver to enforce contract - checking before replacement. Also plumbing between compiler and driver for - enforcement of assigns clauses. +3. Dependencies and ordering among harnesses in `kani-driver` to enforce + contract checking before replacement. Also plumbing between compiler and + driver for enforcement of assigns clauses. ### Code generation in `kani_macros` @@ -686,7 +686,7 @@ times larger than what they expect the function will touch). -- Returning `kani::any()` in a replacement isn't great, because it wouldn't work +- Returning **`kani::any()` in a replacement isn't great**, because it wouldn't work for references as they can't have an `Arbitrary` implementation. Plus the soundness then relies on a correct implementation of `Arbitrary`. Instead it may be better to allow for the user to specify type invariants which can the @@ -702,7 +702,7 @@ times larger than what they expect the function will touch). syntax, e.g. `@old`. See [#2597](https://github.com/model-checking/kani/issues/2597) -- How to check the right contracts at the right time. By default `kani` and +- How to **check the right contracts at the right time**. By default `kani` and `cargo kani` check all contracts in a file/workspace. This represents the safest option for the user but may be too costly in some cases. @@ -727,7 +727,7 @@ times larger than what they expect the function will touch). Aside: I'm obviously having some fun here with the names, happy to change, it's really just about the semantics. -- Can `old` accidentally break scope? The `old` function cannot reference local +- **Can `old` accidentally break scope?** The `old` function cannot reference local variables. For instance `#[ensures({let x = ...; old(x)})]` cannot work as an AST rewrite because the expression in `old` is lifted out of it's context into one where the only bound variables are the function arguments (see also @@ -741,6 +741,16 @@ times larger than what they expect the function will touch). To handle this correctly we would need an extra check that detects if `old` references local variables. That would also enable us to provide a better error message than the default "cannot find value `x` in this scope". +- **Can panicking be expected behavior?** Usually preconditions are used to rule + out panics but it is conceivable that a user would want to specify that a + function panics under certain conditions. Specifying this would require an + extension to the current interface. +- **UB checking.** With unsafe rust it is possible to break the type system + guarantees in Rust without causing immediate errors. Contracts must be + cognizant of this and enforce the guarantees as part of the contract *or* + require users to explicitly defer such checks to use sites. The latter case + requires dedicated support because the potential UB must be reflected in the + havoc. @@ -157,7 +157,7 @@ fn my_div(dividend: u32, divisor: u32) -> u32 { `proof_for_contract` harness for each abstracted function, otherwise an error is thrown. In addition, by default, it requires all `proof_for_contract` harnesses to pass verification before attempting verification of any - harnesses that use the contract as an abstraction. + harnesses that use the contract as a stub. A possible harness that uses our `my_div` contract could be the following: @@ -261,21 +261,22 @@ impl Vec { The `#[modifies(when = CONDITION, targets = { MODIFIES_RANGE, ... })]` consists of a `CONDITION` and zero or more, comma separated `MODIFIES_RANGE`s which are -essentially an lvalue. +essentially a place expression. + +Place expressions describe a position in the abstract program memory. You may +think of it as what goes to the left of an assignment. They compose of the name +of one function argument (or static variable) and zero or more projections +(dereference `*`, field access `.x` and slice indexing `[1]`[^slice-exprs]). If no `when` is provided the condition defaults to `true`, meaning the modifies ranges apply to all invocations of the function. If `targets` is omitted it defaults to `{}`, e.g. an empty set of targets meaning under this condition the function modifies no mutable memory. -Lvalues are simple expressions permissible on the left hand side of an -assignment. They compose of the name of one function argument (or static -variable) and zero or more projections (dereference `*`, field access `.x`, -slice indexing `[1]`[^slice-exprs]). -[^slice-exprs]: Slice indices can be lvalues referencing function arguments, - constants and integer arithmetic expressions. Take for example this vector - function (lvalues simplified vs. actual implementation in `std`): +[^slice-exprs]: Slice indices can be place expressions referencing function + arguments, constants and integer arithmetic expressions. Take for example + this vector function (places simplified vs. actual implementation in `std`): ```rs impl Vec { @@ -285,14 +286,34 @@ slice indexing `[1]`[^slice-exprs]). ``` -Because lvalues are restricted to using projections only, Kani must break -encapsulation here. If need be we can reference fields that are usually hidden, -without an error from the compiler. - -In addition to lvalues, a `MODIFIES_RANGE` can also be terminated with more -complex slice expressions as the last projection. This only applies to `*mut` -pointers to arrays. For instance this is needed for `Vec::truncate` where all of -the latter section of the allocation is assigned (dropped). +Because place expressions are restricted to using projections only, Kani must +break Rusts `pub`/no-`pub` encapsulation here[^assigns-encapsulation-breaking]. +If need be we can reference fields that are usually hidden, without an error +from the compiler. + +[^assigns-encapsulation-breaking]: Breaking the `pub` encapsulation has + unfortunate side effects because it means the contract depends on non-public + elements which are not expected to be stable and can drastically change even + in minor versions. For instance if your project depends on crate `a` which + in turn depends on crate `b`, and `a::foo` has a contract that takes as + input a pointer data structure `b::Bar` then `a::foo`s `assigns` contract + must reference internal fields of `b::Bar`. Say your project depends on the + *replacement* of `a::foo`, if `b` changes the internal representation of + `Bar` in a minor version update cargo could bump your version of `b`, + breaking the contract of `a::foo` (it now crashes because it e.g. references + non-existent fields). + + You cannot easily update the contract for `a::foo`, since it is a + third-party crate; in fact even the author of `a` could not properly update + to the new contract since their old version specification would still admit + the new, broken version of `b`. They would have to yank the old version and + explicitly nail down the exact minor version of `b` which defeats the whole + purpose of semantic versioning. + +In addition to a place expression, a `MODIFIES_RANGE` can also be terminated +with more complex *slice* expressions as the last projection. This only applies +to `*mut` pointers to arrays. For instance this is needed for `Vec::truncate` +where all of the latter section of the allocation is assigned (dropped). ```rs impl Vec { @@ -309,10 +330,10 @@ in Rust `p[i..j]` would be equivalent to `std::slice::from_raw_parts(p.offset(i), i - j)`. `i` must be smaller or equal than `j`. -A `#[frees(when = CONDITION, targets = { LVALUE, ... })]` clause works similarly +A `#[frees(when = CONDITION, targets = { PLACE, ... })]` clause works similarly to `modifies` but denotes memory that is deallocated. Like `modifies` it applies only to pointers but unlike modifies it does not admit slice syntax, only -lvalues, because the whole allocation has to be freed. +place expressions, because the whole allocation has to be freed. [^inferred-footprint]: While inferred memory footprints are sound for both safe and unsafe Rust certain features in unsafe rust (e.g. `RefCell`) get @@ -390,8 +411,7 @@ Kani reports a compile time error if any of the following constraints are violat - A harness may have up to one `proof_for_contract(TARGET)` annotation where `TARGET` must "have a contract". One or more `proof_for_contract` harnesses may have the - same `TARGET`. All such harnesses must pass verification, before `TARGET` may - be used as an abstraction. + same `TARGET`. A `proof_for_contract` harness may use any harness attributes, including `stub` and `stub_verified`, though the `TARGET` may not appear in either. @@ -403,7 +423,10 @@ Kani reports a compile time error if any of the following constraints are violat is already implied by `proof_for_contract`). - A harness may have multiple `stub_verified(TARGET)` attributes. Each `TARGET` - must "have a contract". No `TARGET` may appear twice. + must "have a contract". No `TARGET` may appear twice. Each local `TARGET` is + expected to have at least one associated `proof_for_contract` harness which + passes verification, see also the discussion on when to check contracts in + [open questions](#open-questions). - Harnesses may combine `stub(S_TARGET, ..)` and `stub_verified(V_TARGET)` annotations, though no target may occur in `S_TARGET`s and `V_TARGET`s @@ -774,9 +797,9 @@ times larger than what they expect the function will touch). havoc. - **`modifies` clauses over patterns.** Modifies clauses mention values bound in the function header and as a user I would expect that if I use a pattern in - the function header then I can use the names bound in that pattern as lvalues - in the `modifies` clause. However `modifies` clauses are implemented as - `assigns` clauses in CBMC which does not have a notion of function header + the function header then I can use the names bound in that pattern as base + variables in the `modifies` clause. However `modifies` clauses are implemented + as `assigns` clauses in CBMC which does not have a notion of function header patterns. Thus it is necessary to project any `modifies` ranges deeper by the fields used in the matched pattern. From 800defe603b743c5dcf46c94ae327c7845721446 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 24 Aug 2023 14:02:48 -0700 Subject: [PATCH 36/36] Rename history variables to history expressions --- rfc/src/rfcs/0009-function-contracts.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/rfc/src/rfcs/0009-function-contracts.md b/rfc/src/rfcs/0009-function-contracts.md index 0261f6e23798..957886445d54 100644 --- a/rfc/src/rfcs/0009-function-contracts.md +++ b/rfc/src/rfcs/0009-function-contracts.md @@ -339,12 +339,12 @@ place expressions, because the whole allocation has to be freed. and unsafe Rust certain features in unsafe rust (e.g. `RefCell`) get inferred incorrectly and will lead to a failing contract check. -### History Variables +### History Expressions Kani's contract language contains additional support to reason about changes of mutable memory. One case where this is necessary is whenever `ensures` needs to refer to state before the function call. By default variables in the ensures -clause are interpreted in the post-call state whereas history variables are +clause are interpreted in the post-call state whereas history expressions are interpreted in the pre-call state. Returning to our `pop` function from before we may wish to describe in which @@ -366,7 +366,7 @@ impl Vec { `old` allows evaluating any Rust expression in the pre-call context, so long as it is free of side-effects. See also [this explanation](#changes-to-other-components). The borrow checker enforces that the -mutations performed by e.g. `pop` cannot be observed by the history variable, as +mutations performed by e.g. `pop` cannot be observed by the history expression, as that would defeat the purpose. If you wish to return borrowed content from `old`, make a copy instead (using e.g. `clone()`). @@ -775,7 +775,7 @@ times larger than what they expect the function will touch). variables. For instance `#[ensures({let x = ...; old(x)})]` cannot work as an AST rewrite because the expression in `old` is lifted out of it's context into one where the only bound variables are the function arguments (see also - [history variables](#history-variables)). In most cases this will be a + [history expressions](#history-expressions)). In most cases this will be a compiler error complaining that `x` is unbound, however it is possible that *if* there is also a function argument `x`, then it may silently succeed the code generation but confusingly fail verification. For instance `#[ensures({