betrusted-ed25519-verified/verification/gen/CurveField/Funs.lean

-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
-- [curve25519_dalek]: function definitions
import Aeneas
import CurveField.Types
import CurveField.FunsExternal
open Aeneas Aeneas.Std Result ControlFlow Error
set_option linter.dupNamespace false
set_option linter.hashCommand false
set_option linter.unusedVariables false

/- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/
set_option maxHeartbeats 1000000

/- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/
set_option maxRecDepth 2048

/- You can remove the following line by using the CLI option `-all-computable`: -/
noncomputable section

namespace curve25519_dalek

/-- Trait implementation: [core::fmt::{impl core::fmt::Debug for [T]}]
    Source: '/rustc/library/core/src/fmt/mod.rs', lines 3121:0-3121:28
    Name pattern: [core::fmt::Debug<[@T]>] -/
@[reducible, rust_trait_impl "core::fmt::Debug<[@T]>"]
def Slice.Insts.CoreFmtDebug {T : Type} (DebugInst : core.fmt.Debug T) :
  core.fmt.Debug (Slice T) := {
  fmt := Slice.Insts.CoreFmtDebug.fmt DebugInst
}

/-- Trait implementation: [core::slice::index::private_slice_index::{impl core::slice::index::private_slice_index::Sealed for core::ops::range::RangeFull}]
    Source: '/rustc/library/core/src/slice/index.rs', lines 120:4-120:34
    Name pattern: [core::slice::index::private_slice_index::Sealed<core::ops::range::RangeFull>] -/
@[reducible, rust_trait_impl
  "core::slice::index::private_slice_index::Sealed<core::ops::range::RangeFull>"]
def core.ops.range.RangeFull.Insts.CoreSliceIndexPrivate_slice_indexSealed :
  core.slice.index.private_slice_index.Sealed core.ops.range.RangeFull := {
}

/-- Trait implementation: [core::slice::index::{impl core::slice::index::SliceIndex<[T], [T]> for core::ops::range::RangeFull}]
    Source: '/rustc/library/core/src/slice/index.rs', lines 631:0-631:55
    Name pattern: [core::slice::index::SliceIndex<core::ops::range::RangeFull, [@T], [@T]>] -/
@[reducible, rust_trait_impl
  "core::slice::index::SliceIndex<core::ops::range::RangeFull, [@T], [@T]>"]
def core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice (T :
  Type) : core.slice.index.SliceIndex core.ops.range.RangeFull (Slice T) (Slice
  T) := {
  sealedInst :=
    core.ops.range.RangeFull.Insts.CoreSliceIndexPrivate_slice_indexSealed
  get := core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.get
  get_mut :=
    core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.get_mut
  get_unchecked :=
    core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.get_unchecked
  get_unchecked_mut :=
    core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.get_unchecked_mut
  index :=
    core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.index
  index_mut :=
    core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.index_mut
}

/-- Trait implementation: [subtle::{impl core::convert::From<subtle::Choice> for bool}]
    Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/subtle-2.6.1/src/lib.rs', lines 138:0-138:26
    Name pattern: [core::convert::From<bool, subtle::Choice>] -/
@[reducible, rust_trait_impl "core::convert::From<bool, subtle::Choice>"]
def Bool.Insts.CoreConvertFromChoice : core.convert.From Bool subtle.Choice
  := {
  from_ := Bool.Insts.CoreConvertFromChoice.from
}

/-- Trait implementation: [subtle::{impl core::convert::From<u8> for subtle::Choice}]
    Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/subtle-2.6.1/src/lib.rs', lines 236:0-236:24
    Name pattern: [core::convert::From<subtle::Choice, u8>] -/
@[reducible, rust_trait_impl "core::convert::From<subtle::Choice, u8>"]
def subtle.Choice.Insts.CoreConvertFromU8 : core.convert.From subtle.Choice
  Std.U8 := {
  from_ := subtle.Choice.Insts.CoreConvertFromU8.from
}

/-- Trait implementation: [subtle::{impl subtle::ConstantTimeEq for u8}]
    Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/subtle-2.6.1/src/lib.rs', lines 346:8-346:36
    Name pattern: [subtle::ConstantTimeEq<u8>] -/
@[reducible, rust_trait_impl "subtle::ConstantTimeEq<u8>"]
def U8.Insts.SubtleConstantTimeEq : subtle.ConstantTimeEq Std.U8 := {
  ct_eq := U8.Insts.SubtleConstantTimeEq.ct_eq
}

/-- [curve25519_dalek::backend::serial::u64::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::from_limbs]:
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 258:4-260:5 -/
def backend.serial.u64.field.FieldElement51.from_limbs
  (limbs : Array Std.U64 5#usize) :
  Result backend.serial.u64.field.FieldElement51
  := do
  ok limbs

/-- [curve25519_dalek::backend::serial::u64::constants::SQRT_M1]
    Source: 'curve25519-dalek/src/backend/serial/u64/constants.rs', lines 89:0-95:3 -/
@[global_simps, irreducible]
def backend.serial.u64.constants.SQRT_M1
  : Result backend.serial.u64.field.FieldElement51 :=
  backend.serial.u64.field.FieldElement51.from_limbs
    (Array.make 5#usize [
      1718705420411056#u64, 234908883556509#u64, 2233514472574048#u64,
      2117202627021982#u64, 765476049583133#u64
      ])

/-- [curve25519_dalek::backend::serial::u64::field::{impl core::clone::Clone for curve25519_dalek::backend::serial::u64::field::FieldElement51}::clone]:
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 42:15-42:20
    Visibility: public -/
def backend.serial.u64.field.FieldElement51.Insts.CoreCloneClone.clone
  (self : backend.serial.u64.field.FieldElement51) :
  Result backend.serial.u64.field.FieldElement51
  := do
  ok self

/-- Trait implementation: [curve25519_dalek::backend::serial::u64::field::{impl core::clone::Clone for curve25519_dalek::backend::serial::u64::field::FieldElement51}]
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 42:15-42:20 -/
@[reducible]
def backend.serial.u64.field.FieldElement51.Insts.CoreCloneClone :
  core.clone.Clone backend.serial.u64.field.FieldElement51 := {
  clone := backend.serial.u64.field.FieldElement51.Insts.CoreCloneClone.clone
}

/-- Trait implementation: [curve25519_dalek::backend::serial::u64::field::{impl core::marker::Copy for curve25519_dalek::backend::serial::u64::field::FieldElement51}]
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 42:9-42:13 -/
@[reducible]
def backend.serial.u64.field.FieldElement51.Insts.CoreMarkerCopy :
  core.marker.Copy backend.serial.u64.field.FieldElement51 := {
  cloneInst := backend.serial.u64.field.FieldElement51.Insts.CoreCloneClone
}

/-- [curve25519_dalek::backend::serial::u64::field::{impl core::fmt::Debug for curve25519_dalek::backend::serial::u64::field::FieldElement51}::fmt]:
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 46:4-48:5
    Visibility: public -/
def backend.serial.u64.field.FieldElement51.Insts.CoreFmtDebug.fmt
  (self : backend.serial.u64.field.FieldElement51) (f : core.fmt.Formatter) :
  Result ((core.result.Result Unit core.fmt.Error) × core.fmt.Formatter)
  := do
  let args ←
    core.array.Array.index (core.ops.index.IndexSlice
      (core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice
      Std.U64)) self ()
  let a ←
    core.fmt.rt.Argument.new_debug (core.fmt.DebugShared
      (Slice.Insts.CoreFmtDebug core.fmt.DebugU64)) args
  let a1 ←
    core.fmt.Arguments.new
      (Array.make 20#usize [
        15#u8, 70#u8, 105#u8, 101#u8, 108#u8, 100#u8, 69#u8, 108#u8, 101#u8,
        109#u8, 101#u8, 110#u8, 116#u8, 53#u8, 49#u8, 40#u8, 192#u8, 1#u8,
        41#u8, 0#u8
        ]) (Array.make 1#usize [ a ])
  core.fmt.Formatter.write_fmt f a1

/-- Trait implementation: [curve25519_dalek::backend::serial::u64::field::{impl core::fmt::Debug for curve25519_dalek::backend::serial::u64::field::FieldElement51}]
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 45:0-49:1 -/
@[reducible]
def backend.serial.u64.field.FieldElement51.Insts.CoreFmtDebug : core.fmt.Debug
  backend.serial.u64.field.FieldElement51 := {
  fmt := backend.serial.u64.field.FieldElement51.Insts.CoreFmtDebug.fmt
}

/-- [curve25519_dalek::backend::serial::u64::field::{impl core::ops::arith::AddAssign<&'b curve25519_dalek::backend::serial::u64::field::FieldElement51> for curve25519_dalek::backend::serial::u64::field::FieldElement51}::add_assign]: loop body 0:
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 60:8-62:9
    Visibility: public -/
@[rust_loop_body]
def
  backend.serial.u64.field.FieldElement51.Insts.CoreOpsArithAddAssignSharedBFieldElement51.add_assign_loop.body
  (iter : core.ops.range.Range Std.Usize)
  (self : backend.serial.u64.field.FieldElement51)
  (_rhs : backend.serial.u64.field.FieldElement51) :
  Result (ControlFlow ((core.ops.range.Range Std.Usize) ×
    backend.serial.u64.field.FieldElement51 ×
    backend.serial.u64.field.FieldElement51)
    backend.serial.u64.field.FieldElement51)
  := do
  let (o, iter1) ←
    core.iter.range.IteratorRange.next core.iter.range.StepUsize iter
  match o with
  | none => ok (done self)
  | some i =>
    let i1 ← Array.index_usize _rhs i
    let i2 ← Array.index_usize self i
    let i3 ← i2 + i1
    let a ← Array.update self i i3
    ok (cont (iter1, a, _rhs))

/-- [curve25519_dalek::backend::serial::u64::field::{impl core::ops::arith::AddAssign<&'b curve25519_dalek::backend::serial::u64::field::FieldElement51> for curve25519_dalek::backend::serial::u64::field::FieldElement51}::add_assign]: loop 0:
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 60:8-62:9
    Visibility: public -/
@[rust_loop]
def
  backend.serial.u64.field.FieldElement51.Insts.CoreOpsArithAddAssignSharedBFieldElement51.add_assign_loop
  (iter : core.ops.range.Range Std.Usize)
  (self : backend.serial.u64.field.FieldElement51)
  (_rhs : backend.serial.u64.field.FieldElement51) :
  Result backend.serial.u64.field.FieldElement51
  := do
  loop
    (fun (iter1, self1, _rhs1) =>
      backend.serial.u64.field.FieldElement51.Insts.CoreOpsArithAddAssignSharedBFieldElement51.add_assign_loop.body
      iter1 self1 _rhs1)
    (iter, self, _rhs)

/-- [curve25519_dalek::backend::serial::u64::field::{impl core::ops::arith::AddAssign<&'b curve25519_dalek::backend::serial::u64::field::FieldElement51> for curve25519_dalek::backend::serial::u64::field::FieldElement51}::add_assign]:
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 59:4-63:5
    Visibility: public -/
@[reducible]
def
  backend.serial.u64.field.FieldElement51.Insts.CoreOpsArithAddAssignSharedBFieldElement51.add_assign
  (self : backend.serial.u64.field.FieldElement51)
  (_rhs : backend.serial.u64.field.FieldElement51) :
  Result backend.serial.u64.field.FieldElement51
  := do
  backend.serial.u64.field.FieldElement51.Insts.CoreOpsArithAddAssignSharedBFieldElement51.add_assign_loop
    { start := 0#usize, «end» := 5#usize } self _rhs

/-- Trait implementation: [curve25519_dalek::backend::serial::u64::field::{impl core::ops::arith::AddAssign<&'b curve25519_dalek::backend::serial::u64::field::FieldElement51> for curve25519_dalek::backend::serial::u64::field::FieldElement51}]
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 58:0-64:1 -/
@[reducible]
def
  backend.serial.u64.field.FieldElement51.Insts.CoreOpsArithAddAssignSharedBFieldElement51
  : core.ops.arith.AddAssign backend.serial.u64.field.FieldElement51
  backend.serial.u64.field.FieldElement51 := {
  add_assign :=
    backend.serial.u64.field.FieldElement51.Insts.CoreOpsArithAddAssignSharedBFieldElement51.add_assign
}

/-- [curve25519_dalek::backend::serial::u64::field::{impl core::ops::arith::Add<&'b curve25519_dalek::backend::serial::u64::field::FieldElement51, curve25519_dalek::backend::serial::u64::field::FieldElement51> for &'a curve25519_dalek::backend::serial::u64::field::FieldElement51}::add]:
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 68:4-72:5
    Visibility: public -/
def
  SharedAFieldElement51.Insts.CoreOpsArithAddSharedBFieldElement51FieldElement51.add
  (self : backend.serial.u64.field.FieldElement51)
  (_rhs : backend.serial.u64.field.FieldElement51) :
  Result backend.serial.u64.field.FieldElement51
  := do
  backend.serial.u64.field.FieldElement51.Insts.CoreOpsArithAddAssignSharedBFieldElement51.add_assign
    self _rhs

/-- Trait implementation: [curve25519_dalek::backend::serial::u64::field::{impl core::ops::arith::Add<&'b curve25519_dalek::backend::serial::u64::field::FieldElement51, curve25519_dalek::backend::serial::u64::field::FieldElement51> for &'a curve25519_dalek::backend::serial::u64::field::FieldElement51}]
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 66:0-73:1 -/
@[reducible]
def
  SharedAFieldElement51.Insts.CoreOpsArithAddSharedBFieldElement51FieldElement51
  : core.ops.arith.Add backend.serial.u64.field.FieldElement51
  backend.serial.u64.field.FieldElement51
  backend.serial.u64.field.FieldElement51 := {
  add :=
    SharedAFieldElement51.Insts.CoreOpsArithAddSharedBFieldElement51FieldElement51.add
}

/-- [curve25519_dalek::backend::serial::u64::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::reduce::LOW_51_BIT_MASK]
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 291:8-291:54 -/
@[global_simps, irreducible]
def backend.serial.u64.field.FieldElement51.reduce.LOW_51_BIT_MASK
  : Result Std.U64 := do
  let i ← 1#u64 <<< 51#i32
  i - 1#u64

/-- [curve25519_dalek::backend::serial::u64::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::reduce]:
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 290:4-323:5 -/
def backend.serial.u64.field.FieldElement51.reduce
  (limbs : Array Std.U64 5#usize) :
  Result backend.serial.u64.field.FieldElement51
  := do
  let i ← Array.index_usize limbs 0#usize
  let c0 ← i >>> 51#i32
  let i1 ← Array.index_usize limbs 1#usize
  let c1 ← i1 >>> 51#i32
  let i2 ← Array.index_usize limbs 2#usize
  let c2 ← i2 >>> 51#i32
  let i3 ← Array.index_usize limbs 3#usize
  let c3 ← i3 >>> 51#i32
  let i4 ← Array.index_usize limbs 4#usize
  let c4 ← i4 >>> 51#i32
  let i5 ← backend.serial.u64.field.FieldElement51.reduce.LOW_51_BIT_MASK
  let i6 ← lift (i &&& i5)
  let limbs1 ← Array.update limbs 0#usize i6
  let i7 ← Array.index_usize limbs1 1#usize
  let i8 ← lift (i7 &&& i5)
  let limbs2 ← Array.update limbs1 1#usize i8
  let i9 ← Array.index_usize limbs2 2#usize
  let i10 ← lift (i9 &&& i5)
  let limbs3 ← Array.update limbs2 2#usize i10
  let i11 ← Array.index_usize limbs3 3#usize
  let i12 ← lift (i11 &&& i5)
  let limbs4 ← Array.update limbs3 3#usize i12
  let i13 ← Array.index_usize limbs4 4#usize
  let i14 ← lift (i13 &&& i5)
  let limbs5 ← Array.update limbs4 4#usize i14
  let i15 ← c4 * 19#u64
  let i16 ← Array.index_usize limbs5 0#usize
  let i17 ← i16 + i15
  let limbs6 ← Array.update limbs5 0#usize i17
  let i18 ← Array.index_usize limbs6 1#usize
  let i19 ← i18 + c0
  let limbs7 ← Array.update limbs6 1#usize i19
  let i20 ← Array.index_usize limbs7 2#usize
  let i21 ← i20 + c1
  let limbs8 ← Array.update limbs7 2#usize i21
  let i22 ← Array.index_usize limbs8 3#usize
  let i23 ← i22 + c2
  let limbs9 ← Array.update limbs8 3#usize i23
  let i24 ← Array.index_usize limbs9 4#usize
  let i25 ← i24 + c3
  let limbs10 ← Array.update limbs9 4#usize i25
  ok limbs10

/-- [curve25519_dalek::backend::serial::u64::field::{impl core::ops::arith::Sub<&'b curve25519_dalek::backend::serial::u64::field::FieldElement51, curve25519_dalek::backend::serial::u64::field::FieldElement51> for &'a curve25519_dalek::backend::serial::u64::field::FieldElement51}::sub]:
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 84:4-101:5
    Visibility: public -/
def
  SharedAFieldElement51.Insts.CoreOpsArithSubSharedBFieldElement51FieldElement51.sub
  (self : backend.serial.u64.field.FieldElement51)
  (_rhs : backend.serial.u64.field.FieldElement51) :
  Result backend.serial.u64.field.FieldElement51
  := do
  let i ← Array.index_usize self 0#usize
  let i1 ← i + 36028797018963664#u64
  let i2 ← Array.index_usize _rhs 0#usize
  let i3 ← i1 - i2
  let i4 ← Array.index_usize self 1#usize
  let i5 ← i4 + 36028797018963952#u64
  let i6 ← Array.index_usize _rhs 1#usize
  let i7 ← i5 - i6
  let i8 ← Array.index_usize self 2#usize
  let i9 ← i8 + 36028797018963952#u64
  let i10 ← Array.index_usize _rhs 2#usize
  let i11 ← i9 - i10
  let i12 ← Array.index_usize self 3#usize
  let i13 ← i12 + 36028797018963952#u64
  let i14 ← Array.index_usize _rhs 3#usize
  let i15 ← i13 - i14
  let i16 ← Array.index_usize self 4#usize
  let i17 ← i16 + 36028797018963952#u64
  let i18 ← Array.index_usize _rhs 4#usize
  let i19 ← i17 - i18
  backend.serial.u64.field.FieldElement51.reduce
    (Array.make 5#usize [ i3, i7, i11, i15, i19 ])

/-- [curve25519_dalek::backend::serial::u64::field::{impl core::ops::arith::SubAssign<&'b curve25519_dalek::backend::serial::u64::field::FieldElement51> for curve25519_dalek::backend::serial::u64::field::FieldElement51}::sub_assign]:
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 76:4-79:5
    Visibility: public -/
def
  backend.serial.u64.field.FieldElement51.Insts.CoreOpsArithSubAssignSharedBFieldElement51.sub_assign
  (self : backend.serial.u64.field.FieldElement51)
  (_rhs : backend.serial.u64.field.FieldElement51) :
  Result backend.serial.u64.field.FieldElement51
  := do
  let result ←
    SharedAFieldElement51.Insts.CoreOpsArithSubSharedBFieldElement51FieldElement51.sub
      self _rhs
  ok result

/-- Trait implementation: [curve25519_dalek::backend::serial::u64::field::{impl core::ops::arith::SubAssign<&'b curve25519_dalek::backend::serial::u64::field::FieldElement51> for curve25519_dalek::backend::serial::u64::field::FieldElement51}]
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 75:0-80:1 -/
@[reducible]
def
  backend.serial.u64.field.FieldElement51.Insts.CoreOpsArithSubAssignSharedBFieldElement51
  : core.ops.arith.SubAssign backend.serial.u64.field.FieldElement51
  backend.serial.u64.field.FieldElement51 := {
  sub_assign :=
    backend.serial.u64.field.FieldElement51.Insts.CoreOpsArithSubAssignSharedBFieldElement51.sub_assign
}

/-- Trait implementation: [curve25519_dalek::backend::serial::u64::field::{impl core::ops::arith::Sub<&'b curve25519_dalek::backend::serial::u64::field::FieldElement51, curve25519_dalek::backend::serial::u64::field::FieldElement51> for &'a curve25519_dalek::backend::serial::u64::field::FieldElement51}]
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 82:0-102:1 -/
@[reducible]
def
  SharedAFieldElement51.Insts.CoreOpsArithSubSharedBFieldElement51FieldElement51
  : core.ops.arith.Sub backend.serial.u64.field.FieldElement51
  backend.serial.u64.field.FieldElement51
  backend.serial.u64.field.FieldElement51 := {
  sub :=
    SharedAFieldElement51.Insts.CoreOpsArithSubSharedBFieldElement51FieldElement51.sub
}

/-- [curve25519_dalek::backend::serial::u64::field::{impl core::ops::arith::Mul<&'b curve25519_dalek::backend::serial::u64::field::FieldElement51, curve25519_dalek::backend::serial::u64::field::FieldElement51> for &'a curve25519_dalek::backend::serial::u64::field::FieldElement51}::mul::LOW_51_BIT_MASK]
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 172:8-172:54 -/
@[global_simps, irreducible]
def
  backend.serial.u64.field.MulSharedAFieldElement51SharedBFieldElement51FieldElement51.mul.LOW_51_BIT_MASK
  : Result Std.U64 := do
  let i ← 1#u64 <<< 51#i32
  i - 1#u64

/-- [curve25519_dalek::backend::serial::u64::field::{impl core::ops::arith::Mul<&'b curve25519_dalek::backend::serial::u64::field::FieldElement51, curve25519_dalek::backend::serial::u64::field::FieldElement51> for &'a curve25519_dalek::backend::serial::u64::field::FieldElement51}::mul::m]:
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 119:8-119:66 -/
def
  backend.serial.u64.field.MulSharedAFieldElement51SharedBFieldElement51FieldElement51.mul.m
  (x : Std.U64) (y : Std.U64) : Result Std.U128 := do
  let i ← lift (UScalar.cast .U128 x)
  let i1 ← lift (UScalar.cast .U128 y)
  i * i1

/-- [curve25519_dalek::backend::serial::u64::field::{impl core::ops::arith::Mul<&'b curve25519_dalek::backend::serial::u64::field::FieldElement51, curve25519_dalek::backend::serial::u64::field::FieldElement51> for &'a curve25519_dalek::backend::serial::u64::field::FieldElement51}::mul]:
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 115:4-213:5
    Visibility: public -/
def
  SharedAFieldElement51.Insts.CoreOpsArithMulSharedBFieldElement51FieldElement51.mul
  (self : backend.serial.u64.field.FieldElement51)
  (_rhs : backend.serial.u64.field.FieldElement51) :
  Result backend.serial.u64.field.FieldElement51
  := do
  let i ← Array.index_usize _rhs 1#usize
  let b1_19 ← i * 19#u64
  let i1 ← Array.index_usize _rhs 2#usize
  let b2_19 ← i1 * 19#u64
  let i2 ← Array.index_usize _rhs 3#usize
  let b3_19 ← i2 * 19#u64
  let i3 ← Array.index_usize _rhs 4#usize
  let b4_19 ← i3 * 19#u64
  let i4 ← Array.index_usize self 0#usize
  let i5 ← Array.index_usize _rhs 0#usize
  let i6 ←
    backend.serial.u64.field.MulSharedAFieldElement51SharedBFieldElement51FieldElement51.mul.m
      i4 i5
  let i7 ← Array.index_usize self 4#usize
  let i8 ←
    backend.serial.u64.field.MulSharedAFieldElement51SharedBFieldElement51FieldElement51.mul.m
      i7 b1_19
  let i9 ← i6 + i8
  let i10 ← Array.index_usize self 3#usize
  let i11 ←
    backend.serial.u64.field.MulSharedAFieldElement51SharedBFieldElement51FieldElement51.mul.m
      i10 b2_19
  let i12 ← i9 + i11
  let i13 ← Array.index_usize self 2#usize
  let i14 ←
    backend.serial.u64.field.MulSharedAFieldElement51SharedBFieldElement51FieldElement51.mul.m
      i13 b3_19
  let i15 ← i12 + i14
  let i16 ← Array.index_usize self 1#usize
  let i17 ←
    backend.serial.u64.field.MulSharedAFieldElement51SharedBFieldElement51FieldElement51.mul.m
      i16 b4_19
  let c0 ← i15 + i17
  let i18 ←
    backend.serial.u64.field.MulSharedAFieldElement51SharedBFieldElement51FieldElement51.mul.m
      i16 i5
  let i19 ←
    backend.serial.u64.field.MulSharedAFieldElement51SharedBFieldElement51FieldElement51.mul.m
      i4 i
  let i20 ← i18 + i19
  let i21 ←
    backend.serial.u64.field.MulSharedAFieldElement51SharedBFieldElement51FieldElement51.mul.m
      i7 b2_19
  let i22 ← i20 + i21
  let i23 ←
    backend.serial.u64.field.MulSharedAFieldElement51SharedBFieldElement51FieldElement51.mul.m
      i10 b3_19
  let i24 ← i22 + i23
  let i25 ←
    backend.serial.u64.field.MulSharedAFieldElement51SharedBFieldElement51FieldElement51.mul.m
      i13 b4_19
  let c1 ← i24 + i25
  let i26 ←
    backend.serial.u64.field.MulSharedAFieldElement51SharedBFieldElement51FieldElement51.mul.m
      i13 i5
  let i27 ←
    backend.serial.u64.field.MulSharedAFieldElement51SharedBFieldElement51FieldElement51.mul.m
      i16 i
  let i28 ← i26 + i27
  let i29 ←
    backend.serial.u64.field.MulSharedAFieldElement51SharedBFieldElement51FieldElement51.mul.m
      i4 i1
  let i30 ← i28 + i29
  let i31 ←
    backend.serial.u64.field.MulSharedAFieldElement51SharedBFieldElement51FieldElement51.mul.m
      i7 b3_19
  let i32 ← i30 + i31
  let i33 ←
    backend.serial.u64.field.MulSharedAFieldElement51SharedBFieldElement51FieldElement51.mul.m
      i10 b4_19
  let c2 ← i32 + i33
  let i34 ←
    backend.serial.u64.field.MulSharedAFieldElement51SharedBFieldElement51FieldElement51.mul.m
      i10 i5
  let i35 ←
    backend.serial.u64.field.MulSharedAFieldElement51SharedBFieldElement51FieldElement51.mul.m
      i13 i
  let i36 ← i34 + i35
  let i37 ←
    backend.serial.u64.field.MulSharedAFieldElement51SharedBFieldElement51FieldElement51.mul.m
      i16 i1
  let i38 ← i36 + i37
  let i39 ←
    backend.serial.u64.field.MulSharedAFieldElement51SharedBFieldElement51FieldElement51.mul.m
      i4 i2
  let i40 ← i38 + i39
  let i41 ←
    backend.serial.u64.field.MulSharedAFieldElement51SharedBFieldElement51FieldElement51.mul.m
      i7 b4_19
  let c3 ← i40 + i41
  let i42 ←
    backend.serial.u64.field.MulSharedAFieldElement51SharedBFieldElement51FieldElement51.mul.m
      i7 i5
  let i43 ←
    backend.serial.u64.field.MulSharedAFieldElement51SharedBFieldElement51FieldElement51.mul.m
      i10 i
  let i44 ← i42 + i43
  let i45 ←
    backend.serial.u64.field.MulSharedAFieldElement51SharedBFieldElement51FieldElement51.mul.m
      i13 i1
  let i46 ← i44 + i45
  let i47 ←
    backend.serial.u64.field.MulSharedAFieldElement51SharedBFieldElement51FieldElement51.mul.m
      i16 i2
  let i48 ← i46 + i47
  let i49 ←
    backend.serial.u64.field.MulSharedAFieldElement51SharedBFieldElement51FieldElement51.mul.m
      i4 i3
  let c4 ← i48 + i49
  let i50 ← 1#u64 <<< 54#i32
  massert (i4 < i50)
  massert (i5 < i50)
  massert (i16 < i50)
  massert (i < i50)
  massert (i13 < i50)
  massert (i1 < i50)
  massert (i10 < i50)
  massert (i2 < i50)
  massert (i7 < i50)
  massert (i3 < i50)
  let out := Array.repeat 5#usize 0#u64
  let i51 ← c0 >>> 51#i32
  let i52 ← lift (UScalar.cast .U64 i51)
  let i53 ← lift (UScalar.cast .U128 i52)
  let c11 ← c1 + i53
  let i54 ← lift (UScalar.cast .U64 c0)
  let i55 ←
    backend.serial.u64.field.MulSharedAFieldElement51SharedBFieldElement51FieldElement51.mul.LOW_51_BIT_MASK
  let i56 ← lift (i54 &&& i55)
  let out1 ← Array.update out 0#usize i56
  let i57 ← c11 >>> 51#i32
  let i58 ← lift (UScalar.cast .U64 i57)
  let i59 ← lift (UScalar.cast .U128 i58)
  let c21 ← c2 + i59
  let i60 ← lift (UScalar.cast .U64 c11)
  let i61 ← lift (i60 &&& i55)
  let out2 ← Array.update out1 1#usize i61
  let i62 ← c21 >>> 51#i32
  let i63 ← lift (UScalar.cast .U64 i62)
  let i64 ← lift (UScalar.cast .U128 i63)
  let c31 ← c3 + i64
  let i65 ← lift (UScalar.cast .U64 c21)
  let i66 ← lift (i65 &&& i55)
  let out3 ← Array.update out2 2#usize i66
  let i67 ← c31 >>> 51#i32
  let i68 ← lift (UScalar.cast .U64 i67)
  let i69 ← lift (UScalar.cast .U128 i68)
  let c41 ← c4 + i69
  let i70 ← lift (UScalar.cast .U64 c31)
  let i71 ← lift (i70 &&& i55)
  let out4 ← Array.update out3 3#usize i71
  let i72 ← c41 >>> 51#i32
  let carry ← lift (UScalar.cast .U64 i72)
  let i73 ← lift (UScalar.cast .U64 c41)
  let i74 ← lift (i73 &&& i55)
  let out5 ← Array.update out4 4#usize i74
  let i75 ← carry * 19#u64
  let i76 ← Array.index_usize out5 0#usize
  let i77 ← i76 + i75
  let out6 ← Array.update out5 0#usize i77
  let i78 ← Array.index_usize out6 0#usize
  let i79 ← i78 >>> 51#i32
  let i80 ← Array.index_usize out6 1#usize
  let i81 ← i80 + i79
  let out7 ← Array.update out6 1#usize i81
  let i82 ← Array.index_usize out7 0#usize
  let i83 ← lift (i82 &&& i55)
  let out8 ← Array.update out7 0#usize i83
  ok out8

/-- [curve25519_dalek::backend::serial::u64::field::{impl core::ops::arith::MulAssign<&'b curve25519_dalek::backend::serial::u64::field::FieldElement51> for curve25519_dalek::backend::serial::u64::field::FieldElement51}::mul_assign]:
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 105:4-108:5
    Visibility: public -/
def
  backend.serial.u64.field.FieldElement51.Insts.CoreOpsArithMulAssignSharedBFieldElement51.mul_assign
  (self : backend.serial.u64.field.FieldElement51)
  (_rhs : backend.serial.u64.field.FieldElement51) :
  Result backend.serial.u64.field.FieldElement51
  := do
  let result ←
    SharedAFieldElement51.Insts.CoreOpsArithMulSharedBFieldElement51FieldElement51.mul
      self _rhs
  ok result

/-- Trait implementation: [curve25519_dalek::backend::serial::u64::field::{impl core::ops::arith::MulAssign<&'b curve25519_dalek::backend::serial::u64::field::FieldElement51> for curve25519_dalek::backend::serial::u64::field::FieldElement51}]
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 104:0-109:1 -/
@[reducible]
def
  backend.serial.u64.field.FieldElement51.Insts.CoreOpsArithMulAssignSharedBFieldElement51
  : core.ops.arith.MulAssign backend.serial.u64.field.FieldElement51
  backend.serial.u64.field.FieldElement51 := {
  mul_assign :=
    backend.serial.u64.field.FieldElement51.Insts.CoreOpsArithMulAssignSharedBFieldElement51.mul_assign
}

/-- Trait implementation: [curve25519_dalek::backend::serial::u64::field::{impl core::ops::arith::Mul<&'b curve25519_dalek::backend::serial::u64::field::FieldElement51, curve25519_dalek::backend::serial::u64::field::FieldElement51> for &'a curve25519_dalek::backend::serial::u64::field::FieldElement51}]
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 111:0-214:1 -/
@[reducible]
def
  SharedAFieldElement51.Insts.CoreOpsArithMulSharedBFieldElement51FieldElement51
  : core.ops.arith.Mul backend.serial.u64.field.FieldElement51
  backend.serial.u64.field.FieldElement51
  backend.serial.u64.field.FieldElement51 := {
  mul :=
    SharedAFieldElement51.Insts.CoreOpsArithMulSharedBFieldElement51FieldElement51.mul
}

/-- [curve25519_dalek::backend::serial::u64::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::negate]:
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 276:4-286:5
    Visibility: public -/
def backend.serial.u64.field.FieldElement51.negate
  (self : backend.serial.u64.field.FieldElement51) :
  Result backend.serial.u64.field.FieldElement51
  := do
  let i ← Array.index_usize self 0#usize
  let i1 ← 36028797018963664#u64 - i
  let i2 ← Array.index_usize self 1#usize
  let i3 ← 36028797018963952#u64 - i2
  let i4 ← Array.index_usize self 2#usize
  let i5 ← 36028797018963952#u64 - i4
  let i6 ← Array.index_usize self 3#usize
  let i7 ← 36028797018963952#u64 - i6
  let i8 ← Array.index_usize self 4#usize
  let i9 ← 36028797018963952#u64 - i8
  let neg ←
    backend.serial.u64.field.FieldElement51.reduce
      (Array.make 5#usize [ i1, i3, i5, i7, i9 ])
  ok neg

/-- [curve25519_dalek::backend::serial::u64::field::{impl core::ops::arith::Neg<curve25519_dalek::backend::serial::u64::field::FieldElement51> for &'a curve25519_dalek::backend::serial::u64::field::FieldElement51}::neg]:
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 218:4-222:5
    Visibility: public -/
def SharedAFieldElement51.Insts.CoreOpsArithNegFieldElement51.neg
  (self : backend.serial.u64.field.FieldElement51) :
  Result backend.serial.u64.field.FieldElement51
  := do
  backend.serial.u64.field.FieldElement51.negate self

/-- Trait implementation: [curve25519_dalek::backend::serial::u64::field::{impl core::ops::arith::Neg<curve25519_dalek::backend::serial::u64::field::FieldElement51> for &'a curve25519_dalek::backend::serial::u64::field::FieldElement51}]
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 216:0-223:1 -/
@[reducible]
def SharedAFieldElement51.Insts.CoreOpsArithNegFieldElement51 :
  core.ops.arith.Neg backend.serial.u64.field.FieldElement51
  backend.serial.u64.field.FieldElement51 := {
  neg := SharedAFieldElement51.Insts.CoreOpsArithNegFieldElement51.neg
}

/-- [curve25519_dalek::backend::serial::u64::field::{impl subtle::ConditionallySelectable for curve25519_dalek::backend::serial::u64::field::FieldElement51}::conditional_assign]:
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 248:4-254:5
    Visibility: public -/
def
  backend.serial.u64.field.FieldElement51.Insts.SubtleConditionallySelectable.conditional_assign
  (self : backend.serial.u64.field.FieldElement51)
  (other : backend.serial.u64.field.FieldElement51) (choice : subtle.Choice) :
  Result backend.serial.u64.field.FieldElement51
  := do
  let (i, index_mut_back) ← Array.index_mut_usize self 0#usize
  let i1 ← Array.index_usize other 0#usize
  let i2 ←
    U64.Insts.SubtleConditionallySelectable.conditional_assign i i1 choice
  let a := index_mut_back i2
  let (i3, index_mut_back1) ← Array.index_mut_usize a 1#usize
  let i4 ← Array.index_usize other 1#usize
  let i5 ←
    U64.Insts.SubtleConditionallySelectable.conditional_assign i3 i4 choice
  let a1 := index_mut_back1 i5
  let (i6, index_mut_back2) ← Array.index_mut_usize a1 2#usize
  let i7 ← Array.index_usize other 2#usize
  let i8 ←
    U64.Insts.SubtleConditionallySelectable.conditional_assign i6 i7 choice
  let a2 := index_mut_back2 i8
  let (i9, index_mut_back3) ← Array.index_mut_usize a2 3#usize
  let i10 ← Array.index_usize other 3#usize
  let i11 ←
    U64.Insts.SubtleConditionallySelectable.conditional_assign i9 i10 choice
  let a3 := index_mut_back3 i11
  let (i12, index_mut_back4) ← Array.index_mut_usize a3 4#usize
  let i13 ← Array.index_usize other 4#usize
  let i14 ←
    U64.Insts.SubtleConditionallySelectable.conditional_assign i12 i13 choice
  let a4 := index_mut_back4 i14
  ok a4

/-- [curve25519_dalek::backend::serial::u64::field::{impl subtle::ConditionallySelectable for curve25519_dalek::backend::serial::u64::field::FieldElement51}::conditional_swap]:
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 240:4-246:5
    Visibility: public -/
def
  backend.serial.u64.field.FieldElement51.Insts.SubtleConditionallySelectable.conditional_swap
  (a : backend.serial.u64.field.FieldElement51)
  (b : backend.serial.u64.field.FieldElement51) (choice : subtle.Choice) :
  Result (backend.serial.u64.field.FieldElement51 ×
    backend.serial.u64.field.FieldElement51)
  := do
  let (i, index_mut_back) ← Array.index_mut_usize a 0#usize
  let (i1, index_mut_back1) ← Array.index_mut_usize b 0#usize
  let (i2, i3) ←
    U64.Insts.SubtleConditionallySelectable.conditional_swap i i1 choice
  let a1 := index_mut_back i2
  let (i4, index_mut_back2) ← Array.index_mut_usize a1 1#usize
  let a2 := index_mut_back1 i3
  let (i5, index_mut_back3) ← Array.index_mut_usize a2 1#usize
  let (i6, i7) ←
    U64.Insts.SubtleConditionallySelectable.conditional_swap i4 i5 choice
  let a3 := index_mut_back2 i6
  let (i8, index_mut_back4) ← Array.index_mut_usize a3 2#usize
  let a4 := index_mut_back3 i7
  let (i9, index_mut_back5) ← Array.index_mut_usize a4 2#usize
  let (i10, i11) ←
    U64.Insts.SubtleConditionallySelectable.conditional_swap i8 i9 choice
  let a5 := index_mut_back4 i10
  let (i12, index_mut_back6) ← Array.index_mut_usize a5 3#usize
  let a6 := index_mut_back5 i11
  let (i13, index_mut_back7) ← Array.index_mut_usize a6 3#usize
  let (i14, i15) ←
    U64.Insts.SubtleConditionallySelectable.conditional_swap i12 i13 choice
  let a7 := index_mut_back6 i14
  let (i16, index_mut_back8) ← Array.index_mut_usize a7 4#usize
  let a8 := index_mut_back7 i15
  let (i17, index_mut_back9) ← Array.index_mut_usize a8 4#usize
  let (i18, i19) ←
    U64.Insts.SubtleConditionallySelectable.conditional_swap i16 i17 choice
  let a9 := index_mut_back8 i18
  let a10 := index_mut_back9 i19
  ok (a9, a10)

/-- [curve25519_dalek::backend::serial::u64::field::{impl subtle::ConditionallySelectable for curve25519_dalek::backend::serial::u64::field::FieldElement51}::conditional_select]:
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 226:4-238:5
    Visibility: public -/
def
  backend.serial.u64.field.FieldElement51.Insts.SubtleConditionallySelectable.conditional_select
  (a : backend.serial.u64.field.FieldElement51)
  (b : backend.serial.u64.field.FieldElement51) (choice : subtle.Choice) :
  Result backend.serial.u64.field.FieldElement51
  := do
  let i ← Array.index_usize a 0#usize
  let i1 ← Array.index_usize b 0#usize
  let i2 ←
    U64.Insts.SubtleConditionallySelectable.conditional_select i i1 choice
  let i3 ← Array.index_usize a 1#usize
  let i4 ← Array.index_usize b 1#usize
  let i5 ←
    U64.Insts.SubtleConditionallySelectable.conditional_select i3 i4 choice
  let i6 ← Array.index_usize a 2#usize
  let i7 ← Array.index_usize b 2#usize
  let i8 ←
    U64.Insts.SubtleConditionallySelectable.conditional_select i6 i7 choice
  let i9 ← Array.index_usize a 3#usize
  let i10 ← Array.index_usize b 3#usize
  let i11 ←
    U64.Insts.SubtleConditionallySelectable.conditional_select i9 i10 choice
  let i12 ← Array.index_usize a 4#usize
  let i13 ← Array.index_usize b 4#usize
  let i14 ←
    U64.Insts.SubtleConditionallySelectable.conditional_select i12 i13 choice
  ok (Array.make 5#usize [ i2, i5, i8, i11, i14 ])

/-- Trait implementation: [curve25519_dalek::backend::serial::u64::field::{impl subtle::ConditionallySelectable for curve25519_dalek::backend::serial::u64::field::FieldElement51}]
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 225:0-255:1 -/
@[reducible]
def backend.serial.u64.field.FieldElement51.Insts.SubtleConditionallySelectable
  : subtle.ConditionallySelectable backend.serial.u64.field.FieldElement51 := {
  coremarkerCopyInst :=
    backend.serial.u64.field.FieldElement51.Insts.CoreMarkerCopy
  conditional_select :=
    backend.serial.u64.field.FieldElement51.Insts.SubtleConditionallySelectable.conditional_select
  conditional_assign :=
    backend.serial.u64.field.FieldElement51.Insts.SubtleConditionallySelectable.conditional_assign
  conditional_swap :=
    backend.serial.u64.field.FieldElement51.Insts.SubtleConditionallySelectable.conditional_swap
}

/-- [curve25519_dalek::backend::serial::u64::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::ZERO]
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 263:4-263:81
    Visibility: public -/
@[global_simps, irreducible]
def backend.serial.u64.field.FieldElement51.ZERO
  : Result backend.serial.u64.field.FieldElement51 :=
  let a := Array.repeat 5#usize 0#u64
  backend.serial.u64.field.FieldElement51.from_limbs a

/-- [curve25519_dalek::backend::serial::u64::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::ONE]
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 265:4-265:80
    Visibility: public -/
@[global_simps, irreducible]
def backend.serial.u64.field.FieldElement51.ONE
  : Result backend.serial.u64.field.FieldElement51 :=
  backend.serial.u64.field.FieldElement51.from_limbs
    (Array.make 5#usize [ 1#u64, 0#u64, 0#u64, 0#u64, 0#u64 ])

/-- [curve25519_dalek::backend::serial::u64::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::MINUS_ONE]
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 267:4-273:7
    Visibility: public -/
@[global_simps, irreducible]
def backend.serial.u64.field.FieldElement51.MINUS_ONE
  : Result backend.serial.u64.field.FieldElement51 :=
  backend.serial.u64.field.FieldElement51.from_limbs
    (Array.make 5#usize [
      2251799813685228#u64, 2251799813685247#u64, 2251799813685247#u64,
      2251799813685247#u64, 2251799813685247#u64
      ])

/-- [curve25519_dalek::backend::serial::u64::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::from_bytes::{impl core::ops::function::Fn<(&'_ [u8],), u64> for curve25519_dalek::backend::serial::u64::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::from_bytes::closure}::call]:
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 339:20-348:9 -/
def
  backend.serial.u64.field.FieldElement51.from_bytes.closure.Insts.CoreOpsFunctionFnTupleSharedSliceU8U64.call
  (c : backend.serial.u64.field.FieldElement51.from_bytes.closure)
  (tupled_args : Slice Std.U8) :
  Result Std.U64
  := do
  let i ← Slice.index_usize tupled_args 0#usize
  let i1 ← lift (UScalar.cast .U64 i)
  let i2 ← Slice.index_usize tupled_args 1#usize
  let i3 ← lift (UScalar.cast .U64 i2)
  let i4 ← i3 <<< 8#i32
  let i5 ← lift (i1 ||| i4)
  let i6 ← Slice.index_usize tupled_args 2#usize
  let i7 ← lift (UScalar.cast .U64 i6)
  let i8 ← i7 <<< 16#i32
  let i9 ← lift (i5 ||| i8)
  let i10 ← Slice.index_usize tupled_args 3#usize
  let i11 ← lift (UScalar.cast .U64 i10)
  let i12 ← i11 <<< 24#i32
  let i13 ← lift (i9 ||| i12)
  let i14 ← Slice.index_usize tupled_args 4#usize
  let i15 ← lift (UScalar.cast .U64 i14)
  let i16 ← i15 <<< 32#i32
  let i17 ← lift (i13 ||| i16)
  let i18 ← Slice.index_usize tupled_args 5#usize
  let i19 ← lift (UScalar.cast .U64 i18)
  let i20 ← i19 <<< 40#i32
  let i21 ← lift (i17 ||| i20)
  let i22 ← Slice.index_usize tupled_args 6#usize
  let i23 ← lift (UScalar.cast .U64 i22)
  let i24 ← i23 <<< 48#i32
  let i25 ← lift (i21 ||| i24)
  let i26 ← Slice.index_usize tupled_args 7#usize
  let i27 ← lift (UScalar.cast .U64 i26)
  let i28 ← i27 <<< 56#i32
  ok (i25 ||| i28)

/-- [curve25519_dalek::backend::serial::u64::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::from_bytes]:
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 338:4-363:5
    Visibility: public -/
def backend.serial.u64.field.FieldElement51.from_bytes
  (bytes : Array Std.U8 32#usize) :
  Result backend.serial.u64.field.FieldElement51
  := do
  let i ← 1#u64 <<< 51#i32
  let low_51_bit_mask ← i - 1#u64
  let s ←
    core.array.Array.index (core.ops.index.IndexSlice
      (core.slice.index.SliceIndexRangeFromUsizeSlice Std.U8)) bytes
      { start := 0#usize }
  let i1 ←
    backend.serial.u64.field.FieldElement51.from_bytes.closure.Insts.CoreOpsFunctionFnTupleSharedSliceU8U64.call
      () s
  let i2 ← lift (i1 &&& low_51_bit_mask)
  let s1 ←
    core.array.Array.index (core.ops.index.IndexSlice
      (core.slice.index.SliceIndexRangeFromUsizeSlice Std.U8)) bytes
      { start := 6#usize }
  let i3 ←
    backend.serial.u64.field.FieldElement51.from_bytes.closure.Insts.CoreOpsFunctionFnTupleSharedSliceU8U64.call
      () s1
  let i4 ← i3 >>> 3#i32
  let i5 ← lift (i4 &&& low_51_bit_mask)
  let s2 ←
    core.array.Array.index (core.ops.index.IndexSlice
      (core.slice.index.SliceIndexRangeFromUsizeSlice Std.U8)) bytes
      { start := 12#usize }
  let i6 ←
    backend.serial.u64.field.FieldElement51.from_bytes.closure.Insts.CoreOpsFunctionFnTupleSharedSliceU8U64.call
      () s2
  let i7 ← i6 >>> 6#i32
  let i8 ← lift (i7 &&& low_51_bit_mask)
  let s3 ←
    core.array.Array.index (core.ops.index.IndexSlice
      (core.slice.index.SliceIndexRangeFromUsizeSlice Std.U8)) bytes
      { start := 19#usize }
  let i9 ←
    backend.serial.u64.field.FieldElement51.from_bytes.closure.Insts.CoreOpsFunctionFnTupleSharedSliceU8U64.call
      () s3
  let i10 ← i9 >>> 1#i32
  let i11 ← lift (i10 &&& low_51_bit_mask)
  let s4 ←
    core.array.Array.index (core.ops.index.IndexSlice
      (core.slice.index.SliceIndexRangeFromUsizeSlice Std.U8)) bytes
      { start := 24#usize }
  let i12 ←
    backend.serial.u64.field.FieldElement51.from_bytes.closure.Insts.CoreOpsFunctionFnTupleSharedSliceU8U64.call
      () s4
  let i13 ← i12 >>> 12#i32
  let i14 ← lift (i13 &&& low_51_bit_mask)
  ok (Array.make 5#usize [ i2, i5, i8, i11, i14 ])

/-- [curve25519_dalek::backend::serial::u64::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::from_bytes::{impl core::ops::function::FnMut<(&'_ [u8],), u64> for curve25519_dalek::backend::serial::u64::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::from_bytes::closure}::call_mut]:
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 339:20-348:9 -/
def
  backend.serial.u64.field.FieldElement51.from_bytes.closure.Insts.CoreOpsFunctionFnMutTupleSharedSliceU8U64.call_mut
  (state : backend.serial.u64.field.FieldElement51.from_bytes.closure)
  (args : Slice Std.U8) :
  Result (Std.U64 ×
    backend.serial.u64.field.FieldElement51.from_bytes.closure)
  := do
  let i ←
    backend.serial.u64.field.FieldElement51.from_bytes.closure.Insts.CoreOpsFunctionFnTupleSharedSliceU8U64.call
      state args
  ok (i, state)

/-- [curve25519_dalek::backend::serial::u64::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::from_bytes::{impl core::ops::function::FnOnce<(&'_ [u8],), u64> for curve25519_dalek::backend::serial::u64::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::from_bytes::closure}::call_once]:
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 339:20-348:9 -/
def
  backend.serial.u64.field.FieldElement51.from_bytes.closure.Insts.CoreOpsFunctionFnOnceTupleSharedSliceU8U64.call_once
  (c : backend.serial.u64.field.FieldElement51.from_bytes.closure)
  (s : Slice Std.U8) :
  Result Std.U64
  := do
  let (i, _) ←
    backend.serial.u64.field.FieldElement51.from_bytes.closure.Insts.CoreOpsFunctionFnMutTupleSharedSliceU8U64.call_mut
      c s
  ok i

/-- Trait implementation: [curve25519_dalek::backend::serial::u64::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::from_bytes::{impl core::ops::function::FnOnce<(&'_ [u8],), u64> for curve25519_dalek::backend::serial::u64::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::from_bytes::closure}]
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 339:20-348:9 -/
@[reducible]
def
  backend.serial.u64.field.FieldElement51.from_bytes.closure.Insts.CoreOpsFunctionFnOnceTupleSharedSliceU8U64
  : core.ops.function.FnOnce
  backend.serial.u64.field.FieldElement51.from_bytes.closure (Slice Std.U8)
  Std.U64 := {
  call_once :=
    backend.serial.u64.field.FieldElement51.from_bytes.closure.Insts.CoreOpsFunctionFnOnceTupleSharedSliceU8U64.call_once
}

/-- Trait implementation: [curve25519_dalek::backend::serial::u64::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::from_bytes::{impl core::ops::function::FnMut<(&'_ [u8],), u64> for curve25519_dalek::backend::serial::u64::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::from_bytes::closure}]
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 339:20-348:9 -/
@[reducible]
def
  backend.serial.u64.field.FieldElement51.from_bytes.closure.Insts.CoreOpsFunctionFnMutTupleSharedSliceU8U64
  : core.ops.function.FnMut
  backend.serial.u64.field.FieldElement51.from_bytes.closure (Slice Std.U8)
  Std.U64 := {
  FnOnceInst :=
    backend.serial.u64.field.FieldElement51.from_bytes.closure.Insts.CoreOpsFunctionFnOnceTupleSharedSliceU8U64
  call_mut :=
    backend.serial.u64.field.FieldElement51.from_bytes.closure.Insts.CoreOpsFunctionFnMutTupleSharedSliceU8U64.call_mut
}

/-- Trait implementation: [curve25519_dalek::backend::serial::u64::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::from_bytes::{impl core::ops::function::Fn<(&'_ [u8],), u64> for curve25519_dalek::backend::serial::u64::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::from_bytes::closure}]
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 339:20-348:9 -/
@[reducible]
def
  backend.serial.u64.field.FieldElement51.from_bytes.closure.Insts.CoreOpsFunctionFnTupleSharedSliceU8U64
  : core.ops.function.Fn
  backend.serial.u64.field.FieldElement51.from_bytes.closure (Slice Std.U8)
  Std.U64 := {
  FnMutInst :=
    backend.serial.u64.field.FieldElement51.from_bytes.closure.Insts.CoreOpsFunctionFnMutTupleSharedSliceU8U64
  call :=
    backend.serial.u64.field.FieldElement51.from_bytes.closure.Insts.CoreOpsFunctionFnTupleSharedSliceU8U64.call
}

/-- [curve25519_dalek::backend::serial::u64::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::as_bytes]:
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 368:4-450:5
    Visibility: public -/
def backend.serial.u64.field.FieldElement51.as_bytes
  (self : backend.serial.u64.field.FieldElement51) :
  Result (Array Std.U8 32#usize)
  := do
  let fe ← backend.serial.u64.field.FieldElement51.reduce self
  let i ← Array.index_usize fe 0#usize
  let i1 ← i + 19#u64
  let q ← i1 >>> 51#i32
  let i2 ← Array.index_usize fe 1#usize
  let i3 ← i2 + q
  let q1 ← i3 >>> 51#i32
  let i4 ← Array.index_usize fe 2#usize
  let i5 ← i4 + q1
  let q2 ← i5 >>> 51#i32
  let i6 ← Array.index_usize fe 3#usize
  let i7 ← i6 + q2
  let q3 ← i7 >>> 51#i32
  let i8 ← Array.index_usize fe 4#usize
  let i9 ← i8 + q3
  let q4 ← i9 >>> 51#i32
  let i10 ← 19#u64 * q4
  let i11 ← i + i10
  let limbs ← Array.update fe 0#usize i11
  let i12 ← 1#u64 <<< 51#i32
  let low_51_bit_mask ← i12 - 1#u64
  let i13 ← Array.index_usize limbs 0#usize
  let i14 ← i13 >>> 51#i32
  let i15 ← Array.index_usize limbs 1#usize
  let i16 ← i15 + i14
  let limbs1 ← Array.update limbs 1#usize i16
  let i17 ← Array.index_usize limbs1 0#usize
  let i18 ← lift (i17 &&& low_51_bit_mask)
  let limbs2 ← Array.update limbs1 0#usize i18
  let i19 ← Array.index_usize limbs2 1#usize
  let i20 ← i19 >>> 51#i32
  let i21 ← Array.index_usize limbs2 2#usize
  let i22 ← i21 + i20
  let limbs3 ← Array.update limbs2 2#usize i22
  let i23 ← Array.index_usize limbs3 1#usize
  let i24 ← lift (i23 &&& low_51_bit_mask)
  let limbs4 ← Array.update limbs3 1#usize i24
  let i25 ← Array.index_usize limbs4 2#usize
  let i26 ← i25 >>> 51#i32
  let i27 ← Array.index_usize limbs4 3#usize
  let i28 ← i27 + i26
  let limbs5 ← Array.update limbs4 3#usize i28
  let i29 ← Array.index_usize limbs5 2#usize
  let i30 ← lift (i29 &&& low_51_bit_mask)
  let limbs6 ← Array.update limbs5 2#usize i30
  let i31 ← Array.index_usize limbs6 3#usize
  let i32 ← i31 >>> 51#i32
  let i33 ← Array.index_usize limbs6 4#usize
  let i34 ← i33 + i32
  let limbs7 ← Array.update limbs6 4#usize i34
  let i35 ← Array.index_usize limbs7 3#usize
  let i36 ← lift (i35 &&& low_51_bit_mask)
  let limbs8 ← Array.update limbs7 3#usize i36
  let i37 ← Array.index_usize limbs8 4#usize
  let i38 ← lift (i37 &&& low_51_bit_mask)
  let limbs9 ← Array.update limbs8 4#usize i38
  let s := Array.repeat 32#usize 0#u8
  let i39 ← Array.index_usize limbs9 0#usize
  let i40 ← lift (UScalar.cast .U8 i39)
  let s1 ← Array.update s 0#usize i40
  let i41 ← i39 >>> 8#i32
  let i42 ← lift (UScalar.cast .U8 i41)
  let s2 ← Array.update s1 1#usize i42
  let i43 ← i39 >>> 16#i32
  let i44 ← lift (UScalar.cast .U8 i43)
  let s3 ← Array.update s2 2#usize i44
  let i45 ← i39 >>> 24#i32
  let i46 ← lift (UScalar.cast .U8 i45)
  let s4 ← Array.update s3 3#usize i46
  let i47 ← i39 >>> 32#i32
  let i48 ← lift (UScalar.cast .U8 i47)
  let s5 ← Array.update s4 4#usize i48
  let i49 ← i39 >>> 40#i32
  let i50 ← lift (UScalar.cast .U8 i49)
  let s6 ← Array.update s5 5#usize i50
  let i51 ← i39 >>> 48#i32
  let i52 ← Array.index_usize limbs9 1#usize
  let i53 ← i52 <<< 3#i32
  let i54 ← lift (i51 ||| i53)
  let i55 ← lift (UScalar.cast .U8 i54)
  let s7 ← Array.update s6 6#usize i55
  let i56 ← i52 >>> 5#i32
  let i57 ← lift (UScalar.cast .U8 i56)
  let s8 ← Array.update s7 7#usize i57
  let i58 ← i52 >>> 13#i32
  let i59 ← lift (UScalar.cast .U8 i58)
  let s9 ← Array.update s8 8#usize i59
  let i60 ← i52 >>> 21#i32
  let i61 ← lift (UScalar.cast .U8 i60)
  let s10 ← Array.update s9 9#usize i61
  let i62 ← i52 >>> 29#i32
  let i63 ← lift (UScalar.cast .U8 i62)
  let s11 ← Array.update s10 10#usize i63
  let i64 ← i52 >>> 37#i32
  let i65 ← lift (UScalar.cast .U8 i64)
  let s12 ← Array.update s11 11#usize i65
  let i66 ← i52 >>> 45#i32
  let i67 ← Array.index_usize limbs9 2#usize
  let i68 ← i67 <<< 6#i32
  let i69 ← lift (i66 ||| i68)
  let i70 ← lift (UScalar.cast .U8 i69)
  let s13 ← Array.update s12 12#usize i70
  let i71 ← i67 >>> 2#i32
  let i72 ← lift (UScalar.cast .U8 i71)
  let s14 ← Array.update s13 13#usize i72
  let i73 ← i67 >>> 10#i32
  let i74 ← lift (UScalar.cast .U8 i73)
  let s15 ← Array.update s14 14#usize i74
  let i75 ← i67 >>> 18#i32
  let i76 ← lift (UScalar.cast .U8 i75)
  let s16 ← Array.update s15 15#usize i76
  let i77 ← i67 >>> 26#i32
  let i78 ← lift (UScalar.cast .U8 i77)
  let s17 ← Array.update s16 16#usize i78
  let i79 ← i67 >>> 34#i32
  let i80 ← lift (UScalar.cast .U8 i79)
  let s18 ← Array.update s17 17#usize i80
  let i81 ← i67 >>> 42#i32
  let i82 ← lift (UScalar.cast .U8 i81)
  let s19 ← Array.update s18 18#usize i82
  let i83 ← i67 >>> 50#i32
  let i84 ← Array.index_usize limbs9 3#usize
  let i85 ← i84 <<< 1#i32
  let i86 ← lift (i83 ||| i85)
  let i87 ← lift (UScalar.cast .U8 i86)
  let s20 ← Array.update s19 19#usize i87
  let i88 ← i84 >>> 7#i32
  let i89 ← lift (UScalar.cast .U8 i88)
  let s21 ← Array.update s20 20#usize i89
  let i90 ← i84 >>> 15#i32
  let i91 ← lift (UScalar.cast .U8 i90)
  let s22 ← Array.update s21 21#usize i91
  let i92 ← i84 >>> 23#i32
  let i93 ← lift (UScalar.cast .U8 i92)
  let s23 ← Array.update s22 22#usize i93
  let i94 ← i84 >>> 31#i32
  let i95 ← lift (UScalar.cast .U8 i94)
  let s24 ← Array.update s23 23#usize i95
  let i96 ← i84 >>> 39#i32
  let i97 ← lift (UScalar.cast .U8 i96)
  let s25 ← Array.update s24 24#usize i97
  let i98 ← i84 >>> 47#i32
  let i99 ← Array.index_usize limbs9 4#usize
  let i100 ← i99 <<< 4#i32
  let i101 ← lift (i98 ||| i100)
  let i102 ← lift (UScalar.cast .U8 i101)
  let s26 ← Array.update s25 25#usize i102
  let i103 ← i99 >>> 4#i32
  let i104 ← lift (UScalar.cast .U8 i103)
  let s27 ← Array.update s26 26#usize i104
  let i105 ← i99 >>> 12#i32
  let i106 ← lift (UScalar.cast .U8 i105)
  let s28 ← Array.update s27 27#usize i106
  let i107 ← i99 >>> 20#i32
  let i108 ← lift (UScalar.cast .U8 i107)
  let s29 ← Array.update s28 28#usize i108
  let i109 ← i99 >>> 28#i32
  let i110 ← lift (UScalar.cast .U8 i109)
  let s30 ← Array.update s29 29#usize i110
  let i111 ← i99 >>> 36#i32
  let i112 ← lift (UScalar.cast .U8 i111)
  let s31 ← Array.update s30 30#usize i112
  let i113 ← i99 >>> 44#i32
  let i114 ← lift (UScalar.cast .U8 i113)
  let s32 ← Array.update s31 31#usize i114
  let i115 ← Array.index_usize s32 31#usize
  let i116 ← lift (i115 &&& 128#u8)
  massert (i116 = 0#u8)
  ok s32

/-- [curve25519_dalek::backend::serial::u64::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::pow2k::LOW_51_BIT_MASK]
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 511:12-511:58 -/
@[global_simps, irreducible]
def backend.serial.u64.field.FieldElement51.pow2k.LOW_51_BIT_MASK
  : Result Std.U64 := do
  let i ← 1#u64 <<< 51#i32
  i - 1#u64

/-- [curve25519_dalek::backend::serial::u64::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::pow2k::m]:
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 460:8-462:9 -/
def backend.serial.u64.field.FieldElement51.pow2k.m
  (x : Std.U64) (y : Std.U64) : Result Std.U128 := do
  let i ← lift (UScalar.cast .U128 x)
  let i1 ← lift (UScalar.cast .U128 y)
  i * i1

/-- [curve25519_dalek::backend::serial::u64::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::pow2k]: loop body 0:
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 480:16-492:86
    Visibility: public -/
@[rust_loop_body]
def backend.serial.u64.field.FieldElement51.pow2k_loop.body
  (k : Std.U32) (a : Array Std.U64 5#usize) :
  Result (ControlFlow (Std.U32 × (Array Std.U64 5#usize)) (Array Std.U64
    5#usize))
  := do
  let i ← Array.index_usize a 3#usize
  let a3_19 ← 19#u64 * i
  let i1 ← Array.index_usize a 4#usize
  let a4_19 ← 19#u64 * i1
  let i2 ← Array.index_usize a 0#usize
  let i3 ← backend.serial.u64.field.FieldElement51.pow2k.m i2 i2
  let i4 ← Array.index_usize a 1#usize
  let i5 ← backend.serial.u64.field.FieldElement51.pow2k.m i4 a4_19
  let i6 ← Array.index_usize a 2#usize
  let i7 ← backend.serial.u64.field.FieldElement51.pow2k.m i6 a3_19
  let i8 ← i5 + i7
  let i9 ← 2#u128 * i8
  let c0 ← i3 + i9
  let i10 ← backend.serial.u64.field.FieldElement51.pow2k.m i a3_19
  let i11 ← backend.serial.u64.field.FieldElement51.pow2k.m i2 i4
  let i12 ← backend.serial.u64.field.FieldElement51.pow2k.m i6 a4_19
  let i13 ← i11 + i12
  let i14 ← 2#u128 * i13
  let c1 ← i10 + i14
  let i15 ← backend.serial.u64.field.FieldElement51.pow2k.m i4 i4
  let i16 ← backend.serial.u64.field.FieldElement51.pow2k.m i2 i6
  let i17 ← backend.serial.u64.field.FieldElement51.pow2k.m i1 a3_19
  let i18 ← i16 + i17
  let i19 ← 2#u128 * i18
  let c2 ← i15 + i19
  let i20 ← backend.serial.u64.field.FieldElement51.pow2k.m i1 a4_19
  let i21 ← backend.serial.u64.field.FieldElement51.pow2k.m i2 i
  let i22 ← backend.serial.u64.field.FieldElement51.pow2k.m i4 i6
  let i23 ← i21 + i22
  let i24 ← 2#u128 * i23
  let c3 ← i20 + i24
  let i25 ← backend.serial.u64.field.FieldElement51.pow2k.m i6 i6
  let i26 ← backend.serial.u64.field.FieldElement51.pow2k.m i2 i1
  let i27 ← backend.serial.u64.field.FieldElement51.pow2k.m i4 i
  let i28 ← i26 + i27
  let i29 ← 2#u128 * i28
  let c4 ← i25 + i29
  let i30 ← 1#u64 <<< 54#i32
  massert (i2 < i30)
  massert (i4 < i30)
  massert (i6 < i30)
  massert (i < i30)
  massert (i1 < i30)
  let i31 ← c0 >>> 51#i32
  let i32 ← lift (UScalar.cast .U64 i31)
  let i33 ← lift (UScalar.cast .U128 i32)
  let c11 ← c1 + i33
  let i34 ← lift (UScalar.cast .U64 c0)
  let i35 ← backend.serial.u64.field.FieldElement51.pow2k.LOW_51_BIT_MASK
  let i36 ← lift (i34 &&& i35)
  let a1 ← Array.update a 0#usize i36
  let i37 ← c11 >>> 51#i32
  let i38 ← lift (UScalar.cast .U64 i37)
  let i39 ← lift (UScalar.cast .U128 i38)
  let c21 ← c2 + i39
  let i40 ← lift (UScalar.cast .U64 c11)
  let i41 ← lift (i40 &&& i35)
  let a2 ← Array.update a1 1#usize i41
  let i42 ← c21 >>> 51#i32
  let i43 ← lift (UScalar.cast .U64 i42)
  let i44 ← lift (UScalar.cast .U128 i43)
  let c31 ← c3 + i44
  let i45 ← lift (UScalar.cast .U64 c21)
  let i46 ← lift (i45 &&& i35)
  let a3 ← Array.update a2 2#usize i46
  let i47 ← c31 >>> 51#i32
  let i48 ← lift (UScalar.cast .U64 i47)
  let i49 ← lift (UScalar.cast .U128 i48)
  let c41 ← c4 + i49
  let i50 ← lift (UScalar.cast .U64 c31)
  let i51 ← lift (i50 &&& i35)
  let a4 ← Array.update a3 3#usize i51
  let i52 ← c41 >>> 51#i32
  let carry ← lift (UScalar.cast .U64 i52)
  let i53 ← lift (UScalar.cast .U64 c41)
  let i54 ← lift (i53 &&& i35)
  let a5 ← Array.update a4 4#usize i54
  let i55 ← carry * 19#u64
  let i56 ← Array.index_usize a5 0#usize
  let i57 ← i56 + i55
  let a6 ← Array.update a5 0#usize i57
  let i58 ← Array.index_usize a6 0#usize
  let i59 ← i58 >>> 51#i32
  let i60 ← Array.index_usize a6 1#usize
  let i61 ← i60 + i59
  let a7 ← Array.update a6 1#usize i61
  let i62 ← Array.index_usize a7 0#usize
  let i63 ← lift (i62 &&& i35)
  let (_, index_mut_back) ← Array.index_mut_usize a7 0#usize
  let k1 ← k - 1#u32
  if k1 = 0#u32
  then let a8 := index_mut_back i63
       ok (done a8)
  else let a8 := index_mut_back i63
       ok (cont (k1, a8))

/-- [curve25519_dalek::backend::serial::u64::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::pow2k]: loop 0:
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 480:16-492:86
    Visibility: public -/
@[rust_loop]
def backend.serial.u64.field.FieldElement51.pow2k_loop
  (k : Std.U32) (a : Array Std.U64 5#usize) :
  Result (Array Std.U64 5#usize)
  := do
  loop
    (fun (k1, a1) => backend.serial.u64.field.FieldElement51.pow2k_loop.body k1
      a1)
    (k, a)

/-- [curve25519_dalek::backend::serial::u64::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::pow2k]:
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 454:4-559:5
    Visibility: public -/
def backend.serial.u64.field.FieldElement51.pow2k
  (self : backend.serial.u64.field.FieldElement51) (k : Std.U32) :
  Result backend.serial.u64.field.FieldElement51
  := do
  massert (k > 0#u32)
  let a ← backend.serial.u64.field.FieldElement51.pow2k_loop k self
  ok a

/-- [curve25519_dalek::backend::serial::u64::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::square]:
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 562:4-564:5
    Visibility: public -/
def backend.serial.u64.field.FieldElement51.square
  (self : backend.serial.u64.field.FieldElement51) :
  Result backend.serial.u64.field.FieldElement51
  := do
  backend.serial.u64.field.FieldElement51.pow2k self 1#u32

/-- [curve25519_dalek::backend::serial::u64::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::square2]: loop body 0:
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 569:8-571:9
    Visibility: public -/
@[rust_loop_body]
def backend.serial.u64.field.FieldElement51.square2_loop.body
  (iter : core.ops.range.Range Std.Usize)
  (square : backend.serial.u64.field.FieldElement51) :
  Result (ControlFlow ((core.ops.range.Range Std.Usize) ×
    backend.serial.u64.field.FieldElement51)
    backend.serial.u64.field.FieldElement51)
  := do
  let (o, iter1) ←
    core.iter.range.IteratorRange.next core.iter.range.StepUsize iter
  match o with
  | none => ok (done square)
  | some i =>
    let i1 ← Array.index_usize square i
    let i2 ← i1 * 2#u64
    let a ← Array.update square i i2
    ok (cont (iter1, a))

/-- [curve25519_dalek::backend::serial::u64::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::square2]: loop 0:
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 569:8-571:9
    Visibility: public -/
@[rust_loop]
def backend.serial.u64.field.FieldElement51.square2_loop
  (iter : core.ops.range.Range Std.Usize)
  (square : backend.serial.u64.field.FieldElement51) :
  Result backend.serial.u64.field.FieldElement51
  := do
  loop
    (fun (iter1, square1) =>
      backend.serial.u64.field.FieldElement51.square2_loop.body iter1 square1)
    (iter, square)

/-- [curve25519_dalek::backend::serial::u64::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::square2]:
    Source: 'curve25519-dalek/src/backend/serial/u64/field.rs', lines 567:4-574:5
    Visibility: public -/
def backend.serial.u64.field.FieldElement51.square2
  (self : backend.serial.u64.field.FieldElement51) :
  Result backend.serial.u64.field.FieldElement51
  := do
  let square ← backend.serial.u64.field.FieldElement51.pow2k self 1#u32
  backend.serial.u64.field.FieldElement51.square2_loop
    { start := 0#usize, «end» := 5#usize } square

/-- [curve25519_dalek::field::{impl subtle::ConstantTimeEq for curve25519_dalek::backend::serial::u64::field::FieldElement51}::ct_eq]:
    Source: 'curve25519-dalek/src/field.rs', lines 96:4-98:5
    Visibility: public -/
def backend.serial.u64.field.FieldElement51.Insts.SubtleConstantTimeEq.ct_eq
  (self : backend.serial.u64.field.FieldElement51)
  (other : backend.serial.u64.field.FieldElement51) :
  Result subtle.Choice
  := do
  let a ← backend.serial.u64.field.FieldElement51.as_bytes self
  let s ← lift (Array.to_slice a)
  let a1 ← backend.serial.u64.field.FieldElement51.as_bytes other
  let s1 ← lift (Array.to_slice a1)
  Slice.Insts.SubtleConstantTimeEq.ct_eq U8.Insts.SubtleConstantTimeEq s s1

/-- [curve25519_dalek::field::{impl core::cmp::PartialEq<curve25519_dalek::backend::serial::u64::field::FieldElement51> for curve25519_dalek::backend::serial::u64::field::FieldElement51}::eq]:
    Source: 'curve25519-dalek/src/field.rs', lines 87:4-89:5
    Visibility: public -/
def
  backend.serial.u64.field.FieldElement51.Insts.CoreCmpPartialEqFieldElement51.eq
  (self : backend.serial.u64.field.FieldElement51)
  (other : backend.serial.u64.field.FieldElement51) :
  Result Bool
  := do
  let c ←
    backend.serial.u64.field.FieldElement51.Insts.SubtleConstantTimeEq.ct_eq
      self other
  core.convert.IntoFrom.into Bool.Insts.CoreConvertFromChoice c

/-- Trait implementation: [curve25519_dalek::field::{impl core::cmp::PartialEq<curve25519_dalek::backend::serial::u64::field::FieldElement51> for curve25519_dalek::backend::serial::u64::field::FieldElement51}]
    Source: 'curve25519-dalek/src/field.rs', lines 86:0-90:1 -/
@[reducible]
def
  backend.serial.u64.field.FieldElement51.Insts.CoreCmpPartialEqFieldElement51
  : core.cmp.PartialEq backend.serial.u64.field.FieldElement51
  backend.serial.u64.field.FieldElement51 := {
  eq :=
    backend.serial.u64.field.FieldElement51.Insts.CoreCmpPartialEqFieldElement51.eq
}

/-- Trait implementation: [curve25519_dalek::field::{impl core::cmp::Eq for curve25519_dalek::backend::serial::u64::field::FieldElement51}]
    Source: 'curve25519-dalek/src/field.rs', lines 84:0-84:27 -/
@[reducible]
def backend.serial.u64.field.FieldElement51.Insts.CoreCmpEq : core.cmp.Eq
  backend.serial.u64.field.FieldElement51 := {
  partialEqInst :=
    backend.serial.u64.field.FieldElement51.Insts.CoreCmpPartialEqFieldElement51
}

/-- Trait implementation: [curve25519_dalek::field::{impl subtle::ConstantTimeEq for curve25519_dalek::backend::serial::u64::field::FieldElement51}]
    Source: 'curve25519-dalek/src/field.rs', lines 92:0-99:1 -/
@[reducible]
def backend.serial.u64.field.FieldElement51.Insts.SubtleConstantTimeEq :
  subtle.ConstantTimeEq backend.serial.u64.field.FieldElement51 := {
  ct_eq :=
    backend.serial.u64.field.FieldElement51.Insts.SubtleConstantTimeEq.ct_eq
}

/-- [curve25519_dalek::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::is_negative]:
    Source: 'curve25519-dalek/src/field.rs', lines 109:4-112:5 -/
def field.FieldElement51.is_negative
  (self : backend.serial.u64.field.FieldElement51) : Result subtle.Choice := do
  let bytes ← backend.serial.u64.field.FieldElement51.as_bytes self
  let i ← Array.index_usize bytes 0#usize
  let i1 ← lift (i &&& 1#u8)
  core.convert.IntoFrom.into subtle.Choice.Insts.CoreConvertFromU8 i1

/-- [curve25519_dalek::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::is_zero]:
    Source: 'curve25519-dalek/src/field.rs', lines 119:4-124:5 -/
def field.FieldElement51.is_zero
  (self : backend.serial.u64.field.FieldElement51) : Result subtle.Choice := do
  let zero := Array.repeat 32#usize 0#u8
  let bytes ← backend.serial.u64.field.FieldElement51.as_bytes self
  let s ← lift (Array.to_slice bytes)
  let s1 ← lift (Array.to_slice zero)
  Slice.Insts.SubtleConstantTimeEq.ct_eq U8.Insts.SubtleConstantTimeEq s s1

/-- [curve25519_dalek::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::pow22501]:
    Source: 'curve25519-dalek/src/field.rs', lines 129:4-163:5 -/
def field.FieldElement51.pow22501
  (self : backend.serial.u64.field.FieldElement51) :
  Result (backend.serial.u64.field.FieldElement51 ×
    backend.serial.u64.field.FieldElement51)
  := do
  let t0 ← backend.serial.u64.field.FieldElement51.square self
  let fe ← backend.serial.u64.field.FieldElement51.square t0
  let t1 ← backend.serial.u64.field.FieldElement51.square fe
  let t2 ←
    SharedAFieldElement51.Insts.CoreOpsArithMulSharedBFieldElement51FieldElement51.mul
      self t1
  let t3 ←
    SharedAFieldElement51.Insts.CoreOpsArithMulSharedBFieldElement51FieldElement51.mul
      t0 t2
  let t4 ← backend.serial.u64.field.FieldElement51.square t3
  let t5 ←
    SharedAFieldElement51.Insts.CoreOpsArithMulSharedBFieldElement51FieldElement51.mul
      t2 t4
  let t6 ← backend.serial.u64.field.FieldElement51.pow2k t5 5#u32
  let t7 ←
    SharedAFieldElement51.Insts.CoreOpsArithMulSharedBFieldElement51FieldElement51.mul
      t6 t5
  let t8 ← backend.serial.u64.field.FieldElement51.pow2k t7 10#u32
  let t9 ←
    SharedAFieldElement51.Insts.CoreOpsArithMulSharedBFieldElement51FieldElement51.mul
      t8 t7
  let t10 ← backend.serial.u64.field.FieldElement51.pow2k t9 20#u32
  let t11 ←
    SharedAFieldElement51.Insts.CoreOpsArithMulSharedBFieldElement51FieldElement51.mul
      t10 t9
  let t12 ← backend.serial.u64.field.FieldElement51.pow2k t11 10#u32
  let t13 ←
    SharedAFieldElement51.Insts.CoreOpsArithMulSharedBFieldElement51FieldElement51.mul
      t12 t7
  let t14 ← backend.serial.u64.field.FieldElement51.pow2k t13 50#u32
  let t15 ←
    SharedAFieldElement51.Insts.CoreOpsArithMulSharedBFieldElement51FieldElement51.mul
      t14 t13
  let t16 ← backend.serial.u64.field.FieldElement51.pow2k t15 100#u32
  let t17 ←
    SharedAFieldElement51.Insts.CoreOpsArithMulSharedBFieldElement51FieldElement51.mul
      t16 t15
  let t18 ← backend.serial.u64.field.FieldElement51.pow2k t17 50#u32
  let t19 ←
    SharedAFieldElement51.Insts.CoreOpsArithMulSharedBFieldElement51FieldElement51.mul
      t18 t13
  ok (t19, t3)

/-- [curve25519_dalek::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::invert]:
    Source: 'curve25519-dalek/src/field.rs', lines 214:4-223:5 -/
def field.FieldElement51.invert
  (self : backend.serial.u64.field.FieldElement51) :
  Result backend.serial.u64.field.FieldElement51
  := do
  let (t19, t3) ← field.FieldElement51.pow22501 self
  let t20 ← backend.serial.u64.field.FieldElement51.pow2k t19 5#u32
  SharedAFieldElement51.Insts.CoreOpsArithMulSharedBFieldElement51FieldElement51.mul
    t20 t3

/-- [curve25519_dalek::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::pow_p58]:
    Source: 'curve25519-dalek/src/field.rs', lines 228:4-237:5 -/
def field.FieldElement51.pow_p58
  (self : backend.serial.u64.field.FieldElement51) :
  Result backend.serial.u64.field.FieldElement51
  := do
  let (t19, _) ← field.FieldElement51.pow22501 self
  let t20 ← backend.serial.u64.field.FieldElement51.pow2k t19 2#u32
  SharedAFieldElement51.Insts.CoreOpsArithMulSharedBFieldElement51FieldElement51.mul
    self t20

/-- [curve25519_dalek::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::sqrt_ratio_i]:
    Source: 'curve25519-dalek/src/field.rs', lines 251:4-297:5 -/
def field.FieldElement51.sqrt_ratio_i
  (u : backend.serial.u64.field.FieldElement51)
  (v : backend.serial.u64.field.FieldElement51) :
  Result (subtle.Choice × backend.serial.u64.field.FieldElement51)
  := do
  let fe ← backend.serial.u64.field.FieldElement51.square v
  let v3 ←
    SharedAFieldElement51.Insts.CoreOpsArithMulSharedBFieldElement51FieldElement51.mul
      fe v
  let fe1 ← backend.serial.u64.field.FieldElement51.square v3
  let v7 ←
    SharedAFieldElement51.Insts.CoreOpsArithMulSharedBFieldElement51FieldElement51.mul
      fe1 v
  let fe2 ←
    SharedAFieldElement51.Insts.CoreOpsArithMulSharedBFieldElement51FieldElement51.mul
      u v3
  let fe3 ←
    SharedAFieldElement51.Insts.CoreOpsArithMulSharedBFieldElement51FieldElement51.mul
      u v7
  let fe4 ← field.FieldElement51.pow_p58 fe3
  let r ←
    SharedAFieldElement51.Insts.CoreOpsArithMulSharedBFieldElement51FieldElement51.mul
      fe2 fe4
  let fe5 ← backend.serial.u64.field.FieldElement51.square r
  let check ←
    SharedAFieldElement51.Insts.CoreOpsArithMulSharedBFieldElement51FieldElement51.mul
      v fe5
  let i ← backend.serial.u64.constants.SQRT_M1
  let correct_sign_sqrt ←
    backend.serial.u64.field.FieldElement51.Insts.SubtleConstantTimeEq.ct_eq
      check u
  let fe6 ← SharedAFieldElement51.Insts.CoreOpsArithNegFieldElement51.neg u
  let flipped_sign_sqrt ←
    backend.serial.u64.field.FieldElement51.Insts.SubtleConstantTimeEq.ct_eq
      check fe6
  let fe7 ←
    SharedAFieldElement51.Insts.CoreOpsArithMulSharedBFieldElement51FieldElement51.mul
      fe6 i
  let flipped_sign_sqrt_i ←
    backend.serial.u64.field.FieldElement51.Insts.SubtleConstantTimeEq.ct_eq
      check fe7
  let r_prime ←
    SharedAFieldElement51.Insts.CoreOpsArithMulSharedBFieldElement51FieldElement51.mul
      i r
  let c ←
    subtle.Choice.Insts.CoreOpsBitBitOrChoiceChoice.bitor flipped_sign_sqrt
      flipped_sign_sqrt_i
  let r1 ←
    backend.serial.u64.field.FieldElement51.Insts.SubtleConditionallySelectable.conditional_assign
      r r_prime c
  let r_is_negative ← field.FieldElement51.is_negative r1
  let r_neg ←
    SharedAFieldElement51.Insts.CoreOpsArithNegFieldElement51.neg r1
  let r2 ←
    backend.serial.u64.field.FieldElement51.Insts.SubtleConditionallySelectable.conditional_assign
      r1 r_neg r_is_negative
  let was_nonzero_square ←
    subtle.Choice.Insts.CoreOpsBitBitOrChoiceChoice.bitor correct_sign_sqrt
      flipped_sign_sqrt
  ok (was_nonzero_square, r2)

/-- [curve25519_dalek::field::{curve25519_dalek::backend::serial::u64::field::FieldElement51}::invsqrt]:
    Source: 'curve25519-dalek/src/field.rs', lines 311:4-313:5 -/
def field.FieldElement51.invsqrt
  (self : backend.serial.u64.field.FieldElement51) :
  Result (subtle.Choice × backend.serial.u64.field.FieldElement51)
  := do
  let fe ← backend.serial.u64.field.FieldElement51.ONE
  field.FieldElement51.sqrt_ratio_i fe self

end curve25519_dalek