Add cv compute support for string-keyed finite maps

[xrchz]

cv compute currently has excellent support for num-keyed finite maps via sptrees (cv_stdScript.sml:432-495), with operations like FEMPTY, FLOOKUP, FUPDATE, and DOMSUB translated to efficient cv_insert/cv_lookup/cv_delete operations.

However, there is no corresponding support for string-keyed finite maps (:string |-> 'a). This would be useful for applications that naturally use string keys (e.g., symbol tables, environments in language semantics, configuration maps).

Current infrastructure that might help:

• from_char/to_char exist (cv_typeScript.sml), so strings (char list) can be represented
• alist_tree provides generic sorted association list operations with any ordered key type

Possible approaches:

1. Trie/Patricia trie for strings: Most efficient for lookup, but would need new theory and cv translations
2. Sorted association lists: Could leverage alist_tree machinery with string comparison; less efficient than tries but simpler to implement
3. Encode strings as numbers: Use existing sptree infrastructure with some bijection (like treating strings as base-256 numbers); may be inefficient for long strings

Use case: The vyper-hol project currently uses the string-to-number encoding workaround to work with cv compute. Native string-keyed finite map support would provide a cleaner and potentially more efficient solution.

---

🤖 Generated with Claude Code

[myreen]

I have plans to do this in the short term (next few weeks). If you also plan to do it then we should coordinate.