Skip to content

Commit

Permalink
Avoid bottomify-ing higher order functions
Browse files Browse the repository at this point in the history
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 `value`s 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).
  • Loading branch information
JasonGross committed Dec 4, 2023
1 parent 1eacb1e commit 46fdfb6
Show file tree
Hide file tree
Showing 5 changed files with 1,128 additions and 829 deletions.
Loading

0 comments on commit 46fdfb6

Please sign in to comment.