Home
last modified time | relevance | path

Searched refs:flat (Results 1 – 1 of 1) sorted by relevance

/mbedtls-3.4.0/3rdparty/everest/library/kremlib/
DFStar_UInt128_extracted.c38 flat = { a.low + b.low, a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low) }; in FStar_UInt128_add() local
39 return flat; in FStar_UInt128_add()
46 flat = { a.low + b.low, a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low) }; in FStar_UInt128_add_underspec() local
47 return flat; in FStar_UInt128_add_underspec()
53 flat = { a.low + b.low, a.high + b.high + FStar_UInt128_carry(a.low + b.low, b.low) }; in FStar_UInt128_add_mod() local
54 return flat; in FStar_UInt128_add_mod()
60 flat = { a.low - b.low, a.high - b.high - FStar_UInt128_carry(a.low, a.low - b.low) }; in FStar_UInt128_sub() local
61 return flat; in FStar_UInt128_sub()
68 flat = { a.low - b.low, a.high - b.high - FStar_UInt128_carry(a.low, a.low - b.low) }; in FStar_UInt128_sub_underspec() local
69 return flat; in FStar_UInt128_sub_underspec()
[all …]