Make `MapBot` total again

The following are excerpts from a Slack conversation. The goal is to fix MapBot such that it normalizes itself to not contain bottom values (and have all its operations behave right w.r.t that). This requires fixing some usages of MapBot (like base's CPA) which currently abuse the map's keyset (e.g. using mem, fold, iter, etc).

The same applies to MapTop.

Here's a fun little puzzle in fundamental lattice theory:
Consider our MapBot domain, which return default bot values of the inner lattice for missing keys. And consider a = {k -> bot} and b = {} (empty map) as elements of MapBot.
For all keys k' we have find k' a = find k' b due to the default bot behavior. So they're observably the same map (functional extensionality).
Should a leq b be true or false?

Goblint says false because of the following code: https://github.com/goblint/analyzer/blob/cbd7987327def50883abbe07fde03f08bc8776be/src/domains/mapDomain.ml#L363-L372

Since k is not in b and the default-bottoming find is not yet defined (the standard Map.find is used), Not_found is raised and the result is false.
On the other hand, they're observably the same map, so reflexivity should hold.

An even more basic puzzle: should a equal b be true or false?
Again, Goblint says false because it uses the standard Map.equal which says false due to differing key sets.

The consequence of it is that if you put such maps into the context, then they're considered different, despite functionally being the same. This doubles the number of contexts per each key where this may happen.
Same goes for keeping such maps inside sets.

Yet another puzzle about these maps: for all maps m and keys k, is add k (find k m) m equal to m?
If you do this for b and k from above, you get a since it makes the previously implicit default value explicit. But should it?

This isn't hypothetical, but actually happens inside Goblint.

I think it boils down to what mathematical structure MapBot is supposed to be, because there are two incompatible concepts:
Partial maps, which carry their domain set (which is what OCaml's Map does) and have their equality/leq also depend on the compatibility of each of their domains. But if this were so, find should never return default bottoms, because they're outside the mathematical domain of the partial map. So pretending to have gotten a value from a non-existent key is nonsense.
Total maps, which are defined for their entire key type (i.e. never raise Not_found) but are only non-bottom at finitely many keys (something like being finitely-generated). These would have the default bottom behavior for find and since they're total, their equality/leq doesn't care for which keys it's defined (in the implementation with Map) since mathematically it's defined everywhere and in case of missing keys in the implementation, the default bottoms should always be considered.