From 76c018d44454934f386bf85fcdec5e5fb94ddde2 Mon Sep 17 00:00:00 2001 From: Marcella Hastings Date: Tue, 15 Oct 2024 14:52:30 -0400 Subject: [PATCH] mlkem: format properties correctly #147 Several properties didn't have correct `repl` commands in the docstrings. --- .../Asymmetric/Cipher/ML_KEM/Specification.cry | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry b/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry index 003f6d0..aee7fe3 100644 --- a/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry +++ b/Primitive/Asymmetric/Cipher/ML_KEM/Specification.cry @@ -647,7 +647,7 @@ submodule NTT where /** * This property demonstrates that NaiveNTT is self-inverting. - * ``` + * ```repl * :prove NaiveNTT_Inverts * ``` */ @@ -656,7 +656,7 @@ submodule NTT where /** * This property demonstrates that NaiveNTTInv is self-inverting. - * ``` + * ```repl * :prove NaiveNTTInv_Inverts * ``` */ @@ -665,7 +665,7 @@ submodule NTT where /** * This property demonstrates that `fast_ntt` is the inverse of `fast_invntt`. - * ``` + * ```repl * :prove fast_ntt_inverts * ``` */ @@ -674,7 +674,7 @@ submodule NTT where /** * This property demonstrates that `fast_invntt` is the inverse of `fast_ntt`. - * ``` + * ```repl * :prove fast_invntt_inverts * ``` */ @@ -683,7 +683,7 @@ submodule NTT where /** * This property demonstrates that `naive_ntt` is equivalent to `fast_ntt`. - * ``` + * ```repl * :prove naive_fast_ntt_equiv * ``` */ @@ -692,7 +692,7 @@ submodule NTT where /** * This property demonstrates that `naive_invntt` is equivalent to `fast_invntt`. - * ``` + * ```repl * :prove naive_fast_invntt_equiv * ``` */ @@ -759,7 +759,7 @@ MultiplyNTTs a b = join [BaseCaseMultiply (f_hat_i i) (g_hat_i i) (root i) | i : root i = (zeta^^(reverse (64 + (i >> 1)) >> 1) * ((-1 : (Z q)) ^^ (i))) /** - * Testing that (1+x)^2 = 1+2x+x^2 + * Testing that (1+x)^2 = 1+2x+x^2. * ```repl * :prove TestMult * ```