From b3c8ec8957d5eb4c319af9ab7baae96cb92cda6a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 28 Jun 2018 20:01:50 -0400 Subject: Synthesize selectznz --- Makefile | 2 +- src/Experiments/NewPipeline/Toplevel1.v | 29 +++++++++++++++++++++++++++++ 2 files changed, 30 insertions(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 4d891d425..f9d64ac83 100644 --- a/Makefile +++ b/Makefile @@ -488,7 +488,7 @@ standalone-haskell: $(STANDALONE:%=src/Experiments/NewPipeline/ExtractionHaskell standalone-ocaml: $(STANDALONE:%=src/Experiments/NewPipeline/ExtractionOCaml/%) UNSATURATED_SOLINAS_C_FILES := curve25519_64.c curve25519_32.c -FUNCTIONS_FOR_25519 := carry_mul carry_square carry_scmul121666 carry add sub opp to_bytes from_bytes +FUNCTIONS_FOR_25519 := carry_mul carry_square carry_scmul121666 carry add sub opp selectznz to_bytes from_bytes UNSATURATED_SOLINAS := src/Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas .PHONY: c-files c-files: $(UNSATURATED_SOLINAS_C_FILES) diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v index 80fbf398e..6a04a8b88 100644 --- a/src/Experiments/NewPipeline/Toplevel1.v +++ b/src/Experiments/NewPipeline/Toplevel1.v @@ -808,6 +808,15 @@ Derive id_gen Proof. cache_reify (). Qed. Hint Extern 1 (_ = id _) => simple apply id_gen_correct : reify_gen_cache. +Derive selectznz_gen + SuchThat (forall (cond : Z) (f g : list Z), + Interp (t:=reify_type_of Positional.select) + selectznz_gen cond f g + = Positional.select cond f g) + As selectznz_gen_correct. +Proof. cache_reify (). Qed. +Hint Extern 1 (_ = Positional.select _ _ _) => simple apply selectznz_gen_correct : reify_gen_cache. + Derive to_bytes_gen SuchThat (forall (limbwidth_num limbwidth_den : Z) (n : nat) @@ -891,8 +900,12 @@ Module Import UnsaturatedSolinas. prime_upperbound_list. Definition prime_bound : ZRange.type.option.interp (base.type.Z) := Some r[0~>(s - Associational.eval c - 1)]%zrange. + Definition prime_bounds : ZRange.type.option.interp (base.type.list (base.type.Z)) + := Some (List.map (fun v => Some r[0 ~> v]%zrange) prime_upperbound_list). Definition prime_bytes_bounds : ZRange.type.option.interp (base.type.list (base.type.Z)) := Some (List.map (fun v => Some r[0 ~> v]%zrange) prime_bytes_upperbound_list). + Definition saturated_bounds : ZRange.type.option.interp (base.type.list (base.type.Z)) + := Some (List.repeat (Some r[0 ~> 2^machine_wordsize-1]%zrange) n). Definition m_enc : list Z := encode (weight (Qnum limbwidth) (Qden limbwidth)) n s c (s-Associational.eval c). @@ -1114,6 +1127,19 @@ Module Import UnsaturatedSolinas. (Some loose_bounds) (oppmod (Qnum limbwidth) (Z.pos (Qden limbwidth)) s c n coef). + Definition srselectznz prefix + := BoundsPipelineToStrings_with_bytes_no_subst01 + prefix "selectznz" + selectznz_gen + (Some r[0~>1], (saturated_bounds, (saturated_bounds, tt)))%zrange + saturated_bounds. + + Definition rselectznz_correct + := BoundsPipeline_with_bytes_no_subst01_correct + (Some r[0~>1], (saturated_bounds, (saturated_bounds, tt)))%zrange + saturated_bounds + Positional.select. + Definition srto_bytes prefix := BoundsPipelineToStrings_with_bytes_no_subst01 prefix "to_bytes" @@ -1233,6 +1259,8 @@ Module Import UnsaturatedSolinas. := type_of_strip_3arrow (@rsub_correct rv). Definition ropp_correctT rv : Prop := type_of_strip_3arrow (@ropp_correct rv). + Definition rselectznz_correctT rv : Prop + := type_of_strip_3arrow (@rselectznz_correct rv). Definition rto_bytes_correctT rv : Prop := type_of_strip_3arrow (@rto_bytes_correct rv). Definition rfrom_bytes_correctT rv : Prop @@ -1490,6 +1518,7 @@ Module Import UnsaturatedSolinas. ("add", sradd); ("sub", srsub); ("opp", sropp); + ("selectznz", srselectznz); ("to_bytes", srto_bytes); ("from_bytes", srfrom_bytes)]. -- cgit v1.2.3