Gaëtan Gilbert said:
but using module abstraction to hide foo in Coq requires turning bar opaque
Module Type T. Parameter bar : nat. End T. Module M : T. Definition foo := 1. Definition bar := foo + 1. End M. Fail Check M.foo. (* not found [I have added this line] *) Eval cbv in M.bar. (* = M.bar *)
Cool, but Is there any way to have that bar
not opaque and compute? Otherwise that seems not really a viable approach (for private scoping, at least not in most cases).
FWIW, I'd vote for such a feature, though I might be missing the implications. My 2c: unless I am missing something, not having private scope proper makes it impossible for a piece of code to keep a secret (e.g. a component that takes a secret as argument, but then there is no way to keep it secret). -- Indeed, missing private scoping proper, I am not even sure how one would formalize such a functionality and then extract code that does in fact have private scope...?
Incidentally, at least Print
does not respect that hiding:
Print M.
(*
Module M : T := Struct
Definition foo : nat.
Definition bar : nat.
End
*)
Clients of M
only see what's part of T
, so if you want bar
to compute, you have to expose its definition:
Module Type T. Definition bar : nat := 2. End T.
Module M : T. Definition foo := 1. Definition bar := foo + 1. End M.
Fail Check M.foo. (* not found [I have added this line] *)
Eval cbv in M.bar.
to reduce duplication, here one can also reuse T
in M
:
Module Type T. Definition bar : nat := 2. End T.
Module M : T. Include T. Definition foo := 1. End M.
I'm not sure that's what you were asking, but one can't expose bar := foo + 1.
(to enable computation) while hiding the existence of foo
. However, if one hides bar := foo + 1
, I believe that bar
would still compute after extraction.
Cool, but Is there any way to have that bar not opaque and compute?
not with module abstraction
Print respects nothing
Paolo Giarrusso said:
to reduce duplication, here one can also reuse
T
inM
:Module Type T. Definition bar : nat := 2. End T. Module M : T. Include T. Definition foo := 1. End M.
Wait, that doesn't actually work if T
contains parameters which are defined in M, right? It would be a duplicate definition error
(Reading about the module system now, and it is odd how much syntax there isn't for defining modules, the abstract theory contains "module expressions" and these are printed by Print
on modules but you can't actually type that...? What's the interactive module equivalent of with Definition foo := 1
?)
Here is a motivating example, meant to be the target code (this is TypeScript, but please take it as pseudo-code, any language with a notion of private scope would do):
type SafeInteger = number; // (we can do better, assume no problem here...)
interface IEncryptor {
encrypt(plain: SafeInteger): SafeInteger;
decrypt(cipher: SafeInteger): SafeInteger;
}
class SimpleEncryptor implements IEncryptor {
#secret: SafeInteger; // <<private>>
constructor(secret: SafeInteger) {
this.#secret = secret;
}
encrypt(plain: SafeInteger): SafeInteger {
return plain ^ this.#secret;
}
decrypt(cipher: SafeInteger): SafeInteger {
return cipher ^ this.#secret;
}
}
And it would be nice to have that formalized in Coq then extracted, where in the formalization we could e.g. prove that indeed that implementation is a symmetric cipher, that it is total (works for all input of the SafeInteger
type), etc. etc, and even, crucially, that there is no way to extract the secret from SimpleEncryptor
[I mean, without "breaking the cipher"]!
Then, with reference to Paolo's comment in particular, I can guess one could write Coq code that extracts to the above, still just disregard any notion of private/hidden scope in the formalization, but of course my point is how to not disregard that aspect... and, can we?
(To be clear, I know there are Coq-certified compilers, but I have not yet dug into any of that, so apologies if my question here is just naive: any advice or specific references are very welcome.)
Julio Di Egidio said:
And it would be nice to have that formalized in Coq then extracted, where in the formalization we could e.g. prove that indeed that implementation is a symmetric cipher, that it is total (works for all input of the
SafeInteger
type), etc. etc, and even, crucially, that there is no way to extract the secret fromSimpleEncryptor
[I mean, without "breaking the cipher"]!
Do you want that secret
to be hidden from Coq code being extracted, or also from programs linked after extraction? Both make sense, and both are hard. Most compilers do _not_ preserve data abstraction in compiled output — compilers to machine code can't; compilers to bytecode (.NET/JVM) could in principle, but attacks have been demonstrated IIRC, and this is a topic of ongoing research.
@Paolo Giarrusso
Do you want that secret to be hidden from Coq code being extracted, or also from programs linked after extraction?
No code depends on a specific value of secret, not even the generated one, so I am not sure I understand what you are saying: we/I are rather interested in proving properties of programs, in the general sense. The problem I have presented in its simplest terms is how to formalize the very notion that a program component can have private state/members.
That said, the more I think of it, the more I'd think it must be possible, we just need to go "higher-level enough" in formalizing the target language: but, as said, I have not yet concretely dug into or tried any of that. So, any quick hints or references appreciated, otherwise I am happy to close it here and keep studying.
Just a side note: this may be interesting from a CS point of view. When I was saying that I would like something like private
, I was more thinking about robustness of libraries in Coq. I think it would be very nice if people were more aware of which constants they expose.
I think there might be an XY problem here, it's not clear to me that "secrecy" is a property you want extraction to obey in general; instead you should consider designing a deeply embedded DSL and prove properties about the semantics of that.
Coq also has a bunch of design principles that are incompatible with what you're requesting, such as:
Private Inductive
breaks this one)The question is definitely non-trivial, but compiling Coq modules to ML modules would conceivably preserve abstraction and let the operations compute after extraction. Abstraction via modules prevents clients in Coq from unfolding definitions, but that's not necessary: proofs that depend on the definition can be done inside the module
@Jason Gross
I think there might be an XY problem here, it's not clear to me that "secrecy" is a property you want extraction to obey in general; instead you should consider designing a deeply embedded DSL and prove properties about the semantics of that.
I must admit I have messed up a little bit: initially I was asking about "private" in Coq itself, then, especially since I thought @Gaëtan Gilbert had closed that one, I have slipped into "private" for extracted code...
Eventually, I can see that the latter is not a problem: as for the former, while I would agree e.g. with @Pierre Rousselin that it is a pretty nice feature to have in a language (for code structuring purposes even before such a need from a functional point of view), I am looking at Coq as a kind of low-level programming where one can indeed do without a notion of "private" (and thank you Jason for providing some indication as to why changing that would possibly introduce more problems than it solves) -- at least, for what I understand at this point.
OTOH, I am still thinking opaque terms and functions is not really a viable solution: namely, I'm thinking we need to be able to check and run the code we are writing (I mean, already the spec in Coq), even if just for very small inputs, as it's not practical to have to wait for after extraction to see some output (maybe I could say "runnable specifications" is an important part of the/my requirement): though, again, with the caution that I am still quite a rookie as to the mechanics of these development workflows.
At the very least, you can run those tests inside the module. Maybe it's not great software engineering but it should help.
You can also define a transparent module and seal it later, which might be useful in some scenarios or not
@Paolo Giarrusso
At the very least, you can run those tests inside the module. Maybe it's not great software engineering but it should help.
But the main requirement there is not testing, of which thanks verification we can indeed do (at least ideally, at least until in Coq) altogether without: the issue is runnable specifications, which is crucial not only to discuss with the client, but also for ourselves (software analysts to begin with) to even get to understand the problem and its possible solution(s). In other words, and a bit more technically and to the point, "runnable specifications" is fundamental to an iterative and actually evolutionary development process.
compiling Coq modules to ML modules
Also, I was reluctant to comment with the following, as I am either stating something obvious or I am simply wrong :) but, speaking in general (the target might be ML, C, TS, whatever), would that be enough for "verified software", extracting code (only)? Namely, I was thinking either the compiler/interpreter to begin with is written, verified, and extracted from Coq, or we can't really be sure that our expectations match reality... no? -- Where I would hope that cuts it for software, of course then there is the problem of hardware, but let's leave maybe that for another day...
Inside the module you can also run the specification and prove theorems — you can even expose them to clients.
Your question about extraction deserves a separate thread, but in short: there is ongoing research on verified extraction, and there are alternatives to extraction — for instance, with VST the code is in C but you can prove functional correctness results, that apply both to the source program and to CompCert's output.
VST builds on CompCert, so it looks like an example of what I was saying, that we eventually need a verified compiler in order to get to verified code. That said, I don't know the details of VST or CompCert, so I don't know what you mean by "alternatives to extraction": anyway agreed that this deserves a separate thread, and surely some more digging on my part.
VST doesn't "compile/extract" Coq to C, it just lets you prove in Coq that some C program implements a certain specification (also written in Coq), that's why it's not extraction.
Inside the module you can also run the specification and prove theorems — you can even expose them to clients.
How can we "expose" what is opaque? Considering also that module hierarchies (or equivalent) in real software applications, meaning already in the specifications, can get to dozens if not, for extensive frameworks, hundreds of levels deep.
So, unless I am missing your point, opaqueness at any point is just a show-stopper for the purpose of runnable specifications: the system/program must compute and work end-to-end, where that it computes at the top level of the modules hierarchy is in fact crucial, not only for workability and understanding, but also in the direction of a truly evolutionary development process, which is logically (I mean, the logic of it) a top-down approach...
You can expose theorems to clients
That's just not a runnable specification, which is similar to "(runnable) simulations"...
Well, if you choose to expose a runnable specification foo (you never have to, but it's an option), that means exactly exposing the definition of foo.
And yet, if I understand correctly, you also demand that foo is not exposed, so your wishes are not compatible.
So I'm probably missing something!
The technical term and the requirement here is runnable specifications, and it entails that, if foo is a computable function, then we can actually compute with it.
Coq definitely allows that.
Just as long as foo's definition is also visible to clients.
But honestly, since specifications are part of a public interface, that seems entirely fine.
@Paolo Giarrusso
Coq definitely allows that.
Together with the opaqueness that comes from "private" module members (as intended upthread)? How?? Consider this example, inspired by the TS example up-thread:
From Coq Require Import Nat.
Module Type ISecret.
Parameter value : nat.
End ISecret.
Module Type IEncryptor.
Parameter encrypt : nat -> nat.
Parameter decrypt : nat -> nat.
End IEncryptor.
Module CSimpleEncryptor (Secret : ISecret) : IEncryptor.
Definition encrypt plain := Nat.lxor plain Secret.value.
Definition decrypt cipher := Nat.lxor cipher Secret.value.
End CSimpleEncryptor.
Module MySecret : ISecret.
Definition value := 10.
End MySecret.
Module MyEncryptor : IEncryptor := CSimpleEncryptor MySecret.
Print MyEncryptor. (* := (SimpleEncryptor MySecret) *)
Print MySecret. (* := Struct Definition value : nat. End *)
Print MySecret.value. (* *** [ MySecret.value : nat ] *)
(* OK that far... except that now: *)
Eval cbv in MyEncryptor.encrypt 3.
(* = MyEncryptor.encrypt 3: nat *)
How do you make that MyEncryptor.encrypt
compute while hiding the secret?
okay, I see a distinction that might help.
what I meant is that you can definitely expose runnable specifications as part of the interface, _but then_ they must be public.
here, we don't need to hide Definition encrypt plain := Nat.lxor plain Secret.value.
, just the value.
above, the problem is that MySecret.value
can't be both a runnable specification and secret. But we can give a runnable specification of the cypher, even if not of the key. The behavior of abstraction here is different, because it's hard to make sense of opaque programs in a reasoning system.
Module Type IEncryptor.
(* Definition keyT : Type := nat. *)
Parameter keyT : Type.
Parameter encrypt : keyT -> nat -> nat.
Parameter decrypt : keyT -> nat -> nat.
End IEncryptor.
Module CSimpleEncryptor <: IEncryptor.
Definition keyT := nat.
Definition encrypt key plain := Nat.lxor plain key.
Definition decrypt key cipher := Nat.lxor cipher key.
End CSimpleEncryptor.
Module Type ISecret (Import Encryptor : IEncryptor).
Parameter key : keyT.
End ISecret.
Module MySecret : ISecret CSimpleEncryptor.
Definition key := 10.
End MySecret.
Print CSimpleEncryptor.
(*
Module
CSimpleEncryptor
:= Struct
Definition keyT : Set.
Definition encrypt : nat -> nat -> nat.
Definition decrypt : nat -> nat -> nat.
End
*)
Print MySecret. (* :=
Module
MySecret
: (ISecret CSimpleEncryptor)
:= Struct Definition key : nat. End
*)
Print MySecret.key. (* *** [ MySecret.value : nat ] *)
(* *** [ MySecret.key : CSimpleEncryptor.keyT ] *)
(* What works : we can perform encryption using a concrete key. *)
Eval cbv in CSimpleEncryptor.encrypt 10 3.
(* = 9 *)
(* Encryption using a hidden key typechecks, but the result cannot be computed using only the runnable specifications. *)
Eval cbv in CSimpleEncryptor.encrypt MySecret.key 3.
So, we agree that my requirement cannot be implemented, period.
Yeah, but I don't believe they're as fundamental as you suggest — plenty of people have verified code using runnable specifications, after all.
Since (runnable) specifications are, by definition, (a) public and (b) something that you must necessarily trust — you can't fully prove a specification correct — hiding parts of specifications from other parts of the spec doesn't seem fundamental; we do it to make code more robust to evolution, not to protect secrets.
Paolo Giarrusso said:
Since (runnable) specifications are, by definition, (a) public and (b) something that you must necessarily trust
Sorry but that is just wrong. But we should now open a thread about what runnable specifications actually are, so I'm thinking I'll leave it here: anyway we are not disagreeing on what can or cannot be done in Coq, which is enough for me.
that is just wrong
As a recommendation: Something like "that makes no sense to me" is still a clear disagreement, but it's accurate whatever turns out to be the truth, and it's more conducive to further discussion in the future. If you already know you know better than your conversation partner, should we be discussing?
Paolo, discussion is useful although, at least in this context, if it is rational and possibly to the point, and a piece of that rationality is that we are not as competent in the same areas, which is also what makes the discussion interesting and useful: namely, that you know things that I don't know and vice versa. And here I have the confidence to give you that one not as yet another working hypothesis on my part. Then if you think you do have that expertise, I am sorry but I simply disagree with you. -- And now let's please just leave it at that: I am available to discuss the point in a dedicated thread if you wish.
Last updated: Oct 13 2024 at 01:02 UTC