law essiv_round_trip_if

bend-osdev-aead@0.1.0.0 · LAWS.bend:97

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-crypto@0.1.0.0/crypto.bend as Cr
import bend-osdev-aead@0.1.0.0/essiv.bend as Es

97law essiv_round_trip_if:
98  for ~KD: Data
99  for ~KS: Data
100  for ~Blk: Data
101  for ~enc: KS -> Blk -> Blk
102  for ~blk_of: B.Octets -> Maybe<&2, Blk>
103  for ~blk_to: Blk -> B.Octets
104  for ~cenc: KD -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>
105  for ~cdec: KD -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets>
106  for +kd: KD
107  for +ks: KS
108  for +iv: B.Octets
109  for +m: B.Octets
110  for h: {Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, cenc(kd, Es.AdEssiv.iv(~KD, ~KS, ~Blk, ~enc, ~blk_of, ~blk_to, Es.AdEssivKey{kd, ks}, iv), m), c => cdec(kd, Es.AdEssiv.iv(~KD, ~KS, ~Blk, ~enc, ~blk_of, ~blk_to, Es.AdEssivKey{kd, ks}, iv), c)) == Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => m, cenc(kd, Es.AdEssiv.iv(~KD, ~KS, ~Blk, ~enc, ~blk_of, ~blk_to, Es.AdEssivKey{kd, ks}, iv), m)) : Result<&2, &2, Cr.CrError, B.Octets>}
111  {Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, Es.AdEssiv.encrypt(~KD, ~KS, ~Blk, ~enc, ~blk_of, ~blk_to, ~cenc, Es.AdEssivKey{kd, ks}, iv, m), c => Es.AdEssiv.decrypt(~KD, ~KS, ~Blk, ~enc, ~blk_of, ~blk_to, ~cdec, Es.AdEssivKey{kd, ks}, iv, c)) == Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => m, Es.AdEssiv.encrypt(~KD, ~KS, ~Blk, ~enc, ~blk_of, ~blk_to, ~cenc, Es.AdEssivKey{kd, ks}, iv, m)) : Result<&2, &2, Cr.CrError, B.Octets>}