Skip to content

Latest commit

 

History

History
249 lines (183 loc) · 7.81 KB

TODO.org

File metadata and controls

249 lines (183 loc) · 7.81 KB

Summarise bugs, features to add, etc. here, in addition to littering the source with “XXX” comments.

Bugs

multiple contracts on the same function are translated incorrectly

If

f ::: c1

and

f ::: c2

in the source, then the generated theory is

T /\ ~(f:::c1) /\ ~(f:::c2)

when it should be

T /\ ~(f:::c1&&c2),

i.e.

T \ (~(f:::c1) \ ~(f:::c2)).

NB: the generated theory is unsat when either of c1 or c2 hold, which is very wrong!

Features

[1/4] command line switches to control theory parameters

  • [X] whether or not ‘min’s are generated at all.
  • [ ] placement of various “design decision” ‘min’s.
    • [ ] leading ‘min’s on arrows
    • [ ] leading ‘min’s on negative CFs
  • [ ] what kind of definition-by-cases translation is used

    there are at least two styles

    1. [(e = BAD) \/ (\/_i exists xs_i . e = K_i xs_i) \/ (f e = UNR)] \ (\_i forall xs_i . e = K_i xs_i -> f(e) = e_i) /\ (e = BAD -> f e = BAD)
    2. (e = BAD/\ f e = BAD) \/ (\/_i exists xs_i . e = K_i xs_i/\ f(e) = e_i) \/ (e = BAD /\ (\_i forall xs_i . e /= K_i xs_i) /\ f e = UNR)

    and either of those can also use projectors instead of quantifiers. e.g. (2) becomes

    2’. (e = BAD/\ f e = BAD) \/ (\/_i e = K_i (pi_1 e) … (pia_i e)/\ f(e) = e_i) \/ (e = BAD /\ (\_i e /= K_i (pi_1 e) … (pia_i e)) /\ f e = UNR)

    fewer quantifiers seems good, but i need to experiment to see if there is an improvement in practice.

    UPDATE: equinox 5 does not do well with 2’, but equinox 6 is ok. see 911ac185bb45a1a4d3754262bd8d9d8531daa4f3 in haskellcontracts.git

  • [ ] whether the ‘forall a. a = …’ versions are used.

move ‘Bool’ into a library

the translation of ‘Bool’ is hardcoded in the translation, but we could have lib/bool.hs and then tests could ‘import “../lib/bool.hs”’.

restrict generated theory to relevant defs

right now we insert more defs than neccessary when generating the theory, which slows things down significantly in some cases. something like a transitive free variable check should be sufficient.

better test suite

borrow IsaPlanner examples from Zeno directly, or from the IsaPlanner site. the urls are in the zeno tech report:

remove the “only allow top level case expressions” restriction

we can provide this as a source to source translation if necessary, but it’s annoying when creating examples. it’s not hard to translate nested cases. i.e., currently we translate (approximate, ignoring Min’s)

[[ f xs = case e of [pi -> ei] ]]

==>

(e = BAD \/ (\/_i e = pi) \/ f xs = UNR) /\ (e = BAD -> f xs = BAD) \ (\_i (e = pi -> f xs = ei))

but if nested case were allowed we’d simply need to change the (e = pi -> f xs = ei) part to

[[ f xs = ei ]]

when ei = case e’ of [pi’ -> ei’].

use haskell syntax

zeno does this, and it seems like a good idea. we only require a few changes:

  1. use real imports
  2. move contracts into comments
  3. declare data types properly, i.e. give arguments instead of arities.

this has an immediate benefit: we can use haskell to type check our examples. it also means we’re closer to feeding our examples to zeno or lazy quickcheck or … i.e., more tool support.

decide how to best support ‘min(K(x1,…,xn)) -> min(x1) /\ … /\ min(xn)’

update: the motivation below is still correct, but the solutions below are dumb. a better solution is to add

[[K_i ::: CF^a_i -> CF]]-
forall xs. CF(K xs) -> forall x: CF(x)

instead of the current phi_cf. We don’t have a principled argument for the second axiom above, but the first gives K_i a contract in a principled way, and it works because of how arrow axioms are translated. For example, consider Succ:

[[Succ ::: CF^1 -> CF]]- ==> forall x. min(Succ x) -> (min(x) -> CF(x)) -> CF(Succ x)

So, we get to assume min(x) when proving CF(x), which is what we needed for x = add_R(A’,B) below.

see file:./egs/yes/add-is-cf-to-cf-to-cf.hs for an example. The proof gets stuck in the A = Succ(Succ_1(A)) branch where the result is Succ(add_R(Succ_1(A),B)). The problem is that we need min(add_R(Succ_1(A),B)) to conclude cf(add_R(Succ_1(A),B)).

The easiest solution is too add

forall f,x. min(f x) -> min(f) /\ min(x)

But this might generate more ‘min’s than we’d like. Intuitively, we only need this propagation of ‘min’s into arguments for term constructors, since the equations defining functions propagate ‘min’s to the scrutinised parts already. So, we could add

forall x1,…,xn. min(K(x1,…,xn)) -> min(x1) /\ … /\ min(xn)

for each term constructor ‘K’.

Another, more flexible solution, could be to introduce a “deep” ‘min’, s.t.

forall x. deepmin(x) -> min(x) forall f,x. deepmin(f x) -> deepmin(f) /\ deepmin(x)

and then maybe

forall x1,…,xn. min(K(x1,…,xn)) -> deepmin(K(x1,…,xn))

or maybe some other, more specific, ways to introduce ‘deepmin’.

implement new phi_cf

support ‘import’s in example files

there is a lot of code duplication across examples.

prettier arrow contracts

it’s annoying and ugly to write

x:{x:p} -> c

so, introduce a source level translation

{x:p} -> c ==> x:{x:p} -> c

or, maybe better to change {x:p} to x:{p}, and then

x:x:{p} -> c ==> x:{p} -> c

This is better in the case of compound contracts, e.g.

x:(CF&&{gt x Zero}) -> c

vs

x:(CF&&{x:gt x Zero}) -> c

But what’s the translation here?

comments on generated formulas

e.g.

% phi_lazy <type> <constructor> fof(phi_lazy,axiom,…).

better classifiers on generated formulas

right now we use “axiom” for everything. the goal formula should be a “conjecture”. basically, we want ‘-’ ==> ‘axiom’ and ‘+’ ==> ‘conjecture’.

add support for ‘Any’ contract

the easy way to do this is to parse ‘Any’ to ‘{_:True}’

MAYBE add a typed translation

the zeno paper reports that this improved results in ACL2s. looking at zeno’s ACL2s examples at http://www.doc.ic.ac.uk/~ws506/tryzeno/comparison we see the typing takes the form of predicates and relations between inputs and outputs of functions w.r.t. these predicates. e.g., multiplication gets

(defthm type_mul
  (implies (and (natp x)
                (natp y))
           (natp (z_mul x y)))
  :rule-classes (:type-prescription))

the zeno paper also mentions that encoding datatypes in ACL2s is not ideal. e.g. binary trees (the encoding is ‘tree a = () | (a, (tree a, tree a))

(defun btreep (x)
  (or (= x nil)
      (and (consp x)
           (consp (cdr x))
           (btreep (car (cdr x)))
           (btreep (cdr (cdr x))))))

for us, natp might look like

forall x. x = Z 
       \/ (exists x_ . x = S x_ /\ Nat(x_))
       \/ Undef(x)
       <-> Nat(x)

forall x. x = BAD \/ x = UNR <-> Undef(x)

then, when axiomitizing a function def, we can have

forall x1 ... xn. T1(x1) /\ ... /\ Tn(xn) 
               -> T(f x1 ... xn) /\ <the usual axiomitization>

where f : T1 -> … -> Tn -> T.

add type checking for contracts

they’re in comments and not haskell, so GHC ignores them. one easy way to type check them would be to generate a lambda and typecheck it with ghc. a translation like

[[ x:c -> c' ]] ==> \x -> ([[ c ]], [[ c' ]])
[[ c -> c' ]]   ==> [[ _:c -> c' ]]
[[ c1&&c2 ]] ==> ([[ c1 ]], [[ c2 ]])
[[ c1||c2 ]] ==> ([[ c1 ]], [[ c2 ]])
[[ CF ]]     ==> ()
[[ {x : p } ]] ==> \x . p

might work. so, e.g., we’d have

[[ CF -> {x: nonZero x} -> y:(CF&&{y: p y}) -> {r : q y r} ]]
==>
\_ -> ((),
       \_ -> (\x -> nonZero x,
              \y -> (((),
                      \y -> p y),
                     \r -> q y r)))