func()

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
}