diff options
Diffstat (limited to 'src/Experiments/NewPipeline')
-rw-r--r-- | src/Experiments/NewPipeline/Rewriter.v | 2 | ||||
-rw-r--r-- | src/Experiments/NewPipeline/Toplevel2.v | 41 |
2 files changed, 43 insertions, 0 deletions
diff --git a/src/Experiments/NewPipeline/Rewriter.v b/src/Experiments/NewPipeline/Rewriter.v index a055c4735..aecf401d8 100644 --- a/src/Experiments/NewPipeline/Rewriter.v +++ b/src/Experiments/NewPipeline/Rewriter.v @@ -1418,6 +1418,8 @@ In the RHS, the follow notation applies: ; make_rewrite_step (* _step, so that if one of the arguments is concrete, we automatically get the rewrite rule for [Z_cast] applying to it *) (#pident.Z_cast2 @ (??{ℤ}, ??{ℤ})) (fun r x y => (#(ident.Z_cast (fst r)) @ $x, #(ident.Z_cast (snd r)) @ $y)) + + ; make_rewrite (-??{ℤ}) (fun e => ret (UnderLets.UnderLet e (fun v => UnderLets.Base (-$v))) when negb (SubstVarLike.is_var_fst_snd_pair_opp e)) (* inline negation when the rewriter wouldn't already inline it *) ]%list%pattern%cps%option%under_lets%Z%bool. Definition dtree' diff --git a/src/Experiments/NewPipeline/Toplevel2.v b/src/Experiments/NewPipeline/Toplevel2.v index 4cba170bd..34a758d87 100644 --- a/src/Experiments/NewPipeline/Toplevel2.v +++ b/src/Experiments/NewPipeline/Toplevel2.v @@ -239,6 +239,47 @@ void fesub(uint64_t[5] x1, uint64_t[5] x2, uint64_t[5] x3) { *) End X25519_64. +Module P224_64. + Definition s := 2^224. + Definition c := [(2^96, 1); (1,-1)]. + Definition machine_wordsize := 128. + + Derive mulmod + SuchThat (SaturatedSolinas.rmulmod_correctT s c machine_wordsize mulmod) + As mulmod_correct. + Proof. Time solve_rmulmod machine_wordsize. Time Qed. + + Import PrintingNotations. + Open Scope expr_scope. + Set Printing Width 100000. + Set Printing Depth 100000. + + Local Notation "'mul128' '(' x ',' y ')'" := + (#(Z_cast2 (uint128, _)%core) @ (#(Z_mul_split_concrete 340282366920938463463374607431768211456) @ x @ y))%expr (at level 50) : expr_scope. + Local Notation "'add128' '(' x ',' y ')'" := + (#(Z_cast2 (uint128, bool)%core) @ (#(Z_add_get_carry_concrete 340282366920938463463374607431768211456) @ x @ y))%expr (at level 50) : expr_scope. + Local Notation "'adc128' '(' c ',' x ',' y ')'" := + (#(Z_cast2 (uint128, bool)%core) @ (#(Z_add_with_get_carry_concrete 340282366920938463463374607431768211456) @ c @ x @ y))%expr (at level 50) : expr_scope. + Local Notation "'sub128' '(' x ',' y ')'" := + (#(Z_cast2 (uint128, bool)%core) @ (#(Z_sub_get_borrow_concrete 340282366920938463463374607431768211456) @ x @ y))%expr (at level 50) : expr_scope. + Local Notation "'sbb128' '(' c ',' x ',' y ')'" := + (#(Z_cast2 (uint128, bool)%core) @ (#(Z_sub_with_get_borrow_concrete 340282366920938463463374607431768211456) @ c @ x @ y))%expr (at level 50) : expr_scope. + Local Notation "'mul64' '(' x ',' y ')'" := + (#(Z_cast2 (uint64, _)%core) @ (#(Z_mul_split_concrete 18446744073709551616) @ x @ y))%expr (at level 50) : expr_scope. + Local Notation "'add64' '(' x ',' y ')'" := + (#(Z_cast2 (uint64, bool)%core) @ (#(Z_add_get_carry_concrete 18446744073709551616) @ x @ y))%expr (at level 50) : expr_scope. + Local Notation "'adc64' '(' c ',' x ',' y ')'" := + (#(Z_cast2 (uint64, bool)%core) @ (#(Z_add_with_get_carry_concrete 18446744073709551616) @ c @ x @ y))%expr (at level 50) : expr_scope. + Local Notation "'adx64' '(' c ',' x ',' y ')'" := + (#(Z_cast bool) @ (#Z_add_with_carry @ c @ x @ y))%expr (at level 50) : expr_scope. + Local Notation "'sub64' '(' x ',' y ')'" := + (#(Z_cast2 (uint64, bool)%core) @ (#(Z_sub_get_borrow_concrete 18446744073709551616) @ x @ y))%expr (at level 50) : expr_scope. + Local Notation "'sbb64' '(' c ',' x ',' y ')'" := + (#(Z_cast2 (uint64, bool)%core) @ (#(Z_sub_with_get_borrow_concrete 18446744073709551616) @ c @ x @ y))%expr (at level 50) : expr_scope. + Set Printing Width 1000000. + Print mulmod. +End P224_64. + Module P192_64. Definition s := 2^192. Definition c := [(2^64, 1); (1,1)]. |