search

EasyCrypt / easycrypt

EasyCrypt: Computer-Aided Cryptographic Proofs
MIT License
320 stars 49 forks source link

Polynomial division #523

Open strub opened 8 months ago

Boutry commented 8 months ago

Hi PY,

Did you replace the lengthy set calls by sequences of rewrites?

Boutry commented 8 months ago

Also I might have some uncommitted proofs. I will check later today.

strub commented 8 months ago

@Boutry I changed nothing. I just pulled out the PolyDiv file from the finite fields branch so that we can eventually merge it. What do you mean by "lengthly sets calls"?

fdupress commented 8 months ago

I assume smt?

Boutry commented 8 months ago

I assume smt?

Indeed. Got auto"corrected". Is there something to measure the duration of set calls atm? Maybe I do not need to replace them all if only a few take too much time.

We should also try and merge the field extension development at some point. After the 29th I can start by rebasing it. There were only a few admits left I think.

https://github.com/EasyCrypt/easycrypt/blob/3787dc9536faa1460783c1470618a0b59d72b4de/theories/algebra/Perms.ec

strub commented 8 months ago

When the file compiles, we can start looking at smt calls :)

strub commented 8 months ago

And yes, the ultimate goal is to merge the finite field theory. However, I'd like to merge polydiv first.

strub commented 3 months ago

Going back to that. I don't think we need to pseudo-division (TL;DR we do crypto). I would like to prune that part and just to keep the division for k[x] for k a field. Moreover, a large of the results could be then directly imported for the GCD-domain theory.