Opaquify proofs in gmap_partial_alter (fix #46)

• Ensure gmap well-formedness proofs are fully opaque.
• Use pattern-matching lambdas over lets.

Interesting catch. By not having this stuff opaque, what's the complexity of the original def?

Thanks! Good question and not sure, that depends on the exact strategy. But if there's no laziness involved, the proofs should still be computed, leading to a quadratic cost.

Indeed, in #46, the cost seems superlinear in the the map element count after the fix and in both maps. OTOH, the keys are also increasing, which means maybe I shouldn't expect cost to be linear (or even n log n); element size matters.

• To confirm the superlinear/almost quadratic cost, take the test case in #46 and increase the size to 10^4, 2*10^4, 4*10^4. With sizes big enough to ignore the fixed costs, the runtime multiple by > 3x for each size doubling. E.g. for Pmap (gmap gives similar results):

Finished transaction in 0.836 secs (0.561u,0.069s) (successful)
Finished transaction in 2.264 secs (1.935u,0.118s) (successful)
Finished transaction in 6.829 secs (6.351u,0.134s) (successful)
Finished transaction in 24.931 secs (24.432u,0.193s) (successful)

added 1 commit

• 09f990d3 - Opaquify proofs in gmap_partial_alter (fix #46)

Compare with previous version

changed the description

unmarked as a Work In Progress

changed title from Opaquify proofs in gmap_partial_alter (wip for #46) to Opaquify proofs in gmap_partial_alter (fix #46)

added 1 commit

• e7f5ec01 - Opaquify proofs in gmap_partial_alter (fix #46)

Compare with previous version

added 1 commit

• f92b4c3c - Opaquify proofs in gmap_partial_alter (fix #46)

Compare with previous version

added 1 commit

• e28df8ac - Opaquify proofs in gmap_partial_alter (fix #46)

Compare with previous version

resolved all threads

mentioned in commit 2b916512

merged

LGTM. Thanks.

mentioned in issue #64