val int_to_natN (n:pos) (i:int) : j:natN n{0 <= i /\ i < n ==> i == j}
let int_to_natN n i = i % n
val int_to_natN (n:pos) (i:int) : j:natN n{0 <= i /\ i < n ==> i == j}
let int_to_natN n i =
i % n
Vale.Def.Words_s.fst.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Def.Words_s.fst
Prims.pos Prims.int Prims.op_Modulus Vale.Def.Words_s.natN Prims.l_imp Prims.l_and Prims.b2t Prims.op_LessThanOrEqual Prims.op_LessThan Prims.eq2
module Vale.Def.Words_s
open FStar.Mul

// Sanity check our constants
let _ = assert_norm (pow2 8 = pow2_8)
let _ = assert_norm (pow2 16 = pow2_16)
let _ = assert_norm (pow2 32 = pow2_32)
let _ = assert_norm (pow2 64 = pow2_64)
let _ = assert_norm (pow2 128 = pow2_128)
val int_to_natN (n:pos) (i:int) : j:natN n{0 <= i /\ i < n ==> i == j}
n: Prims.pos -> i: Prims.int -> j: Vale.Def.Words_s.natN n {0 <= i /\ i < n ==> i == j}