How to push representation changes through `Let_In`?

[andres-erbsen]

@JasonGross @achlipala: I am failing to derive a version of EdDSA.sign where types of Let-bound variables are changed to an efficient representation.

There seem to be three issues

• The definition of sign is not parametrized over nat, so I cannot do representation changes by plugging in both spec and optimized parameters and proving relatedness as we ended up doing for the field and elliptic curve levels.
• unification fails on pattern fragment modulo beta (https://github.com/mit-plv/fiat-crypto/commit/cfdc4236c19db609a67d816b15cc1480a106974a#diff-5366caedd04016399124d528353b4a5cR258, of course I tried to do this using rewrite first). In particular I cannot rewrite<- with Let_In (f e) C = Let_In e (fun v => C (f v)).
• the return type of sign is determined by combine : forall a, word a -> forall b, word b -> word (a+b), which prevents most tactics from filling in the return type automatically; specifying it manually works but makes tactic code quite verbose.

Unless something comes up from this thread that bypasses all three issues, I will give up on synthesizing the representation change part of optimizing signing, and write and verify the fast version manually.

[JasonGross]

For 1: can we fix this? Parameterize sign?

For 3: that's a hard toe signature to write a Proper instance for. Does it go better if you make combine : forall a b, word a -> word b -> word (a+b)?

I'll think about 2.

[andres-erbsen]

1. We could parametrize sign if we had a specification of the interfaces nat, Z and F q provide, and how they relate to each other. I think this would be a fair bit of work, and while I am optimistic about this strategy in the long run, I don't know whether it would actually pay off here.
2. Yeah, I think you're right. I will try it the next time I work on this.

[JasonGross]

1. What do we actually need here? Is it semiring? Integral_domain?

[JasonGross]

Regarding 2, following a hint from Hugo (private email from earlier today) that this isn't actually the pattern fragment, but an extension of the pattern fragment studied by Tomer Libal and Dale Miller (FSCD 2016), here is code that works (if you make use of this, you'll probably want to rename some things):

        Focus 2.
        Record aggregate_for_unextended_pattern_fragmentR0 {A B} (f : A -> B)
          := { base : A;
               app : B;
               aggregate_for_unextended_pattern_fragment' : f base = app }.
        Arguments aggregate_for_unextended_pattern_fragment' {_ _} f {_}.
        Arguments app {_ _} f _.
        Arguments base {_ _ _} _.
        Lemma aggregate_for_unextended_pattern_fragment {A' B'} (f : A' -> B') (x : A')
          : f x = @app _ _ f {| base := x ; aggregate_for_unextended_pattern_fragment' := eq_refl |}.
        Proof. reflexivity. Defined.
        Definition Let_In_pull_app_nd {A B} (f : A -> B) C (v : A) (g : A -> C)
          : Let_In v g
            = Let_In {| base := v ; app := f v ; aggregate_for_unextended_pattern_fragment' := eq_refl |} (fun v' => g (base v'))
          := eq_refl.
        Definition Let_In_push_app_nd {A B} (f : A -> B) (x : A) (a : B) (pf : f x = a) C (v : A) (g : _ -> C)
          : Let_In {| base := x ; app := a ; aggregate_for_unextended_pattern_fragment' := pf |} g
            = Let_In pf (Let_In a (fun a' pf' => g {| base := x ; app := a' ; aggregate_for_unextended_pattern_fragment' := pf' |}))
          := eq_refl.
        Definition eta_contract_aggregate {A' B'} (f : A' -> B') (v : aggregate_for_unextended_pattern_fragmentR0 f)
          : app _ {| base := base v ; app := f (base v) ; aggregate_for_unextended_pattern_fragment' := eq_refl |}
            = app _ v
          := aggregate_for_unextended_pattern_fragment' _.
        Definition unfold_app {A B f x y z}
          : @app A B f (@Build_aggregate_for_unextended_pattern_fragmentR0 A B f x y z) = y
          := eq_refl.
        (* next could be just [Instance] if we lift this outside a proof; see https://coq.inria.fr/bugs/show_bug.cgi?id=4638 *)
        Lemma Let_In_fun_Proper A' B' v
          : Proper (forall_relation (fun a' => pointwise_relation (v = a') eq) ==> eq ==> eq)
                   (@Let_In A' (fun a' => v = a' -> B') v).
        Proof. compute; intros; subst; auto. Qed.
        Global Existing Instance Let_In_fun_Proper.
        Definition lift_fun_Let_In {A B C} (v : A) (f : forall v : A, B v)
          : Let_In v (fun v' (_ : C v') => f v') = (fun _ : C v => Let_In v f)
          := eq_refl.
        Definition strip_dummy_Let_In {A B} (v : A) (f : B)
          : Let_In v (fun _ => f) = f
          := eq_refl.
        Opaque app. (* without this, "no constraint can apply on a dependent argument" *)
        Opaque Let_In. (* without this, "no constraint can apply on a dependent argument" *)
        setoid_rewrite (aggregate_for_unextended_pattern_fragment S2Rep).
        setoid_rewrite (Let_In_pull_app_nd S2Rep).
        setoid_rewrite Let_In_push_app_nd.
        setoid_rewrite eta_contract_aggregate.
        setoid_rewrite unfold_app.
        setoid_rewrite lift_fun_Let_In.
        setoid_rewrite strip_dummy_Let_In.

Some of these could be fused (the first and second; the third and fourth; the fifth and sixth), but I figured it would be instructive to leave in all the intermediate stages that I came up with in my head (actually, originally, I did eta_contract_aggregate before Let_In_push_app_nd).

There are also other sequences of setoid_rewrites that work, such as:

        setoid_rewrite (Let_In_pull_app_nd S2Rep).
        setoid_rewrite Let_In_push_app_nd.
        setoid_rewrite aggregate_for_unextended_pattern_fragment'.
        setoid_rewrite unfold_app.
        setoid_rewrite lift_fun_Let_In.
        setoid_rewrite strip_dummy_Let_In.

[andres-erbsen]

1. We need to use nat to parametrize word and to do arithmetic on it (add, sub, mod, powers).
2. This looks like black magic to me. I am leaning towards not using the hack you posted, and manually writing the much less hairy term that would result from the rewrites. Good to know that one day this might "just work", though.

[JasonGross]

1. How do you plan to express the optimized version, if you need something other than nat, and word is dependent on nat?
2. Let me try to clarify it a bit: the idea is that you need to make sure that Coq never has to solve a problem of the form ?P (f n) == expression, and only problems of the form ?P n == expression for n a variable. We want to transform Let_In v (fun n => P (f n)) into Let_In (f v) P. We need to "hide" the f from Coq, so we build a package that contains both v and f v. Then we can bind this package in the Let_In, as Let_In package (fun pkg => P (f (project_v pkg))). Now we can replace f (project_v pkg) with project_fv pkg. Finally, we need to do clean-up; we actually want to bind f v, not the package, and we want to unfold the projection.

[andres-erbsen]

1. nat will remain in the word indices for now, but will be replaced with a different representation in other places. In more distant future we would probably replace the words with specialized types as well.
2. Okay.

[JasonGross]

1. So can you specify your interface as "something isomorphic to nat"? And then use the back-and-forth conversion functions as necessary when defining the initial version?

[andres-erbsen]

Yeah, but I really don't think it is worth it for now. One day we might set out to create a standard library where all constructions are defined by their properties instead of structure, and based on what I currently see, it would probably be a good thing.

Right now, though, I will have a more manual variant of this derivation soon, and we can discuss that.

[andres-erbsen]

https://github.com/mit-plv/fiat-crypto/commit/afc72c575db1d6f52d8b167450e45ba05f98eb74#diff-5366caedd04016399124d528353b4a5cR251

I am tempted to merge that and move on to other stuff.

[JasonGross]

Seems reasonable. Consider dropping a comment with a reference to this issue, and the consideration of just doing setoid_rewrite.

You should also fix the 8.4 build before merging; 8.4 is unhappy with your _ ^ _ notation.