leanprover
Verifying gcm_init_v8 -- a proof strategy
Description:
Currently, LNSym could not handle gcm_init_v8 fully expanded out and solved by bv_decide. Simply expand out the definitions (even with pmult uninterpreted) will result in stack overflow from Lean.
In this PR, instead of brute-force expansion, we conduct the proof in controlled steps. We first simulate for 17 steps to get the expression for H0 and verify that the value stored in v20 (H0) is equivalent to the spec, we insert a hypothesis (h_H0) into the precedents. Then we simulate for another 22 steps to get H1, H2 and H3, and likewise insert hypothesis (h_H1, h_H2, and h_H3) that represents their equivalence into the hypotheses. When conducting the proof in the second step, we only expand expression until it reaches the value stored in v20 (H0), as a result, controlling the size of the term to be small. We do this for the rest of the elements in the Htable.
This proof depends on a key result gcm_polyval_asm_gcm_polyval_equiv which states the equivalence between the gcm polyval operation implemented in the assembly is equivalent to the gcm polyval operation in the specification. This is a non-trivial proof and currently could not be proved. One possibility is to try the RME decision procedure implemented in the SAW proofs [1][2].
Testing:
What tests have been run? Did make all succeed for your changes? Was
conformance testing successful on an Aarch64 machine?
License:
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.
