blob: 4158a5277ed65d78b8a39c62ee733b572f825466 (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
Require Import Crypto.Specific.GF25519Reflective.Common.
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 Open Scope string_scope.
Compute ("Freeze", compute_bounds_for_display rfreezeW ExprUnOp_bounds).
(*Compute ("Freeze overflows? ", sanity_check rfreezeW ExprUnOp_bounds).*)
|
