blob: 0dcea29e48b3d8963ea7453615a7d040ce7009bd (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
Require Import Crypto.Specific.GF25519Reflective.CommonUnOp.
Definition rfreezeZ_sig : rexpr_unop_sig freeze. Proof. reify_sig. Defined.
Definition rfreezeW := Eval vm_compute in rword_of_Z rfreezeZ_sig.
Lemma rfreezeW_correct_and_bounded_gen : correct_and_bounded_genT rfreezeW rfreezeZ_sig.
Proof. rexpr_correct. Qed.
Definition rfreeze_output_bounds := Eval vm_compute in compute_bounds rfreezeW ExprUnOp_bounds.
Local Obligation Tactic := intros; vm_compute; constructor.
Axiom proof_admitted : False.
(** XXX TODO: Fix bounds analysis on freeze *)
Definition rfreezeW_correct_and_bounded
:= ExprUnOp_correct_and_bounded
rfreezeW freeze rfreezeZ_sig rfreezeW_correct_and_bounded_gen
match proof_admitted with end match proof_admitted with end.
Local Open Scope string_scope.
Compute ("Freeze", compute_bounds_for_display rfreezeW ExprUnOp_bounds).
(*Compute ("Freeze overflows? ", sanity_check rfreezeW ExprUnOp_bounds).*)
|
