Synthetic Way and Analytic Way
The most of us, including other formal verification project researchers, are relying on the “analytic” way of program verification. That is, program first, verification later. However, using such way means we write a program in a certain language and after that we verify the program satisfying the specification we want; the programming language has no restriction about their programs that can occur with respect to the specification. On the other hand, in using “synthetic” languages such as Coq, we specify the specification precisely and first. Thanking that there is Generalization of Curry-Howard Correspondence, program can be generated if and only if we proved that the program specification is right.
Here we saw two opposite ways of program verification, analytic v.s. synthetic.
I would not mention which is better because the both ways have each weak points.
e.g. synthetic way always can have trivial program. (Even if we write specifications S_1, ... S_n , and if we forget to add a specification S_{n+1} which we need, we can always have the trivial synthetic program. And, the proving technique in synthetic language such as Coq is sometimes much harder than formal verification of program analysis using approximation. )
Guard Condition
Concerning Pen Compiler, currently we have defined Syntax Tree, its Program Graph, and the representation matrix, that is, we have been developing the analytic side.
Particularly, concerning Program Graph, we did not decide how to handle loops in the graph.
One of the analytic way of loop verification is “invariant analyisis” which is studied in the theory of Hoare Logic. However, invariant analysis needs that we have to specify what the invariant is and it might be difficult to find it in cases. Then how to handle loops? For the question, we would like to apply synthetic way to pen compiler. It’s called “guard condition”.
Guard condition asserts that the loop branch condition has inductive data structure and each time we reach the condition, we have to shrink the structure, and it must shrink to just a “point structure”, breaking the loop.
For example, Coq compiler uses the guard condition in order that it assures that programs in Coq stops, and it is statically analyzed.
Many compilers, such as solidity, use Integer, but we might not need it.
Rather, we have Natural Numbers( , positive numbers, and integers as in Coq style).
Negative numbers can be represented by natural numbers in double-entry bookkeeping.
We might not need integers in formal ways.
We sometimes say loop branch condition is “noetherian” if it satisfies the guard condition, since the condition sequence is descending and has the end, as descending sequences in algebraic geometry is noetherian if it has the end point named from a great mathematician “Emmy Noether”.
Formal Opcodes
In such assumptions, we cannot use EVM’s ADD Opcode directory in adding two numbers since ADD works exactly as defined in EVM.
We have inductive data structures and we have to embed them into EVM. Since embedded EVM code works and it is called in EVM, static checking does not mean even if we check the code carefully in compile time. So, in embedding data structure, we have to define Formal Addition FADD to be addition with boundary condition check, FMUL to be multiplication with boundary condition check, and so on. Of course, the gas prices of the Formal Opcodes should be cheap.