[isabelle] Code Generator: Sealed Data


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'".


René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.