std4#748 unbundle array size constraint from hash map bucket

Stream: PR reviews

[Markus Himmel]

@Mario Carneiro Just to make sure I understand your suggestion correctly: adopting your proposal would mean that all operations on HashMap.Imp take a proof of HashMap.Imp.WF as an argument, right?

[Mario Carneiro]

oh whoops I forgot we had such a tier of functions. These should just take 0 < buckets.size as an argument, not the full WF (at least, this is what will minimize the proof burden on direct uses of the Imp functions, in addition to being the same as the current code up to tupling order so lemmas will be mostly unaffected)

[Mario Carneiro]

this should probably be done via an ad hoc subtype

[Mario Carneiro]

because we want the condition to stay as an "intrinsic verification" proof

[Mario Carneiro]

e.g.

def expand [Hashable α] (size : Nat) (buckets : Buckets α β) :
    {m : Imp α β // 0 < m.buckets.size} :=

[Markus Himmel]

Alright, thanks, I'll try that and see how it works out.

[Markus Himmel]

@Mario Carneiro okay, I tested this out for a bit in std4#754, but I haven't really gotten it to work. There is now a lot of unpacking and repacking in the definitions of the operations, and this makes fixing the proofs quite tedious. Is what I did what you had in mind or were you thinking of a different/better approach? So far, I don't think that the new approach is simpler or produces a smaller diff than the previous one. I also don't love that working with HashMap.Imp always requires passing proofs around now, I think it would be nice to defer that to the rest of the verification work.

[Mario Carneiro]

I'll take a more detailed look after the meeting. I agree that it's not great to be packing and unpacking, I preferred the original version, but I understand the motivation for pursuing this. Attempt 1 had runtime overhead, which I think is not a worthwhile tradeoff for accomodating this nested-inductive-safe property

[Markus Himmel]

Is there any runtime overhead in addition to the array size check? I could try to take some measurements to see how large the impact of this is. Would you be otherwise happy with the change if it turned out that the impact is very small?

[Mario Carneiro]

I pushed some more changes to https://github.com/leanprover/std4/compare/mario/hashmap-positivity-2 . My impression is that it will be better if the conversion from Imp and Buckets is hidden even further, with simp lemmas such that one can treat Imp as having Buckets as a member

[Mario Carneiro]

Another proposal: we take the type currently written {m : Imp α β // 0 < m.2.size} and rename it to Imp α β, and rename Imp α β to Raw α β

[Mario Carneiro]

yes, this is working a lot better than my previous suggestion @Markus Himmel . The main thing that gets in the way is if the functions start with a pattern match like

  let ⟨⟨size, bucketArray⟩, hm⟩ := self
  let buckets : Buckets α β := ⟨bucketArray, hm⟩

If it is instead

  let size := m.1.1
  let buckets := m.buckets

(which should be the same from the compiler's perspective), then simp works much more closely to the previous version