From 160418762bbd63eaed704411b3eea926cab2f923 Mon Sep 17 00:00:00 2001 From: Reily Siegel Date: Wed, 4 Sep 2024 13:37:34 -0400 Subject: [PATCH 1/3] Fix indentation error. --- src/Crypto/Random/JS.idr | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Crypto/Random/JS.idr b/src/Crypto/Random/JS.idr index 548198d..2d3df9b 100644 --- a/src/Crypto/Random/JS.idr +++ b/src/Crypto/Random/JS.idr @@ -23,7 +23,7 @@ public export HasIO io => MonadRandom io where random_bytes Z = pure [] random_bytes n = - case codegen of - "node" => buffer_content prim_io__randomBytes n - "javascript" => buffer_content prim_io__getRandomValues n - _ => assert_total $ idris_crash "no random backend availible" + case codegen of + "node" => buffer_content prim_io__randomBytes n + "javascript" => buffer_content prim_io__getRandomValues n + _ => assert_total $ idris_crash "no random backend availible" From 3be2e17d2d8faa75bee8670f4c207dbbb5c9aef7 Mon Sep 17 00:00:00 2001 From: Reily Siegel Date: Wed, 4 Sep 2024 13:37:56 -0400 Subject: [PATCH 2/3] Export infixr for <*>>. This resolves a build warning. --- src/Network/TLS/Parsing.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Network/TLS/Parsing.idr b/src/Network/TLS/Parsing.idr index 42e033e..0125297 100644 --- a/src/Network/TLS/Parsing.idr +++ b/src/Network/TLS/Parsing.idr @@ -14,7 +14,7 @@ namespace Parserializer encode : a -> List c decode : Parser i e a - infixr 5 <*>> + export infixr 5 <*>> export apair : (Semigroup e, Monoid i) => Parserializer c i e a -> Parserializer c i e b -> Parserializer c i e (a, b) From 93cc5fdb1b9a1e5885f543b9693bad195d31b692 Mon Sep 17 00:00:00 2001 From: Reily Siegel Date: Wed, 4 Sep 2024 13:49:07 -0400 Subject: [PATCH 3/3] Replace deprecated functions. --- src/Utils/Bytes.idr | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Utils/Bytes.idr b/src/Utils/Bytes.idr index 21b2132..ad51ac6 100644 --- a/src/Utils/Bytes.idr +++ b/src/Utils/Bytes.idr @@ -140,9 +140,9 @@ shiftR' x i = maybe_a_a zeroBits $ do export rotl : FiniteBits a => {n : Nat} -> {auto prf : ((S n) = bitSize {a})} -> Fin (S n) -> a -> a rotl FZ x = x -rotl (FS i) x = (shiftL x $ bitsToIndex (coerce prf $ FS i)) .|. (shiftR x $ bitsToIndex $ invFin $ coerce prf $ weaken i) +rotl (FS i) x = (shiftL x $ bitsToIndex (coerce prf $ FS i)) .|. (shiftR x $ bitsToIndex $ complement $ coerce prf $ weaken i) export rotr : FiniteBits a => {n : Nat} -> {auto prf : ((S n) = bitSize {a})} -> Fin (S n) -> a -> a rotr FZ x = x -rotr (FS i) x = (shiftR x $ bitsToIndex (coerce prf $ FS i)) .|. (shiftL x $ bitsToIndex $ invFin $ coerce prf $ weaken i) +rotr (FS i) x = (shiftR x $ bitsToIndex (coerce prf $ FS i)) .|. (shiftL x $ bitsToIndex $ complement $ coerce prf $ weaken i)