Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Code Generator: Sealed Data

Email Gateway (Aug 19 2022 at 13:39):

From: René Neumann <rene.neumann@in.tum.de>
Hi,

I have an algorithm that needs to receive state information to be passed
inbetween invocations from outside code. To actually prove something
meaningful about this, I need this state data to preserve certain
invariants. Now, as outside code is involved, I must also make sure,
that this code has no way to tamper with the state.

First I thought to use the approach given in Library/Dlist.thy: a
structure annotated with an invariant. Unfortunately, the code generator
exports the constructor as part of signature. Hence, in outside code, I
simply can write "Dlist [1,2,2,2,2]" -- and any code exported from
Isabelle is convinced that the underlying list is distinct, while in
fact it is not.

Of course, in my code, I could enforce the invariant explictly, but this
is not feasible.

So I need something similar to how the Isabelle core guarantees
tamper-free proofs: Do not export constructors you don't control.

Is something like this possible with the code generator? Is it somehow
possible to say "export definition, but not into signature", and, more
important, "export datatype, but in signature only as 'type'".

Thanks,
René
smime.p7s

Email Gateway (Aug 19 2022 at 13:41):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi René,

First I thought to use the approach given in Library/Dlist.thy: a
structure annotated with an invariant.

this is how you have to start anyway to deal with invariants.

Unfortunately, the code generator

exports the constructor as part of signature. Hence, in outside code, I
simply can write "Dlist [1,2,2,2,2]" -- and any code exported from
Isabelle is convinced that the underlying list is distinct, while in
fact it is not.

Currently it is indeed assumed that »client code« knows how to deal with
generated code.

As a workaround, you can do something like (e.g. in SML):

structure Generated_Code =
struct
<generated code>
end

signature FOO =
sig
<what is really needed for client code without abstract constructors>
end

structure Foo: FOO =
struct
open Generated_Code
end

Future Isabelle releases will minimize their exports. In the more
remote future this could also be used as a vehicle to prevent export of
abstract constructors entirely.

Hope this helps,
Florian
signature.asc

Last updated: Apr 24 2024 at 16:18 UTC