Hi guys, I was thinking lots about the strategy for Milestone 3, and here's what's in my head at the moment.
First, there's the Minimal Djed paper, which describes the state machine underpinning Minimal Djed and comes with machine-checked proofs of the desired stability properties.
The fact that the proofs are machine-checked might give us some leeway, in that we could separate:
proofs that the state machine evolves as expected; and
the actual stability proofs.
The reason I am thinking in this way is because the state-machine proofs should be structural in nature and not very difficult (my intuition is that the complexity of the compiled uplc code will be the only proper bottleneck), whereas the stability proofs are mathematical and complex, done semi-automatically in Isabelle, using several powerful decision procedures it has built in, and I am not sure how well this will translate to the automated setting of K and Z3. We can paralellize the effort here possibly, by, on the one hand, assuming the correctness of the transition system and then trying to push for the stability properties, while, on the other hand, doing the actual proofs for the assumed claims.
Next, I think it's essential to immediately understand in detail, guided by Jean-Frédéric, the structure of the source-language code, and in particular how the state is represented and which function corresponds to which operation in the protocol. We should be able to quickly confirm that the state transition system is as expected.
When it comes to verification, we will have code at three levels---source-language, pir, and uplc---and will need to think about datatypes, functions, and specifications across these levels. I think the main challenge there lies with the datatypes, because once we have them sorted, we can use them to write function specifications. I think the pir level will be mostly informative rather than requiring infrastructure. I've laid out some ideas about what this infrastructure would consist of in #269, with the current main challenge being parametric and inductive datatypes (such as tuples, lists, and maps) coming from source-language code.
We will also need the pyk library to automatically extract some of the global environment, ideally. In particular, we will certainly need some sort of a mass find/replace on identifiers, removing some de-Bruijn-like suffixes and possibly adding prefixes so that they can be parsed by kplc. Some of the auto-generatable patterns are given in #269, and there is some information there that I need to update. In addition, I will be able to do some simple modifications manually, regardless of the size of the code.
Hi guys, I was thinking lots about the strategy for Milestone 3, and here's what's in my head at the moment.
First, there's the Minimal Djed paper, which describes the state machine underpinning Minimal Djed and comes with machine-checked proofs of the desired stability properties.
The fact that the proofs are machine-checked might give us some leeway, in that we could separate:
The reason I am thinking in this way is because the state-machine proofs should be structural in nature and not very difficult (my intuition is that the complexity of the compiled uplc code will be the only proper bottleneck), whereas the stability proofs are mathematical and complex, done semi-automatically in Isabelle, using several powerful decision procedures it has built in, and I am not sure how well this will translate to the automated setting of K and Z3. We can paralellize the effort here possibly, by, on the one hand, assuming the correctness of the transition system and then trying to push for the stability properties, while, on the other hand, doing the actual proofs for the assumed claims.
Next, I think it's essential to immediately understand in detail, guided by Jean-Frédéric, the structure of the source-language code, and in particular how the state is represented and which function corresponds to which operation in the protocol. We should be able to quickly confirm that the state transition system is as expected.
When it comes to verification, we will have code at three levels---source-language,
pir, anduplc---and will need to think about datatypes, functions, and specifications across these levels. I think the main challenge there lies with the datatypes, because once we have them sorted, we can use them to write function specifications. I think thepirlevel will be mostly informative rather than requiring infrastructure. I've laid out some ideas about what this infrastructure would consist of in #269, with the current main challenge being parametric and inductive datatypes (such as tuples, lists, and maps) coming from source-language code.We will also need the
pyklibrary to automatically extract some of the global environment, ideally. In particular, we will certainly need some sort of a mass find/replace on identifiers, removing some de-Bruijn-like suffixes and possibly adding prefixes so that they can be parsed bykplc. Some of the auto-generatable patterns are given in #269, and there is some information there that I need to update. In addition, I will be able to do some simple modifications manually, regardless of the size of the code.