Draft: use SProp for well-formedness condition in Pmap and gmap

Proof of concept for #85. I'm not sure the reduction behavior is actually what we want, but I was able to get a lookup on a concrete map to reduce using only simpl (ordinarily you can get this to work with vm_compute, which breaks the opacity of proofs).

Interesting! I'll review this properly later.

In order to see if we have the right reduction behavior, it might be worth to have some tests where we insert n elements into a map and perform n lookups, and check that this indeed appears to take O(n log n) time.

When doing such tests, it would also be interesting to see the times for vm_compute, compute, cbv, and lazy.

Another fun one, insert the sequence 0..n into an empty map, insert the sequence n..0 into an empty map, and then try to prove an equality between the two resulting maps using reflexivity. That should be O(n log n) for the insertions, and O(n) for the equality checking.

added 1 commit

• 1590e131 - Add a complexity test

Compare with previous version

@tchajed @robbertkrebbers it has been a while since we saw any activity in this MR. Do either of you have plans to further work on this? Looks to me like it is currently waiting for a more in-depth review, so marking as such.

added S-waiting-for-review label

mentioned in merge request !266 (merged)

I finally had time to take a proper look at this. I have done a couple of things, which can be found at https://gitlab.mpi-sws.org/iris/stdpp/-/tree/tchajed/stdpp-sprop-gmap

• I noticed that the complexity of the map operations was no longer O(log-n). The problem is that each time you call an operation like partial_alter it would reestablish that Pmap_wf holds, giving rise to O(n), complexity due to the check. Why this happened was very subtle. You use functions like is_true_bind to construct the wf proof. These functions have the Boolean as an implicit argument, and hence vm_compute evaluates it eagerly. Instead, in my branch, I state lemmas like Ppartial_alter_wf using an explicit SIs_true, making sure that the proof is properly opaque.
• Since the above problem, I removed the bindand fmap combinators.
• I ported coPset and Qp to use SProp. The change for Qp is rather invasive, but it does not change the API.

What's the easiest way to proceed? Can you give me push access to this MR?

I gave you push access. :)

But honestly it might be easier if you just open a new MR?

Another option: We consider the general SProp setup and the changes to pmap/gmap here, and after we're settled with that, I make MRs for coPset and Qp.

Let's see what @tchajed thinks.

I've had a quick look at https://gitlab.mpi-sws.org/iris/stdpp/-/tree/tchajed/stdpp-sprop-gmap and found the following problems when using Coq 8.10.2:

• I need to add Global Set Allow StrictProp. in sprop.v
• The new tests fail as simpl does not seem to do anything. I.e. the first Show. prints {[3 := false; 2 := true]} = {[2 := true; 3 := false]} and the second Show. prints {[3 := false; 2 := true]} !! 2 = Some true.

I need to add Global Set Allow StrictProp. in sprop.v

Ah, they seem to have changed that default? In 8.13 it seems to be enabled by default. I guess we can add that so as to make 8.10 happy too.

The new tests fail as simpl does not seem to do anything.

I am afraid that there's nothing to do about that. There's two problems:

• There's no way of telling simpl that it should only reduce a gmap whenever its entirely concrete. You surely don't want simpl to reduce anything involving variables. For example, {[ 1 := 1; 2 := 2 ]} ∪ m is not going to anything meaningful.
• The simpl tactic will not turn complex_sprop_proof : SUnit into just stt : SUnit. So even if we were to enable simpl for the gmap operations, you end up with large proofs in the end (unless you project out). The alternative is to make the proofs transparent, but that destroys the log-n complexity of the map operations.

I am confused about the tests that use simpl. Do the tests pass with Coq 8.13? Because the ref file seems to assume that simpl does something, but now you seem to be saying that simpl should not do anything.

Tej had such tests in this MR, but he a.) explicitly changed Arguments to make simpl work on just the tests (an option that we surely do not want to set globally), and b.) made proofs transparent. Such tests are not in my branch.

What about https://gitlab.mpi-sws.org/iris/stdpp/-/blob/tchajed/stdpp-sprop-gmap/tests/gmap.v#L56 and https://gitlab.mpi-sws.org/iris/stdpp/-/blob/tchajed/stdpp-sprop-gmap/tests/gmap.v#L56? Or am I looking at the wrong branch?

Looks like I forgot to update the .ref files... Sorry about that.

I updated the branch.

I see. So do I understand correctly that the main benefit of this branch is that vm_compute now has O(log n) performance for computing lookups (and reflexivity is probably also faster)?

Yes.

Ok, makes sense. When this branch is updated to the current stdpp master, I can try it on RefinedC and see how much of a performance win it would be there.

I rebased on stdpp/master when updating the .ref file.

Great Then I will try this on RefinedC.

It seems like this branch breaks Iris: https://gitlab.mpi-sws.org/iris/refinedc/-/jobs/137510

[ERROR] The compilation of coq-iris failed at "/builds/iris/refinedc/_opam/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-iris.dev.2021-07-26.8.eb05e835/./make-package iris -j2".
#=== ERROR while compiling coq-iris.dev.2021-07-26.8.eb05e835 =================#
# context              2.0.8 | linux/x86_64 | ocaml-base-compiler.4.07.1 | git+https://gitlab.mpi-sws.org/iris/opam.git
# path                 /builds/iris/refinedc/_opam/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-iris.dev.2021-07-26.8.eb05e835
# command              /builds/iris/refinedc/_opam/ocaml-base-compiler.4.07.1/.opam-switch/build/coq-iris.dev.2021-07-26.8.eb05e835/./make-package iris -j2
# exit-code            2
# env-file             /builds/iris/refinedc/_opam/log/coq-iris-405-736596.env
# output-file          /builds/iris/refinedc/_opam/log/coq-iris-405-736596.out
### output ###
# [...]
# invGS0 : invGS Σ
# na_invG0 : na_invG Σ
# p : na_inv_pool_name
# E : coPset
# The term "E" has type "coPset" while it is expected to have type
#  "coPset_raw".

Great, we suffer once again from Coq's poor namespacing

Constructor stdpp.coPset.CoPset
Constructor iris.algebra.coPset.CoPset

If only we could make the constructor in stdpp private.

Instead, I am afraid we need to come up with some silly dummy name for the constructor in stdpp.

I don't think I understand why std++'s CoPset is preferred over Iris's in that file...

Which file is that failure in?

EDIT: Ah, na_invariants.v.

The algebra version has precedence up until From iris.base_logic.lib Require Export invariants..

That invariants file does

From stdpp Require Export namespaces.

which means when importing it, the std++ CoPset takes precedence.

This is exactly why using Export is bad. (But I know the alternatives are bad, too, in different ways.)

We could add From iris.algebra Export coPset to invariants?

Alternatively, we could just use a different constructor name in std++ since it's an internal thing anyway.

What do you prefer?

We could add From iris.algebra Export coPset to invariants?

We'd have to do that everywhere we Export stdpp.namespaces.

Alternatively, we could just use a different constructor name in std++ since it's an internal thing anyway.

This seems more robust.

I added an _.

@msammler Iris compiles against this branch now.

I spoke too soon:

--- tests/one_shot.ref	2021-06-14 15:59:07.869410384 +0200
+++ /tmp/tmp.1Ggvh5kuCz	2021-07-27 15:12:22.573606962 +0200
@@ -40,4 +40,5 @@
                     | InjR "m" => assert: #m = "m"
                     end {{ _, True }}
   
-Closed under the global context
+Axioms:
+sUnit relies on definitional UIP.

Ah... so now we need to decide if we are okay with that axiom?

It's not really an axiom, is it?

Coqchk calls it an axiom I don't know the situation around SProp-UIP. (What is the "S" for again anyway?)

"s" = strict

This doc sounds to me like that axiom is unsound? Or how else should I interpret "The special reduction rule of UIP combined with an impredicative sort breaks termination of reduction"?

mentioned in commit refinedc@82c8290f

mentioned in commit refinedc@1f49292f

@robbertkrebbers I'd be happy if you took this over! I had fun figuring out the initial implementation but I think this feature is a bit too subtle for me at the moment. Once I've seen a productive SProp use case then I'll be more sold but for now I don't really get it.

I'd be happy if you took this over!

Ok, great.

Once I've seen a productive SProp use case then I'll be more sold but for now I don't really get it.

I am not sure what you mean here, or what you don't get?

What does using SProp solve here? Does it help to avoid spending time reducing proofs? Or is it just a systematic way to definitional equality? How does this strategy compare to manually proving uniqueness of these canonicity proofs (assuming that even holds in this case)?

It ensures that more equalities hold definitionally, and can thus be proved by reflexivity or even by conversion as part of unification.

For example 1/4 + 3/4 = 1, or {[ 1 := 1; 2 := 2 ]} = {[ 2 := 2; 1 := 1 ]}, or {[ 1 ]} ∖ {[ 1 ]} = ∅ can be proved using a mere reflexivity with this MR. Also, if you have a goal that involves, say 1/4 + 3/4, then you can just apply a lemma involving 1 because both are convertible.

mentioned in merge request !309 (merged)

Closing in favor of !309 (merged)

closed