Skip to content

Commit 2406978

Browse files
committed
fixup! codespell: fix typos
1 parent ebfd269 commit 2406978

File tree

2 files changed

+4
-4
lines changed

2 files changed

+4
-4
lines changed

Coq/C/secp256k1/verif_modinv64_impl.v

+3-3
Original file line numberDiff line numberDiff line change
@@ -1915,7 +1915,7 @@ assert (Hqrve : Z.abs (divstep.Trans.q mtx * (d mod 2 ^ 62) + divstep.Trans.r mt
19151915
transitivity (Z.abs (divstep.Trans.q mtx) * (2 ^ 62 - 1)+ Z.abs (divstep.Trans.r mtx) * (2 ^ 62 - 1));[|lia].
19161916
apply Z.add_le_mono; apply Z.mul_le_mono_nonneg_l; lia.
19171917
}
1918-
rewrite ?Z.abs_lt, ?Z.abs_le in *. (* This speeds up lia exponetially. *)
1918+
rewrite ?Z.abs_lt, ?Z.abs_le in *. (* This speeds up lia exponentially. *)
19191919
forward_call (v_cd, Tsh, divstep.Trans.u mtx, d mod 2 ^ 62).
19201920
forward_call;[
19211921
change Int128_min_signed with (-2^127);change Int128_max_signed with (2^127-1);solve_bounds
@@ -1933,7 +1933,7 @@ forward_call;forward;progressC.
19331933
rewrite !Z.land_ones by lia.
19341934
assert (Habsmodinvd := Habsmod62 (modInv m (2 ^ 62) * cd0 + md0)).
19351935
assert (Habsmodinve := Habsmod62 (modInv m (2 ^ 62) * ce0 + me0)).
1936-
rewrite ?Z.abs_lt, ?Z.abs_le in *. (* This speeds up lia exponetially. *)
1936+
rewrite ?Z.abs_lt, ?Z.abs_le in *. (* This speeds up lia exponentially. *)
19371937
assert (Habsmd0modinv : Z.abs (m mod 2 ^ 62 * (md0 - (modInv m (2 ^ 62) * cd0 + md0) mod 2 ^ 62)) <= 2^125).
19381938
1:{
19391939
rewrite Z.abs_mul.
@@ -1946,7 +1946,7 @@ assert (Habsme0modinv : Z.abs (m mod 2 ^ 62 * (me0 - (modInv m (2 ^ 62) * ce0 +
19461946
change (2^125) with (2^62 * 2^63).
19471947
apply Zmult_le_compat; lia.
19481948
}
1949-
rewrite ?Z.abs_lt, ?Z.abs_le in *. (* This speeds up lia exponetially. *)
1949+
rewrite ?Z.abs_lt, ?Z.abs_le in *. (* This speeds up lia exponentially. *)
19501950
simpl (Signed62.reprn 5 m).
19511951
assert (Hcd0'b : -2^126 <=
19521952
cd0 + m mod 2 ^ 62 * (md0 - (modInv m (2 ^ 62) * cd0 + md0) mod 2 ^ 62) <=

Haskell/Core/Simplicity/BitMachine/Translate/TCO.hs

+1-1
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ data Translation a b = Translation { tcoOn :: MachineCodeK
1818
translate0 :: Translation a b -> MachineCode
1919
translate0 trans = tcoOff trans end
2020

21-
-- | 'translate' coverts a Simplicity term to the Bit Machine's 'MachineCode' with tail call optimization.
21+
-- | 'translate' converts a Simplicity term to the Bit Machine's 'MachineCode' with tail call optimization.
2222
--
2323
-- Simplicity terms are represented in tagless-final style, so any Simplicity term can be instantiated as @'Translation' a b@ and can be passed to the 'translate' function.
2424
translate :: Delegator Translation a b -> MachineCode

0 commit comments

Comments
 (0)