in releases/go/encryption-sdk/MessageBody/MessageBody.go [454:494]
func (_static *CompanionStruct_Default___) DecryptFramedMessageBody(body FramedMessageBody, key _dafny.Sequence, crypto *m_AtomicPrimitives.AtomicPrimitivesClient) m_Wrappers.Result {
var res m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq)
_ = res
var _0_plaintext _dafny.Sequence
_ = _0_plaintext
_0_plaintext = _dafny.SeqOf()
var _hi0 _dafny.Int = _dafny.IntOfUint32(((body).Dtor_regularFrames()).Cardinality())
_ = _hi0
for _1_i := _dafny.Zero; _1_i.Cmp(_hi0) < 0; _1_i = _1_i.Plus(_dafny.One) {
var _2_valueOrError0 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq)
_ = _2_valueOrError0
var _out0 m_Wrappers.Result
_ = _out0
_out0 = Companion_Default___.DecryptFrame(((body).Dtor_regularFrames()).Select((_1_i).Uint32()).(m_Frames.Frame), key, crypto)
_2_valueOrError0 = _out0
if (_2_valueOrError0).IsFailure() {
res = (_2_valueOrError0).PropagateFailure()
return res
}
var _3_plaintextSegment _dafny.Sequence
_ = _3_plaintextSegment
_3_plaintextSegment = (_2_valueOrError0).Extract().(_dafny.Sequence)
_0_plaintext = _dafny.Companion_Sequence_.Concatenate(_0_plaintext, _3_plaintextSegment)
}
var _4_valueOrError1 m_Wrappers.Result = m_Wrappers.Companion_Result_.Default(_dafny.EmptySeq)
_ = _4_valueOrError1
var _out1 m_Wrappers.Result
_ = _out1
_out1 = Companion_Default___.DecryptFrame((body).Dtor_finalFrame(), key, crypto)
_4_valueOrError1 = _out1
if (_4_valueOrError1).IsFailure() {
res = (_4_valueOrError1).PropagateFailure()
return res
}
var _5_finalPlaintextSegment _dafny.Sequence
_ = _5_finalPlaintextSegment
_5_finalPlaintextSegment = (_4_valueOrError1).Extract().(_dafny.Sequence)
_0_plaintext = _dafny.Companion_Sequence_.Concatenate(_0_plaintext, _5_finalPlaintextSegment)
res = m_Wrappers.Companion_Result_.Create_Success_(_0_plaintext)
return res
}