diff options
Diffstat (limited to 'src/PushButtonSynthesis')
-rw-r--r-- | src/PushButtonSynthesis/Primitives.v | 9 | ||||
-rw-r--r-- | src/PushButtonSynthesis/WordByWordMontgomery.v | 5 |
2 files changed, 10 insertions, 4 deletions
diff --git a/src/PushButtonSynthesis/Primitives.v b/src/PushButtonSynthesis/Primitives.v index ee2793c40..4d3e9c047 100644 --- a/src/PushButtonSynthesis/Primitives.v +++ b/src/PushButtonSynthesis/Primitives.v @@ -183,6 +183,9 @@ Module CorrectnessStringification. => strip_bounds_info T | list_Z_bounded_by _ _ -> ?T => strip_bounds_info T + | (_ = List.map (fun z => (_ mod _) / _) (List.seq _ _)) /\ (?a <= ?b < ?c) -> ?T + => let T := strip_bounds_info T in + constr:(a <= b < c -> T) | ?T /\ list_Z_bounded_by _ _ => T | ?T /\ (match _ with pair _ _ => _ end = true) @@ -191,8 +194,10 @@ Module CorrectnessStringification. => T | iff _ _ => correctness - | _ = _ /\ (_ = _ /\ (_ <= _ < _)) - => correctness + | ?x = ?y /\ (_ = List.map (fun z => (_ mod _) / _) (List.seq _ _)) /\ (?a <= ?b < ?c) + => constr:(x = y /\ a <= b < c) + | (_ = List.map (fun z => (_ mod _) / _) (List.seq _ _)) /\ (?a <= ?b < ?c) + => constr:(a <= b < c) | _ = _ :> list Z => correctness | forall x : ?T, ?f diff --git a/src/PushButtonSynthesis/WordByWordMontgomery.v b/src/PushButtonSynthesis/WordByWordMontgomery.v index 46ffa083f..d95f35bf4 100644 --- a/src/PushButtonSynthesis/WordByWordMontgomery.v +++ b/src/PushButtonSynthesis/WordByWordMontgomery.v @@ -235,10 +235,11 @@ Section __. (CorrectnessStringification.dyn_context.cons r' ("((2^" ++ decimal_string_of_Z machine_wordsize ++ ")⁻¹ mod m)")%string (CorrectnessStringification.dyn_context.cons - from_montgomery_res (prefix ++ "from_montgomery")%string + from_montgomery_res "from_montgomery"%string (CorrectnessStringification.dyn_context.cons (@eval 8 n_bytes) "bytes_eval"%string - CorrectnessStringification.dyn_context.nil)))). + CorrectnessStringification.dyn_context.nil)))) + (only parsing). Local Notation stringify_correctness prefix pre_extra correctness := (stringify_correctness_with_ctx (initial_ctx prefix) |