hacspec / hax

A Rust verification tool
https://hacspec.org/blog
Apache License 2.0
195 stars 20 forks source link

Raw view on `concrete_ident` #793

Open paulmure opened 3 months ago

paulmure commented 3 months ago

Currently, concrete_ident is exported to engines as an opaque type. To get its underlying content, one would need to make a VIEW_API which transform the underlying path and definition into a view.

While the VIEW_API can accept options such as a NAME_POLICY, it seems intractable to have an API that is flexible to accommodate all possible name transformation schemes. For example, there is currently no way to configure the prefix scheme built-in to the default view api.

It seems appropriate to just export the raw underlying content without any transformations, giving each engine the option to have full control over how to translate concrete_idents.

github-actions[bot] commented 1 month ago

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

franziskuskiefer commented 1 month ago

@W95Psp @paulmure what's the state here? It looks to me like the PR only needs a review?

paulmure commented 1 month ago

Yes, I think the PR just needs a review.

W95Psp commented 1 month ago

Hi @paulmure, I've been trying to review a few times, but each time I end up wondering if that's the right thing to do.

I agree with you, the view API is restrictive: it imposes a common view on naming for every backend. But I suspect most of the backend will have the same needs. I don't want the backends to re-implement, over and over, name translation.

Could you give me some examples of a custom naming scheme you would like to have, and that would be too specific to your use case to be mainlined? Clearly, for something like prefixes, we could make it parametric (as you say)

paulmure commented 1 month ago

Controlling the prefix is definitely a priority right now. But we think it would also be useful to control how much of the fully qualified path is used based on what’s currently imported. But this may be easily implemented by allowing the view API to export a list of path items.

The reason why I suggested exporting the entire type is because it seems like this sort of fine-grained tweaking can easily lead to a messy and unprincipled view API. But there’s definitely a lot of room for design choices and I’m not entirely certain what’s the best solution here.

W95Psp commented 1 month ago

Yeah. I see what you mean. Indeed, we may end up with a messy and complicated API...

The implementation itself is already quite messy and complicated, actually 😅 I would like to revisit it at some point...

I think we should maybe brainstorm and figure out what kind of naming transformations one could want, and then decide whether a unified API is possible. I wonder what would be the best way of doing that: maybe a GH discussion?

I think a unified API & unified transformation "engine" would be great. Having a declarative description of what a specific backend needs in terms of naming scheme, and then invoking the name transformation mechanism seems the right think to do to me. The concrete_ident module has invariants, and it's easy to break them, so doing something uniformly would be great.