FloVer issueshttps://gitlab.mpi-sws.org/AVA/FloVer/-/issues2018-03-07T09:44:28Zhttps://gitlab.mpi-sws.org/AVA/FloVer/-/issues/2Unify input for both in-logic scripts and binaries to be custom, parsed strings2018-03-07T09:44:28ZHeiko BeckerUnify input for both in-logic scripts and binaries to be custom, parsed stringsThis will allow to develop more elaborate checkers, that could compute information if it is not present in the certificate, for example a user might only specify roundoff errors and consequently we would need to compute the ranges dynami...This will allow to develop more elaborate checkers, that could compute information if it is not present in the certificate, for example a user might only specify roundoff errors and consequently we would need to compute the ranges dynamically.https://gitlab.mpi-sws.org/AVA/FloVer/-/issues/3Support checking of fixed-point programs2018-04-27T09:22:57ZHeiko BeckerSupport checking of fixed-point programshttps://gitlab.mpi-sws.org/AVA/FloVer/-/issues/9Port functions reasoning about options in HOL4 to monad_syntax2018-07-12T08:39:59ZHeiko BeckerPort functions reasoning about options in HOL4 to monad_syntaxhttps://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/1Add verbose versions of validator functions2018-07-17T11:26:05ZHeiko BeckerAdd verbose versions of validator functionsAll of the implemented validator functions current return a result of type `:bool`. For debugging failed certificates, it would be handy to have a verbose version of each validator which returns an option containing the failed expression...All of the implemented validator functions current return a result of type `:bool`. For debugging failed certificates, it would be handy to have a verbose version of each validator which returns an option containing the failed expression if any or `None` otherwise.https://gitlab.mpi-sws.org/AVA/FloVer/-/issues/11Implement interval validation with memorization2018-08-17T13:46:01ZHeiko BeckerImplement interval validation with memorizationImplementing `validIntervalbounds` similar to `validAffineBounds` and `getValidMap` allows to return an interval map and use accumulators to speed up computations. It further allows to implement Interval Subdivision as a range analysis.Implementing `validIntervalbounds` similar to `validAffineBounds` and `getValidMap` allows to return an interval map and use accumulators to speed up computations. It further allows to implement Interval Subdivision as a range analysis.https://gitlab.mpi-sws.org/AVA/FloVer/-/issues/10Look into using Taylor polynomials for transcendental functions2018-08-22T10:13:04ZHeiko BeckerLook into using Taylor polynomials for transcendental functionsThe multivariate case seems interesting.
If we implement them it would also be interesting if we could make them parametric in the degree of approximation (i.e. `n` for an `n`-th order taylor polynomial)The multivariate case seems interesting.
If we implement them it would also be interesting if we could make them parametric in the degree of approximation (i.e. `n` for an `n`-th order taylor polynomial)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/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/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/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/4Unify command and expr levels into single expression datatype2019-04-11T06:20:10ZHeiko BeckerUnify command and expr levels into single expression datatype