@@ -80184,7 +80184,7 @@ pub mod _JSON_Compile {
8018480184 } else {
8018580185 let mut c: u16 = str.get(&(start.clone() + int!(1)));
8018680186 if c == DafnyCharUTF16(117 as u16).0 as u16 {
80187- if !( start.clone() + int!(6) < str.cardinality() ) {
80187+ if str.cardinality() < start.clone() + int!(6) {
8018880188 return Arc::new(Result::<Sequence<u16>, Arc<DeserializationError>>::Failure {
8018980189 error: Arc::new(DeserializationError::EscapeAtEOS {})
8019080190 });
@@ -82966,14 +82966,14 @@ pub mod _JSON_Compile {
8296682966 pub fn EscapeUnicode(c: u16) -> Sequence<u16> {
8296782967 let mut sStr: Sequence<DafnyCharUTF16> = crate::implementation_from_dafny::_JSON_Compile::_Utils_Compile::_Str_Compile::_default::OfNat(&int!((&c).clone()), &int!(16));
8296882968 let mut s: Sequence<u16> = crate::implementation_from_dafny::_UnicodeStrings_Compile::_default::ASCIIToUTF16(&sStr);
82969- s.concat(& ({
82970- let _initializer = {
82971- Arc::new(move |_v0: &DafnyInt| -> u16{
82972- DafnyCharUTF16(32 as u16).0 as u16
82973- })
82974- };
82975- integer_range(Zero::zero(), int!(4) - s.cardinality()).map(move |i| _initializer(&i)).collect::<Sequence<_>>()
82976- }) )
82969+ ({
82970+ let _initializer = {
82971+ Arc::new(move |_v0: &DafnyInt| -> u16{
82972+ DafnyCharUTF16(48 as u16).0 as u16
82973+ })
82974+ };
82975+ integer_range(Zero::zero(), int!(4) - s.cardinality()).map(move |i| _initializer(&i)).collect::<Sequence<_>>()
82976+ }).concat(&s )
8297782977 }
8297882978 /// ../mpl/libraries/src/JSON/Spec.dfy(51,3)
8297982979 pub fn Escape(str: &Sequence<u16>, start: &nat) -> Sequence<u16> {
@@ -97825,20 +97825,34 @@ pub mod _Structure_Compile {
9782597825 }
9782697826 /// ../mpl/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Structure.dfy(258,3)
9782797827 pub fn ExtractCustomEncryptionContext(encryptionContext: &BranchKeyContext) -> Arc<Result<Map<ValidUTF8Bytes, ValidUTF8Bytes>, Arc<Error>>> {
97828+ let mut prefixKeys: Set<Sequence<DafnyCharUTF16>> = (&({
97829+ let mut encryptionContext = encryptionContext.clone();
97830+ Arc::new(move || -> Set<Sequence<DafnyCharUTF16>>{
97831+ let mut _coll0: SetBuilder<Sequence<DafnyCharUTF16>> = SetBuilder::<Sequence<DafnyCharUTF16>>::new();
97832+ for __compr_0 in (&encryptionContext.keys()).iter().cloned() {
97833+ let mut k: Sequence<DafnyCharUTF16> = __compr_0.clone();
97834+ if encryptionContext.keys().contains(&k) && _default::ENCRYPTION_CONTEXT_PREFIX() <= k.clone() {
97835+ _coll0.add(&k)
97836+ }
97837+ }
97838+ _coll0.build()
97839+ })
97840+ }))();
9782897841 let mut encodedEncryptionContext: Set<(Arc<Result<ValidUTF8Bytes, Sequence<DafnyCharUTF16>>>, Arc<Result<ValidUTF8Bytes, Sequence<DafnyCharUTF16>>>)> = (&({
97842+ let mut prefixKeys = prefixKeys.clone();
9782997843 let mut encryptionContext = encryptionContext.clone();
9783097844 Arc::new(move || -> Set<(Arc<Result<ValidUTF8Bytes, Sequence<DafnyCharUTF16>>>, Arc<Result<ValidUTF8Bytes, Sequence<DafnyCharUTF16>>>)>{
97831- let mut _coll0 : SetBuilder<(Arc<Result<ValidUTF8Bytes, Sequence<DafnyCharUTF16>>>, Arc<Result<ValidUTF8Bytes, Sequence<DafnyCharUTF16>>>)> = SetBuilder::<(Arc<Result<ValidUTF8Bytes, Sequence<DafnyCharUTF16>>>, Arc<Result<ValidUTF8Bytes, Sequence<DafnyCharUTF16>>>)>::new();
97832- for __compr_0 in (&encryptionContext).keys( ).iter().cloned() {
97833- let mut k: Sequence<DafnyCharUTF16> = __compr_0 .clone();
97834- if encryptionContext .contains(&k) && _default::ENCRYPTION_CONTEXT_PREFIX() < k.clone( ) {
97835- _coll0 .add(&((
97845+ let mut _coll1 : SetBuilder<(Arc<Result<ValidUTF8Bytes, Sequence<DafnyCharUTF16>>>, Arc<Result<ValidUTF8Bytes, Sequence<DafnyCharUTF16>>>)> = SetBuilder::<(Arc<Result<ValidUTF8Bytes, Sequence<DafnyCharUTF16>>>, Arc<Result<ValidUTF8Bytes, Sequence<DafnyCharUTF16>>>)>::new();
97846+ for __compr_1 in (&prefixKeys ).iter().cloned() {
97847+ let mut k: Sequence<DafnyCharUTF16> = __compr_1 .clone();
97848+ if prefixKeys .contains(&k) {
97849+ _coll1 .add(&((
9783697850 crate::implementation_from_dafny::UTF8::_default::Encode(&k.drop(&int!((&truncate!((&_default::ENCRYPTION_CONTEXT_PREFIX().cardinality()).clone(), u32)).clone()))),
9783797851 crate::implementation_from_dafny::UTF8::_default::Encode(&encryptionContext.get(&k))
9783897852 )))
9783997853 }
9784097854 }
97841- _coll0 .build()
97855+ _coll1 .build()
9784297856 })
9784397857 }))();
9784497858 let mut valueOrError0: Arc<Outcome<Arc<Error>>> = crate::implementation_from_dafny::_Wrappers_Compile::_default::Need::<Arc<Error>>((&encodedEncryptionContext).iter().all(({
@@ -97857,14 +97871,14 @@ pub mod _Structure_Compile {
9785797871 value: (&({
9785897872 let mut encodedEncryptionContext = encodedEncryptionContext.clone();
9785997873 Arc::new(move || -> Map<ValidUTF8Bytes, ValidUTF8Bytes>{
97860- let mut _coll1 : MapBuilder<ValidUTF8Bytes, ValidUTF8Bytes> = MapBuilder::<ValidUTF8Bytes, ValidUTF8Bytes>::new();
97861- for __compr_1 in (&encodedEncryptionContext).iter().cloned() {
97862- let mut i: (Arc<Result<ValidUTF8Bytes, Sequence<DafnyCharUTF16>>>, Arc<Result<ValidUTF8Bytes, Sequence<DafnyCharUTF16>>>) = __compr_1 .clone();
97874+ let mut _coll2 : MapBuilder<ValidUTF8Bytes, ValidUTF8Bytes> = MapBuilder::<ValidUTF8Bytes, ValidUTF8Bytes>::new();
97875+ for __compr_2 in (&encodedEncryptionContext).iter().cloned() {
97876+ let mut i: (Arc<Result<ValidUTF8Bytes, Sequence<DafnyCharUTF16>>>, Arc<Result<ValidUTF8Bytes, Sequence<DafnyCharUTF16>>>) = __compr_2 .clone();
9786397877 if encodedEncryptionContext.contains(&i) {
97864- _coll1 .add(i.0.clone().value(), i.1.clone().value())
97878+ _coll2 .add(i.0.clone().value(), i.1.clone().value())
9786597879 }
9786697880 }
97867- _coll1 .build()
97881+ _coll2 .build()
9786897882 })
9786997883 }))()
9787097884 })
0 commit comments