def le_sign_spec

bend-collections-laws-crypto@1.0.0.0 · proofs/math/u64/u64.bend:103

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as U
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/src/wide.bend as W
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S

103def le_sign_spec(+alo: U32, +ahi: U32, +blo: U32, +bhi: U32, +na: Bool, +nb: Bool) -> {U.le_sign(alo, ahi, blo, bhi, na, nb) == S.order(W.pack(alo, ahi), W.pack(blo, bhi), na, nb) : Bool}:
104  match na nb:
105    case True{} False{}:
106      {==}
107    case False{} True{}:
108      {==}
109    case True{} True{}:
110      %cmp_pack(alo, ahi, blo, bhi) : {Cmp.is_le(_) == Cmp.is_le(Word.cmp(64n, W.pack(alo, ahi), W.pack(blo, bhi))) : Bool}
111      {==}
112    case False{} False{}:
113      %cmp_pack(alo, ahi, blo, bhi) : {Cmp.is_le(_) == Cmp.is_le(Word.cmp(64n, W.pack(alo, ahi), W.pack(blo, bhi))) : Bool}
114      {==}