Add generic polynomial #5

Hvassaa · 2023-06-17T10:37:39Z

This is an attempt at a hacspec v2 compliant generic (uni-variate) polynomial spec.

It supports

polynomial-polynomial addition/subtraction/multiplication/division
polynomial-scalar addition/subtraction/multiplication/division
evaluation
Some convenience functions for getting degree, coefficient form, ...

As of 17-06-2023 (via docker image):

cargo-hax lint hacspec returns no errors or warnings
cargo-hax into coq gives

bash-5.2# cargo-hax into coq
warning: some crates are on edition 2021 which defaults to `resolver = "2"`, but virtual workspaces default to `resolver = "1"`
note: to keep the current resolver, specify `workspace.resolver = "1"` in the workspace root's manifest
note: to use the edition 2021 resolver, specify `workspace.resolver = "2"` in the workspace root's manifest
   Compiling hacspec-pasta v1.0.0 (/work/examples/pasta)
note: Writing file "/work/examples/polynomial/out/Hacspec_pasta.v"

   Compiling hacspec-polynomial v0.1.0 (/work/examples/polynomial)
error[CE0001]: (Diagnostics.Context.Phase FunctionalizeLoops): something is not implemented yet.
               Loop without mutation?
  --> polynomial/src/polynomial.rs:46:9
   |
46 | /         for i in (1..len).rev() {
47 | |             if self.coefficients[i] != T::default() {
48 | |                 return Polynomial {
49 | |                     coefficients: self.coefficients.slice(0, i + usize::one()),
50 | |                 };
51 | |             }
52 | |         }
   | |_________^

error[CE0001]: (Diagnostics.Context.Phase CfIntoMonads): something is not implemented yet.This is discussed in issue https://github.com/hacspec/hacspec-v2/issues/96.
               Please upvote or comment this issue if you see this error message.
               TODO: Monad for loop-related control flow
   --> polynomial/src/polynomial.rs:200:9
    |
200 | /         for _ in 0..loop_upper_bound {
201 | |             if r.trim() != Polynomial::<T>::default() && r.degree() >= rhs.degree() {
202 | |                 let degree_diff = r.degree() - rhs.degree();
203 | |                 let mut t = Seq::<T>::create(degree_diff + usize::one());
...   |
210 | |             }
211 | |         }
    | |_________^

error[CE0001]: (Diagnostics.Context.Phase FunctionalizeLoops): something is not implemented yet.
               Only for loop are being functionalized for now
   --> polynomial/src/polynomial.rs:200:9
    |
200 | /         for _ in 0..loop_upper_bound {
201 | |             if r.trim() != Polynomial::<T>::default() && r.degree() >= rhs.degree() {
202 | |                 let degree_diff = r.degree() - rhs.degree();
203 | |                 let mut t = Seq::<T>::create(degree_diff + usize::one());
...   |
210 | |             }
211 | |         }
    | |_________^

error[CE0001]: (Diagnostics.Context.Phase FunctionalizeLoops): something is not implemented yet.
               Loop without mutation?
   --> polynomial/src/polynomial.rs:236:16
    |
236 |           } else {
    |  ________________^
237 | |             for i in 0..lhs.len() {
238 | |                 if lhs[i] != rhs[i] {
239 | |                     return false;
240 | |                 }
241 | |             }
242 | |         }
    | |_________^

error[CE0001]: (Diagnostics.Context.Backend Coq): something is not implemented yet.
               [ty] node typ
   --> polynomial/src/polynomial.rs:83:1
    |
83  | / impl<T: Numeric + NumericCopy + PartialEq> Add<Polynomial<T>> for Polynomial<T> {
84  | |     type Output = Self;
85  | |
86  | |     fn add(self, other: Self) -> Self {
...   |
106 | |     }
107 | | }
    | |_^

error[CE0001]: (Diagnostics.Context.Backend Coq): something is not implemented yet.
               [ty] node typ
   --> polynomial/src/polynomial.rs:109:1
    |
109 | / impl<T: Numeric + NumericCopy + PartialEq> Add<T> for Polynomial<T> {
110 | |     type Output = Self;
111 | |
112 | |     fn add(self, other: T) -> Self {
...   |
116 | |     }
117 | | }
    | |_^

error[CE0001]: (Diagnostics.Context.Backend Coq): something is not implemented yet.
               [ty] node typ
   --> polynomial/src/polynomial.rs:119:1
    |
119 | / impl<T: Numeric + NumericCopy + PartialEq> Sub<Polynomial<T>> for Polynomial<T> {
120 | |     type Output = Self;
121 | |
122 | |     fn sub(self, other: Self) -> Self {
...   |
134 | |     }
135 | | }
    | |_^

error[CE0001]: (Diagnostics.Context.Backend Coq): something is not implemented yet.
               [ty] node typ
   --> polynomial/src/polynomial.rs:137:1
    |
137 | / impl<T: Numeric + NumericCopy + PartialEq> Sub<T> for Polynomial<T> {
138 | |     type Output = Self;
139 | |
140 | |     fn sub(self, other: T) -> Self {
...   |
144 | |     }
145 | | }
    | |_^

error[CE0001]: (Diagnostics.Context.Backend Coq): something is not implemented yet.
               [ty] node typ
   --> polynomial/src/polynomial.rs:147:1
    |
147 | / impl<T: Numeric + NumericCopy + PartialEq> Mul<Polynomial<T>> for Polynomial<T> {
148 | |     type Output = Self;
149 | |
150 | |     fn mul(self, rhs: Self) -> Self::Output {
...   |
167 | |     }
168 | | }
    | |_^

error[CE0001]: (Diagnostics.Context.Backend Coq): something is not implemented yet.
               [ty] node typ
   --> polynomial/src/polynomial.rs:170:1
    |
170 | / impl<T: Numeric + NumericCopy + PartialEq> Mul<T> for Polynomial<T> {
171 | |     type Output = Self;
172 | |
173 | |     fn mul(self, rhs: T) -> Self::Output {
...   |
179 | |     }
180 | | }
    | |_^

error[CE0001]: (Diagnostics.Context.Backend Coq): something is not implemented yet.
               [ty] node typ
   --> polynomial/src/polynomial.rs:182:1
    |
182 | / impl<T: Numeric + NumericCopy + PartialEq + hacspec_lib::Div<Output = T>> Div<Polynomial<T>>
183 | |     for Polynomial<T>
184 | | {
185 | |     type Output = (Self, Self);
...   |
214 | |     }
215 | | }
    | |_^

error[CE0001]: (Diagnostics.Context.Backend Coq): something is not implemented yet.
               [ty] node typ
   --> polynomial/src/polynomial.rs:217:1
    |
217 | / impl<T: Numeric + NumericCopy + PartialEq + hacspec_lib::Div<Output = T>> Div<T> for Polynomial<T> {
218 | |     type Output = Self;
219 | |
220 | |     fn div(self, rhs: T) -> Self {
...   |
226 | |     }
227 | | }
    | |_^

note: Writing file "/work/examples/polynomial/out/Hacspec_polynomial.v"

error: could not compile `hacspec-polynomial` (lib) due to 12 previous errors

cargo-hax into fstar gives

bash-5.2# cargo-hax into fstar
warning: some crates are on edition 2021 which defaults to `resolver = "2"`, but virtual workspaces default to `resolver = "1"`
note: to keep the current resolver, specify `workspace.resolver = "1"` in the workspace root's manifest
note: to use the edition 2021 resolver, specify `workspace.resolver = "2"` in the workspace root's manifest
   Compiling hacspec-pasta v1.0.0 (/work/examples/pasta)
note: Writing file "/work/examples/polynomial/out/Hacspec_pasta.fst"

   Compiling hacspec-polynomial v0.1.0 (/work/examples/polynomial)
error[CE0001]: (Diagnostics.Context.Phase FunctionalizeLoops): something is not implemented yet.
               Loop without mutation?
  --> polynomial/src/polynomial.rs:46:9
   |
46 | /         for i in (1..len).rev() {
47 | |             if self.coefficients[i] != T::default() {
48 | |                 return Polynomial {
49 | |                     coefficients: self.coefficients.slice(0, i + usize::one()),
50 | |                 };
51 | |             }
52 | |         }
   | |_________^

error[CE0001]: (Diagnostics.Context.Phase CfIntoMonads): something is not implemented yet.This is discussed in issue https://github.com/hacspec/hacspec-v2/issues/96.
               Please upvote or comment this issue if you see this error message.
               TODO: Monad for loop-related control flow
   --> polynomial/src/polynomial.rs:200:9
    |
200 | /         for _ in 0..loop_upper_bound {
201 | |             if r.trim() != Polynomial::<T>::default() && r.degree() >= rhs.degree() {
202 | |                 let degree_diff = r.degree() - rhs.degree();
203 | |                 let mut t = Seq::<T>::create(degree_diff + usize::one());
...   |
210 | |             }
211 | |         }
    | |_________^

error[CE0001]: (Diagnostics.Context.Phase FunctionalizeLoops): something is not implemented yet.
               Only for loop are being functionalized for now
   --> polynomial/src/polynomial.rs:200:9
    |
200 | /         for _ in 0..loop_upper_bound {
201 | |             if r.trim() != Polynomial::<T>::default() && r.degree() >= rhs.degree() {
202 | |                 let degree_diff = r.degree() - rhs.degree();
203 | |                 let mut t = Seq::<T>::create(degree_diff + usize::one());
...   |
210 | |             }
211 | |         }
    | |_________^

error[CE0001]: (Diagnostics.Context.Phase FunctionalizeLoops): something is not implemented yet.
               Loop without mutation?
   --> polynomial/src/polynomial.rs:236:16
    |
236 |           } else {
    |  ________________^
237 | |             for i in 0..lhs.len() {
238 | |                 if lhs[i] != rhs[i] {
239 | |                     return false;
240 | |                 }
241 | |             }
242 | |         }
    | |_________^

error[CE0001]: (Diagnostics.Context.Backend FStar): something is not implemented yet.
               anonymous impl
  --> polynomial/src/polynomial.rs:11:1
   |
11 | / impl<T: Numeric + NumericCopy + PartialEq> Polynomial<T> {
12 | |     /// Create a polynomial, defined from its coefficient form
13 | |     ///
14 | |     /// # Arguments
...  |
80 | |     }
81 | | }
   | |_^

note: Writing file "/work/examples/polynomial/out/Hacspec_polynomial.fst"

error: could not compile `hacspec-polynomial` (lib) due to 5 previous errors

spitters · 2023-06-19T10:12:35Z

@W95Psp @cmester0 are these error messages expected?

If the hacspec is correct, but the backends are lagging, then I think it could be OK to proceed with reviewing and then merging.

spitters · 2023-06-19T10:18:41Z

polynomial/src/polynomial.rs

+        }
+    }
+}
+


Some short friendly documentation would be kind here.

Maybe just:
/// We wil now define the ring operations on polynomials.

spitters · 2023-06-19T10:20:17Z

LGTM. I only marked a small nit.

karthikbhargavan · 2023-06-19T11:15:25Z

Hello, we discussed the errors today.

For the F* backend:

the second and third errors (for _ = ...) should be fixed now (Allow any pattern on for loops (fixes #147) hax#150)
the first and fourth errors (return) feature a return within a loop which is not currently supported. It may be easiest to simply rewrite this code to do the return outside the loop.
the fourth error involves an implicit impl (without a trait). This is currently unallowed but will be fixed soon.

So, if you make the return modification, this code will pass the toolchain soon.

Hvassaa · 2023-06-20T06:40:26Z

Some short friendly documentation would be kind here.

@spitters
I am not sure what lines this refers to, is it in general or for impl<T: Numeric + NumericCopy + PartialEq> Add<Polynomial<T>> for Polynomial<T>?

Hvassaa · 2023-06-20T06:40:52Z

Hello, we discussed the errors today.

For the F* backend:

* the second and third errors (`for _ = ...`) should be fixed now ([Allow any pattern on for loops (fixes #147) hacspec-v2#150](https://github.com/hacspec/hacspec-v2/pull/150))

* the first and fourth errors (`return`) feature a `return` within a loop which is not currently supported. It may be easiest to simply rewrite this code to do the `return` outside the loop.

* the fourth error involves an implicit `impl` (without a trait). This is currently unallowed but will be fixed soon.

So, if you make the return modification, this code will pass the toolchain soon.

Great! I will look into that.

Hvassaa · 2023-08-09T19:58:54Z

I added the requested comment!

Furthermore, I wondered whether it might be useful with a function to create a polynomial using lagrange interpolation. I am not sure if that functionality is suitable for inclusion in a polynomial spec or not? (Maybe that should be separate?)

spitters · 2023-08-10T06:56:42Z

I think one could include it here, as it's too small for a separate library. It can always be moved later. from my phone

…

On Wed, Aug 9, 2023, 21:59 Rasmus T. Bjerg ***@***.***> wrote: I added the requested comment! Furthermore, I wondered whether it might be useful with a function to create a polynomial using lagrange interpolation. I am not sure if that functionality is suitable for inclusion in a polynomial spec or not? (Maybe that should be separate?) — Reply to this email directly, view it on GitHub <#5 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AABTNTQM47FK4ZYKY3SI4X3XUPTYRANCNFSM6AAAAAAZKE2INU> . You are receiving this because you were mentioned.Message ID: ***@***.***>

Rasmus T. Bjerg added 3 commits June 17, 2023 12:21

added generic polynomial

b951cc2

updated Cargo with polynomial

66d11a8

trim after more ops

24f1da6

franziskuskiefer self-requested a review June 19, 2023 05:32

spitters reviewed Jun 19, 2023

View reviewed changes

remove unrequired (Clone) type bound

49cc400

added comments for clarity

86232f4

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add generic polynomial #5

Add generic polynomial #5

Hvassaa commented Jun 17, 2023

spitters commented Jun 19, 2023

spitters Jun 19, 2023

spitters Jun 20, 2023

spitters commented Jun 19, 2023

karthikbhargavan commented Jun 19, 2023

Hvassaa commented Jun 20, 2023

Hvassaa commented Jun 20, 2023

Hvassaa commented Aug 9, 2023

spitters commented Aug 10, 2023 via email

Add generic polynomial #5

Are you sure you want to change the base?

Add generic polynomial #5

Conversation

Hvassaa commented Jun 17, 2023

spitters commented Jun 19, 2023

spitters Jun 19, 2023

Choose a reason for hiding this comment

spitters Jun 20, 2023

Choose a reason for hiding this comment

spitters commented Jun 19, 2023

karthikbhargavan commented Jun 19, 2023

Hvassaa commented Jun 20, 2023

Hvassaa commented Jun 20, 2023

Hvassaa commented Aug 9, 2023

spitters commented Aug 10, 2023 via email