Refactoring FreeSpec #37
Conversation
lthms
added
kind | refactor
lthms
changed the title
lthms
changed the title
|
We are getting there. Sorry for the number of commits (and the massive diff). This is for the best. |
|
And it’s green! |
lthms
changed the title
|
For the record, I am currently trying to reduce the number of commits in order to make this big PR a bit more organized. |
In this patch, we introduce a complete rewriting of FreeSpec.Core key modules, as a first step towards a complete clean-up of the framework. Compare to the initial libraries, this rewriting provides several benefits: - We provide a hint database named freespec - We correctly scope them inside the FreeSpec.Core namespace - We do not rely on the functional extensionality axiom of the Coq standard library, meaning FreeSpec.Core revert to be axiom-free - We use a less opinionated coding style, taking our inspiration from libraries such as MetaCoq
A correct component is trustworthy wrt. to the specs of the interface it uses and complies to the specs of the interface it exposes.
We need this change to be able to prove that:
p == q -> trustworthy_program c w p -> trustworthy_program c w q
This way, when we have to prove
trustworthy_program c w (bind (bind p f) g)
We can rewrite this equation using the bind associativity law.
Note that, although I have never been able to prove it, I do believe
the two definitions (the old and the new one) are basically
equivalent.
Our main goal with this modification is to be able to reason about the airlock program trustworthiness without the need to explore manually the case where we open one door or the other.
|
The codebase is now in a reasonable shape, so feel free to have a look at I need to finish coq-prelude pending PR, and clean-up the various examples. Then, we will be able to merge that, push it to opam, and write a small announcement to coq-club ml. |
|
So, the last commit is almost ready, I just need to update the documentation when it is relevant. That being said, the formalism works, the tactics works (but remains hard to read :), and the examples have been updated. @yurug, feel free to have a look and tell me what you think about this PR (: Sorry for its size. |
There was a problem hiding this comment.
Here is my review of this huge (but beautiful patch). I am still confused about the terminology.
Trustworthiness: We usually say that a software component is trustworthy when we can use it with total confidence. Here, a software component is trustworthy when it uses an interface correctly. I understand that you have a security-oriented perspective (an opponent is trustworthy if it does not try to exploit a security breach) but from a formal method point of view, I think that is not the right terminology. I would prefer "respectfulness".
Promises: In PL, promises refer to a notion of concurrent programming introduced by Friedman in 1976. These are currently heavily used in JavaScript. What about using something like "guarantees" or "valid_answer" or "valid_response"?
Less critical: I am not a big fan of Provide. I would prefer writing:
Definition foo `{ix <| I1 I2 I3} := ...
would that still be possible?
| @mv mlihtml docs/ml | ||
|
|
||
| install: clean | ||
| @cd core; dune build; dune install; cd - |
There was a problem hiding this comment.
I would prefer a for-iteration here.
There was a problem hiding this comment.
I will have to dig a bit in make man page to see how to write a for, but it should be fairly easy and it makes sense.
| end | ||
| end. | ||
|
|
||
| (** * Verifying the Airlock Controller *) |
There was a problem hiding this comment.
At this point, a reader might want a summary of what you want to verify.
| [j] in addition to an impure computation [p], by means of a FreeSpec | ||
| component [c : compoment j ix s]. Two impure computations have to be | ||
| provided: [initializer] to create the initial state of [c], and [finalizer] | ||
| to clean-up the final state of [c] after the interpretation of [p]. *) |
There was a problem hiding this comment.
Is this a way to encapsulation?
|
The CI is green again \o/. To fix the regression introduced by @yurug commit, I introduced a dedicated attribute for the This is pretty ad-hoc, and you might probably want to find a better way to do it in the future… Now that coq-8.10 is released, I will try to clean-up this PR, address @yurug feedback, update the terminology, and ask for another round of review. The PR is huge now, and we really should merge it as quickly as possible to start working via PRs again. |
This shall fix GitHub issue #31, as the added test case attempt to demonstrate.
The goal of this tactic is to more easily exploit an hypothesis based on the predicate [trustworthy_run]. In addition to this change, we also propose a simple counter-based test case that we use to test [prove_impure] and [unroll_impure_run].
This patch introduces at least two significant refactoring. They are
committed together because they are deeply tied and have been
implemented at once (changes induce by one impacting the other).
With respect to the verification formalism:
- When reasoning on an impure computation trustworthiness, the
interface of the computation does not have to be the same as the
specification. It is just require that there is an instance of
the [MayProvide] typeclass to select primitives used by the
impure computation that are concerned by the specification
- The same approach has also been implemented for semantics
compliance.
- The [specsplus] operator has been changed, and allows for more
easily composed specification. This remains to be formally
proven, but this new operator is symmetric (c <.> c' ~~ c' <.> c)
and associative (c <.> (c' <.> c'') ~~ (c <.> c') <.> c'').
A major advantage of this approach is that it becomes possible to
compose specification of the same interface together. A drawback,
however, is that composing the same interface twice does not make
sense anymore (that is, i <+> i is morally equivalent to i). Note
that, from the perspective of the [Provide] typeclass, this was
already the case.
With respect to the component formalism:
- The component becomes stateless, and therefore a mere proxy from
the interface it exposes to the interface it used. A component
can rely on an external state thanks to the [STORE] interface.
- The different related definitions have been updated to reflect
this change.
According to our recent experiment implementing MiniHTTPServer, it
appears we have not yet found “one reduction strategy to rule them
all.” We therefore equip [Exec] to use two different reduction
strategies: [whd] (preferred by default) and [nf] (compatible with
[Program Fixpoint] and well-founded recursion).
To enable the [nf] strategy, FreeSpec users can use the `nf'
attribute:
#[nf] Exec my_impure.
In addition to this change, we use this opportunity to clean-up the
[exec] function.
This patch is based on the initial work of Yann Régis-Gianas.
Without this instance, the [impure_bind_assoc] lemma cannot be used when reasoning about trustworthy run. The [unroll_impure_run] tactic actually is trying to do just that when it finds an impure computation of the form [impure_bind (impure_bind _ _) _], and therefore was failing with a lovely setoid-related error message.
Before this patch, Coq could not find a concrete instance of [ix] for [Provide2 ix i1 i2] and more. We change the [find_may_provide] tactic in order to fix this issue. The change consists in using [eapply] rather than [apply], in order to work with existential variables.
This patch introduces many useful utility features which were
necessary to implement a robust [FILES] interface.
From [Exec] perspective, it adds several functions to manipulate
[prod] and [sum]. They have the particularity to be polymorphic, where
previous types handled by [Exec] where not. The interface could be a
bit easier to use, but the current implementation is straightforward
enough.
From the [Stdlib] perspective, we add the [RAISE] interface, to easily
specify “computation shortcuts.” The main idea is that an impure
computation of type [impure (RAISE a) b] is a computation which is
expected to produce a term of type [b], but may also be interrupted
while doing it, and in such a case produces a value of type [b] to be
handled by the callee.
We use this mechanics to deal with primitives of the [FILES]
interface. The resulting interface is pretty straightforward to
use. See for instance the following code snippet:
recover
do var fd <- try_open "index.html" in
var s <- try_file_size fd in
var txt <- try_read fd 10 in
echo (snd txt);
close fd;
echo "it worked"
end
with err of files_err =>
echo "it did not worked."
end
|
@yurug FYI, I am almost ready for a second round of review \o/. I mostly need to take into account your remarks about the examples. |
This large patch updates the code base to use the latest decided terminology. We take the opportunity to rearrange the organization of the module in the [FreeSpec.Core] library, and to fix several issues found in the codebase by Yann Régis-Gianas.
We prefer [bytes] (list of [byte]) over [string] (list of [ascii], that is 8 booleans each), and [int] over [Z].
This function allows for easily write computations which can be interrupt before they had a chance to compute a result. This can be used for instance to implement an exception mechanism, or the [break] operator of a loop.
Not all Coq terms behave nicely with every Coq reduction strategy. The strategy used by FreeSpec.Exec in order to find the next primitive to execute works well in most case, but during our experiments we have found at least one case where performance where pretty bad: non-structural recursion. In this case, the strategy used by FreeSpec to reduce the primitive itself work well. The [EVAL] interface leverages the internals of FreeSpec.Exec to avoid performance drops due to this scenario. By isolating problematic terms as arguments of the [Eval] primitive, it is possible to improve the performance of a program significantly.
Once closed,
Programhas been renamedimpureBefore merging
Here
dune-based buildAnd there