Difficulty adding a rewrite rule #1617

OwenConoly · 2023-07-03T06:20:22Z

I'm trying to add a Karatsuba template to fiat-crypto, but bounds analysis isn't smart enough to get the proper bounds for Karatsuba. In particular, I have written a function adk_mul (stands for 'arbitrary-degree karatsuba'), the outputs of which I would like to put some tight bounds on. My idea to accomplish this is as follows:

Add adk_mul as a basic identifier - one of the things in the all_ident_named_interped list in Language/IdentifierParameters.v
Add some logic in AbstractInterpretation/ZRange.v to properly bound the outputs of the adk_mul function.
Add a rule in Rewriter/Rules.v that unfolds the adk_mul identifier. The idea is that this rule will be triggered after the correct bounds are already established for the outputs of the adk_mul function.

I'm struggling with accomplishing part 3. When I try to add this rule, I get a lengthy error message which is mysterious to me.
Note that the adk_mul and ident_adk_mul functions are defined in Arithmetic/ADK.v.

I tried to reduce the size of the error message and hopefully get something that's comprehensible. It turns out that even trying to add this rule (using a subexpression of the expression that occurred in the rule that I'm trying to add) causes this error message. This error message is much shorter, but I still have no idea what's going on there.

Is there a way to fix these issues, and get the rewrite rule to work? Or should I take a different approach entirely to getting the right bounds for karatsuba multiplication?

The text was updated successfully, but these errors were encountered:

JasonGross · 2023-07-06T03:48:15Z

This should work in theory, but this part of the code is ad-hoc and unsatisfactory. I have some debugging suggestions at #1609 (comment). If you're down to implement that suggestion, you should get better error messages, and then I can plausibly direct you a bit more. But it looks like maybe the problem is that the machinery is unfolding something it shouldn't be?

Regarding the shorter error message, rules like (Z.to_nat (1 + ((Z.of_nat i + 1)/2 - 1) - Z.of_nat (i - (n - 1))%nat)%Z) aren't supported because the rewriter can't handle non-linear (duplicate) occurrences of non-literals. (Granted, "can't unify" is a bad error message, and if I had the time I'd make it give a better error message on these.)

OwenConoly · 2023-07-06T08:09:48Z

I see - I was getting confused about what the problem was here, because I made the incorrect assumption that if a was a subexpression of b, and the rewriter failed to handle a = a, then it couldn't handle b = b either. Now it's clear that I wasn't debugging this in a helpful way.

For context: I defined ident_adk_mul := adk_mul, and I added ident_adk_mul to the all_ident_named_interped list in Language/IdentifierParameters.v. Here is some information that's probably more useful than what I provided in my previous comment.

I tried redefining adk_mul (n : nat) (x y : list Z) : list Z := []. When I did this, the rewriter happily ingested the rule forall n x y, ident_adk_mul n x y = adk_mul n x y.
I tried redefining adk_mul (n : nat) (x y : list Z) : list Z := [6]. When I did this, the make_rewriter tactic failed in Arith.v, due to the presence of the rule forall n x y, ident_adk_mul n x y = adk_mul n x y. Here's the error message - I hope you can make some sense of it?

The error message:

Proving Rewriter_Interp...
Tactic call ran for 1.317 secs (1.307u,0.s) (success)
============================
WARNING: UNSOLVED GOAL:
max_const_val : Z
x1 :
(RewriteRules.Compile.value' false
   (type.base (base.type.type_base Compilers.nat)))
x2 : (API.interp_type (type.base (base.type.type_base Compilers.nat)))
H :
(ProofsCommon.Compilers.RewriteRules.Compile.value_interp_related
   (@Compilers.ident_interp) x1 x2)
x0 :
(RewriteRules.Compile.value' false
   (type.base (base.type.list (base.type.type_base Compilers.Z))))
x3 :
(API.interp_type
   (type.base (base.type.list (base.type.type_base Compilers.Z))))
H0 :
(ProofsCommon.Compilers.RewriteRules.Compile.value_interp_related
   (@Compilers.ident_interp) x0 x3)
x4 :
(RewriteRules.Compile.value' false
   (type.base (base.type.list (base.type.type_base Compilers.Z))))
x5 :
(API.interp_type
   (type.base (base.type.list (base.type.type_base Compilers.Z))))
H1 :
(ProofsCommon.Compilers.RewriteRules.Compile.value_interp_related
   (@Compilers.ident_interp) x4 x5)
============================
(expr.interp_related_gen (@Compilers.ident_interp)
   (fun t : API.type =>
    ProofsCommon.Compilers.RewriteRules.Compile.value_interp_related
      (@Compilers.ident_interp)) (#Compilers.ident_cons @ ###6%Z)
   (ADK.adk_mul x2 x3))
============================
============================
WARNING: UNSOLVED GOAL:
max_const_val : Z
x1 :
(RewriteRules.Compile.value' false
   (type.base (base.type.type_base Compilers.nat)))
x2 : (API.interp_type (type.base (base.type.type_base Compilers.nat)))
H :
(ProofsCommon.Compilers.RewriteRules.Compile.value_interp_related
   (@Compilers.ident_interp) x1 x2)
x0 :
(RewriteRules.Compile.value' false
   (type.base (base.type.list (base.type.type_base Compilers.Z))))
x3 :
(API.interp_type
   (type.base (base.type.list (base.type.type_base Compilers.Z))))
H0 :
(ProofsCommon.Compilers.RewriteRules.Compile.value_interp_related
   (@Compilers.ident_interp) x0 x3)
x4 :
(RewriteRules.Compile.value' false
   (type.base (base.type.list (base.type.type_base Compilers.Z))))
x5 :
(API.interp_type
   (type.base (base.type.list (base.type.type_base Compilers.Z))))
H1 :
(ProofsCommon.Compilers.RewriteRules.Compile.value_interp_related
   (@Compilers.ident_interp) x4 x5)
============================
(Compilers.ident_interp Compilers.ident_nil = x5)
============================
Tactic call ran for 0.442 secs (0.441u,0.s) (success)
WARNING: Remaining goal:
max_const_val : Z
x1 :
(RewriteRules.Compile.value' false
   (type.base (base.type.type_base Compilers.nat)))
x2 : (API.interp_type (type.base (base.type.type_base Compilers.nat)))
H :
(ProofsCommon.Compilers.RewriteRules.Compile.value_interp_related
   (@Compilers.ident_interp) x1 x2)
x0 :
(RewriteRules.Compile.value' false
   (type.base (base.type.list (base.type.type_base Compilers.Z))))
x3 :
(API.interp_type
   (type.base (base.type.list (base.type.type_base Compilers.Z))))
H0 :
(ProofsCommon.Compilers.RewriteRules.Compile.value_interp_related
   (@Compilers.ident_interp) x0 x3)
x4 :
(RewriteRules.Compile.value' false
   (type.base (base.type.list (base.type.type_base Compilers.Z))))
x5 :
(API.interp_type
   (type.base (base.type.list (base.type.type_base Compilers.Z))))
H1 :
(ProofsCommon.Compilers.RewriteRules.Compile.value_interp_related
   (@Compilers.ident_interp) x4 x5)
============================
(expr.interp_related_gen (@Compilers.ident_interp)
   (fun t : API.type =>
    ProofsCommon.Compilers.RewriteRules.Compile.value_interp_related
      (@Compilers.ident_interp)) (#Compilers.ident_cons @ ###6%Z)
   (ADK.adk_mul x2 x3))
WARNING: Remaining goal:
max_const_val : Z
x1 :
(RewriteRules.Compile.value' false
   (type.base (base.type.type_base Compilers.nat)))
x2 : (API.interp_type (type.base (base.type.type_base Compilers.nat)))
H :
(ProofsCommon.Compilers.RewriteRules.Compile.value_interp_related
   (@Compilers.ident_interp) x1 x2)
x0 :
(RewriteRules.Compile.value' false
   (type.base (base.type.list (base.type.type_base Compilers.Z))))
x3 :
(API.interp_type
   (type.base (base.type.list (base.type.type_base Compilers.Z))))
H0 :
(ProofsCommon.Compilers.RewriteRules.Compile.value_interp_related
   (@Compilers.ident_interp) x0 x3)
x4 :
(RewriteRules.Compile.value' false
   (type.base (base.type.list (base.type.type_base Compilers.Z))))
x5 :
(API.interp_type
   (type.base (base.type.list (base.type.type_base Compilers.Z))))
H1 :
(ProofsCommon.Compilers.RewriteRules.Compile.value_interp_related
   (@Compilers.ident_interp) x4 x5)
============================
(Compilers.ident_interp Compilers.ident_nil = x5)
File "./src/Rewriter/Passes/Arith.v", line 23, characters 23-36:
Error: Proof is not complete.

With adk_mul defined as in (2), I tried adding the rule ident_adk_mul = adk_mul. This also failed, with a similar error message as in (2).
I tried adding the rule [6] = [6]. This worked fine.
I tried adding the rule (fun (n : nat) (x y : list Z) => [6]) = (fun (n : nat) (x y : list Z) => [6]. This failed, complaining of an ILLEGAL_ABS_ON_LHS. I suppose lambdas on the LHS are bad.

It seems like the issue is related to the fact that I have an identifier that the rewriter recognizes on the left hand side, and a regular function on the right hand side. Do I need to somehow inform the rewriter that these things are equal?

JasonGross · 2023-07-06T14:34:25Z

2. I tried redefining adk_mul (n : nat) (x y : list Z) : list Z := [6]. When I did this, the make_rewriter tactic failed in Arith.v, due to the presence of the rule forall n x y, ident_adk_mul n x y = adk_mul n x y. Here's the error message - I hope you can make some sense of it?

For some reason, ident_adk_mul n x y seems to be getting reified on the LHS as [6] rather than as the identifier you added to the list of identifiers. Not sure what's causing this, but I suspect this is the root of the error.

JasonGross · 2023-07-06T14:39:48Z

Oh, no, nevermind, there must be a symmetry somewhere, I think the unfolding is expected.

I think what's happening is that you're seeing a failure to prove ADK.adk_mul x2 x3 equal to the interpretation of it's reification.

JasonGross · 2023-07-06T14:59:29Z

What if instead of adding forall n x y, ident_adk_mul n x y = adk_mul n x y. you add the rewrite rule forall n x y, ident_adk_mul n x y = ltac:(let rhs := eval cbv [adk_mul] in (adk_mul n x y) in exact rhs).?

JasonGross · 2023-07-06T15:05:07Z

Alternatively, stick something like Create HintDb reification_proofs discriminated. in https://github.com/mit-plv/rewriter/blob/c79bbc9148fb8386e188267c684a882d8634293b/src/Rewriter/Language/Pre.v
add a branch | progress repeat autounfold with reification_proofs to
https://github.com/mit-plv/rewriter/blob/c79bbc9148fb8386e188267c684a882d8634293b/src/Rewriter/Rewriter/ProofsCommonTactics.v#L501-503 right after assumption, and then add #[global] Hint Unfold adk_mul : reification_proofs. to Language/IdentifierParameters.v or something.

OwenConoly · 2023-07-06T19:50:00Z

What if instead of adding forall n x y, ident_adk_mul n x y = adk_mul n x y. you add the rewrite rule forall n x y, ident_adk_mul n x y = ltac:(let rhs := eval cbv [adk_mul] in (adk_mul n x y) in exact rhs).?

This works, thank you! I assume your second suggestion works as well, since it seems equivalent.
Do you think the second solution would be better in some way, or should I just stick with the first one?

OwenConoly · 2023-07-06T20:03:27Z

Never mind, your second suggestion does not appear to work. Not exactly that, anyway; perhaps something similar would work.
I'll just use the eval cbv solution then.

OwenConoly · 2023-07-06T20:08:19Z

I don't know how to close this without making a comment, so here is a comment

OwenConoly closed this as completed Jul 6, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Difficulty adding a rewrite rule #1617

Difficulty adding a rewrite rule #1617

OwenConoly commented Jul 3, 2023

JasonGross commented Jul 6, 2023

OwenConoly commented Jul 6, 2023 •

edited

Loading

JasonGross commented Jul 6, 2023

JasonGross commented Jul 6, 2023

JasonGross commented Jul 6, 2023

JasonGross commented Jul 6, 2023

OwenConoly commented Jul 6, 2023

OwenConoly commented Jul 6, 2023 •

edited

Loading

OwenConoly commented Jul 6, 2023

Difficulty adding a rewrite rule #1617

Difficulty adding a rewrite rule #1617

Comments

OwenConoly commented Jul 3, 2023

JasonGross commented Jul 6, 2023

OwenConoly commented Jul 6, 2023 • edited Loading

JasonGross commented Jul 6, 2023

JasonGross commented Jul 6, 2023

JasonGross commented Jul 6, 2023

JasonGross commented Jul 6, 2023

OwenConoly commented Jul 6, 2023

OwenConoly commented Jul 6, 2023 • edited Loading

OwenConoly commented Jul 6, 2023

OwenConoly commented Jul 6, 2023 •

edited

Loading

OwenConoly commented Jul 6, 2023 •

edited

Loading