Add documentation to affine arithmetic invariants
The affine arithmetic error validator soundness statement is very complicated and undocumented.
Each separate assumption/invariant in https://gitlab.mpi-sws.org/AVA/FloVer/blob/master/coq/ErrorValidationAA.v#L780 should have some explanation what it expresses.
Ideally the checked_expressions
predicate should also have some docstring explaining its purpose. Currently it looks like the setup causes duplication of proofs (see https://gitlab.mpi-sws.org/AVA/FloVer/blob/master/coq/ErrorValidationAA.v#L1442 and https://gitlab.mpi-sws.org/AVA/FloVer/blob/master/coq/ErrorValidationAA.v#L1482 where the second is a subproof of the first...)