FloVer issueshttps://gitlab.mpi-sws.org/AVA/FloVer/-/issues2019-04-11T06:20:10Zhttps://gitlab.mpi-sws.org/AVA/FloVer/-/issues/4Unify command and expr levels into single expression datatype2019-04-11T06:20:10ZHeiko BeckerUnify command and expr levels into single expression datatypehttps://gitlab.mpi-sws.org/AVA/FloVer/-/issues/13Add documentation to affine arithmetic invariants2019-03-27T15:17:40ZHeiko BeckerAdd documentation to affine arithmetic invariantsThe 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 explan...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...)Heiko BeckerHeiko Beckerhttps://gitlab.mpi-sws.org/AVA/FloVer/-/issues/12FMA semantics are wrong2019-03-20T15:12:17ZHeiko BeckerFMA semantics are wrongAs is FMA (a,b,c) = a + (b * c) which ideally should be FMA (a,b,c) = a * b + c for now this can be fixed by flipping arguments when generating certificates, but there should be a cleaner solution, that changes the semantics on the FloV...As is FMA (a,b,c) = a + (b * c) which ideally should be FMA (a,b,c) = a * b + c for now this can be fixed by flipping arguments when generating certificates, but there should be a cleaner solution, that changes the semantics on the FloVer sidehttps://gitlab.mpi-sws.org/AVA/FloVer/-/issues/6Reenable regression tests in CI2018-09-12T13:40:38ZHeiko BeckerReenable regression tests in CIThis requires properly setting up a cache for HOL4 and the CakeML binary.This requires properly setting up a cache for HOL4 and the CakeML binary.https://gitlab.mpi-sws.org/AVA/FloVer/-/issues/7Implement a new type validator2018-08-22T10:13:04ZHeiko BeckerImplement a new type validatorAs is, there are two functions running, that should be merged into one.
The idea is as follows:
Given a partial map, we build a function that checks anything in the partial map to be the correct type and updates the map with mappings fo...As is, there are two functions running, that should be merged into one.
The idea is as follows:
Given a partial map, we build a function that checks anything in the partial map to be the correct type and updates the map with mappings for every unbound expression.
This should also *redo the fixed-point typing* as this will allow to add the fractional bits to the type map.Heiko BeckerHeiko Beckerhttps://gitlab.mpi-sws.org/AVA/FloVer/-/issues/8Make the HOL4 development compile with the latest version of CakeML/HOL42018-07-17T11:21:15ZHeiko BeckerMake the HOL4 development compile with the latest version of CakeML/HOL4HOL4 has had some changes to `drule` so the proofs need to be updatedHOL4 has had some changes to `drule` so the proofs need to be updatedhttps://gitlab.mpi-sws.org/AVA/FloVer/-/issues/3Support checking of fixed-point programs2018-04-27T09:22:57ZHeiko BeckerSupport checking of fixed-point programs