November 09, 2019
On Saturday, 9 November 2019 at 17:16:40 UTC, Ola Fosheim Grøstad wrote:
> Well, not necessarily, some C++ compilers support it.  The problem is that you probably don't want to introduce too many auxiliary facts, as that would just slow down compilation with no gain (and perhaps even confuse a naive optimizer). Anyway, you should be able to add facts to LLVM by compiling a boolean expression and then assuming it to hold.

Maybe by doing something along the lines of:

if ( !must_be_true ) { llvm.unreachable }


November 09, 2019
On Saturday, 9 November 2019 at 17:16:40 UTC, Ola Fosheim Grøstad wrote:
>
> Well, not necessarily, some C++ compilers support it.  The problem is that you probably don't want to introduce too many auxiliary facts, as that would just slow down compilation with no gain (and perhaps even confuse a naive optimizer). Anyway, you should be able to add facts to LLVM by compiling a boolean expression and then assuming it to hold.
>
> But maybe the language syntax should allow you to select which propositions you want to propagate to the optimizer. Not sure if LLVM can express quantifiers though (forall/exists).
>

I'm pretty ignorant of how all that would all work, is there some sort of a standard way to give optimizers "hints" based on what the solver can show? I don't want to over-sell the potential performance gains. (Like Rust fans talking about how _theoretically_, Rust is much faster than C because of the lack of pointer aliasing, but the benchmarks just don't bear it out. (yet))

>
> But I guess one will have to distinguish the two cases somehow. Which is basically why I think trying to improve basic libraries with assume-statements and manual proofs is the best starting point. Then you get an idea for how it can affect optimization.

Oof. You're gonna have a hard time finding volunteers for that one. I think that's how projects like SeL4 do it though, translating C into HOL and then adding verification conditions manually. I want to say the SeL4 proofs are something like 10x the number of lines as the code itself. Working manual proofs can be kind of fun, like a puzzle, but I've read about some negative case studies where manually verified code had some incorrect assumptions in the proofs, or proved things that ended up being orthogonal to the desired outcome. It's murky.

>
> I will certainly read and comment on it, if you want to write one. You could start with specc'ing out a list of requirements?
>

I'll take a look at the DIP author guidelines and start putting something together. I think it's worth the community's consideration if we can do this in a way that minimizes impact. As a long time mostly-lurker and D user, I don't have any credibility with compiler changes, so I don't want to be one of those guys who jumps in with a big DIP that tries to make Walter and all the other contributors jump through their ass.

I was toying with the idea of 2 or more parts: start with a single DIP for "D Formal Verification Support" that maybe just describes which UDAs should be agreed upon for external proof tools to use, the behavior that should be expected when using contracts in those tools, and maybe a small set of changes to the language spec:

- Universal quantification: The low-impact way would be to set aside an attribute @forall or @foreach, then figure out what tuple elements you'd need to generate a VC from them and how you'd tie them to a function, module, variable, etc.

(Longer-term, consider a change to the language to create a foreach expression or add a new expression "forall" (or something). I would anticipate a lot of weeping and gnashing of teeth.)

- Existential quantification: I think you can do this in a low-impact way is to set aside an attribute @exists or @forsome and sort out the UDA tuple spec that provers would use. Longer term, add an "exists" or "forsome" expression.

- Loop invariants: Allow invariant{} blocks inside loop statements in addition to classes and structs. This is the only part of the DIP that I can foresee requiring a language change; I don't know any way of attaching a UDA to a statement. I _think_ this would be the only blocker.

LATER ON: if there's interest and any promise, then we could look at making parts of Phobos verified, adding compiler support for provers, etc. in follow-on DIPs. A very powerful addition would be user-defined scalar types with their own invariants, but this is a BIG language change.

(Even better would be strong subtypes, refinement types, or first-order types, but you can simulate them well enough with contracts in an invariant clause).

A smaller language change would be to give invariant a parameter with a hypothetical or ghost variable and allow it on aliases:

alias uint ShoeSize;
invariant(ShoeSize T){
  assert(T > 0);
  assert(T < 24);
}

void buyBiggerShoes(ShoeSize s){
  Shoe t;

  t.size = s + 1;   //Consider this line

//Invariant asserts get run if in Debug mode, so hopefully during
// unit-testing you tried it with s == 23.

//During proof time, this would warn with something like:
// "Cannot prove t.size < 24 (example: when s == 23)
// Possible solution: add s to list of preconditions for buyNewSchoolShoes"
// (this is almost exactly what SPARK gives)

  sendOrder(t);
}

Built-in types would have implied invariants, at least as far as proofs are concerned:
invariant(int i){
  assert(i <= int.max);
  assert(i >= int.min);
}

So it might be that this initial DIP could just focus on beefing up invariant{}?

I'd welcome any more-informed thoughts on how to proceed and go through the DIP process, if there's interest!

>
> I actually meant source code only. You distribute the source code, but with certified "requires"/"assume"/"ensures" statements that is bound to the source code using cryptographic hashing and an online index (so that it can be checked or revoked).
>
> I guess one issue is that it has to be a standalone library (e.g. only depend on a specific version of the standard library) for this to work. Otherwise you would have to tie it to a specific certified version of all the libraries you depend on.
>
> But... I don't actually think that is a big deal, you typically would pre-verify basic libraries. You could use a simple concatenation for the hash with sorted filenames and some sentinel character sequence for separating files, e.g.:  filename1, sep, file1, sep, filename2, sep, file2, sep, sep.
>
>
> I am actually not sure how this could be done well. Because you could have array accesses within a conditional expression.

Flow analysis can sort that out, checking both branches of the conditional and making sure that contracts hold in every case.

>
> Maybe you'd actually have to annotate the indexing with some new syntax to tell the compiler that the access does not need bounds checks as it has been proven already to hold... So I guess this is an area that needs to be fleshed out with many examples.
>
> Anyway, it seems reasonable that a tool would take source code, verify it and emit an annotated version of the source code. Then less capable compilers could use the verified results.
>
> Most users are not going to write verifiable code themselves.
>

Ideally, it will be easy to run the proof tool on existing code as a sort of linter in addition to unit tests and other static analysis. The first time you see warnings like "Cannot prove abc is less than def (example: def = 255)" because you didn't consider edge cases, it opens your eyes to how proofs can really save you from a lot of testing and debugging.

The goal is that a user doesn't have to do anything different than normal to write verifiable code. It's all verifiable, but it's up to the user how deep they want to go down the rabbit hole to prove functional correctness by adding a ton of contracts.

> I think so, if they are proven to hold by a tool/compiler then they hold. Dataflow analysis is sufficient, when it succeeds, but will fail in many cases at it is a weak approach. However, it is also much faster than a proper solver. Basically just an optimization for performance reasons.
>
> But you also want to use assume manually sometimes when describing hardware registers (e.g. describing that bit 8-32 always are zero), or when something has been proven by hand and has a significant performance impact.
>

One kind of neat thing that SPARK has is the ability to break volatile down into sub-categories like "Effective_Reads", where reading a value takes something off a UART, or "Effective_Writes", where writing to a hardware register has some effect on the system, and "Async_Readers/Writers" where some hardware will be accessing memory behind the scenes... now how that affects the state of a proof, I'm not totally sure.

>
> Yes, this is where different goals may lead to different designs... so the challenge is to come up with something that can both support correctness and optimization without being extremely complicated in terms of syntax.
>

I'm not super smart on the optimization side of the house, my focus would be on correctness first and then let the optimization wizards extract what useful information they can from that.

>
> Sure, you could also just define a dummy "ensures", "requires", whatever… function that takes a boolean as a parameter. With an empty body, or an assert.
>

I'll have to give some thought to this.

>
> There are papers on proof-carrying-assembly code...
>
> Although the basic idea behind certification would be that you get to use the postconditions and assumes without having to run costly verification on your own machine.
>
> You might even see a commercial service with very strong provers and effective hardware.
>

I think you'll see SaaS offerings like this in 10 years, kind of like big ML farms now. Proofs on big code bases can take a long time, definitely something you would want as part of an overnight build in a CI pipeline. Single file proofs can go pretty quick though, depending on how deep you let them search.

>
>
> Perhaps Why3ML is a good choice, but I would've started with Boogie.

I hadn't heard of Boogie before, but it looks promising - It doesn't feel quite as mature as Why3, but the syntax looks a lot friendlier, for sure.

So, having done no DMD compiler hacking myself, is the state of the "DMD as a library" mature enough now to where somebody could import dmd.compiler, get an AST and start figuring out VCs?

A DIP without some sort of prototype tooling, even if primitive, is going to be pretty toothless, IMO.

-Doc

November 09, 2019
On 11/8/2019 6:43 PM, Doc Andrew wrote:
> Even without specific contracts, a list of things that you _know_ are run-time errors (divide-by-zero, null-pointer dereference, etc.) could be proven absent from code.

Actually, I deliberately insert null-pointer dereferences to get stack traces when debugging :-)

Anyhow, don't worry, in/out contracts are remaining because some people do use them. There are some benefits to them, but I just don't think they're worth the cost.
November 09, 2019
On 11/9/2019 4:23 AM, Timon Gehr wrote:
> You need in and out contracts for modular verification.

You can pick up both from looking at the assert's in the prolog and epilog of the function.

More importantly, nobody is working on a modular verification system for D, and haven't for 20 years, so the contracts aren't particularly useful.
November 10, 2019
On Saturday, 9 November 2019 at 21:11:14 UTC, Doc Andrew wrote:
> I'm pretty ignorant of how all that would all work, is there some sort of a standard way to give optimizers "hints" based on what the solver can show?

I don't think so, but if you establish something that is to weak for verification it still can potentially be used for optimization.


> I don't want to over-sell the potential performance gains.

Of course not, you would have to provide actual examples.  The "easy" gains would be from removing dynamic checks, but not so easy in reality.  If it is easy then the optimizer can already do it using dataflow analysis.

So figuring out "trivial" small examples where the optimizer fails by looking at generated assembly is a good starting point.


> - Universal quantification: The low-impact way would be to set aside an attribute @forall or @foreach, then figure out what tuple elements you'd need to generate a VC from them and how you'd tie them to a function, module, variable, etc.

I was more thinking, what do you do if it fails? One cannot keep O(N) or O(N^2) asserts in the code as a dynamic check... :-/

I guess the easy solution is to require that "ensure" is fulfilled at compile time and not allow quantified expressions in asserts.


> (Longer-term, consider a change to the language to create a foreach expression or add a new expression "forall" (or something). I would anticipate a lot of weeping and gnashing of teeth.)

I once added a unicode-token-layer to the dmd-lexer, and added alternative unicode math symbols to expressions. It only took a few hours. Modifying the lexer is a lot easier than expanding the parser. I think people who would write VC also would be familiar with math notation, so I one could just use that to avoid clashes.

E.g. you could have a not-so-pretty ascii syntax and a unicode shorthand.

Like:  "∀" vs "@vc_forall"

Unicode tokens is really easy to do this way as you just can rewrite "∀" to "@vc_forall" and "∃" to "@vc_exists", so no major changes are needed to add unicode symbols.


> - Loop invariants: Allow invariant{} blocks inside loop statements in addition to classes and structs. This is the only part of the DIP that I can foresee requiring a language change; I don't know any way of attaching a UDA to a statement. I _think_ this would be the only blocker.

Proving loop progression and termination is very important, and not so easy. What some FV languages do is that they introduce ghost-variables  for this (variables that are conceptually computed but not used for code generation).

So basically you increment the ghost variable(s) every iteration and prove that there is a threshold for the value where the loop terminates.

But it won't really change the language that is compiled. It only changes the language that is verified. So not an effective change.

But verification will probably have to happen after template expansion... Not sure how to deal with that.  Unless you want to verify templated code... which would be cool, but not sure of what roadblocks you would hit.

> (Even better would be strong subtypes, refinement types, or first-order types, but you can simulate them well enough with contracts in an invariant clause).

Lots of potential with more advanced typing... but prepare to be met with a lot of resistance for things that are actual language changes (things that can affect code gen and not only the verifier).

> A smaller language change would be to give invariant a parameter with a hypothetical or ghost variable and allow it on aliases:

Well, yes, but not necessarily a language change... As a start you could just define a local function "__vc_invariant" and treat it special by the verifier?

> I'd welcome any more-informed thoughts on how to proceed and go through the DIP process, if there's interest!

I don't know enough about what makes a DIP succeed.  What is common in other languages is to make a library/tool implementation first as  proof of concept and then argue that it would be better as a language extension.

So that probably is the better approach... But I don't know.

But reserving the vocabulary makes a lot of sense. Then I would point to other languages, particularly FV languages, so that you reserve the most common terms "@requires", "@ensures", "@forall", "@exists" etc.

But in a proof-of-concept you can just use "_vc_requires" or some other prefix.

>> I am actually not sure how this could be done well. Because you could have array accesses within a conditional expression.
>
> Flow analysis can sort that out, checking both branches of the conditional and making sure that contracts hold in every case.

No, I meant how to express it syntactically in a way that allows you to distribute pre-verified code.

(The point of having verification would be to cover those cases that standard flow analysis fail on.)

> analysis. The first time you see warnings like "Cannot prove abc is less than def (example: def = 255)" because you didn't consider edge cases, it opens your eyes to how proofs can really save you from a lot of testing and debugging.

Yes, maybe that is a use case.

If you write up something formal you ought to list such use-cases, and what they require.


> The goal is that a user doesn't have to do anything different than normal to write verifiable code.

:-/ not possible though.


> One kind of neat thing that SPARK has is the ability to break volatile down into sub-categories like "Effective_Reads", where reading a value takes something off a UART, or "Effective_Writes", where writing to a hardware register has some effect on the system, and "Async_Readers/Writers" where some hardware will be accessing memory behind the scenes... now how that affects the state of a proof, I'm not totally sure.

IIRC, D does not provide volatile though... You have to use something intrinsics-like. So memory mapped registers are not types in D, it is dealt with as a memory fenced access-action...


> So, having done no DMD compiler hacking myself, is the state of the "DMD as a library" mature enough now to where somebody could import dmd.compiler, get an AST and start figuring out VCs?

No idea. I think the major hurdle for you would be the templating.

Maybe only deal with non-templated code, because then you can use one of the D parsers and rewrite the code with verification-annotations instead of modifying the actual compiler. For a proof-of-concept.


> A DIP without some sort of prototype tooling, even if primitive, is going to be pretty toothless, IMO.

Yes. You could write something "informational". Then evolve it later.

But you'll get feedback on whether there is any interest at all in the community? If there is no interest then it would not be possible to maintain it in the compiler either.

Starting a discussion on the vocabulary might tell you something about what kind of support you can expect for your ideas.

November 10, 2019
On Saturday, 9 November 2019 at 21:11:14 UTC, Doc Andrew wrote:
> A DIP without some sort of prototype tooling, even if primitive, is going to be pretty toothless, IMO.

A fun way to get started might be to create your own verified mini-language and compile it to D code and use that as a proof-of-concept.

November 10, 2019
On Sunday, 10 November 2019 at 00:27:46 UTC, Ola Fosheim Grøstad wrote:
>
>> - Universal quantification: The low-impact way would be to set aside an attribute @forall or @foreach, then figure out what tuple elements you'd need to generate a VC from them and how you'd tie them to a function, module, variable, etc.
>
> I was more thinking, what do you do if it fails? One cannot keep O(N) or O(N^2) asserts in the code as a dynamic check... :-/
>
> I guess the easy solution is to require that "ensure" is fulfilled at compile time and not allow quantified expressions in asserts.

Yeah, you could make ensure work like assert but strictly for proofs and not at runtime, but I kind of like the idea that if you can't prove a check at compile-time, it still makes it into your Debug code for thorough testing.

For the most part you're back to the status quo when a proof fails - you've got some unit tests to write, the checks will live in Debug code and they'll go away in Release code just like they do now. If the Debug performance hit is too onerous, then comment it out, or have a separate "proof-time assert". I'd have to think it through.

The one thing I'm not sure about is the situation I hinted at where post-conditions are on an interface where the function body itself wasn't proven. In this case, maybe they just act like assumptions. I have to do some more homework here.

>
> I once added a unicode-token-layer to the dmd-lexer, and added alternative unicode math symbols to expressions. It only took a few hours. Modifying the lexer is a lot easier than expanding the parser. I think people who would write VC also would be familiar with math notation, so I one could just use that to avoid clashes.
>
> E.g. you could have a not-so-pretty ascii syntax and a unicode shorthand.
>
> Like:  "∀" vs "@vc_forall"
>
> Unicode tokens is really easy to do this way as you just can rewrite "∀" to "@vc_forall" and "∃" to "@vc_exists", so no major changes are needed to add unicode symbols.
>

You're going to scare people off with that sorta stuff :)

>
> Proving loop progression and termination is very important, and not so easy. What some FV languages do is that they introduce ghost-variables  for this (variables that are conceptually computed but not used for code generation).
>
> So basically you increment the ghost variable(s) every iteration and prove that there is a threshold for the value where the loop terminates.
>
> But it won't really change the language that is compiled. It only changes the language that is verified. So not an effective change.
>
> But verification will probably have to happen after template expansion... Not sure how to deal with that.  Unless you want to verify templated code... which would be cool, but not sure of what roadblocks you would hit.

Yeeeah... I'm not sure how that is going to play out. I don't really know how contracts work with templated code currently. It could be that if the contracts appear in template code, then they just get copy-pasted into each new instantiation of the template, and life is good. The prover will do a ton of extra work re-proving the same thing for each new type, but who cares? And actually, you might discover that the perfectly generic function you wrote actually has a bunch of nasty corner cases lurking inside...

I think you'd just have to wait until all the CTFE and template stuff is done before you start generating VCs. It might not be a deal-breaker, but that's speaking from ignorance, frankly.

>
> Lots of potential with more advanced typing... but prepare to be met with a lot of resistance for things that are actual language changes (things that can affect code gen and not only the verifier).
>

Oh yeah, I'm not holding my breath for anything like that. Baby steps.

>
> Well, yes, but not necessarily a language change... As a start you could just define a local function "__vc_invariant" and treat it special by the verifier?

True, we might be able to just use a nested function with some contracts baked into it.

>
> If you write up something formal you ought to list such use-cases, and what they require.
>
>
>> The goal is that a user doesn't have to do anything different than normal to write verifiable code.
>
> :-/ not possible though.
>

Oh I dunno, aside from adding some extra contracts and avoiding certain language constructs* (like goto), not much really has to change for the average user to get some benefit from running the code through a proof tool, even if they could care less about stamping a function as "certified" or not.

* Granted, those "certain language constructs" may end up being an insurmountable barrier, where the formally verifiable subset of D is stripped of so many features that it isn't really worth it. Too early to tell.

>
> But you'll get feedback on whether there is any interest at all in the community? If there is no interest then it would not be possible to maintain it in the compiler either.
>
> Starting a discussion on the vocabulary might tell you something about what kind of support you can expect for your ideas.

Let me mull it over a bit. I might start a separate thread where people can weigh in. The field is still pretty new [AI/ML 70 years ago ;) ], so it might be a good way to raise awareness and at least get people thinking about some of the possibilities for writing _real_ safe code.
November 10, 2019
On Sunday, 10 November 2019 at 00:31:18 UTC, Ola Fosheim Grøstad wrote:
>
> A fun way to get started might be to create your own verified mini-language and compile it to D code and use that as a proof-of-concept.

So that brings up the question of which approach to use.

The idea you mentioned there is how F* (or at least the subset "Low"), Coq, and probably some others I can't think of - do it. You write verified functional code, run it either through an automated solver or write proofs manually, and then "extract" a compile-able (basically C) or interpret-able (OCaml, Scheme, Haskell...) program in another language from it. For C, I think usually they target the CLight dialect of C, so they can use the CompCert verified compiler http://compcert.inria.fr/doc/index.html.

The cool thing here is that you can basically guarantee that the assembly that's generated matches the specifications of the original code. I consider this approach the "Obsessive-Compulsive" method. This is for the programmer who just _knows_ that there's a compiler bug causing his code to be wrong. :) This is more suited towards the goal of a totally verified toolchain.

(Side note: There's a certain, say, "academic" beauty in thinking that you've got "turtles all the way down" with a totally verified language and toolchain. But there's always going to be hardware bugs, cosmic rays, out-of-memory conditions, etc.)

Personally, I'm less worried about what DMD, GCC or LDC might have gotten wrong than what _I_ goofed up in my own code, so this option isn't super appealing to me.

Eventually, I'd love for my compiler, standard library, OS, etc. to be formally-verified. But... they're probably not going to be written in Coq or ML, if we're being honest. D or Rust? More probable - so we get to option 2:

Option 2, taken by Dafny and SPARK (and I think FRAMA-C too, but don't quote me on that), is take the language you want (or at least something close), then generate an intermediate language that can be easily broken down into verification conditions to run through the solver.

For formally-verified D, this is the route I'd want, because I like writing D!

Writing a verified language that extracts to D is sort of a dead-end, in my opinion. It doesn't make people's D code any safer, and if I'm going to extract to a compiled language, then I might as well decide on C/CLight and take advantage of CompCert or some other toolchain that's been verified already, or just use GCC and get wider platform exposure.

Option 3 is to just take the language as it is and try to generate some kind of formal logic based on the language constructs as you parse it, then work out the solver mechanics or some kind of proof assistant for working through it. There might be _somebody_ out there that could take this on, but it ain't me!

A lot of smart people have already worked out automated provers for ML-ish languages, and D is unique in that it already has nice contract syntax that could map nicely to the axioms and verification conditions that those languages use.

I suspect that ultimately, we could get what we need by taking some intermediate DMD front-end state (maybe AST + UDA __traits), doing flow analysis, and dumping out (a lot of) some intermediate verification language with the assertions baked in and run an existing proof tool on it. You'd have to do some gonkulation of the solver output to figure out what your original line of code was for sensible error messages, but that's possible.

Microsoft's VCC multithreaded C verifier tool might be a good starting point, since it's got a friendly license (MIT) - https://github.com/microsoft/vcc. It uses Boogie, too. SPARK (the GNATProve tool, specifically) is all GPLed, so not sure if it's a good resource or not. IANAL and all that.

That's an almost criminally-understated view of the task, but I think it might give D a path towards FV, if people think it's worth it. D has always been on the cutting edge of good SW engineering support in a language, so who knows?

-Doc
November 10, 2019
On 10.11.19 00:23, Walter Bright wrote:
> On 11/9/2019 4:23 AM, Timon Gehr wrote:
>> You need in and out contracts for modular verification.
> 
> You can pick up both from looking at the assert's in the prolog and epilog of the function.
> ...

- Modular verification means it's enough to have DI files for functions you call, without a function body.

- Some asserts in the prologue of your function might really be asserts and not assumes.

- Similarly, some asserts in the epilogue of your function might not be things you actually want to guarantee to the caller.

> More importantly, nobody is working on a modular verification system for D, and haven't for 20 years, so the contracts aren't particularly useful.

Programmers can read contracts too, not just verification systems. They are useful documentation and can be used for assigning blame: Is the assertion failure the fault of the caller or the callee?
November 10, 2019
On Saturday, 9 November 2019 at 02:18:41 UTC, rikki cattermole wrote:
> On 09/11/2019 11:41 AM, Walter Bright wrote:
>> 
>> I've thought for 35 years that assert()s can be the input to a program prover, i.e. it's nothing new, but I do not have the expertise to figure out such proofs might work, other than simplistic cases.
>
> Sounds like some universities need to be contacted, perhaps a future PHD student would be interested in doing the theory.

At UPB Bucharest we have discussed with a formal verification professor and published a research project for a masters student (2 years) where the goal is to implement a simple solver for contracts in D.