Don't replace abstract state of higher order functions with bottom when we can avoid it (now guarded by --fancy-and-powerful-but-exponentially-slow-bounds-analysis)

[JasonGross]

Partial progress towards #1609.

Reworked value type to more closely match the possible spec.

Deduplicated interp_ident / abstract_interp_ident overlapped state.

The specification of reify and reflect has been simplified to more
closely match the intuition: reify's spec no longer talks about output
bounds, only interpretation, and a companion lemma
abstraction_relation_of_related_bounded_value' shows that the spec of
reflect is effectively one direction of an isomorphism between
interpreted-values bounded by abstract state, and values which are in
relationship with the given interpreted-value. Not really sure how best
to describe this in words yet, probably needs some digesting work.

There's some interesting lemmas where we have an equivalency between two
ways of representing things only for up-to-second-order types, and an
implication for up-to-third-order types, which is currently all the
identifiers. But this means that if we add fourth-order identifiers,
we'll have to deal with two different sorts of Proper abstraction
relations (one used by Assembly/Symbolic and one used by bounds
analysis, though it's possible the Assembly/Symbolic one can be
adapted).

Timing info coming soon

Remaining admits:

• wf_interp (this is a big one, but hopefully nothing too surprising)
• always_strip_annotation_related
• interp_eval_with_bound (requires fixing a mismatch between abstraction_relation and type.related_hetero abstraction_relation', maybe some other stuff)
• interp_eta_expand_with_bound
• Interp_EvalWithBound (requires dealing with newly introduced ToFlat / FromFlat round-trip)
• interp_strip_annotations
• Interp_PartialEvaluateWithBounds_bounded
• CheckedPartialEvaluateWithBounds_Correct

Note that, other than the wf_interp lemma, I expect most of these to just be figuring out some gluing.

cc @andres-erbsen

[JasonGross]

I think I found the source of the performance issue.

[JasonGross]

This is one source of bad asymptotics: we run the abstract state twice, both as f sx and as f_e (sx, x). I guess the computation needs to be shared?

[JasonGross]

Possibly the duplication of absf here is bad, not sure

[JasonGross]

Here we interpret the entire state expression at every abstraction node, seems like a likely source of asymptotic blowup.

[JasonGross]

Even more clearly, we interpret the entire remainder of the expression at every let-in. Almost certainly this is giving us asymptotic blowup.

[JasonGross]

@andres-erbsen What do you think of this? 😝

[JasonGross]

I thought #1809 would help but now I'm not so sure.

When I went to apply it to abstract interpretation, I very quickly ran into a problem. I think the essential difficulty can be seen in trying to make a cached version of interp. That is, I want to write a function interp : expr (var:=type.interp) t -> datastructure t such that

1. interp(e) is O(# nodes in e) (linear)
2. there is a function extract : datastructure t -> type.interp t that is O(1) such that extract(interp(e)) == expr.interp e
3. there is a function invertAbs : datastructure (s -> d) -> option (type.interp s -> datastructure d) that is O(1) such that invertAbs(interp(Abs f)) = Some g and forall v, g v = interp (f v)
4. there is an O(1) function invertApp : datastructure d -> option { s : _ & datastructure (s -> d) * datastructure s } such that invertApp(interp(App f x)) = Some (_; (interp(f), interp(x)))
5. there is an O(1) function invertLetIn : datastructure d -> option { s : _ & datastructure s * datastructure d } such that invertLetIn(interp(LetIn x f)) = Some (_; (interp(x), interp(f (extract(interp(x))))))

I think we can do this by routing through de Bruijn indices: we build a flat tree where each node holds the interp of the expr below that point embedded in the context above that point.

And I think once we have this tree-of-interp we can do abstract interpretation without incurring too much overhead (I think we get O(# Abs binders * size of expr), which is quadratic in the worst case but manageable when # Abs binders is less than 10, which I think it is for all of our expressions (notably we aren't quadratic in the number of LetIn binders), though maybe it will still kill us on early abstract interpretation passes)

I guess if we uncurry the surrounding context we don't incur a multiplicative factor of the # abs binders (or, well, we do, but it's not beyond the overhead of using PHOAS in the first place and carrying type annotations at every node)

[JasonGross]

I guess the fundamental problem here is that PHOAS is a semantic encoding of terms, and going from f : A -> B * C to something of type (A -> B) * (A -> C) "without running the code twice" is really a syntactic operation?

[JasonGross]

I guess if we uncurry the surrounding context we don't incur a multiplicative factor of the # abs binders (or, well, we do, but it's not beyond the overhead of using PHOAS in the first place and carrying type annotations at every node)

I guess the way to do this is to have the cache result type depend not just on the type of the PHOAS expression at the current point, but also on the type of the uncurried stack above this point