From 6498b3808c81eeb19f5b1b3a3c8797c1c4adc83a Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 27 Oct 2016 10:12:54 -0400 Subject: put EdDSA encoding sign bit at the MSB --- src/Util/WordUtil.v | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'src/Util/WordUtil.v') diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v index fd2e5e098..7a856f1e9 100644 --- a/src/Util/WordUtil.v +++ b/src/Util/WordUtil.v @@ -311,3 +311,10 @@ Proof. Admitted. Hint Rewrite @wordToN_wor using word_util_arith : push_wordToN. Hint Rewrite <- @wordToN_wor using word_util_arith : pull_wordToN. + +Axiom wlast : forall sz, word (sz+1) -> bool. Arguments wlast {_} _. +Axiom winit : forall sz, word (sz+1) -> word sz. Arguments winit {_} _. +Axiom combine_winit_wlast : forall {sz} a b (c:word (sz+1)), + @combine sz a 1 b = c <-> a = winit c /\ b = (WS (wlast c) WO). +Axiom winit_combine : forall sz a b, @winit sz (combine a b) = a. +Axiom wlast_combine : forall sz a b, @wlast sz (combine a (WS b WO)) = b. \ No newline at end of file -- cgit v1.2.3