From 83b8293fa1cd24383fe19f51863409c37e501502 Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Fri, 16 Feb 2018 19:02:16 +0100 Subject: define mul and add placeholders for new operations in bounds parts --- src/Experiments/SimplyTypedArithmetic.v | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) (limited to 'src') diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v index 1510fc741..d3b3d5e84 100644 --- a/src/Experiments/SimplyTypedArithmetic.v +++ b/src/Experiments/SimplyTypedArithmetic.v @@ -692,6 +692,14 @@ Module Columns. end; auto; try omega. rewrite IHp by tauto. ring. } Qed. + + Section mul. + Definition mul s n m (p q : list Z) : list Z := + let p_a := Positional.to_associational weight n p in + let q_a := Positional.to_associational weight n q in + let pq_a := MulSplit.Associational.sat_mul s p_a q_a in + fst (compact (from_associational m pq_a)). + End mul. End Columns. End Columns. @@ -3817,7 +3825,14 @@ Module Compilers. | ident.Z_div | ident.Z_modulo | ident.Z_eqb + | ident.Z_leb | ident.Z_of_nat + | ident.Z.mul_split (* TODO: is this the right thing? *) + | ident.Z.add_get_carry (* TODO: is this the right thing? *) + | ident.Z.add_with_get_carry (* TODO: is this the right thing? *) + | ident.Z.sub_get_borrow (* TODO: is this the right thing? *) + | ident.Z.zselect (* TODO: is this the right thing? *) + | ident.Z.add_modulo (* TODO: is this the right thing? *) => None end. End ident. @@ -5282,6 +5297,7 @@ Print Montgomery256.montred256. 115792089210356248762697446949407573530086143415290314195533631308867097853951)))), v1)) in Z.add_modulo @@ (v2, 0, 115792089210356248762697446949407573530086143415290314195533631308867097853951))%expr) : Z * Z -> Z + *) (* with named constants *) -- cgit v1.2.3