law next_correct

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/sha512/conformance.bend:35

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/types.bend as T
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/core.bend as C
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha512.bend as F

35law next_correct:
36  for +a: T.Lane
37  for +b: T.Lane
38  for +c: T.Lane
39  for +d: T.Lane
40  for +e: T.Lane
41  for +f: T.Lane
42  for +g: T.Lane
43  for +h: T.Lane
44  for +i: T.Lane
45  for +j: T.Lane
46  for +k: T.Lane
47  for +l: T.Lane
48  for +m: T.Lane
49  for +n: T.Lane
50  for +o: T.Lane
51  for +p: T.Lane
52  for +rest: List<&2, T.Lane>
53  {C.next(b, g, o, p) == F.recurrence(a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest) : T.Lane}