diff --git a/DynamoDbEncryption/runtimes/rust/Cargo.toml b/DynamoDbEncryption/runtimes/rust/Cargo.toml index 4e75acfcc..e7349946d 100644 --- a/DynamoDbEncryption/runtimes/rust/Cargo.toml +++ b/DynamoDbEncryption/runtimes/rust/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "aws-db-esdk" -version = "1.1.0" +version = "1.1.1" edition = "2021" rust-version = "1.81.0" keywords = ["cryptography", "security", "dynamodb", "encryption", "client-side"] @@ -16,7 +16,7 @@ readme = "README.md" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [dependencies] -aws-config = "1.6.2" +aws-config = "1.6.3" aws-lc-rs = "1.13.1" aws-lc-sys = "0.29.0" aws-sdk-dynamodb = "1.73.0" @@ -28,8 +28,8 @@ cpu-time = "1.0.0" dafny_runtime = { path = "../../../submodules/smithy-dafny/TestModels/dafny-dependencies/dafny_runtime_rust", features = ["sync","small-int"] } dashmap = "6.1.0" pem = "3.0.5" -tokio = {version = "1.45.0", features = ["full"] } -uuid = { version = "1.16.0", features = ["v4"] } +tokio = {version = "1.45.1", features = ["full"] } +uuid = { version = "1.17.0", features = ["v4"] } [[example]] name = "main" diff --git a/TestVectors/runtimes/rust/Cargo.toml b/TestVectors/runtimes/rust/Cargo.toml index dace76318..3941592c5 100644 --- a/TestVectors/runtimes/rust/Cargo.toml +++ b/TestVectors/runtimes/rust/Cargo.toml @@ -11,7 +11,7 @@ default = ["wrapped-client"] wrapped-client = [] [dependencies] -aws-config = "1.6.2" +aws-config = "1.6.3" aws-lc-rs = "1.13.1" aws-lc-sys = "0.29.0" aws-sdk-dynamodb = "1.73.0" @@ -23,5 +23,5 @@ cpu-time = "1.0.0" dafny_runtime = { path = "../../../submodules/smithy-dafny/TestModels/dafny-dependencies/dafny_runtime_rust", features = ["sync","small-int"] } dashmap = "6.1.0" pem = "3.0.5" -tokio = {version = "1.45.0", features = ["full"] } -uuid = { version = "1.16.0", features = ["v4"] } +tokio = {version = "1.45.1", features = ["full"] } +uuid = { version = "1.17.0", features = ["v4"] } diff --git a/releases/rust/db_esdk/Cargo.toml b/releases/rust/db_esdk/Cargo.toml index 08a483e39..e62d4fb93 100644 --- a/releases/rust/db_esdk/Cargo.toml +++ b/releases/rust/db_esdk/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "aws-db-esdk" -version = "1.1.0" +version = "1.1.1" edition = "2021" rust-version = "1.81.0" keywords = ["cryptography", "security", "dynamodb", "encryption", "client-side"] @@ -16,7 +16,7 @@ readme = "README.md" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [dependencies] -aws-config = "1.6.2" +aws-config = "1.6.3" aws-lc-rs = "1.13.1" aws-lc-sys = "0.29.0" aws-sdk-dynamodb = "1.73.0" @@ -25,11 +25,11 @@ aws-smithy-runtime-api = {version = "1.8.0", features = ["client"] } aws-smithy-types = "1.3.1" chrono = "0.4.41" cpu-time = "1.0.0" -dafny-runtime = { version = "0.3.0", features = ["sync", "small-int"] } +dafny-runtime = { version = "0.3.1", features = ["sync", "small-int"] } dashmap = "6.1.0" pem = "3.0.5" -tokio = {version = "1.45.0", features = ["full"] } -uuid = { version = "1.16.0", features = ["v4"] } +tokio = {version = "1.45.1", features = ["full"] } +uuid = { version = "1.17.0", features = ["v4"] } [[example]] name = "main" diff --git a/releases/rust/db_esdk/src/implementation_from_dafny.rs b/releases/rust/db_esdk/src/implementation_from_dafny.rs index dc6ae5c56..1460a6d22 100644 --- a/releases/rust/db_esdk/src/implementation_from_dafny.rs +++ b/releases/rust/db_esdk/src/implementation_from_dafny.rs @@ -5621,7 +5621,7 @@ pub mod software { pub struct _default {} impl _default { - /// dafny/DynamoDbItemEncryptor/src/Index.dfy(24,3) + /// dafny/DynamoDbItemEncryptor/src/Index.dfy(23,3) pub fn DefaultDynamoDbItemEncryptorConfig() -> Arc { Arc::new(DynamoDbItemEncryptorConfig::DynamoDbItemEncryptorConfig { logicalTableName: string_utf16_of("foo"), @@ -5637,11 +5637,11 @@ pub mod software { plaintextOverride: Arc::new(Option::>::None {}) }) } - /// dafny/DynamoDbItemEncryptor/src/Index.dfy(41,3) + /// dafny/DynamoDbItemEncryptor/src/Index.dfy(40,3) pub fn UnreservedPrefix(attr: &Sequence) -> bool { !(crate::implementation_from_dafny::_DynamoDbItemEncryptorUtil_Compile::_default::ReservedPrefix() <= attr.clone()) && !(crate::implementation_from_dafny::_StructuredEncryptionUtil_Compile::_default::ReservedCryptoContextPrefixString() <= attr.clone()) } - /// dafny/DynamoDbItemEncryptor/src/Index.dfy(47,3) + /// dafny/DynamoDbItemEncryptor/src/Index.dfy(46,3) pub fn DynamoDbItemEncryptor(config: &Arc) -> Arc, Arc>> { let mut res = MaybePlacebo::, Arc>>>::new(); let mut valueOrError0: Arc>>; @@ -5829,7 +5829,7 @@ pub mod software { } } - /// dafny/DynamoDbItemEncryptor/src/Index.dfy(232,3) + /// dafny/DynamoDbItemEncryptor/src/Index.dfy(231,3) pub struct DynamoDbItemEncryptorClient { pub __i_config: Arc } @@ -5839,7 +5839,7 @@ pub mod software { pub fn _allocate_object() -> Object { allocate_object::() } - /// dafny/DynamoDbItemEncryptor/src/Index.dfy(241,5) + /// dafny/DynamoDbItemEncryptor/src/Index.dfy(240,5) pub fn _ctor(this: &Object, config: &Arc) -> () { let mut _set___i_config: bool = false; update_field_uninit_object!(this.clone(), __i_config, _set___i_config, config.clone()); @@ -7101,13 +7101,13 @@ pub mod software { pub struct _default {} impl _default { - /// dafny/DynamoDbEncryptionTransforms/src/Index.dfy(25,3) + /// dafny/DynamoDbEncryptionTransforms/src/Index.dfy(24,3) pub fn DefaultDynamoDbTablesEncryptionConfig() -> Arc { Arc::new(DynamoDbTablesEncryptionConfig::DynamoDbTablesEncryptionConfig { tableEncryptionConfigs: map![] }) } - /// dafny/DynamoDbEncryptionTransforms/src/Index.dfy(61,3) + /// dafny/DynamoDbEncryptionTransforms/src/Index.dfy(60,3) pub fn AddSignedBeaconActions(names: &Sequence>, actions: &Map, Arc>, pos: &nat) -> Map, Arc> { let mut _r0 = names.clone(); let mut _r1 = actions.clone(); @@ -7129,7 +7129,7 @@ pub mod software { } } } - /// dafny/DynamoDbEncryptionTransforms/src/Index.dfy(76,3) + /// dafny/DynamoDbEncryptionTransforms/src/Index.dfy(75,3) pub fn IsConfigured(config: &Arc, name: &Sequence) -> bool { config.attributeActionsOnEncrypt().contains(name) || matches!(config.allowedUnsignedAttributes().as_ref(), Some{ .. }) && config.allowedUnsignedAttributes().value().contains(name) || matches!(config.allowedUnsignedAttributePrefix().as_ref(), Some{ .. }) && config.allowedUnsignedAttributePrefix().value().clone() <= name.clone() } @@ -7137,7 +7137,7 @@ pub mod software { /// = type=implication /// # When mapping [DynamoDB Table Names](#dynamodb-table-name) to [logical table name](#logical-table-name) /// # there MUST a one to one mapping between the two. - /// dafny/DynamoDbEncryptionTransforms/src/Index.dfy(111,3) + /// dafny/DynamoDbEncryptionTransforms/src/Index.dfy(110,3) pub fn DynamoDbEncryptionTransforms(config: &Arc) -> Arc, Arc>> { let mut res = MaybePlacebo::, Arc>>>::new(); let mut internalConfigs: Map, ValidTableConfig> = map![]; @@ -7279,7 +7279,7 @@ pub mod software { } } - /// dafny/DynamoDbEncryptionTransforms/src/Index.dfy(296,3) + /// dafny/DynamoDbEncryptionTransforms/src/Index.dfy(295,3) pub struct DynamoDbEncryptionTransformsClient { pub __i_config: Arc } @@ -7289,7 +7289,7 @@ pub mod software { pub fn _allocate_object() -> Object { allocate_object::() } - /// dafny/DynamoDbEncryptionTransforms/src/Index.dfy(305,5) + /// dafny/DynamoDbEncryptionTransforms/src/Index.dfy(304,5) pub fn _ctor(this: &Object, config: &Arc) -> () { let mut _set___i_config: bool = false; update_field_uninit_object!(this.clone(), __i_config, _set___i_config, config.clone()); @@ -11923,11 +11923,11 @@ pub mod software { pub struct _default {} impl _default { - /// dafny/DynamoDbEncryption/src/Index.dfy(25,3) + /// dafny/DynamoDbEncryption/src/Index.dfy(24,3) pub fn DefaultDynamoDbEncryptionConfig() -> Arc { Arc::new(DynamoDbEncryptionConfig::DynamoDbEncryptionConfig {}) } - /// dafny/DynamoDbEncryption/src/Index.dfy(30,3) + /// dafny/DynamoDbEncryption/src/Index.dfy(29,3) pub fn DynamoDbEncryption(config: &Arc) -> Arc, Arc>> { let mut res: Arc, Arc>>; let mut internalConfig: Arc = Arc::new(Config::Config {}); @@ -11954,7 +11954,7 @@ pub mod software { } } - /// dafny/DynamoDbEncryption/src/Index.dfy(39,3) + /// dafny/DynamoDbEncryption/src/Index.dfy(38,3) pub struct DynamoDbEncryptionClient { pub __i_config: Arc } @@ -11964,7 +11964,7 @@ pub mod software { pub fn _allocate_object() -> Object { allocate_object::() } - /// dafny/DynamoDbEncryption/src/Index.dfy(48,5) + /// dafny/DynamoDbEncryption/src/Index.dfy(47,5) pub fn _ctor(this: &Object, config: &Arc) -> () { let mut _set___i_config: bool = false; update_field_uninit_object!(this.clone(), __i_config, _set___i_config, config.clone()); @@ -16240,11 +16240,11 @@ pub mod software { pub struct _default {} impl _default { - /// dafny/StructuredEncryption/src/Index.dfy(15,3) + /// dafny/StructuredEncryption/src/Index.dfy(14,3) pub fn DefaultStructuredEncryptionConfig() -> Arc { Arc::new(StructuredEncryptionConfig::StructuredEncryptionConfig {}) } - /// dafny/StructuredEncryption/src/Index.dfy(20,3) + /// dafny/StructuredEncryption/src/Index.dfy(19,3) pub fn StructuredEncryption(config: &Arc) -> Arc, Arc>> { let mut res = MaybePlacebo::, Arc>>>::new(); let mut maybePrimitives: Arc, Arc>>; @@ -16305,7 +16305,7 @@ pub mod software { } } - /// dafny/StructuredEncryption/src/Index.dfy(36,3) + /// dafny/StructuredEncryption/src/Index.dfy(35,3) pub struct StructuredEncryptionClient { pub __i_config: Arc } @@ -16315,7 +16315,7 @@ pub mod software { pub fn _allocate_object() -> Object { allocate_object::() } - /// dafny/StructuredEncryption/src/Index.dfy(45,5) + /// dafny/StructuredEncryption/src/Index.dfy(44,5) pub fn _ctor(this: &Object, config: &Arc) -> () { let mut _set___i_config: bool = false; update_field_uninit_object!(this.clone(), __i_config, _set___i_config, config.clone()); @@ -91439,6 +91439,7 @@ pub mod _DynamoDBFilterExpr_Compile { pub use crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::Token::Size; pub use ::dafny_runtime::DafnyInt; pub use ::dafny_runtime::seq; + pub use ::dafny_runtime::truncate; pub use crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::Token::Attr; pub use crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::Token::Ne; pub use crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::Token::In; @@ -91484,11 +91485,12 @@ pub mod _DynamoDBFilterExpr_Compile { pub use crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::StackValue::Bool; pub use crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::StackValue::Str; pub use ::dafny_runtime::DafnyTypeEq; + pub use ::std::default::Default; + pub use ::dafny_runtime::MaybePlacebo; pub use crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::StackValue::DoesNotExist; pub use ::dafny_runtime::NumCast; pub use ::std::marker::Sync; pub use ::std::marker::Send; - pub use ::dafny_runtime::MaybePlacebo; pub use ::dafny_runtime::integer_range; pub use ::dafny_runtime::map; pub use crate::implementation_from_dafny::_CompoundBeacon_Compile::BeaconPart; @@ -91503,68 +91505,77 @@ pub mod _DynamoDBFilterExpr_Compile { pub use ::dafny_runtime::DafnyPrint; pub use ::std::hash::Hash; pub use ::std::hash::Hasher; - pub use ::std::default::Default; pub use ::std::convert::AsRef; pub struct _default {} impl _default { - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(47,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(49,3) pub fn ExtractAttributes(s: &Sequence, ex: &Arc, Sequence>>>) -> Sequence> { - let mut tokens: Sequence> = _default::ParseExpr(s); - _default::ExtractAttributes2(&tokens, ex, &int!(-1)) + let mut tokens: Sequence> = _default::ParseExpr(s, 0); + _default::ExtractAttributes2(&tokens, ex, &int!(-1), 0) } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(54,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(56,3) pub fn IsSpecial(t: &Arc) -> bool { matches!(t.as_ref(), AttributeExists{ .. }) || matches!(t.as_ref(), AttributeNotExists{ .. }) || matches!(t.as_ref(), Size{ .. }) } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(62,3) - pub fn ExtractAttributes2(tokens: &Sequence>, names: &Arc, Sequence>>>, tokensUntilSkip: &DafnyInt) -> Sequence> { + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(64,3) + pub fn ExtractAttributes2(tokens: &Sequence>, names: &Arc, Sequence>>>, tokensUntilSkip: &DafnyInt, pos: u64) -> Sequence> { let mut _accumulator: Sequence> = seq![] as Sequence>; let mut _r0 = tokens.clone(); let mut _r1 = names.clone(); let mut _r2 = tokensUntilSkip.clone(); + let mut _r3 = pos; 'TAIL_CALL_START: loop { let tokens = _r0; let names = _r1; let tokensUntilSkip = _r2; - if tokens.cardinality() == int!(0) { + let pos = _r3; + if truncate!(tokens.cardinality(), u64) == pos { return _accumulator.concat(&(seq![] as Sequence>)); } else { - if _default::IsSpecial(&tokens.get(&int!(0))) { - let mut _in0: Sequence> = tokens.drop(&int!(1)); + if _default::IsSpecial(&tokens.get(&int!((&pos).clone()))) { + let mut _in0: Sequence> = tokens.clone(); let mut _in1: Arc, Sequence>>> = names.clone(); let mut _in2: DafnyInt = int!(1); + let mut _in3: u64 = pos + 1; _r0 = _in0.clone(); _r1 = _in1.clone(); _r2 = _in2.clone(); + _r3 = _in3; continue 'TAIL_CALL_START; } else { - if matches!((&tokens.get(&int!(0))).as_ref(), Attr{ .. }) && tokensUntilSkip.clone() == int!(0) { - let mut _in3: Sequence> = tokens.drop(&int!(1)); - let mut _in4: Arc, Sequence>>> = names.clone(); - let mut _in5: DafnyInt = int!(-1); - _r0 = _in3.clone(); - _r1 = _in4.clone(); - _r2 = _in5.clone(); + if matches!((&tokens.get(&int!((&pos).clone()))).as_ref(), Attr{ .. }) && tokensUntilSkip.clone() == int!(0) { + let mut _in4: Sequence> = tokens.clone(); + let mut _in5: Arc, Sequence>>> = names.clone(); + let mut _in6: DafnyInt = int!(-1); + let mut _in7: u64 = pos + 1; + _r0 = _in4.clone(); + _r1 = _in5.clone(); + _r2 = _in6.clone(); + _r3 = _in7; continue 'TAIL_CALL_START; } else { - if matches!((&tokens.get(&int!(0))).as_ref(), Attr{ .. }) { - _accumulator = _accumulator.concat(&seq![_default::GetAttrName(&tokens.get(&int!(0)), &names)]); - let mut _in6: Sequence> = tokens.drop(&int!(1)); - let mut _in7: Arc, Sequence>>> = names.clone(); - let mut _in8: DafnyInt = int!(-1); - _r0 = _in6.clone(); - _r1 = _in7.clone(); - _r2 = _in8.clone(); + if matches!((&tokens.get(&int!((&pos).clone()))).as_ref(), Attr{ .. }) { + _accumulator = _accumulator.concat(&seq![_default::GetAttrName(&tokens.get(&int!((&pos).clone())), &names)]); + let mut _in8: Sequence> = tokens.clone(); + let mut _in9: Arc, Sequence>>> = names.clone(); + let mut _in10: DafnyInt = int!(-1); + let mut _in11: u64 = pos + 1; + _r0 = _in8.clone(); + _r1 = _in9.clone(); + _r2 = _in10.clone(); + _r3 = _in11; continue 'TAIL_CALL_START; } else { - let mut _in9: Sequence> = tokens.drop(&int!(1)); - let mut _in10: Arc, Sequence>>> = names.clone(); - let mut _in11: DafnyInt = tokensUntilSkip.clone() - int!(1); - _r0 = _in9.clone(); - _r1 = _in10.clone(); - _r2 = _in11.clone(); + let mut _in12: Sequence> = tokens.clone(); + let mut _in13: Arc, Sequence>>> = names.clone(); + let mut _in14: DafnyInt = tokensUntilSkip.clone() - int!(1); + let mut _in15: u64 = pos + 1; + _r0 = _in12.clone(); + _r1 = _in13.clone(); + _r2 = _in14.clone(); + _r3 = _in15; continue 'TAIL_CALL_START; } } @@ -91572,15 +91583,15 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(99,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(105,3) pub fn IsEquality(t: &Arc) -> bool { matches!(t.as_ref(), crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::Token::Eq{ .. }) || matches!(t.as_ref(), Ne{ .. }) || matches!(t.as_ref(), In{ .. }) } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(104,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(110,3) pub fn IsInequality(t: &Arc) -> bool { matches!(t.as_ref(), Lt{ .. }) || matches!(t.as_ref(), Le{ .. }) || matches!(t.as_ref(), Gt{ .. }) || matches!(t.as_ref(), Ge{ .. }) } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(109,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(115,3) pub fn TokenToString(t: &Arc) -> Sequence { let mut _source0: Arc = t.clone(); if matches!((&_source0).as_ref(), Attr{ .. }) { @@ -91675,7 +91686,7 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(141,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(147,3) pub fn GetInPos(expr: &Sequence>, pos: &nat) -> Arc> { let mut _r0 = expr.clone(); let mut _r1 = pos.clone(); @@ -91703,7 +91714,7 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(156,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(162,3) pub fn RealName(s: &Sequence) -> Sequence { if crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::BeaconPrefix() < s.clone() { s.drop(&crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::BeaconPrefix().cardinality()) @@ -91711,7 +91722,7 @@ pub mod _DynamoDBFilterExpr_Compile { s.clone() } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(165,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(171,3) pub fn HasBeacon(b: &Arc, t: &Arc, names: &Arc, Sequence>>>) -> bool { if matches!(t.as_ref(), Attr{ .. }) { let mut name: Sequence = _default::RealName(t.s()); @@ -91720,7 +91731,7 @@ pub mod _DynamoDBFilterExpr_Compile { false } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(177,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(183,3) pub fn GetBeacon2(b: &Arc, t: &Arc, names: &Arc, Sequence>>>) -> Arc, Arc>> { let mut name: Sequence = _default::RealName(t.s()); if b.beacons().contains(&name) { @@ -91753,7 +91764,7 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(210,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(216,3) pub fn GetBeacon(bv: &Arc, t: &Arc, op: &Arc, value: &Arc, names: &Arc, Sequence>>>, values: &Map, Arc>) -> Arc, Arc>> { let mut valueOrError0: Arc, Arc>> = _default::GetBeacon2(bv, t, names); if valueOrError0.IsFailure() { @@ -91777,7 +91788,7 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(227,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(233,3) pub fn GetBetweenBeacon(bv: &Arc, t: &Arc, op: &Arc, leftValue: &Arc, rightValue: &Arc, names: &Arc, Sequence>>>, values: &Map, Arc>) -> Arc, Arc>> { let mut valueOrError0: Arc, Arc>> = _default::GetBeacon2(bv, t, names); if valueOrError0.IsFailure() { @@ -91801,7 +91812,7 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(254,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(260,3) pub fn CanStandardBeacon(op: &Arc) -> Arc>> { let mut _source0: Arc = op.clone(); if matches!((&_source0).as_ref(), Attr{ .. }) { @@ -91937,7 +91948,7 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(263,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(269,3) pub fn CanCompoundBeacon(b: &Arc, op: &Arc, value: &Sequence) -> Arc>> { let mut _source0: Arc = op.clone(); if matches!((&_source0).as_ref(), Attr{ .. }) { @@ -92125,7 +92136,7 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(290,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(296,3) pub fn GetStringFromValue(value: &Sequence, values: &Map, Arc>, b: &Arc) -> Arc, Arc>> { if values.contains(value) { let mut val: Arc = values.get(value); @@ -92144,7 +92155,7 @@ pub mod _DynamoDBFilterExpr_Compile { }) } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(304,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(310,3) pub fn CanBeacon(b: &Arc, op: &Arc, value: &Sequence, values: &Map, Arc>) -> Arc>> { if matches!(b.as_ref(), Standard{ .. }) { _default::CanStandardBeacon(op) @@ -92158,28 +92169,32 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(320,3) - pub fn RemoveCommonPrefix(x: &Sequence>, y: &Sequence>) -> (Sequence>, Sequence>) { + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(326,3) + pub fn RemoveCommonPrefix(x: &Sequence>, y: &Sequence>, pos: u64) -> (Sequence>, Sequence>) { let mut _r0 = x.clone(); let mut _r1 = y.clone(); + let mut _r2 = pos; 'TAIL_CALL_START: loop { let x = _r0; let y = _r1; - if x.cardinality() == int!(0) || y.cardinality() == int!(0) || x.get(&int!(0)) != y.get(&int!(0)) { + let pos = _r2; + if truncate!(x.cardinality(), u64) == pos || truncate!(y.cardinality(), u64) == pos || x.get(&int!((&pos).clone())) != y.get(&int!((&pos).clone())) { return ( - x.clone(), - y.clone() + x.drop(&int!((&pos).clone())), + y.drop(&int!((&pos).clone())) ); } else { - let mut _in0: Sequence> = x.drop(&int!(1)); - let mut _in1: Sequence> = y.drop(&int!(1)); + let mut _in0: Sequence> = x.clone(); + let mut _in1: Sequence> = y.clone(); + let mut _in2: u64 = crate::implementation_from_dafny::_StandardLibrary_Compile::_MemoryMath_Compile::_default::Add(pos, 1); _r0 = _in0.clone(); _r1 = _in1.clone(); + _r2 = _in2; continue 'TAIL_CALL_START; } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(329,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(340,3) pub fn CanBetween(b: &Arc, op: &Arc, leftValue: &Sequence, rightValue: &Sequence, values: &Map, Arc>) -> Arc>> { if matches!(b.as_ref(), Standard{ .. }) { Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::>::Failure { @@ -92198,7 +92213,7 @@ pub mod _DynamoDBFilterExpr_Compile { let mut rightVal: Sequence = valueOrError1.Extract(); let mut leftParts: Sequence> = crate::implementation_from_dafny::_StandardLibrary_Compile::_default::Split::(&leftVal, b.cmp().split()); let mut rightParts: Sequence> = crate::implementation_from_dafny::_StandardLibrary_Compile::_default::Split::(&rightVal, b.cmp().split()); - let mut __let_tmp_rhs0: (Sequence>, Sequence>) = _default::RemoveCommonPrefix(&leftParts, &rightParts); + let mut __let_tmp_rhs0: (Sequence>, Sequence>) = _default::RemoveCommonPrefix(&leftParts, &rightParts, 0); let mut newLeft: Sequence> = __let_tmp_rhs0.0.clone(); let mut newRight: Sequence> = __let_tmp_rhs0.1.clone(); let mut valueOrError2: Arc>> = CompoundBeacon::IsLessThanComparable(b.cmp(), &newLeft); @@ -92225,7 +92240,7 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(381,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(392,3) pub fn BeaconForValue(b: &Arc, expr: &Sequence>, pos: &nat, names: &Arc, Sequence>>>, values: &Map, Arc>) -> Arc, Arc>> { if pos.clone() + int!(2) < expr.cardinality() && _default::IsComp(&expr.get(&(pos.clone() + int!(1)))) && _default::HasBeacon(b, &expr.get(&(pos.clone() + int!(2))), names) { _default::GetBeacon(b, &expr.get(&(pos.clone() + int!(2))), &expr.get(&(pos.clone() + int!(1))), &expr.get(pos), names, values) @@ -92284,7 +92299,7 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(426,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(437,3) pub fn AttrForValue(expr: &Sequence>, pos: &nat) -> Arc>> { if pos.clone() + int!(2) < expr.cardinality() && _default::IsComp(&expr.get(&(pos.clone() + int!(1)))) && matches!((&expr.get(&(pos.clone() + int!(2)))).as_ref(), Attr{ .. }) { Arc::new(Option::>::Some { @@ -92329,7 +92344,7 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(464,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(475,3) pub fn OpNeedsBeacon(expr: &Sequence>, pos: &nat) -> bool { if pos.clone() < int!(2) { true @@ -92341,7 +92356,7 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(480,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(491,3) pub fn IsAllowedOnBeaconPred(expr: &Sequence>, pos: &nat) -> bool { if pos.clone() < int!(2) { true @@ -92357,7 +92372,7 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(498,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(509,3) pub fn IsAllowedOnBeacon(expr: &Sequence>, pos: &nat, name: &Sequence) -> Arc>> { if _default::IsAllowedOnBeaconPred(expr, pos) { Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::>::Success { @@ -92369,15 +92384,15 @@ pub mod _DynamoDBFilterExpr_Compile { }) } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(508,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(519,3) pub fn TokenNeedsBeacon(t: &Arc) -> bool { !(matches!(t.as_ref(), AttributeExists{ .. }) || matches!(t.as_ref(), AttributeNotExists{ .. })) } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(515,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(526,3) pub fn TokenAllowsBeacon(t: &Arc) -> bool { !(matches!(t.as_ref(), AttributeType{ .. }) || matches!(t.as_ref(), Size{ .. })) } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(523,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(534,3) pub fn BeaconizeParsedExpr(b: &Arc, expr: &Sequence>, pos: &nat, oldValues: &Map, Arc>, names: &Arc, Sequence>>>, keys: &Arc, newValues: &Map, Arc>, acc: &Sequence>) -> Arc, Arc>> { let mut _r0 = b.clone(); let mut _r1 = expr.clone(); @@ -92579,7 +92594,7 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(573,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(584,3) pub fn ParsedExprToString(t: &Sequence>) -> Sequence { let mut x: Sequence> = crate::implementation_from_dafny::_Seq_Compile::_default::Map::, Sequence>(&({ Arc::new(move |x: &Arc| -> Sequence{ @@ -92592,7 +92607,7 @@ pub mod _DynamoDBFilterExpr_Compile { crate::implementation_from_dafny::_StandardLibrary_Compile::_default::Join::(&x, &string_utf16_of(" ")) } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(583,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(594,3) pub fn IsUnary(t: &Arc) -> bool { let mut _source0: Arc = t.clone(); if matches!((&_source0).as_ref(), Attr{ .. }) { @@ -92684,7 +92699,7 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(590,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(601,3) pub fn IsComp(t: &Arc) -> bool { let mut _source0: Arc = t.clone(); if matches!((&_source0).as_ref(), Attr{ .. }) { @@ -92776,7 +92791,7 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(597,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(608,3) pub fn IsBinaryBool(t: &Arc) -> bool { let mut _source0: Arc = t.clone(); if matches!((&_source0).as_ref(), Attr{ .. }) { @@ -92868,11 +92883,11 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(604,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(615,3) pub fn IsBinary(t: &Arc) -> bool { _default::IsComp(t) || _default::IsBinaryBool(t) } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(609,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(620,3) pub fn IsVar(t: &Arc) -> bool { let mut _source0: Arc = t.clone(); if matches!((&_source0).as_ref(), Attr{ .. }) { @@ -92967,7 +92982,7 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(617,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(628,3) pub fn IsFunction(t: &Arc) -> bool { let mut _source0: Arc = t.clone(); if matches!((&_source0).as_ref(), Attr{ .. }) { @@ -93059,7 +93074,7 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(632,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(643,3) pub fn Precedence(t: &Arc) -> nat { let mut _source0: Arc = t.clone(); if matches!((&_source0).as_ref(), Attr{ .. }) { @@ -93154,24 +93169,28 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(659,3) - pub fn ParseExpr(s: &Sequence) -> Sequence> { + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(670,3) + pub fn ParseExpr(s: &Sequence, pos: u64) -> Sequence> { let mut _accumulator: Sequence> = seq![] as Sequence>; let mut _r0 = s.clone(); + let mut _r1 = pos; 'TAIL_CALL_START: loop { let s = _r0; - let mut tup: (nat, Arc) = _default::FindIndexToken(&s); - if int!(0) < tup.0.clone() { + let pos = _r1; + let mut tup: (u64, Arc) = _default::FindIndexToken(&s, pos); + if 0 < tup.0.clone() { _accumulator = _accumulator.concat(&seq![tup.1.clone()]); - let mut _in0: Sequence = s.drop(&tup.0.clone()); + let mut _in0: Sequence = s.clone(); + let mut _in1: u64 = crate::implementation_from_dafny::_StandardLibrary_Compile::_MemoryMath_Compile::_default::Add(pos, tup.0.clone()); _r0 = _in0.clone(); + _r1 = _in1; continue 'TAIL_CALL_START; } else { return _accumulator.concat(&(seq![] as Sequence>)); } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(668,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(680,3) pub fn ByteLower(ch: u8) -> u8 { if (DafnyCharUTF16(65 as u16).0 as u8) <= ch && ch <= DafnyCharUTF16(90 as u16).0 as u8 { ch - DafnyCharUTF16(65 as u16).0 as u8 + DafnyCharUTF16(97 as u16).0 as u8 @@ -93179,7 +93198,7 @@ pub mod _DynamoDBFilterExpr_Compile { ch } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(676,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(688,3) pub fn CharLower(ch: &DafnyCharUTF16) -> DafnyCharUTF16 { if DafnyCharUTF16(65 as u16) <= ch.clone() && ch.clone() <= DafnyCharUTF16(90 as u16) { ch.clone() - DafnyCharUTF16(65 as u16) + DafnyCharUTF16(97 as u16) @@ -93187,27 +93206,46 @@ pub mod _DynamoDBFilterExpr_Compile { ch.clone() } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(685,3) - pub fn strLower(s: &Sequence) -> Sequence { - let mut _accumulator: Sequence = seq![] as Sequence; - let mut _r0 = s.clone(); + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(697,3) + pub fn EqualLower(pre: &Sequence, s: &Sequence, pos: u64, diff: u64) -> bool { + let mut _r0 = pre.clone(); + let mut _r1 = s.clone(); + let mut _r2 = pos; + let mut _r3 = diff; 'TAIL_CALL_START: loop { - let s = _r0; - if int!(0) == s.cardinality() { - return _accumulator.concat(&s); + let pre = _r0; + let s = _r1; + let pos = _r2; + let diff = _r3; + if truncate!(pre.cardinality(), u64) == pos { + return true; } else { - _accumulator = _accumulator.concat(&seq![_default::CharLower(&s.get(&int!(0)))]); - let mut _in0: Sequence = s.drop(&int!(1)); - _r0 = _in0.clone(); - continue 'TAIL_CALL_START; + if pre.get(&int!((&pos).clone())) != _default::CharLower(&s.get(&int!((&(pos + diff)).clone()))) { + return false; + } else { + let mut _in0: Sequence = pre.clone(); + let mut _in1: Sequence = s.clone(); + let mut _in2: u64 = crate::implementation_from_dafny::_StandardLibrary_Compile::_MemoryMath_Compile::_default::Add(pos, 1); + let mut _in3: u64 = diff; + _r0 = _in0.clone(); + _r1 = _in1.clone(); + _r2 = _in2; + _r3 = _in3; + continue 'TAIL_CALL_START; + } } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(695,3) - pub fn PrefixLower(pre: &Sequence, s: &Sequence) -> bool { - _default::strLower(pre) <= _default::strLower(s) + /// requires pre is already lowercase + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(712,3) + pub fn PrefixLower(pre: &Sequence, s: &Sequence, pos: u64) -> bool { + if truncate!(s.cardinality(), u64) < crate::implementation_from_dafny::_StandardLibrary_Compile::_MemoryMath_Compile::_default::Add(pos, truncate!(pre.cardinality(), u64)) { + false + } else { + _default::EqualLower(pre, s, 0, pos) + } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(701,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(727,3) pub fn ValueChar(ch: &DafnyCharUTF16) -> bool { if DafnyCharUTF16(97 as u16) <= ch.clone() && ch.clone() <= DafnyCharUTF16(122 as u16) { true @@ -93227,7 +93265,7 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(716,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(742,3) pub fn AttributeChar(ch: &DafnyCharUTF16) -> bool { if _default::ValueChar(ch) { true @@ -93239,47 +93277,31 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(727,3) - pub fn ValueLen(s: &Sequence) -> nat { - let mut _accumulator: nat = int!(0); - let mut _r0 = s.clone(); - 'TAIL_CALL_START: loop { - let s = _r0; - if int!(0) == s.cardinality() { - return int!(0) + _accumulator.clone(); + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(753,3) + pub fn ValueLen(s: &Sequence, pos: u64) -> u64 { + if pos == truncate!(s.cardinality(), u64) { + 0 + } else { + if _default::ValueChar(&s.get(&int!((&pos).clone()))) { + crate::implementation_from_dafny::_StandardLibrary_Compile::_MemoryMath_Compile::_default::Add(_default::ValueLen(s, crate::implementation_from_dafny::_StandardLibrary_Compile::_MemoryMath_Compile::_default::Add(pos, 1)), 1) } else { - if _default::ValueChar(&s.get(&int!(0))) { - _accumulator = int!(1) + _accumulator.clone(); - let mut _in0: Sequence = s.drop(&int!(1)); - _r0 = _in0.clone(); - continue 'TAIL_CALL_START; - } else { - return int!(0) + _accumulator.clone(); - } + 0 } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(739,3) - pub fn AttributeLen(s: &Sequence) -> nat { - let mut _accumulator: nat = int!(0); - let mut _r0 = s.clone(); - 'TAIL_CALL_START: loop { - let s = _r0; - if int!(0) == s.cardinality() { - return int!(0) + _accumulator.clone(); + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(768,3) + pub fn AttributeLen(s: &Sequence, pos: u64) -> u64 { + if pos == truncate!(s.cardinality(), u64) { + 0 + } else { + if _default::AttributeChar(&s.get(&int!((&pos).clone()))) { + crate::implementation_from_dafny::_StandardLibrary_Compile::_MemoryMath_Compile::_default::Add(_default::AttributeLen(s, crate::implementation_from_dafny::_StandardLibrary_Compile::_MemoryMath_Compile::_default::Add(pos, 1)), 1) } else { - if _default::AttributeChar(&s.get(&int!(0))) { - _accumulator = int!(1) + _accumulator.clone(); - let mut _in0: Sequence = s.drop(&int!(1)); - _r0 = _in0.clone(); - continue 'TAIL_CALL_START; - } else { - return int!(0) + _accumulator.clone(); - } + 0 } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(750,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(782,3) pub fn MakeAttr(s: &Sequence) -> Arc { let mut loc: Arc>> = crate::implementation_from_dafny::_TermLoc_Compile::_default::MakeTermLoc(s); if matches!((&loc).as_ref(), Success{ .. }) { @@ -93294,172 +93316,187 @@ pub mod _DynamoDBFilterExpr_Compile { }) } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(760,3) - pub fn FindIndexToken(s: &Sequence) -> (nat, Arc) { - if int!(0) == s.cardinality() { + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(792,3) + pub fn FindIndexToken(s: &Sequence, pos: u64) -> (u64, Arc) { + if pos == truncate!(s.cardinality(), u64) { ( - int!(0), + 0, Arc::new(Token::Close {}) ) } else { - let mut ch: DafnyCharUTF16 = s.get(&int!(0)); + let mut ch: DafnyCharUTF16 = s.get(&int!((&pos).clone())); + let mut remaining: u64 = truncate!(s.cardinality(), u64) - pos; if ch.clone() == DafnyCharUTF16(32 as u16) { - let mut foo: (nat, Arc) = _default::FindIndexToken(&s.drop(&int!(1))); - if foo.0.clone() == int!(0) { + let mut foo: (u64, Arc) = _default::FindIndexToken(s, crate::implementation_from_dafny::_StandardLibrary_Compile::_MemoryMath_Compile::_default::Add(pos, 1)); + if foo.0.clone() == 0 { ( foo.0.clone(), foo.1.clone() ) } else { ( - foo.0.clone() + int!(1), + crate::implementation_from_dafny::_StandardLibrary_Compile::_MemoryMath_Compile::_default::Add(foo.0.clone(), 1), foo.1.clone() ) } } else { if ch.clone() == DafnyCharUTF16(40 as u16) { ( - int!(1), + 1, Arc::new(Token::Open {}) ) } else { if ch.clone() == DafnyCharUTF16(41 as u16) { ( - int!(1), + 1, Arc::new(Token::Close {}) ) } else { if ch.clone() == DafnyCharUTF16(44 as u16) { ( - int!(1), + 1, Arc::new(Token::Comma {}) ) } else { if ch.clone() == DafnyCharUTF16(61 as u16) { ( - int!(1), + 1, Arc::new(Token::Eq {}) ) } else { if ch.clone() == DafnyCharUTF16(60 as u16) { - if string_utf16_of("<=") <= s.clone() { + if remaining == 1 { ( - int!(2), - Arc::new(Token::Le {}) + 1, + Arc::new(Token::Lt {}) ) } else { - if string_utf16_of("<>") <= s.clone() { + if s.get(&int!((&(pos + 1)).clone())) == DafnyCharUTF16(61 as u16) { ( - int!(2), - Arc::new(Token::Ne {}) + 2, + Arc::new(Token::Le {}) ) } else { - ( - int!(1), - Arc::new(Token::Lt {}) - ) + if s.get(&int!((&(pos + 1)).clone())) == DafnyCharUTF16(62 as u16) { + ( + 2, + Arc::new(Token::Ne {}) + ) + } else { + ( + 1, + Arc::new(Token::Lt {}) + ) + } } } } else { if ch.clone() == DafnyCharUTF16(62 as u16) { - if string_utf16_of(">=") <= s.clone() { - ( - int!(2), - Arc::new(Token::Ge {}) - ) - } else { + if remaining == 1 { ( - int!(1), + 1, Arc::new(Token::Gt {}) ) + } else { + if s.get(&int!((&(pos + 1)).clone())) == DafnyCharUTF16(61 as u16) { + ( + 2, + Arc::new(Token::Ge {}) + ) + } else { + ( + 1, + Arc::new(Token::Gt {}) + ) + } } } else { - if _default::PrefixLower(&string_utf16_of("in"), s) { + if _default::PrefixLower(&string_utf16_of("in"), s, pos) { ( - int!(2), + 2, Arc::new(Token::In {}) ) } else { - if _default::PrefixLower(&string_utf16_of("between"), s) { + if _default::PrefixLower(&string_utf16_of("between"), s, pos) { ( - int!(7), + 7, Arc::new(Token::Between {}) ) } else { - if _default::PrefixLower(&string_utf16_of("and"), s) { + if _default::PrefixLower(&string_utf16_of("and"), s, pos) { ( - int!(3), + 3, Arc::new(Token::And {}) ) } else { - if _default::PrefixLower(&string_utf16_of("or"), s) { + if _default::PrefixLower(&string_utf16_of("or"), s, pos) { ( - int!(2), + 2, Arc::new(Token::Or {}) ) } else { - if _default::PrefixLower(&string_utf16_of("not"), s) { + if _default::PrefixLower(&string_utf16_of("not"), s, pos) { ( - int!(3), + 3, Arc::new(Token::Not {}) ) } else { - if _default::PrefixLower(&string_utf16_of("attribute_not_exists"), s) { + if _default::PrefixLower(&string_utf16_of("attribute_not_exists"), s, pos) { ( - int!(20), + 20, Arc::new(Token::AttributeNotExists {}) ) } else { - if _default::PrefixLower(&string_utf16_of("attribute_type"), s) { + if _default::PrefixLower(&string_utf16_of("attribute_type"), s, pos) { ( - int!(14), + 14, Arc::new(Token::AttributeType {}) ) } else { - if _default::PrefixLower(&string_utf16_of("begins_with"), s) { + if _default::PrefixLower(&string_utf16_of("begins_with"), s, pos) { ( - int!(11), + 11, Arc::new(Token::BeginsWith {}) ) } else { - if _default::PrefixLower(&string_utf16_of("attribute_exists"), s) { + if _default::PrefixLower(&string_utf16_of("attribute_exists"), s, pos) { ( - int!(16), + 16, Arc::new(Token::AttributeExists {}) ) } else { - if _default::PrefixLower(&string_utf16_of("contains"), s) { + if _default::PrefixLower(&string_utf16_of("contains"), s, pos) { ( - int!(8), + 8, Arc::new(Token::Contains {}) ) } else { - if _default::PrefixLower(&string_utf16_of("size"), s) { + if _default::PrefixLower(&string_utf16_of("size"), s, pos) { ( - int!(4), + 4, Arc::new(Token::Size {}) ) } else { if ch.clone() == DafnyCharUTF16(58 as u16) { - let mut x: DafnyInt = _default::ValueLen(&s.drop(&int!(1))) + int!(1); + let mut x: u64 = crate::implementation_from_dafny::_StandardLibrary_Compile::_MemoryMath_Compile::_default::Add(_default::ValueLen(s, crate::implementation_from_dafny::_StandardLibrary_Compile::_MemoryMath_Compile::_default::Add(pos, 1)), 1); ( - x.clone(), + x, Arc::new(Token::Value { - s: s.slice(&int!(0), &x) + s: s.slice(&int!((&pos).clone()), &int!((&(pos + x)).clone())) }) ) } else { if ch.clone() == DafnyCharUTF16(35 as u16) { - let mut x: DafnyInt = _default::ValueLen(&s.drop(&int!(1))) + int!(1); + let mut x: u64 = crate::implementation_from_dafny::_StandardLibrary_Compile::_MemoryMath_Compile::_default::Add(_default::ValueLen(s, crate::implementation_from_dafny::_StandardLibrary_Compile::_MemoryMath_Compile::_default::Add(pos, 1)), 1); ( - x.clone(), - _default::MakeAttr(&s.slice(&int!(0), &x)) + x, + _default::MakeAttr(&s.slice(&int!((&pos).clone()), &int!((&(pos + x)).clone()))) ) } else { - let mut x: nat = _default::AttributeLen(s); + let mut x: u64 = _default::AttributeLen(s, pos); ( - x.clone(), - _default::MakeAttr(&s.slice(&int!(0), &x)) + x, + _default::MakeAttr(&s.slice(&int!((&pos).clone()), &int!((&(pos + x)).clone()))) ) } } @@ -93483,63 +93520,64 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(826,3) - pub fn VarOrSize(input: &Sequence>) -> nat { - if input.cardinality() == int!(0) { - int!(0) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(866,3) + pub fn VarOrSize(input: &Sequence>, pos: u64) -> u64 { + if truncate!(input.cardinality(), u64) == pos { + 0 } else { - if matches!((&input.get(&int!(0))).as_ref(), Value{ .. }) || matches!((&input.get(&int!(0))).as_ref(), Attr{ .. }) { - int!(1) + if matches!((&input.get(&int!((&pos).clone()))).as_ref(), Value{ .. }) || matches!((&input.get(&int!((&pos).clone()))).as_ref(), Attr{ .. }) { + 1 } else { - if int!(3) < input.cardinality() && matches!((&input.get(&int!(0))).as_ref(), Size{ .. }) && matches!((&input.get(&int!(1))).as_ref(), Open{ .. }) && _default::IsVar(&input.get(&int!(2))) && matches!((&input.get(&int!(3))).as_ref(), Close{ .. }) { - int!(4) + if crate::implementation_from_dafny::_StandardLibrary_Compile::_MemoryMath_Compile::_default::Add(3, pos) < truncate!(input.cardinality(), u64) && matches!((&input.get(&int!((&pos).clone()))).as_ref(), Size{ .. }) && matches!((&input.get(&int!((&(pos + 1)).clone()))).as_ref(), Open{ .. }) && _default::IsVar(&input.get(&int!((&(pos + 2)).clone()))) && matches!((&input.get(&int!((&(pos + 3)).clone()))).as_ref(), Close{ .. }) { + 4 } else { - int!(0) + 0 } } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(841,3) - pub fn IsBetween(input: &Sequence>) -> Arc> { - if input.cardinality() < int!(5) { - Arc::new(Option::<(nat, nat, nat)>::None {}) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(883,3) + pub fn IsBetween(input: &Sequence>, pos: u64) -> Arc> { + let mut input_size: u64 = truncate!(input.cardinality(), u64); + if input_size < crate::implementation_from_dafny::_StandardLibrary_Compile::_MemoryMath_Compile::_default::Add(pos, 5) { + Arc::new(Option::<(u64, u64, u64)>::None {}) } else { - let mut p1: nat = _default::VarOrSize(input); - if int!(0) < p1.clone() && p1.clone() + int!(1) < input.cardinality() && matches!((&input.get(&p1)).as_ref(), Between{ .. }) { - let mut p2: nat = _default::VarOrSize(&input.drop(&(p1.clone() + int!(1)))); - if int!(0) < p2.clone() && p1.clone() + p2.clone() + int!(2) < input.cardinality() && matches!((&input.get(&(p1.clone() + p2.clone() + int!(1)))).as_ref(), And{ .. }) { - let mut p3: nat = _default::VarOrSize(&input.drop(&(p1.clone() + p2.clone() + int!(2)))); - if int!(0) < p3.clone() { - Arc::new(Option::<(nat, nat, nat)>::Some { + let mut p1: u64 = _default::VarOrSize(input, pos); + if 0 < p1 && crate::implementation_from_dafny::_StandardLibrary_Compile::_MemoryMath_Compile::_default::Add(pos + p1, 1) < input_size && matches!((&input.get(&int!((&(pos + p1)).clone()))).as_ref(), Between{ .. }) { + let mut p2: u64 = _default::VarOrSize(input, pos + p1 + 1); + if 0 < p2 && crate::implementation_from_dafny::_StandardLibrary_Compile::_MemoryMath_Compile::_default::Add(pos + p1 + p2, 2) < input_size && matches!((&input.get(&int!((&(pos + p1 + p2 + 1)).clone()))).as_ref(), And{ .. }) { + let mut p3: u64 = _default::VarOrSize(input, pos + p1 + p2 + 2); + if 0 < p3 { + Arc::new(Option::<(u64, u64, u64)>::Some { value: ( - p1.clone(), - p2.clone(), - p3.clone() + p1, + p2, + p3 ) }) } else { - Arc::new(Option::<(nat, nat, nat)>::None {}) + Arc::new(Option::<(u64, u64, u64)>::None {}) } } else { - Arc::new(Option::<(nat, nat, nat)>::None {}) + Arc::new(Option::<(u64, u64, u64)>::None {}) } } else { - Arc::new(Option::<(nat, nat, nat)>::None {}) + Arc::new(Option::<(u64, u64, u64)>::None {}) } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(864,3) - pub fn IsIN(input: &Sequence>) -> bool { - if input.cardinality() < int!(3) { + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(909,3) + pub fn IsIN(input: &Sequence>, pos: u64) -> bool { + if truncate!(input.cardinality(), u64) < crate::implementation_from_dafny::_StandardLibrary_Compile::_MemoryMath_Compile::_default::Add(pos, 3) { false } else { - if !_default::IsVar(&input.get(&int!(0))) { + if !_default::IsVar(&input.get(&int!((&pos).clone()))) { false } else { - if input.get(&int!(1)) != Arc::new(Token::In {}) { + if input.get(&int!((&(pos + 1)).clone())) != Arc::new(Token::In {}) { false } else { - if input.get(&int!(2)) != Arc::new(Token::Open {}) { + if input.get(&int!((&(pos + 2)).clone())) != Arc::new(Token::Open {}) { false } else { true @@ -93548,333 +93586,405 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(880,3) - pub fn ConvertToPrefix(input: &Sequence>) -> Sequence> { + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(927,3) + pub fn ConvertToPrefix(input: &Sequence>, pos: u64) -> Sequence> { let mut _accumulator: Sequence> = seq![] as Sequence>; let mut _r0 = input.clone(); + let mut _r1 = pos; 'TAIL_CALL_START: loop { let input = _r0; - let mut between: Arc> = _default::IsBetween(&input); - if input.cardinality() < int!(5) { - return _accumulator.concat(&input); + let pos = _r1; + if truncate!(input.cardinality(), u64) < crate::implementation_from_dafny::_StandardLibrary_Compile::_MemoryMath_Compile::_default::Add(pos, 5) { + return _accumulator.concat(&input.drop(&int!((&pos).clone()))); } else { - if _default::IsIN(&input) { - _accumulator = _accumulator.concat(&seq![input.get(&int!(1)), input.get(&int!(2)), input.get(&int!(0)), Arc::new(Token::Comma {})]); - let mut _in0: Sequence> = input.drop(&int!(3)); + if _default::IsIN(&input, pos) { + _accumulator = _accumulator.concat(&seq![input.get(&int!((&(pos + 1)).clone())), input.get(&int!((&(pos + 2)).clone())), input.get(&int!((&pos).clone())), Arc::new(Token::Comma {})]); + let mut _in0: Sequence> = input.clone(); + let mut _in1: u64 = pos + 3; _r0 = _in0.clone(); + _r1 = _in1; continue 'TAIL_CALL_START; } else { + let mut between: Arc> = _default::IsBetween(&input, pos); if matches!((&between).as_ref(), Some{ .. }) { - let mut b: (DafnyInt, DafnyInt, DafnyInt) = between.value().clone(); - _accumulator = _accumulator.concat(&seq![Arc::new(Token::Between {}), Arc::new(Token::Open {})].concat(&input.slice(&int!(0), &b.0.clone())).concat(&seq![Arc::new(Token::Comma {})]).concat(&input.slice(&(b.0.clone() + int!(1)), &(b.0.clone() + b.1.clone() + int!(1)))).concat(&seq![Arc::new(Token::Comma {})]).concat(&input.slice(&(b.0.clone() + b.1.clone() + int!(2)), &(b.0.clone() + b.1.clone() + b.2.clone() + int!(2)))).concat(&seq![Arc::new(Token::Close {})])); - let mut _in1: Sequence> = input.drop(&(b.0.clone() + b.1.clone() + b.2.clone() + int!(2))); - _r0 = _in1.clone(); + let mut b: (u64, u64, u64) = between.value().clone(); + _accumulator = _accumulator.concat(&seq![Arc::new(Token::Between {}), Arc::new(Token::Open {})].concat(&input.slice(&int!((&pos).clone()), &int!((&(pos + b.0.clone())).clone()))).concat(&seq![Arc::new(Token::Comma {})]).concat(&input.slice(&int!((&(pos + b.0.clone() + 1)).clone()), &int!((&(pos + b.0.clone() + b.1.clone() + 1)).clone()))).concat(&seq![Arc::new(Token::Comma {})]).concat(&input.slice(&int!((&(pos + b.0.clone() + b.1.clone() + 2)).clone()), &int!((&(pos + b.0.clone() + b.1.clone() + b.2.clone() + 2)).clone()))).concat(&seq![Arc::new(Token::Close {})])); + let mut _in2: Sequence> = input.clone(); + let mut _in3: u64 = pos + b.0.clone() + b.1.clone() + b.2.clone() + 2; + _r0 = _in2.clone(); + _r1 = _in3; continue 'TAIL_CALL_START; } else { - _accumulator = _accumulator.concat(&seq![input.get(&int!(0))]); - let mut _in2: Sequence> = input.drop(&int!(1)); - _r0 = _in2.clone(); + _accumulator = _accumulator.concat(&seq![input.get(&int!((&pos).clone()))]); + let mut _in4: Sequence> = input.clone(); + let mut _in5: u64 = pos + 1; + _r0 = _in4.clone(); + _r1 = _in5; continue 'TAIL_CALL_START; } } } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(903,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(954,3) pub fn ConvertToRpn(input: &Sequence>) -> Sequence> { let mut stack: Sequence> = seq![] as Sequence>; - _default::ConvertToRpn_inner(input, &stack) + _default::ConvertToRpn_inner(input, &stack, 0) } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(910,3) - pub fn ConvertToRpn_inner(input: &Sequence>, stack: &Sequence>) -> Sequence> { + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(961,3) + pub fn ConvertToRpn_inner(input: &Sequence>, stack: &Sequence>, pos: u64) -> Sequence> { let mut _accumulator: Sequence> = seq![] as Sequence>; let mut _r0 = input.clone(); let mut _r1 = stack.clone(); + let mut _r2 = pos; 'TAIL_CALL_START: loop { let input = _r0; let stack = _r1; - if int!(0) == input.cardinality() { + let pos = _r2; + if pos == truncate!(input.cardinality(), u64) { if int!(0) == stack.cardinality() { return _accumulator.concat(&(seq![] as Sequence>)); } else { _accumulator = _accumulator.concat(&seq![stack.get(&(stack.cardinality() - int!(1)))]); let mut _in0: Sequence> = input.clone(); let mut _in1: Sequence> = stack.take(&(stack.cardinality() - int!(1))); + let mut _in2: u64 = pos; _r0 = _in0.clone(); _r1 = _in1.clone(); + _r2 = _in2; continue 'TAIL_CALL_START; } } else { - let mut _source0: Arc = input.get(&int!(0)); + let mut _source0: Arc = input.get(&int!((&pos).clone())); if matches!((&_source0).as_ref(), Attr{ .. }) { let mut ___mcc_h0: Sequence = _source0.s().clone(); let mut ___mcc_h1: TermLoc = _source0.loc().clone(); let mut loc: TermLoc = ___mcc_h1.clone(); let mut s: Sequence = ___mcc_h0.clone(); - return _accumulator.concat(&seq![input.get(&int!(0))].concat(&_default::ConvertToRpn_inner(&input.drop(&int!(1)), &stack))); + return _accumulator.concat(&seq![input.get(&int!((&pos).clone()))].concat(&_default::ConvertToRpn_inner(&input, &stack, pos + 1))); } else { if matches!((&_source0).as_ref(), Value{ .. }) { let mut ___mcc_h2: Sequence = _source0.s().clone(); let mut s: Sequence = ___mcc_h2.clone(); - return _accumulator.concat(&seq![input.get(&int!(0))].concat(&_default::ConvertToRpn_inner(&input.drop(&int!(1)), &stack))); + return _accumulator.concat(&seq![input.get(&int!((&pos).clone()))].concat(&_default::ConvertToRpn_inner(&input, &stack, pos + 1))); } else { if matches!((&_source0).as_ref(), crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::Token::Eq{ .. }) { if int!(0) == stack.cardinality() { - let mut _in2: Sequence> = input.drop(&int!(1)); - let mut _in3: Sequence> = stack.concat(&seq![input.get(&int!(0))]); - _r0 = _in2.clone(); - _r1 = _in3.clone(); + let mut _in3: Sequence> = input.clone(); + let mut _in4: Sequence> = stack.concat(&seq![input.get(&int!((&pos).clone()))]); + let mut _in5: u64 = pos + 1; + _r0 = _in3.clone(); + _r1 = _in4.clone(); + _r2 = _in5; continue 'TAIL_CALL_START; } else { - if _default::Precedence(&stack.get(&(stack.cardinality() - int!(1)))) >= _default::Precedence(&input.get(&int!(0))) { - return _accumulator.concat(&seq![stack.get(&(stack.cardinality() - int!(1)))].concat(&_default::ConvertToRpn_inner(&input, &stack.take(&(stack.cardinality() - int!(1)))))); + if _default::Precedence(&stack.get(&(stack.cardinality() - int!(1)))) >= _default::Precedence(&input.get(&int!((&pos).clone()))) { + return _accumulator.concat(&seq![stack.get(&(stack.cardinality() - int!(1)))].concat(&_default::ConvertToRpn_inner(&input, &stack.take(&(stack.cardinality() - int!(1))), pos))); } else { - let mut _in4: Sequence> = input.drop(&int!(1)); - let mut _in5: Sequence> = stack.concat(&seq![input.get(&int!(0))]); - _r0 = _in4.clone(); - _r1 = _in5.clone(); + let mut _in6: Sequence> = input.clone(); + let mut _in7: Sequence> = stack.concat(&seq![input.get(&int!((&pos).clone()))]); + let mut _in8: u64 = pos + 1; + _r0 = _in6.clone(); + _r1 = _in7.clone(); + _r2 = _in8; continue 'TAIL_CALL_START; } } } else { if matches!((&_source0).as_ref(), Ne{ .. }) { if int!(0) == stack.cardinality() { - let mut _in6: Sequence> = input.drop(&int!(1)); - let mut _in7: Sequence> = stack.concat(&seq![input.get(&int!(0))]); - _r0 = _in6.clone(); - _r1 = _in7.clone(); + let mut _in9: Sequence> = input.clone(); + let mut _in10: Sequence> = stack.concat(&seq![input.get(&int!((&pos).clone()))]); + let mut _in11: u64 = pos + 1; + _r0 = _in9.clone(); + _r1 = _in10.clone(); + _r2 = _in11; continue 'TAIL_CALL_START; } else { - if _default::Precedence(&stack.get(&(stack.cardinality() - int!(1)))) >= _default::Precedence(&input.get(&int!(0))) { - return _accumulator.concat(&seq![stack.get(&(stack.cardinality() - int!(1)))].concat(&_default::ConvertToRpn_inner(&input, &stack.take(&(stack.cardinality() - int!(1)))))); + if _default::Precedence(&stack.get(&(stack.cardinality() - int!(1)))) >= _default::Precedence(&input.get(&int!((&pos).clone()))) { + return _accumulator.concat(&seq![stack.get(&(stack.cardinality() - int!(1)))].concat(&_default::ConvertToRpn_inner(&input, &stack.take(&(stack.cardinality() - int!(1))), pos))); } else { - let mut _in8: Sequence> = input.drop(&int!(1)); - let mut _in9: Sequence> = stack.concat(&seq![input.get(&int!(0))]); - _r0 = _in8.clone(); - _r1 = _in9.clone(); + let mut _in12: Sequence> = input.clone(); + let mut _in13: Sequence> = stack.concat(&seq![input.get(&int!((&pos).clone()))]); + let mut _in14: u64 = pos + 1; + _r0 = _in12.clone(); + _r1 = _in13.clone(); + _r2 = _in14; continue 'TAIL_CALL_START; } } } else { if matches!((&_source0).as_ref(), Lt{ .. }) { if int!(0) == stack.cardinality() { - let mut _in10: Sequence> = input.drop(&int!(1)); - let mut _in11: Sequence> = stack.concat(&seq![input.get(&int!(0))]); - _r0 = _in10.clone(); - _r1 = _in11.clone(); + let mut _in15: Sequence> = input.clone(); + let mut _in16: Sequence> = stack.concat(&seq![input.get(&int!((&pos).clone()))]); + let mut _in17: u64 = pos + 1; + _r0 = _in15.clone(); + _r1 = _in16.clone(); + _r2 = _in17; continue 'TAIL_CALL_START; } else { - if _default::Precedence(&stack.get(&(stack.cardinality() - int!(1)))) >= _default::Precedence(&input.get(&int!(0))) { - return _accumulator.concat(&seq![stack.get(&(stack.cardinality() - int!(1)))].concat(&_default::ConvertToRpn_inner(&input, &stack.take(&(stack.cardinality() - int!(1)))))); + if _default::Precedence(&stack.get(&(stack.cardinality() - int!(1)))) >= _default::Precedence(&input.get(&int!((&pos).clone()))) { + return _accumulator.concat(&seq![stack.get(&(stack.cardinality() - int!(1)))].concat(&_default::ConvertToRpn_inner(&input, &stack.take(&(stack.cardinality() - int!(1))), pos))); } else { - let mut _in12: Sequence> = input.drop(&int!(1)); - let mut _in13: Sequence> = stack.concat(&seq![input.get(&int!(0))]); - _r0 = _in12.clone(); - _r1 = _in13.clone(); + let mut _in18: Sequence> = input.clone(); + let mut _in19: Sequence> = stack.concat(&seq![input.get(&int!((&pos).clone()))]); + let mut _in20: u64 = pos + 1; + _r0 = _in18.clone(); + _r1 = _in19.clone(); + _r2 = _in20; continue 'TAIL_CALL_START; } } } else { if matches!((&_source0).as_ref(), Gt{ .. }) { if int!(0) == stack.cardinality() { - let mut _in14: Sequence> = input.drop(&int!(1)); - let mut _in15: Sequence> = stack.concat(&seq![input.get(&int!(0))]); - _r0 = _in14.clone(); - _r1 = _in15.clone(); + let mut _in21: Sequence> = input.clone(); + let mut _in22: Sequence> = stack.concat(&seq![input.get(&int!((&pos).clone()))]); + let mut _in23: u64 = pos + 1; + _r0 = _in21.clone(); + _r1 = _in22.clone(); + _r2 = _in23; continue 'TAIL_CALL_START; } else { - if _default::Precedence(&stack.get(&(stack.cardinality() - int!(1)))) >= _default::Precedence(&input.get(&int!(0))) { - return _accumulator.concat(&seq![stack.get(&(stack.cardinality() - int!(1)))].concat(&_default::ConvertToRpn_inner(&input, &stack.take(&(stack.cardinality() - int!(1)))))); + if _default::Precedence(&stack.get(&(stack.cardinality() - int!(1)))) >= _default::Precedence(&input.get(&int!((&pos).clone()))) { + return _accumulator.concat(&seq![stack.get(&(stack.cardinality() - int!(1)))].concat(&_default::ConvertToRpn_inner(&input, &stack.take(&(stack.cardinality() - int!(1))), pos))); } else { - let mut _in16: Sequence> = input.drop(&int!(1)); - let mut _in17: Sequence> = stack.concat(&seq![input.get(&int!(0))]); - _r0 = _in16.clone(); - _r1 = _in17.clone(); + let mut _in24: Sequence> = input.clone(); + let mut _in25: Sequence> = stack.concat(&seq![input.get(&int!((&pos).clone()))]); + let mut _in26: u64 = pos + 1; + _r0 = _in24.clone(); + _r1 = _in25.clone(); + _r2 = _in26; continue 'TAIL_CALL_START; } } } else { if matches!((&_source0).as_ref(), Le{ .. }) { if int!(0) == stack.cardinality() { - let mut _in18: Sequence> = input.drop(&int!(1)); - let mut _in19: Sequence> = stack.concat(&seq![input.get(&int!(0))]); - _r0 = _in18.clone(); - _r1 = _in19.clone(); + let mut _in27: Sequence> = input.clone(); + let mut _in28: Sequence> = stack.concat(&seq![input.get(&int!((&pos).clone()))]); + let mut _in29: u64 = pos + 1; + _r0 = _in27.clone(); + _r1 = _in28.clone(); + _r2 = _in29; continue 'TAIL_CALL_START; } else { - if _default::Precedence(&stack.get(&(stack.cardinality() - int!(1)))) >= _default::Precedence(&input.get(&int!(0))) { - return _accumulator.concat(&seq![stack.get(&(stack.cardinality() - int!(1)))].concat(&_default::ConvertToRpn_inner(&input, &stack.take(&(stack.cardinality() - int!(1)))))); + if _default::Precedence(&stack.get(&(stack.cardinality() - int!(1)))) >= _default::Precedence(&input.get(&int!((&pos).clone()))) { + return _accumulator.concat(&seq![stack.get(&(stack.cardinality() - int!(1)))].concat(&_default::ConvertToRpn_inner(&input, &stack.take(&(stack.cardinality() - int!(1))), pos))); } else { - let mut _in20: Sequence> = input.drop(&int!(1)); - let mut _in21: Sequence> = stack.concat(&seq![input.get(&int!(0))]); - _r0 = _in20.clone(); - _r1 = _in21.clone(); + let mut _in30: Sequence> = input.clone(); + let mut _in31: Sequence> = stack.concat(&seq![input.get(&int!((&pos).clone()))]); + let mut _in32: u64 = pos + 1; + _r0 = _in30.clone(); + _r1 = _in31.clone(); + _r2 = _in32; continue 'TAIL_CALL_START; } } } else { if matches!((&_source0).as_ref(), Ge{ .. }) { if int!(0) == stack.cardinality() { - let mut _in22: Sequence> = input.drop(&int!(1)); - let mut _in23: Sequence> = stack.concat(&seq![input.get(&int!(0))]); - _r0 = _in22.clone(); - _r1 = _in23.clone(); + let mut _in33: Sequence> = input.clone(); + let mut _in34: Sequence> = stack.concat(&seq![input.get(&int!((&pos).clone()))]); + let mut _in35: u64 = pos + 1; + _r0 = _in33.clone(); + _r1 = _in34.clone(); + _r2 = _in35; continue 'TAIL_CALL_START; } else { - if _default::Precedence(&stack.get(&(stack.cardinality() - int!(1)))) >= _default::Precedence(&input.get(&int!(0))) { - return _accumulator.concat(&seq![stack.get(&(stack.cardinality() - int!(1)))].concat(&_default::ConvertToRpn_inner(&input, &stack.take(&(stack.cardinality() - int!(1)))))); + if _default::Precedence(&stack.get(&(stack.cardinality() - int!(1)))) >= _default::Precedence(&input.get(&int!((&pos).clone()))) { + return _accumulator.concat(&seq![stack.get(&(stack.cardinality() - int!(1)))].concat(&_default::ConvertToRpn_inner(&input, &stack.take(&(stack.cardinality() - int!(1))), pos))); } else { - let mut _in24: Sequence> = input.drop(&int!(1)); - let mut _in25: Sequence> = stack.concat(&seq![input.get(&int!(0))]); - _r0 = _in24.clone(); - _r1 = _in25.clone(); + let mut _in36: Sequence> = input.clone(); + let mut _in37: Sequence> = stack.concat(&seq![input.get(&int!((&pos).clone()))]); + let mut _in38: u64 = pos + 1; + _r0 = _in36.clone(); + _r1 = _in37.clone(); + _r2 = _in38; continue 'TAIL_CALL_START; } } } else { if matches!((&_source0).as_ref(), Between{ .. }) { - let mut _in26: Sequence> = input.drop(&int!(1)); - let mut _in27: Sequence> = stack.concat(&seq![input.get(&int!(0))]); - _r0 = _in26.clone(); - _r1 = _in27.clone(); + let mut _in39: Sequence> = input.clone(); + let mut _in40: Sequence> = stack.concat(&seq![input.get(&int!((&pos).clone()))]); + let mut _in41: u64 = pos + 1; + _r0 = _in39.clone(); + _r1 = _in40.clone(); + _r2 = _in41; continue 'TAIL_CALL_START; } else { if matches!((&_source0).as_ref(), In{ .. }) { - let mut _in28: Sequence> = input.drop(&int!(1)); - let mut _in29: Sequence> = stack.concat(&seq![input.get(&int!(0))]); - _r0 = _in28.clone(); - _r1 = _in29.clone(); + let mut _in42: Sequence> = input.clone(); + let mut _in43: Sequence> = stack.concat(&seq![input.get(&int!((&pos).clone()))]); + let mut _in44: u64 = pos + 1; + _r0 = _in42.clone(); + _r1 = _in43.clone(); + _r2 = _in44; continue 'TAIL_CALL_START; } else { if matches!((&_source0).as_ref(), Open{ .. }) { - let mut _in30: Sequence> = input.drop(&int!(1)); - let mut _in31: Sequence> = stack.clone(); - _r0 = _in30.clone(); - _r1 = _in31.clone(); + let mut _in45: Sequence> = input.clone(); + let mut _in46: Sequence> = stack.clone(); + let mut _in47: u64 = pos + 1; + _r0 = _in45.clone(); + _r1 = _in46.clone(); + _r2 = _in47; continue 'TAIL_CALL_START; } else { if matches!((&_source0).as_ref(), Close{ .. }) { if int!(0) == stack.cardinality() { - let mut _in32: Sequence> = input.drop(&int!(1)); - let mut _in33: Sequence> = stack.clone(); - _r0 = _in32.clone(); - _r1 = _in33.clone(); + let mut _in48: Sequence> = input.clone(); + let mut _in49: Sequence> = stack.clone(); + let mut _in50: u64 = pos + 1; + _r0 = _in48.clone(); + _r1 = _in49.clone(); + _r2 = _in50; continue 'TAIL_CALL_START; } else { if stack.get(&(stack.cardinality() - int!(1))) == Arc::new(Token::Open {}) { - let mut _in34: Sequence> = input.drop(&int!(1)); - let mut _in35: Sequence> = stack.take(&(stack.cardinality() - int!(1))); - _r0 = _in34.clone(); - _r1 = _in35.clone(); + let mut _in51: Sequence> = input.clone(); + let mut _in52: Sequence> = stack.take(&(stack.cardinality() - int!(1))); + let mut _in53: u64 = pos + 1; + _r0 = _in51.clone(); + _r1 = _in52.clone(); + _r2 = _in53; continue 'TAIL_CALL_START; } else { - return _accumulator.concat(&seq![stack.get(&(stack.cardinality() - int!(1)))].concat(&_default::ConvertToRpn_inner(&input.drop(&int!(1)), &stack.take(&(stack.cardinality() - int!(1)))))); + return _accumulator.concat(&seq![stack.get(&(stack.cardinality() - int!(1)))].concat(&_default::ConvertToRpn_inner(&input, &stack.take(&(stack.cardinality() - int!(1))), pos + 1))); } } } else { if matches!((&_source0).as_ref(), Comma{ .. }) { if int!(0) < stack.cardinality() { if _default::IsFunction(&stack.get(&(stack.cardinality() - int!(1)))) { - let mut _in36: Sequence> = input.drop(&int!(1)); - let mut _in37: Sequence> = stack.clone(); - _r0 = _in36.clone(); - _r1 = _in37.clone(); + let mut _in54: Sequence> = input.clone(); + let mut _in55: Sequence> = stack.clone(); + let mut _in56: u64 = pos + 1; + _r0 = _in54.clone(); + _r1 = _in55.clone(); + _r2 = _in56; continue 'TAIL_CALL_START; } else { - return _accumulator.concat(&seq![stack.get(&(stack.cardinality() - int!(1)))].concat(&_default::ConvertToRpn_inner(&input.drop(&int!(1)), &stack.take(&(stack.cardinality() - int!(1)))))); + return _accumulator.concat(&seq![stack.get(&(stack.cardinality() - int!(1)))].concat(&_default::ConvertToRpn_inner(&input, &stack.take(&(stack.cardinality() - int!(1))), pos + 1))); } } else { - let mut _in38: Sequence> = input.drop(&int!(1)); - let mut _in39: Sequence> = stack.clone(); - _r0 = _in38.clone(); - _r1 = _in39.clone(); + let mut _in57: Sequence> = input.clone(); + let mut _in58: Sequence> = stack.clone(); + let mut _in59: u64 = pos + 1; + _r0 = _in57.clone(); + _r1 = _in58.clone(); + _r2 = _in59; continue 'TAIL_CALL_START; } } else { if matches!((&_source0).as_ref(), Not{ .. }) { - let mut _in40: Sequence> = input.drop(&int!(1)); - let mut _in41: Sequence> = stack.concat(&seq![input.get(&int!(0))]); - _r0 = _in40.clone(); - _r1 = _in41.clone(); + let mut _in60: Sequence> = input.clone(); + let mut _in61: Sequence> = stack.concat(&seq![input.get(&int!((&pos).clone()))]); + let mut _in62: u64 = pos + 1; + _r0 = _in60.clone(); + _r1 = _in61.clone(); + _r2 = _in62; continue 'TAIL_CALL_START; } else { if matches!((&_source0).as_ref(), And{ .. }) { if int!(0) == stack.cardinality() { - let mut _in42: Sequence> = input.drop(&int!(1)); - let mut _in43: Sequence> = stack.concat(&seq![input.get(&int!(0))]); - _r0 = _in42.clone(); - _r1 = _in43.clone(); + let mut _in63: Sequence> = input.clone(); + let mut _in64: Sequence> = stack.concat(&seq![input.get(&int!((&pos).clone()))]); + let mut _in65: u64 = pos + 1; + _r0 = _in63.clone(); + _r1 = _in64.clone(); + _r2 = _in65; continue 'TAIL_CALL_START; } else { - if _default::Precedence(&stack.get(&(stack.cardinality() - int!(1)))) >= _default::Precedence(&input.get(&int!(0))) { - return _accumulator.concat(&seq![stack.get(&(stack.cardinality() - int!(1)))].concat(&_default::ConvertToRpn_inner(&input, &stack.take(&(stack.cardinality() - int!(1)))))); + if _default::Precedence(&stack.get(&(stack.cardinality() - int!(1)))) >= _default::Precedence(&input.get(&int!((&pos).clone()))) { + return _accumulator.concat(&seq![stack.get(&(stack.cardinality() - int!(1)))].concat(&_default::ConvertToRpn_inner(&input, &stack.take(&(stack.cardinality() - int!(1))), pos))); } else { - let mut _in44: Sequence> = input.drop(&int!(1)); - let mut _in45: Sequence> = stack.concat(&seq![input.get(&int!(0))]); - _r0 = _in44.clone(); - _r1 = _in45.clone(); + let mut _in66: Sequence> = input.clone(); + let mut _in67: Sequence> = stack.concat(&seq![input.get(&int!((&pos).clone()))]); + let mut _in68: u64 = pos + 1; + _r0 = _in66.clone(); + _r1 = _in67.clone(); + _r2 = _in68; continue 'TAIL_CALL_START; } } } else { if matches!((&_source0).as_ref(), Or{ .. }) { if int!(0) == stack.cardinality() { - let mut _in46: Sequence> = input.drop(&int!(1)); - let mut _in47: Sequence> = stack.concat(&seq![input.get(&int!(0))]); - _r0 = _in46.clone(); - _r1 = _in47.clone(); + let mut _in69: Sequence> = input.clone(); + let mut _in70: Sequence> = stack.concat(&seq![input.get(&int!((&pos).clone()))]); + let mut _in71: u64 = pos + 1; + _r0 = _in69.clone(); + _r1 = _in70.clone(); + _r2 = _in71; continue 'TAIL_CALL_START; } else { - if _default::Precedence(&stack.get(&(stack.cardinality() - int!(1)))) >= _default::Precedence(&input.get(&int!(0))) { - return _accumulator.concat(&seq![stack.get(&(stack.cardinality() - int!(1)))].concat(&_default::ConvertToRpn_inner(&input, &stack.take(&(stack.cardinality() - int!(1)))))); + if _default::Precedence(&stack.get(&(stack.cardinality() - int!(1)))) >= _default::Precedence(&input.get(&int!((&pos).clone()))) { + return _accumulator.concat(&seq![stack.get(&(stack.cardinality() - int!(1)))].concat(&_default::ConvertToRpn_inner(&input, &stack.take(&(stack.cardinality() - int!(1))), pos))); } else { - let mut _in48: Sequence> = input.drop(&int!(1)); - let mut _in49: Sequence> = stack.concat(&seq![input.get(&int!(0))]); - _r0 = _in48.clone(); - _r1 = _in49.clone(); + let mut _in72: Sequence> = input.clone(); + let mut _in73: Sequence> = stack.concat(&seq![input.get(&int!((&pos).clone()))]); + let mut _in74: u64 = pos + 1; + _r0 = _in72.clone(); + _r1 = _in73.clone(); + _r2 = _in74; continue 'TAIL_CALL_START; } } } else { if matches!((&_source0).as_ref(), AttributeExists{ .. }) { - let mut _in50: Sequence> = input.drop(&int!(1)); - let mut _in51: Sequence> = stack.concat(&seq![input.get(&int!(0))]); - _r0 = _in50.clone(); - _r1 = _in51.clone(); + let mut _in75: Sequence> = input.clone(); + let mut _in76: Sequence> = stack.concat(&seq![input.get(&int!((&pos).clone()))]); + let mut _in77: u64 = pos + 1; + _r0 = _in75.clone(); + _r1 = _in76.clone(); + _r2 = _in77; continue 'TAIL_CALL_START; } else { if matches!((&_source0).as_ref(), AttributeNotExists{ .. }) { - let mut _in52: Sequence> = input.drop(&int!(1)); - let mut _in53: Sequence> = stack.concat(&seq![input.get(&int!(0))]); - _r0 = _in52.clone(); - _r1 = _in53.clone(); + let mut _in78: Sequence> = input.clone(); + let mut _in79: Sequence> = stack.concat(&seq![input.get(&int!((&pos).clone()))]); + let mut _in80: u64 = pos + 1; + _r0 = _in78.clone(); + _r1 = _in79.clone(); + _r2 = _in80; continue 'TAIL_CALL_START; } else { if matches!((&_source0).as_ref(), AttributeType{ .. }) { - let mut _in54: Sequence> = input.drop(&int!(1)); - let mut _in55: Sequence> = stack.concat(&seq![input.get(&int!(0))]); - _r0 = _in54.clone(); - _r1 = _in55.clone(); + let mut _in81: Sequence> = input.clone(); + let mut _in82: Sequence> = stack.concat(&seq![input.get(&int!((&pos).clone()))]); + let mut _in83: u64 = pos + 1; + _r0 = _in81.clone(); + _r1 = _in82.clone(); + _r2 = _in83; continue 'TAIL_CALL_START; } else { if matches!((&_source0).as_ref(), BeginsWith{ .. }) { - let mut _in56: Sequence> = input.drop(&int!(1)); - let mut _in57: Sequence> = stack.concat(&seq![input.get(&int!(0))]); - _r0 = _in56.clone(); - _r1 = _in57.clone(); + let mut _in84: Sequence> = input.clone(); + let mut _in85: Sequence> = stack.concat(&seq![input.get(&int!((&pos).clone()))]); + let mut _in86: u64 = pos + 1; + _r0 = _in84.clone(); + _r1 = _in85.clone(); + _r2 = _in86; continue 'TAIL_CALL_START; } else { if matches!((&_source0).as_ref(), Contains{ .. }) { - let mut _in58: Sequence> = input.drop(&int!(1)); - let mut _in59: Sequence> = stack.concat(&seq![input.get(&int!(0))]); - _r0 = _in58.clone(); - _r1 = _in59.clone(); + let mut _in87: Sequence> = input.clone(); + let mut _in88: Sequence> = stack.concat(&seq![input.get(&int!((&pos).clone()))]); + let mut _in89: u64 = pos + 1; + _r0 = _in87.clone(); + _r1 = _in88.clone(); + _r2 = _in89; continue 'TAIL_CALL_START; } else { - let mut _in60: Sequence> = input.drop(&int!(1)); - let mut _in61: Sequence> = stack.concat(&seq![input.get(&int!(0))]); - _r0 = _in60.clone(); - _r1 = _in61.clone(); + let mut _in90: Sequence> = input.clone(); + let mut _in91: Sequence> = stack.concat(&seq![input.get(&int!((&pos).clone()))]); + let mut _in92: u64 = pos + 1; + _r0 = _in90.clone(); + _r1 = _in91.clone(); + _r2 = _in92; continue 'TAIL_CALL_START; } } @@ -93900,7 +94010,7 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(955,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1009,3) pub fn GetSize(value: &Arc) -> nat { let mut _source0: Arc = value.clone(); if matches!((&_source0).as_ref(), S{ .. }) { @@ -93961,7 +94071,7 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(972,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1026,3) pub fn GetStr(s: &Arc) -> Arc { let mut _source0: Arc = s.clone(); if matches!((&_source0).as_ref(), Bool{ .. }) { @@ -93982,7 +94092,7 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(981,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1035,3) pub fn AsStr(s: &Sequence) -> Arc { Arc::new(StackValue::Str { s: Arc::new(AttributeValue::S { @@ -93990,7 +94100,7 @@ pub mod _DynamoDBFilterExpr_Compile { }) }) } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(986,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1040,3) pub fn StackValueFromValue(s: &Sequence, values: &Map, Arc>) -> Arc { if values.contains(s) { Arc::new(StackValue::Str { @@ -94000,7 +94110,7 @@ pub mod _DynamoDBFilterExpr_Compile { Arc::new(StackValue::DoesNotExist {}) } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(997,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1051,3) pub fn StackValueFromItem(s: &Sequence, item: &Map, Arc>) -> Arc { if item.contains(s) { Arc::new(StackValue::Str { @@ -94010,7 +94120,7 @@ pub mod _DynamoDBFilterExpr_Compile { Arc::new(StackValue::DoesNotExist {}) } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1009,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1063,3) pub fn StackValueFromAttr(t: &Arc, item: &Map, Arc>, names: &Arc, Sequence>>>) -> Arc { if matches!(names.as_ref(), Some{ .. }) && names.value().contains(t.s()) { _default::StackValueFromItem(&names.value().get(t.s()), item) @@ -94025,19 +94135,22 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1028,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1082,3) pub fn GetParsedExpr(input: &Sequence) -> Arc>, Arc>> { - let mut seq1: Sequence> = _default::ParseExpr(input); - let mut seq2: Sequence> = _default::ConvertToPrefix(&seq1); + let mut seq1: Sequence> = _default::ParseExpr(input, 0); + let mut seq2: Sequence> = _default::ConvertToPrefix(&seq1, 0); Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::>, Arc>::Success { value: _default::ConvertToRpn(&seq2) }) } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1036,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1090,3) pub fn EvalExpr(input: &Sequence>, item: &Map, Arc>, names: &Arc, Sequence>>>, values: &Map, Arc>) -> Arc>> { - _default::InnerEvalExpr(input, &(seq![] as Sequence>), item, names, values) + let mut ret: Arc>>; + let mut _out0: Arc>> = _default::InnerEvalExpr(input, &(seq![] as Sequence>), item, names, values, 0); + ret = _out0.clone(); + return ret.clone(); } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1048,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1102,3) pub fn StringsFollowing(input: &Sequence>) -> nat { let mut _accumulator: nat = int!(0); let mut _r0 = input.clone(); @@ -94057,108 +94170,104 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1059,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1113,3) pub fn seq_contains<_T: DafnyTypeEq>(haystack: &Sequence<_T>, needle: &Sequence<_T>) -> bool { - let mut _r0 = haystack.clone(); - let mut _r1 = needle.clone(); - 'TAIL_CALL_START: loop { - let haystack = _r0; - let needle = _r1; - if needle.cardinality() == int!(0) { - return true; - } else { - if haystack.cardinality() == int!(0) { - return false; - } else { - if haystack.cardinality() < needle.cardinality() { - return false; - } else { - if needle.get(&int!(0)) == haystack.get(&int!(0)) && needle.drop(&int!(1)) <= haystack.drop(&int!(1)) { - return true; - } else { - let mut _in0: Sequence<_T> = haystack.drop(&int!(1)); - let mut _in1: Sequence<_T> = needle.clone(); - _r0 = _in0.clone(); - _r1 = _in1.clone(); - continue 'TAIL_CALL_START; - } - } - } - } - } + let mut ret: bool = ::default(); + let mut result: Arc>; + let mut _out0: Arc> = crate::implementation_from_dafny::_StandardLibrary_Compile::_String_Compile::_default::HasSubString::<_T>(haystack, needle); + result = _out0.clone(); + ret = matches!((&result).as_ref(), Some{ .. }); + return ret; } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1074,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1120,3) pub fn does_contain(haystack: &Arc, needle: &Arc) -> bool { + let mut ret: bool = ::default(); let mut _source0: Arc = haystack.clone(); if matches!((&_source0).as_ref(), S{ .. }) { let mut ___mcc_h0: Sequence = _source0.S().clone(); let mut s: Sequence = ___mcc_h0.clone(); if matches!(needle.as_ref(), S{ .. }) { - _default::seq_contains::(haystack.S(), needle.S()) + let mut _out0: bool = _default::seq_contains::(haystack.S(), needle.S()); + ret = _out0; } else { - false + ret = false; + return ret; } } else { if matches!((&_source0).as_ref(), N{ .. }) { let mut ___mcc_h2: Sequence = _source0.N().clone(); let mut n: Sequence = ___mcc_h2.clone(); if matches!(needle.as_ref(), N{ .. }) { - _default::seq_contains::(haystack.N(), needle.N()) + let mut _out1: bool = _default::seq_contains::(haystack.N(), needle.N()); + ret = _out1; } else { - false + ret = false; + return ret; } } else { if matches!((&_source0).as_ref(), B{ .. }) { let mut ___mcc_h4: Sequence = _source0.B().clone(); let mut n: Sequence = ___mcc_h4.clone(); if matches!(needle.as_ref(), B{ .. }) { - _default::seq_contains::(haystack.B(), needle.B()) + let mut _out2: bool = _default::seq_contains::(haystack.B(), needle.B()); + ret = _out2; } else { - false + ret = false; + return ret; } } else { if matches!((&_source0).as_ref(), SS{ .. }) { let mut ___mcc_h6: Sequence> = _source0.SS().clone(); let mut s: Sequence> = ___mcc_h6.clone(); if matches!(needle.as_ref(), S{ .. }) { - haystack.SS().contains(needle.S()) + ret = haystack.SS().contains(needle.S()); + return ret; } else { - false + ret = false; + return ret; } } else { if matches!((&_source0).as_ref(), NS{ .. }) { let mut ___mcc_h8: Sequence> = _source0.NS().clone(); let mut s: Sequence> = ___mcc_h8.clone(); if matches!(needle.as_ref(), N{ .. }) { - haystack.NS().contains(needle.N()) + ret = haystack.NS().contains(needle.N()); + return ret; } else { - false + ret = false; + return ret; } } else { if matches!((&_source0).as_ref(), BS{ .. }) { let mut ___mcc_h10: Sequence> = _source0.BS().clone(); let mut s: Sequence> = ___mcc_h10.clone(); if matches!(needle.as_ref(), B{ .. }) { - haystack.BS().contains(needle.B()) + ret = haystack.BS().contains(needle.B()); + return ret; } else { - false + ret = false; + return ret; } } else { if matches!((&_source0).as_ref(), M{ .. }) { let mut ___mcc_h12: Map, Arc> = _source0.M().clone(); - false + ret = false; + return ret; } else { if matches!((&_source0).as_ref(), L{ .. }) { let mut ___mcc_h14: Sequence> = _source0.L().clone(); let mut list: Sequence> = ___mcc_h14.clone(); - list.contains(needle) + ret = list.contains(needle); + return ret; } else { if matches!((&_source0).as_ref(), NULL{ .. }) { let mut ___mcc_h16: bool = _source0.NULL().clone(); - false + ret = false; + return ret; } else { let mut ___mcc_h18: bool = _source0.BOOL().clone(); - false + ret = false; + return ret; } } } @@ -94167,9 +94276,10 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - } + }; + return ret; } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1113,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1165,3) pub fn begins_with(haystack: &Arc, needle: &Arc) -> bool { let mut _source0: Arc = haystack.clone(); if matches!((&_source0).as_ref(), S{ .. }) { @@ -94248,7 +94358,7 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1145,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1197,3) pub fn is_between(middle: &Arc, left: &Arc, right: &Arc) -> Arc>> { let mut valueOrError0: Arc>> = _default::AttributeLE(left, middle); if valueOrError0.IsFailure() { @@ -94266,29 +94376,33 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1153,3) - pub fn is_in(target: &Arc, list: &Sequence>) -> bool { + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1205,3) + pub fn is_in(target: &Arc, list: &Sequence>, pos: u64) -> bool { let mut _r0 = target.clone(); let mut _r1 = list.clone(); + let mut _r2 = pos; 'TAIL_CALL_START: loop { let target = _r0; let list = _r1; - if list.cardinality() == int!(0) { + let pos = _r2; + if truncate!(list.cardinality(), u64) == pos { return false; } else { - if _default::GetStr(&list.get(&int!(0))) == target.clone() { + if _default::GetStr(&list.get(&int!((&pos).clone()))) == target.clone() { return true; } else { let mut _in0: Arc = target.clone(); - let mut _in1: Sequence> = list.drop(&int!(1)); + let mut _in1: Sequence> = list.clone(); + let mut _in2: u64 = pos + 1; _r0 = _in0.clone(); _r1 = _in1.clone(); + _r2 = _in2; continue 'TAIL_CALL_START; } } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1164,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1219,3) pub fn AttrToStr(attr: &Arc) -> Sequence { let mut _source0: Arc = attr.clone(); if matches!((&_source0).as_ref(), S{ .. }) { @@ -94341,254 +94455,293 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1174,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1229,3) pub fn IsAttrType(attr: &Arc, typeStr: &Arc) -> bool { crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::AttrTypeToStr(&_default::GetStr(attr)) == _default::AttrToStr(&_default::GetStr(typeStr)) } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1180,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1235,3) pub fn apply_function(input: &Arc, stack: &Sequence>, num_args: &nat) -> Arc, Arc>> { + let mut result = MaybePlacebo::, Arc>>>::new(); let mut _source0: Arc = input.clone(); if matches!((&_source0).as_ref(), Attr{ .. }) { let mut ___mcc_h0: Sequence = _source0.s().clone(); let mut ___mcc_h1: TermLoc = _source0.loc().clone(); - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { - value: Arc::new(StackValue::Bool { - b: true - }) - }) - } else { - if matches!((&_source0).as_ref(), Value{ .. }) { - let mut ___mcc_h4: Sequence = _source0.s().clone(); - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { - value: Arc::new(StackValue::Bool { - b: true - }) - }) - } else { - if matches!((&_source0).as_ref(), crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::Token::Eq{ .. }) { - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { + result = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { value: Arc::new(StackValue::Bool { b: true }) - }) - } else { - if matches!((&_source0).as_ref(), Ne{ .. }) { - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { + })); + return result.read(); + } else { + if matches!((&_source0).as_ref(), Value{ .. }) { + let mut ___mcc_h4: Sequence = _source0.s().clone(); + result = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { value: Arc::new(StackValue::Bool { b: true }) - }) - } else { - if matches!((&_source0).as_ref(), Lt{ .. }) { - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { + })); + return result.read(); + } else { + if matches!((&_source0).as_ref(), crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::Token::Eq{ .. }) { + result = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { value: Arc::new(StackValue::Bool { b: true }) - }) - } else { - if matches!((&_source0).as_ref(), Gt{ .. }) { - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { + })); + return result.read(); + } else { + if matches!((&_source0).as_ref(), Ne{ .. }) { + result = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { value: Arc::new(StackValue::Bool { b: true }) - }) - } else { - if matches!((&_source0).as_ref(), Le{ .. }) { - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { + })); + return result.read(); + } else { + if matches!((&_source0).as_ref(), Lt{ .. }) { + result = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { value: Arc::new(StackValue::Bool { b: true }) - }) - } else { - if matches!((&_source0).as_ref(), Ge{ .. }) { - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { + })); + return result.read(); + } else { + if matches!((&_source0).as_ref(), Gt{ .. }) { + result = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { value: Arc::new(StackValue::Bool { b: true }) - }) + })); + return result.read(); + } else { + if matches!((&_source0).as_ref(), Le{ .. }) { + result = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { + value: Arc::new(StackValue::Bool { + b: true + }) + })); + return result.read(); + } else { + if matches!((&_source0).as_ref(), Ge{ .. }) { + result = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { + value: Arc::new(StackValue::Bool { + b: true + }) + })); + return result.read(); } else { if matches!((&_source0).as_ref(), Between{ .. }) { if stack.cardinality() < int!(3) { - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Failure { - error: crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::E(&string_utf16_of("No Stack for Between")) - }) + result = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Failure { + error: crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::E(&string_utf16_of("No Stack for Between")) + })); + return result.read(); } else { if matches!((&stack.get(&(stack.cardinality() - int!(1)))).as_ref(), Str{ .. }) && matches!((&stack.get(&(stack.cardinality() - int!(2)))).as_ref(), Str{ .. }) && matches!((&stack.get(&(stack.cardinality() - int!(3)))).as_ref(), Str{ .. }) { let mut valueOrError0: Arc>> = _default::is_between(stack.get(&(stack.cardinality() - int!(3))).s(), stack.get(&(stack.cardinality() - int!(2))).s(), stack.get(&(stack.cardinality() - int!(1))).s()); if valueOrError0.IsFailure() { - valueOrError0.PropagateFailure::>() - } else { - let mut ret: bool = valueOrError0.Extract(); - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { - value: Arc::new(StackValue::Bool { - b: ret - }) - }) - } + result = MaybePlacebo::from(valueOrError0.PropagateFailure::>()); + return result.read(); + }; + let mut ret: bool = valueOrError0.Extract(); + result = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { + value: Arc::new(StackValue::Bool { + b: ret + }) + })); + return result.read(); } else { - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Failure { - error: crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::E(&string_utf16_of("Wrong Types for contains")) - }) + result = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Failure { + error: crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::E(&string_utf16_of("Wrong Types for Between")) + })); + return result.read(); } } } else { if matches!((&_source0).as_ref(), In{ .. }) { let mut num: nat = _default::StringsFollowing(stack); if stack.cardinality() < num.clone() { - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Failure { - error: crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::E(&string_utf16_of("Tautology False")) - }) + result = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Failure { + error: crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::E(&string_utf16_of("Tautology False")) + })); + return result.read(); } else { if num.clone() == int!(0) { - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Failure { - error: crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::E(&string_utf16_of("In has no args")) - }) + result = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Failure { + error: crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::E(&string_utf16_of("In has no args")) + })); + return result.read(); } else { - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { - value: Arc::new(StackValue::Bool { - b: _default::is_in(&_default::GetStr(&stack.get(&(stack.cardinality() - num.clone()))), &stack.drop(&(stack.cardinality() - num.clone() + int!(1)))) - }) - }) + result = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { + value: Arc::new(StackValue::Bool { + b: _default::is_in(&_default::GetStr(&stack.get(&(stack.cardinality() - num.clone()))), &stack.drop(&(stack.cardinality() - num.clone() + int!(1))), 0) + }) + })); + return result.read(); } } } else { if matches!((&_source0).as_ref(), Open{ .. }) { - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { - value: Arc::new(StackValue::Bool { - b: true - }) - }) - } else { - if matches!((&_source0).as_ref(), Close{ .. }) { - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { - value: Arc::new(StackValue::Bool { - b: true - }) - }) - } else { - if matches!((&_source0).as_ref(), Comma{ .. }) { - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { + result = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { value: Arc::new(StackValue::Bool { b: true }) - }) - } else { - if matches!((&_source0).as_ref(), Not{ .. }) { - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { + })); + return result.read(); + } else { + if matches!((&_source0).as_ref(), Close{ .. }) { + result = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { value: Arc::new(StackValue::Bool { b: true }) - }) - } else { - if matches!((&_source0).as_ref(), And{ .. }) { - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { + })); + return result.read(); + } else { + if matches!((&_source0).as_ref(), Comma{ .. }) { + result = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { value: Arc::new(StackValue::Bool { b: true }) - }) - } else { - if matches!((&_source0).as_ref(), Or{ .. }) { - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { + })); + return result.read(); + } else { + if matches!((&_source0).as_ref(), Not{ .. }) { + result = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { value: Arc::new(StackValue::Bool { b: true }) - }) + })); + return result.read(); + } else { + if matches!((&_source0).as_ref(), And{ .. }) { + result = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { + value: Arc::new(StackValue::Bool { + b: true + }) + })); + return result.read(); + } else { + if matches!((&_source0).as_ref(), Or{ .. }) { + result = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { + value: Arc::new(StackValue::Bool { + b: true + }) + })); + return result.read(); } else { if matches!((&_source0).as_ref(), AttributeExists{ .. }) { if stack.cardinality() < int!(1) { - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Failure { - error: crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::E(&string_utf16_of("No Stack for AttributeExists")) - }) + result = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Failure { + error: crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::E(&string_utf16_of("No Stack for AttributeExists")) + })); + return result.read(); } else { - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { - value: Arc::new(StackValue::Bool { - b: !matches!((&stack.get(&(stack.cardinality() - int!(1)))).as_ref(), DoesNotExist{ .. }) - }) - }) + result = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { + value: Arc::new(StackValue::Bool { + b: !matches!((&stack.get(&(stack.cardinality() - int!(1)))).as_ref(), DoesNotExist{ .. }) + }) + })); + return result.read(); } } else { if matches!((&_source0).as_ref(), AttributeNotExists{ .. }) { if stack.cardinality() < int!(1) { - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Failure { - error: crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::E(&string_utf16_of("No Stack for AttributeExists")) - }) + result = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Failure { + error: crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::E(&string_utf16_of("No Stack for AttributeExists")) + })); + return result.read(); } else { - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { - value: Arc::new(StackValue::Bool { - b: matches!((&stack.get(&(stack.cardinality() - int!(1)))).as_ref(), DoesNotExist{ .. }) - }) - }) + result = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { + value: Arc::new(StackValue::Bool { + b: matches!((&stack.get(&(stack.cardinality() - int!(1)))).as_ref(), DoesNotExist{ .. }) + }) + })); + return result.read(); } } else { if matches!((&_source0).as_ref(), AttributeType{ .. }) { if stack.cardinality() < int!(2) { - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Failure { - error: crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::E(&string_utf16_of("No Stack for AttributeType")) - }) + result = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Failure { + error: crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::E(&string_utf16_of("No Stack for AttributeType")) + })); + return result.read(); } else { - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { - value: Arc::new(StackValue::Bool { - b: _default::IsAttrType(&stack.get(&(stack.cardinality() - int!(2))), &stack.get(&(stack.cardinality() - int!(1)))) - }) - }) + result = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { + value: Arc::new(StackValue::Bool { + b: _default::IsAttrType(&stack.get(&(stack.cardinality() - int!(2))), &stack.get(&(stack.cardinality() - int!(1)))) + }) + })); + return result.read(); } } else { if matches!((&_source0).as_ref(), BeginsWith{ .. }) { if stack.cardinality() < int!(2) { - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Failure { - error: crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::E(&string_utf16_of("No Stack for BeginsWith")) - }) + result = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Failure { + error: crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::E(&string_utf16_of("No Stack for BeginsWith")) + })); + return result.read(); } else { if matches!((&stack.get(&(stack.cardinality() - int!(1)))).as_ref(), Str{ .. }) && matches!((&stack.get(&(stack.cardinality() - int!(2)))).as_ref(), Str{ .. }) { - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { - value: Arc::new(StackValue::Bool { - b: _default::begins_with(stack.get(&(stack.cardinality() - int!(2))).s(), stack.get(&(stack.cardinality() - int!(1))).s()) - }) - }) + result = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { + value: Arc::new(StackValue::Bool { + b: _default::begins_with(stack.get(&(stack.cardinality() - int!(2))).s(), stack.get(&(stack.cardinality() - int!(1))).s()) + }) + })); + return result.read(); } else { - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Failure { - error: crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::E(&string_utf16_of("Wrong Types for BeginsWith")) - }) + result = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Failure { + error: crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::E(&string_utf16_of("Wrong Types for BeginsWith")) + })); + return result.read(); } } } else { if matches!((&_source0).as_ref(), Contains{ .. }) { if stack.cardinality() < int!(2) { - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Failure { - error: crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::E(&string_utf16_of("No Stack for contains")) - }) + result = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Failure { + error: crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::E(&string_utf16_of("No Stack for contains")) + })); + return result.read(); } else { if matches!((&stack.get(&(stack.cardinality() - int!(1)))).as_ref(), Str{ .. }) && matches!((&stack.get(&(stack.cardinality() - int!(2)))).as_ref(), Str{ .. }) { - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { - value: Arc::new(StackValue::Bool { - b: _default::does_contain(stack.get(&(stack.cardinality() - int!(2))).s(), stack.get(&(stack.cardinality() - int!(1))).s()) - }) - }) + let mut xxx: bool; + let mut _out0: bool = _default::does_contain(stack.get(&(stack.cardinality() - int!(2))).s(), stack.get(&(stack.cardinality() - int!(1))).s()); + xxx = _out0; + result = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { + value: Arc::new(StackValue::Bool { + b: xxx + }) + })); + return result.read(); } else { - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Failure { - error: crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::E(&string_utf16_of("Wrong Types for contains")) - }) + result = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Failure { + error: crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::E(&string_utf16_of("Wrong Types for contains")) + })); + return result.read(); } } } else { if stack.cardinality() < int!(1) { - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Failure { - error: crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::E(&string_utf16_of("No Stack for Size")) - }) + result = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Failure { + error: crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::E(&string_utf16_of("No Stack for Size")) + })); + return result.read(); } else { if !matches!((&stack.get(&(stack.cardinality() - int!(1)))).as_ref(), Str{ .. }) { - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Failure { - error: crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::E(&string_utf16_of("Wrong Types for Size")) - }) + result = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Failure { + error: crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::E(&string_utf16_of("Wrong Types for Size")) + })); + return result.read(); } else { let mut n: nat = _default::GetSize(stack.get(&(stack.cardinality() - int!(1))).s()); - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { - value: Arc::new(StackValue::Str { - s: Arc::new(AttributeValue::N { - N: crate::implementation_from_dafny::_StandardLibrary_Compile::_String_Compile::_default::Base10Int2String(&n) - }) - }) - }) + result = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { + value: Arc::new(StackValue::Str { + s: Arc::new(AttributeValue::N { + N: crate::implementation_from_dafny::_StandardLibrary_Compile::_String_Compile::_default::Base10Int2String(&n) + }) + }) + })); + return result.read(); } } } @@ -94611,9 +94764,10 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - } + }; + return result.read(); } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1248,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1309,3) pub fn apply_unary(input: &Arc, stack: &Arc) -> Arc, Arc>> { if matches!(stack.as_ref(), Bool{ .. }) { Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { @@ -94627,7 +94781,7 @@ pub mod _DynamoDBFilterExpr_Compile { }) } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1257,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1318,3) pub fn apply_binary_bool(input: &Arc, x: bool, y: bool) -> Arc>> { let mut _source0: Arc = input.clone(); if matches!((&_source0).as_ref(), Attr{ .. }) { @@ -94763,11 +94917,11 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1265,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1326,3) pub fn IsHighSurrogate(ch: &DafnyCharUTF16) -> bool { DafnyCharUTF16(::from(int!(b"55296")).unwrap()) <= ch.clone() && ch.clone() <= DafnyCharUTF16(::from(int!(b"56319")).unwrap()) } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1274,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1335,3) pub fn UnicodeLess(a: &Sequence, b: &Sequence, pos: &nat) -> bool { let mut _r0 = a.clone(); let mut _r1 = b.clone(); @@ -94807,11 +94961,11 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1299,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1360,3) pub fn UnicodeLessOrEqual(a: &Sequence, b: &Sequence) -> bool { !_default::UnicodeLess(b, a, &int!(0)) } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1304,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1365,3) pub fn CompareFloat(x: &Sequence, y: &Sequence) -> Arc>> { let mut valueOrError0: Arc, Arc>> = crate::implementation_from_dafny::_DynamoDbNormalizeNumber_Compile::_default::NormalizeNumber(x).MapFailure::>(&({ Arc::new(move |e: &Sequence| -> Arc{ @@ -94837,7 +94991,7 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1311,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1372,3) pub fn AttributeEQ(a: &Arc, b: &Arc) -> Arc>> { if matches!(a.as_ref(), N{ .. }) && matches!(b.as_ref(), N{ .. }) { let mut valueOrError0: Arc>> = _default::CompareFloat(a.N(), b.N()); @@ -94855,7 +95009,7 @@ pub mod _DynamoDBFilterExpr_Compile { }) } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1320,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1381,3) pub fn AttributeNE(a: &Arc, b: &Arc) -> Arc>> { let mut valueOrError0: Arc>> = _default::AttributeEQ(a, b); if valueOrError0.IsFailure() { @@ -94867,7 +95021,7 @@ pub mod _DynamoDBFilterExpr_Compile { }) } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1326,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1387,3) pub fn AttributeLE(a: &Arc, b: &Arc) -> Arc>> { if matches!(a.as_ref(), N{ .. }) && matches!(b.as_ref(), N{ .. }) { let mut valueOrError0: Arc>> = _default::CompareFloat(a.N(), b.N()); @@ -94897,7 +95051,7 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1338,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1399,3) pub fn AttributeLT(a: &Arc, b: &Arc) -> Arc>> { let mut valueOrError0: Arc>> = _default::AttributeLE(b, a); if valueOrError0.IsFailure() { @@ -94909,7 +95063,7 @@ pub mod _DynamoDBFilterExpr_Compile { }) } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1343,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1404,3) pub fn AttributeGT(a: &Arc, b: &Arc) -> Arc>> { let mut valueOrError0: Arc>> = _default::AttributeLE(a, b); if valueOrError0.IsFailure() { @@ -94921,7 +95075,7 @@ pub mod _DynamoDBFilterExpr_Compile { }) } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1348,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1409,3) pub fn AttributeGE(a: &Arc, b: &Arc) -> Arc>> { let mut valueOrError0: Arc>> = _default::AttributeLE(b, a); if valueOrError0.IsFailure() { @@ -94933,7 +95087,7 @@ pub mod _DynamoDBFilterExpr_Compile { }) } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1355,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1416,3) pub fn apply_binary_comp(input: &Arc, x: &Arc, y: &Arc) -> Arc>> { let mut _source0: Arc = input.clone(); if matches!((&_source0).as_ref(), Attr{ .. }) { @@ -95057,7 +95211,7 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1368,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1429,3) pub fn apply_binary(input: &Arc, x: &Arc, y: &Arc) -> Arc, Arc>> { if _default::IsComp(input) { if matches!(x.as_ref(), Str{ .. }) && matches!(y.as_ref(), Str{ .. }) { @@ -95097,7 +95251,7 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1385,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1446,3) pub fn NumArgs(t: &Arc, stack: &Sequence>) -> nat { let mut _source0: Arc = t.clone(); if matches!((&_source0).as_ref(), Attr{ .. }) { @@ -95189,145 +95343,94 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1400,3) - pub fn InnerEvalExpr(input: &Sequence>, stack: &Sequence>, item: &Map, Arc>, names: &Arc, Sequence>>>, values: &Map, Arc>) -> Arc>> { - let mut _r0 = input.clone(); - let mut _r1 = stack.clone(); - let mut _r2 = item.clone(); - let mut _r3 = names.clone(); - let mut _r4 = values.clone(); - 'TAIL_CALL_START: loop { - let input = _r0; - let stack = _r1; - let item = _r2; - let names = _r3; - let values = _r4; - if int!(0) == input.cardinality() { - if int!(1) == stack.cardinality() && matches!((&stack.get(&int!(0))).as_ref(), Bool{ .. }) { - return Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::>::Success { + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1461,3) + pub fn InnerEvalExpr(input: &Sequence>, stack: &Sequence>, item: &Map, Arc>, names: &Arc, Sequence>>>, values: &Map, Arc>, pos: u64) -> Arc>> { + let mut ret = MaybePlacebo::>>>::new(); + if pos == truncate!(input.cardinality(), u64) { + if int!(1) == stack.cardinality() && matches!((&stack.get(&int!(0))).as_ref(), Bool{ .. }) { + ret = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::>::Success { value: stack.get(&int!(0)).b().clone() - }); - } else { - return Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::>::Failure { + })); + return ret.read(); + } else { + ret = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::>::Failure { error: crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::E(&string_utf16_of("ended with bad stack")) - }); - } + })); + return ret.read(); + } + } else { + let mut t: Arc = input.get(&int!((&pos).clone())); + if matches!((&t).as_ref(), Value{ .. }) { + let mut _out0: Arc>> = _default::InnerEvalExpr(input, &stack.concat(&seq![_default::StackValueFromValue(t.s(), values)]), item, names, values, pos + 1); + ret = MaybePlacebo::from(_out0.clone()); } else { - let mut t: Arc = input.get(&int!(0)); - if matches!((&t).as_ref(), Value{ .. }) { - let mut _in0: Sequence> = input.drop(&int!(1)); - let mut _in1: Sequence> = stack.concat(&seq![_default::StackValueFromValue(t.s(), &values)]); - let mut _in2: Map, Arc> = item.clone(); - let mut _in3: Arc, Sequence>>> = names.clone(); - let mut _in4: Map, Arc> = values.clone(); - _r0 = _in0.clone(); - _r1 = _in1.clone(); - _r2 = _in2.clone(); - _r3 = _in3.clone(); - _r4 = _in4.clone(); - continue 'TAIL_CALL_START; + if matches!((&t).as_ref(), Attr{ .. }) { + let mut _out1: Arc>> = _default::InnerEvalExpr(input, &stack.concat(&seq![_default::StackValueFromAttr(&t, item, names)]), item, names, values, pos + 1); + ret = MaybePlacebo::from(_out1.clone()); } else { - if matches!((&t).as_ref(), Attr{ .. }) { - let mut _in5: Sequence> = input.drop(&int!(1)); - let mut _in6: Sequence> = stack.concat(&seq![_default::StackValueFromAttr(&t, &item, &names)]); - let mut _in7: Map, Arc> = item.clone(); - let mut _in8: Arc, Sequence>>> = names.clone(); - let mut _in9: Map, Arc> = values.clone(); - _r0 = _in5.clone(); - _r1 = _in6.clone(); - _r2 = _in7.clone(); - _r3 = _in8.clone(); - _r4 = _in9.clone(); - continue 'TAIL_CALL_START; - } else { - if _default::IsUnary(&t) { - if int!(0) == stack.cardinality() { - return Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::>::Failure { + if _default::IsUnary(&t) { + if int!(0) == stack.cardinality() { + ret = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::>::Failure { error: crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::E(&string_utf16_of("Empty stack for unary op")) - }); + })); + } else { + let mut valueOrError0: Arc, Arc>> = _default::apply_unary(&t, &stack.get(&(stack.cardinality() - int!(1)))); + if valueOrError0.IsFailure() { + ret = MaybePlacebo::from(valueOrError0.PropagateFailure::()); + return ret.read(); + }; + let mut val: Arc = valueOrError0.Extract(); + let mut _out2: Arc>> = _default::InnerEvalExpr(input, &stack.take(&(stack.cardinality() - int!(1))).concat(&seq![val.clone()]), item, names, values, pos + 1); + ret = MaybePlacebo::from(_out2.clone()); + } + } else { + if _default::IsBinary(&t) { + if stack.cardinality() < int!(2) { + ret = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::>::Failure { + error: crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::E(&string_utf16_of("Empty stack for binary op")) + })); } else { - let mut valueOrError0: Arc, Arc>> = _default::apply_unary(&t, &stack.get(&(stack.cardinality() - int!(1)))); - if valueOrError0.IsFailure() { - return valueOrError0.PropagateFailure::(); - } else { - let mut val: Arc = valueOrError0.Extract(); - let mut _in10: Sequence> = input.drop(&int!(1)); - let mut _in11: Sequence> = stack.take(&(stack.cardinality() - int!(1))).concat(&seq![val.clone()]); - let mut _in12: Map, Arc> = item.clone(); - let mut _in13: Arc, Sequence>>> = names.clone(); - let mut _in14: Map, Arc> = values.clone(); - _r0 = _in10.clone(); - _r1 = _in11.clone(); - _r2 = _in12.clone(); - _r3 = _in13.clone(); - _r4 = _in14.clone(); - continue 'TAIL_CALL_START; - } + let mut valueOrError1: Arc, Arc>> = _default::apply_binary(&t, &stack.get(&(stack.cardinality() - int!(2))), &stack.get(&(stack.cardinality() - int!(1)))); + if valueOrError1.IsFailure() { + ret = MaybePlacebo::from(valueOrError1.PropagateFailure::()); + return ret.read(); + }; + let mut val: Arc = valueOrError1.Extract(); + let mut _out3: Arc>> = _default::InnerEvalExpr(input, &stack.take(&(stack.cardinality() - int!(2))).concat(&seq![val.clone()]), item, names, values, pos + 1); + ret = MaybePlacebo::from(_out3.clone()); } } else { - if _default::IsBinary(&t) { - if stack.cardinality() < int!(2) { - return Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::>::Failure { - error: crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::E(&string_utf16_of("Empty stack for binary op")) - }); + if _default::IsFunction(&t) { + let mut num_args: nat = _default::NumArgs(&t, stack); + if stack.cardinality() < num_args.clone() { + ret = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::>::Failure { + error: crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::E(&string_utf16_of("Empty stack for function call")) + })); } else { - let mut valueOrError1: Arc, Arc>> = _default::apply_binary(&t, &stack.get(&(stack.cardinality() - int!(2))), &stack.get(&(stack.cardinality() - int!(1)))); - if valueOrError1.IsFailure() { - return valueOrError1.PropagateFailure::(); - } else { - let mut val: Arc = valueOrError1.Extract(); - let mut _in15: Sequence> = input.drop(&int!(1)); - let mut _in16: Sequence> = stack.take(&(stack.cardinality() - int!(2))).concat(&seq![val.clone()]); - let mut _in17: Map, Arc> = item.clone(); - let mut _in18: Arc, Sequence>>> = names.clone(); - let mut _in19: Map, Arc> = values.clone(); - _r0 = _in15.clone(); - _r1 = _in16.clone(); - _r2 = _in17.clone(); - _r3 = _in18.clone(); - _r4 = _in19.clone(); - continue 'TAIL_CALL_START; - } + let mut valueOrError2: Arc, Arc>>; + let mut _out4: Arc, Arc>> = _default::apply_function(&t, stack, &num_args); + valueOrError2 = _out4.clone(); + if valueOrError2.IsFailure() { + ret = MaybePlacebo::from(valueOrError2.PropagateFailure::()); + return ret.read(); + }; + let mut val: Arc = valueOrError2.Extract(); + let mut _out5: Arc>> = _default::InnerEvalExpr(input, &stack.take(&(stack.cardinality() - num_args.clone())).concat(&seq![val.clone()]), item, names, values, pos + 1); + ret = MaybePlacebo::from(_out5.clone()); } } else { - if _default::IsFunction(&t) { - let mut num_args: nat = _default::NumArgs(&t, &stack); - if stack.cardinality() < num_args.clone() { - return Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::>::Failure { - error: crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::E(&string_utf16_of("Empty stack for function call")) - }); - } else { - let mut valueOrError2: Arc, Arc>> = _default::apply_function(&t, &stack, &num_args); - if valueOrError2.IsFailure() { - return valueOrError2.PropagateFailure::(); - } else { - let mut val: Arc = valueOrError2.Extract(); - let mut _in20: Sequence> = input.drop(&int!(1)); - let mut _in21: Sequence> = stack.take(&(stack.cardinality() - num_args.clone())).concat(&seq![val.clone()]); - let mut _in22: Map, Arc> = item.clone(); - let mut _in23: Arc, Sequence>>> = names.clone(); - let mut _in24: Map, Arc> = values.clone(); - _r0 = _in20.clone(); - _r1 = _in21.clone(); - _r2 = _in22.clone(); - _r3 = _in23.clone(); - _r4 = _in24.clone(); - continue 'TAIL_CALL_START; - } - } - } else { - return Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::>::Success { + ret = MaybePlacebo::from(Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::>::Success { value: true - }); - } + })); } } } } } - } + }; + return ret.read(); } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1444,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1515,3) pub fn FilterItems(b: &Arc, parsed: &Sequence>, ItemList: &Sequence, Arc>>, names: &Arc, Sequence>>>, values: &Map, Arc>) -> Arc, Arc>>, Arc>> { let mut output = MaybePlacebo::, Arc>>, Arc>>>::new(); let mut acc: Sequence, Arc>> = seq![] as Sequence, Arc>>; @@ -95341,7 +95444,9 @@ pub mod _DynamoDBFilterExpr_Compile { return output.read(); }; let mut newAttrs: Map, Arc> = valueOrError0.Extract(); - let mut valueOrError1: Arc>> = _default::EvalExpr(parsed, &ItemList.get(&i).merge(&newAttrs), names, values); + let mut valueOrError1: Arc>>; + let mut _out1: Arc>> = _default::EvalExpr(parsed, &ItemList.get(&i).merge(&newAttrs), names, values); + valueOrError1 = _out1.clone(); if valueOrError1.IsFailure() { output = MaybePlacebo::from(valueOrError1.PropagateFailure::, Arc>>>()); return output.read(); @@ -95356,7 +95461,7 @@ pub mod _DynamoDBFilterExpr_Compile { })); return output.read(); } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1468,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1539,3) pub fn FilterResults(b: &Arc, ItemList: &Sequence, Arc>>, KeyExpression: &Arc>>, FilterExpression: &Arc>>, names: &Arc, Sequence>>>, values: &Arc, Arc>>>) -> Arc, Arc>>, Arc>> { let mut output = MaybePlacebo::, Arc>>, Arc>>>::new(); if ItemList.cardinality() == int!(0) || matches!(KeyExpression.as_ref(), None{ .. }) && matches!(FilterExpression.as_ref(), None{ .. }) { @@ -95367,14 +95472,14 @@ pub mod _DynamoDBFilterExpr_Compile { } else { let mut afterKeys: Sequence, Arc>>; if matches!(KeyExpression.as_ref(), Some{ .. }) { - let mut parsed: Sequence> = _default::ParseExpr(KeyExpression.value()); + let mut parsed: Sequence> = _default::ParseExpr(KeyExpression.value(), 0); let mut valueOrError0: Arc, Arc>> = _default::BeaconizeParsedExpr(b, &parsed, &int!(0), &values.UnwrapOr(&map![]), names, &Arc::new(MaybeKeyMap::DontUseKeys {}), &map![], &(seq![] as Sequence>)); if valueOrError0.IsFailure() { output = MaybePlacebo::from(valueOrError0.PropagateFailure::, Arc>>>()); return output.read(); }; let mut expr: Arc = valueOrError0.Extract(); - let mut expr1: Sequence> = _default::ConvertToPrefix(expr.expr()); + let mut expr1: Sequence> = _default::ConvertToPrefix(expr.expr(), 0); let mut expr2: Sequence> = _default::ConvertToRpn(&expr1); let mut valueOrError1: Arc, Arc>>, Arc>>; let mut _out0: Arc, Arc>>, Arc>> = _default::FilterItems(b, &expr2, ItemList, expr.names(), expr.values()); @@ -95388,14 +95493,14 @@ pub mod _DynamoDBFilterExpr_Compile { afterKeys = ItemList.clone(); }; if matches!(FilterExpression.as_ref(), Some{ .. }) { - let mut parsed: Sequence> = _default::ParseExpr(FilterExpression.value()); + let mut parsed: Sequence> = _default::ParseExpr(FilterExpression.value(), 0); let mut valueOrError2: Arc, Arc>> = _default::BeaconizeParsedExpr(b, &parsed, &int!(0), &values.UnwrapOr(&map![]), names, &Arc::new(MaybeKeyMap::DontUseKeys {}), &map![], &(seq![] as Sequence>)); if valueOrError2.IsFailure() { output = MaybePlacebo::from(valueOrError2.PropagateFailure::, Arc>>>()); return output.read(); }; let mut expr: Arc = valueOrError2.Extract(); - let mut expr1: Sequence> = _default::ConvertToPrefix(expr.expr()); + let mut expr1: Sequence> = _default::ConvertToPrefix(expr.expr(), 0); let mut expr2: Sequence> = _default::ConvertToRpn(&expr1); let mut _out1: Arc, Arc>>, Arc>> = _default::FilterItems(b, &expr2, &afterKeys, expr.names(), expr.values()); output = MaybePlacebo::from(_out1.clone()); @@ -95408,7 +95513,7 @@ pub mod _DynamoDBFilterExpr_Compile { }; return output.read(); } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1506,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1577,3) pub fn KeyIdFromPart(bv: &Arc, keyIdField: &Sequence, attr: &Sequence, value: &Sequence) -> Arc>> { if !bv.beacons().contains(attr) || matches!((&bv.beacons().get(attr)).as_ref(), Standard{ .. }) { Arc::new(Option::>::None {}) @@ -95447,7 +95552,7 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1528,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1599,3) pub fn KeyIdFromAttr(bv: &Arc, attr: &Arc>>, value: &Sequence, names: &Arc, Sequence>>>) -> Arc>> { if matches!(attr.as_ref(), None{ .. }) { Arc::new(Option::>::None {}) @@ -95467,7 +95572,7 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1545,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1616,3) pub fn GetBeaconKeyIds2(pos: &nat, bv: &Arc, expr: &Sequence>, values: &Map, Arc>, names: &Arc, Sequence>>>, soFar: &Sequence>) -> Arc>, Arc>> { let mut _r0 = pos.clone(); let mut _r1 = bv.clone(); @@ -95559,14 +95664,14 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1577,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1648,3) pub fn GetBeaconKeyIds(bv: &Arc, expr: &Arc>>, values: &Map, Arc>, names: &Arc, Sequence>>>, soFar: &Sequence>) -> Arc>, Arc>> { if matches!(expr.as_ref(), None{ .. }) { Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::>, Arc>::Success { value: soFar.clone() }) } else { - let mut parsed: Sequence> = _default::ParseExpr(expr.value()); + let mut parsed: Sequence> = _default::ParseExpr(expr.value(), 0); _default::GetBeaconKeyIds2(&int!(0), bv, &parsed, values, names, soFar) } } @@ -95574,7 +95679,7 @@ pub mod _DynamoDBFilterExpr_Compile { /// = type=implication /// # If the [Beacon Key Source](#beacon-key-source) is a [Single Key Store](#single-key-store-initialization) /// # then `beacon key id` MUST be the configured [beacon key id](#beacon-key-id) - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1598,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1669,3) pub fn GetBeaconKeyId(bv: &Arc, keyExpr: &Arc>>, filterExpr: &Arc>>, values: &Arc, Arc>>>, names: &Arc, Sequence>>>) -> Arc, Arc>> { if !matches!(bv.keySource().keyLoc().as_ref(), MultiLoc{ .. }) { Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>::Success { @@ -95618,7 +95723,7 @@ pub mod _DynamoDBFilterExpr_Compile { } } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1666,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1737,3) pub fn Beaconize(b: &Arc, context: &Arc, keyId: &Arc, naked: bool) -> Arc, Arc>> { let mut output = MaybePlacebo::, Arc>>>::new(); if matches!(context.keyExpr().as_ref(), None{ .. }) && matches!(context.filterExpr().as_ref(), None{ .. }) { @@ -95649,7 +95754,7 @@ pub mod _DynamoDBFilterExpr_Compile { let mut newFilterExpr: Arc>> = context.filterExpr().clone(); let mut newNames: Arc, Sequence>>> = context.names().clone(); if matches!(context.keyExpr().as_ref(), Some{ .. }) { - let mut parsed: Sequence> = _default::ParseExpr(context.keyExpr().value()); + let mut parsed: Sequence> = _default::ParseExpr(context.keyExpr().value(), 0); let mut valueOrError1: Arc, Arc>> = _default::BeaconizeParsedExpr(b, &parsed, &int!(0), &values, &newNames, &keys, &newValues, &(seq![] as Sequence>)); if valueOrError1.IsFailure() { output = MaybePlacebo::from(valueOrError1.PropagateFailure::>()); @@ -95663,7 +95768,7 @@ pub mod _DynamoDBFilterExpr_Compile { newNames = newContext.names().clone(); }; if matches!(context.filterExpr().as_ref(), Some{ .. }) { - let mut parsed: Sequence> = _default::ParseExpr(context.filterExpr().value()); + let mut parsed: Sequence> = _default::ParseExpr(context.filterExpr().value(), 0); let mut valueOrError2: Arc, Arc>> = _default::BeaconizeParsedExpr(b, &parsed, &int!(0), &values, &newNames, &keys, &newValues, &(seq![] as Sequence>)); if valueOrError2.IsFailure() { output = MaybePlacebo::from(valueOrError2.PropagateFailure::>()); @@ -95694,7 +95799,7 @@ pub mod _DynamoDBFilterExpr_Compile { }; return output.read(); } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1712,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1783,3) pub fn GetAttrName(t: &Arc, names: &Arc, Sequence>>>) -> Sequence { if matches!(names.as_ref(), Some{ .. }) && names.value().contains(t.s()) { names.value().get(t.s()) @@ -95702,7 +95807,7 @@ pub mod _DynamoDBFilterExpr_Compile { t.s().clone() } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1722,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1793,3) pub fn TestParsedExpr(expr: &Sequence>, encrypted: &Set>, names: &Arc, Sequence>>>) -> Arc>> { let mut output = MaybePlacebo::>>>::new(); let mut _hi0: DafnyInt = expr.cardinality(); @@ -95720,7 +95825,7 @@ pub mod _DynamoDBFilterExpr_Compile { output = MaybePlacebo::from(Arc::new(Outcome::>::Pass {})); return output.read(); } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1741,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1812,3) pub fn TestBeaconize(actions: &Map, Arc>, keyExpr: &Arc>>, filterExpr: &Arc>>, names: &Arc, Sequence>>>) -> Arc>> { let mut output = MaybePlacebo::>>>::new(); let mut encrypted: Set> = (&({ @@ -95738,7 +95843,7 @@ pub mod _DynamoDBFilterExpr_Compile { }))(); if matches!(keyExpr.as_ref(), Some{ .. }) { let mut valueOrError0: Arc>>; - let mut _out0: Arc>> = _default::TestParsedExpr(&_default::ParseExpr(keyExpr.value()), &encrypted, names); + let mut _out0: Arc>> = _default::TestParsedExpr(&_default::ParseExpr(keyExpr.value(), 0), &encrypted, names); valueOrError0 = _out0.clone(); if valueOrError0.IsFailure() { output = MaybePlacebo::from(valueOrError0.PropagateFailure::()); @@ -95747,7 +95852,7 @@ pub mod _DynamoDBFilterExpr_Compile { }; if matches!(filterExpr.as_ref(), Some{ .. }) { let mut valueOrError1: Arc>>; - let mut _out1: Arc>> = _default::TestParsedExpr(&_default::ParseExpr(filterExpr.value()), &encrypted, names); + let mut _out1: Arc>> = _default::TestParsedExpr(&_default::ParseExpr(filterExpr.value(), 0), &encrypted, names); valueOrError1 = _out1.clone(); if valueOrError1.IsFailure() { output = MaybePlacebo::from(valueOrError1.PropagateFailure::()); @@ -95761,7 +95866,7 @@ pub mod _DynamoDBFilterExpr_Compile { } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(80,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(86,3) #[derive(PartialEq, Clone)] pub enum Token { Attr { @@ -96054,7 +96159,7 @@ pub mod _DynamoDBFilterExpr_Compile { } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(203,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(209,3) #[derive(PartialEq, Clone)] pub enum EqualityBeacon { EqualityBeacon { @@ -96144,7 +96249,7 @@ pub mod _DynamoDBFilterExpr_Compile { } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(950,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1004,3) #[derive(PartialEq, Clone)] pub enum StackValue { Bool { @@ -96242,7 +96347,7 @@ pub mod _DynamoDBFilterExpr_Compile { } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1651,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1722,3) #[derive(PartialEq, Clone)] pub enum ExprContext { ExprContext { @@ -96343,7 +96448,7 @@ pub mod _DynamoDBFilterExpr_Compile { } } - /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1658,3) + /// dafny/DynamoDbEncryption/src/FilterExpr.dfy(1729,3) #[derive(PartialEq, Clone)] pub enum ParsedContext { ParsedContext { @@ -101538,13 +101643,22 @@ pub mod _DynamoToStruct_Compile { pub use crate::implementation_from_dafny::software::amazon::cryptography::dbencryptionsdk::structuredencryption::internaldafny::types::CryptoAction; pub use crate::implementation_from_dafny::software::amazon::cryptography::dbencryptionsdk::structuredencryption::internaldafny::types::StructuredDataTerminal; pub use crate::implementation_from_dafny::software::amazon::cryptography::dbencryptionsdk::dynamodb::internaldafny::types::Error; + pub use ::dafny_runtime::MaybePlacebo; + pub use ::dafny_runtime::Object; + pub use crate::implementation_from_dafny::DafnyLibraries::MutableMap; + pub use ::dafny_runtime::truncate; + pub use ::dafny_runtime::integer_range; + pub use ::std::convert::Into; + pub use ::dafny_runtime::int; + pub use crate::implementation_from_dafny::_Wrappers_Compile::Result::Failure; + pub use crate::implementation_from_dafny::DafnyLibraries::MutableMapTrait; + pub use ::dafny_runtime::rd; pub use ::dafny_runtime::MapBuilder; pub use ::dafny_runtime::Set; pub use ::dafny_runtime::SetBuilder; pub use ::std::marker::Sync; pub use ::std::marker::Send; pub use ::dafny_runtime::string_utf16_of; - pub use ::dafny_runtime::truncate; pub use ::dafny_runtime::DafnyType; pub use crate::implementation_from_dafny::_Wrappers_Compile::Result::Success; pub use crate::implementation_from_dafny::_Wrappers_Compile::Outcome; @@ -101560,12 +101674,7 @@ pub mod _DynamoToStruct_Compile { pub use crate::implementation_from_dafny::software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::L; pub use crate::implementation_from_dafny::software::amazon::cryptography::services::dynamodb::internaldafny::types::AttributeValue::NULL; pub use ::dafny_runtime::seq; - pub use ::dafny_runtime::int; pub use crate::implementation_from_dafny::UTF8::ValidUTF8Bytes; - pub use ::dafny_runtime::MaybePlacebo; - pub use ::dafny_runtime::integer_range; - pub use ::std::convert::Into; - pub use crate::implementation_from_dafny::_Wrappers_Compile::Result::Failure; pub use ::dafny_runtime::DafnyTypeEq; pub use crate::implementation_from_dafny::_Wrappers_Compile::Option::None; pub use ::dafny_runtime::map; @@ -101583,125 +101692,124 @@ pub mod _DynamoToStruct_Compile { impl _default { /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(35,3) pub fn ItemToStructured2(item: &Map, Arc>, actions: &Map, Arc>) -> Arc, Arc>, Arc>> { - let mut structuredMap: Map, Arc, Sequence>>> = (&({ - let mut item = item.clone(); - let mut actions = actions.clone(); - Arc::new(move || -> Map, Arc, Sequence>>>{ - let mut _coll0: MapBuilder, Arc, Sequence>>> = MapBuilder::, Arc, Sequence>>>::new(); - for __compr_0 in (&item).keys().iter().cloned() { - let mut k: Sequence = __compr_0.clone(); - if { - let x: Sequence = k.clone(); - crate::implementation_from_dafny::software::amazon::cryptography::services::dynamodb::internaldafny::types::_default::IsValid_AttributeName(&x) - } { - if item.contains(&k) && (!actions.contains(&k) || actions.get(&k) != Arc::new(CryptoAction::DO_NOTHING {}) || crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::ReservedPrefix() <= k.clone()) { - _coll0.add(&k, &_default::AttrToStructured(&item.get(&k))) - } - } - } - _coll0.build() - }) - }))(); - _default::MapError::, Arc>>(&_default::SimplifyMapValue::, Arc>(&structuredMap)) + let mut ret = MaybePlacebo::, Arc>, Arc>>>::new(); + let mut attrNames: Sequence>; + let mut _out0: Sequence> = crate::implementation_from_dafny::SortedSets::_default::SetToSequence::>(&item.keys()); + attrNames = _out0.clone(); + let mut m: Object, Arc>>; + let mut _nw0: Object, Arc>> = MutableMap::, Arc>::_allocate_object(); + m = _nw0.clone(); + let mut _hi0: u64 = truncate!(attrNames.cardinality(), u64); + for i in integer_range(0, _hi0).map(Into::::into) { + let mut k: Sequence = attrNames.get(&int!((&i).clone())); + if !actions.contains(&k) || actions.get(&k) != Arc::new(CryptoAction::DO_NOTHING {}) || crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::ReservedPrefix() <= k.clone() { + let mut val: Arc, Sequence>> = _default::AttrToStructured(&item.get(&k)); + if matches!((&val).as_ref(), Failure{ .. }) { + let mut result: Arc, Arc>, Arc>> = Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>, Arc>::Failure { + error: crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::E(val.error()) + }); + ret = MaybePlacebo::from(result.clone()); + return ret.read(); + }; + MutableMapTrait::, Arc>::Put(rd!(m.clone()), &k, val.value()) + } + } + let mut result: Arc, Arc>, Arc>> = Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>, Arc>::Success { + value: MutableMapTrait::, Arc>::content(rd!(m.clone())) + }); + ret = MaybePlacebo::from(result.clone()); + return ret.read(); } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(48,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(65,3) pub fn StructuredToItemEncrypt(s: &Map, Arc>, orig: &Map, Arc>, actions: &Map, Arc>) -> Arc, Arc>, Arc>> { - let mut ddbMap: Map, Arc, Sequence>>> = (&({ - let mut s = s.clone(); - let mut orig = orig.clone(); - let mut actions = actions.clone(); - Arc::new(move || -> Map, Arc, Sequence>>>{ - let mut _coll0: MapBuilder, Arc, Sequence>>> = MapBuilder::, Arc, Sequence>>>::new(); - for __compr_0 in (&orig).keys().iter().cloned() { - let mut k: Sequence = __compr_0.clone(); - if { - let x: Sequence = k.clone(); - crate::implementation_from_dafny::software::amazon::cryptography::services::dynamodb::internaldafny::types::_default::IsValid_AttributeName(&x) - } { - if orig.contains(&k) { - _coll0.add(&k, &(if s.contains(&k) && actions.contains(&k) && actions.get(&k) == Arc::new(CryptoAction::ENCRYPT_AND_SIGN {}) { - _default::StructuredToAttr(&s.get(&k)) - } else { - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Sequence>::Success { - value: orig.get(&k) - }) - })) - } - } - } - _coll0.build() - }) - }))(); - let mut valueOrError0: Arc, Arc>, Arc>> = _default::MapError::, Arc>>(&_default::SimplifyMapValue::, Arc>(&ddbMap)); - if valueOrError0.IsFailure() { - valueOrError0.PropagateFailure::, Arc>>() - } else { - let mut oldMap: Map, Arc> = valueOrError0.Extract(); - let mut ddbMap2: Map, Arc, Sequence>>> = (&({ - let mut s = s.clone(); - let mut orig = orig.clone(); - Arc::new(move || -> Map, Arc, Sequence>>>{ - let mut _coll1: MapBuilder, Arc, Sequence>>> = MapBuilder::, Arc, Sequence>>>::new(); - for __compr_1 in (&s).keys().iter().cloned() { - let mut k: Sequence = __compr_1.clone(); - if { - let x: Sequence = k.clone(); - crate::implementation_from_dafny::software::amazon::cryptography::services::dynamodb::internaldafny::types::_default::IsValid_AttributeName(&x) - } { - if s.contains(&k) && !orig.contains(&k) { - _coll1.add(&k, &_default::StructuredToAttr(&s.get(&k))) - } - } - } - _coll1.build() - }) - }))(); - let mut valueOrError1: Arc, Arc>, Arc>> = _default::MapError::, Arc>>(&_default::SimplifyMapValue::, Arc>(&ddbMap2)); - if valueOrError1.IsFailure() { - valueOrError1.PropagateFailure::, Arc>>() - } else { - let mut newMap: Map, Arc> = valueOrError1.Extract(); - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>, Arc>::Success { - value: oldMap.merge(&newMap) - }) + let mut ret = MaybePlacebo::, Arc>, Arc>>>::new(); + let mut attrNames: Sequence>; + let mut _out0: Sequence> = crate::implementation_from_dafny::SortedSets::_default::SetToSequence::>(&orig.keys()); + attrNames = _out0.clone(); + let mut m: Object, Arc>>; + let mut _nw0: Object, Arc>> = MutableMap::, Arc>::_allocate_object(); + m = _nw0.clone(); + let mut _hi0: u64 = truncate!(attrNames.cardinality(), u64); + for i in integer_range(0, _hi0).map(Into::::into) { + let mut k: Sequence = attrNames.get(&int!((&i).clone())); + if !(crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::ReservedPrefix() <= k.clone()) { + if s.contains(&k) && actions.contains(&k) && actions.get(&k) == Arc::new(CryptoAction::ENCRYPT_AND_SIGN {}) { + let mut val: Arc, Sequence>> = _default::StructuredToAttr(&s.get(&k)); + if matches!((&val).as_ref(), Failure{ .. }) { + let mut result: Arc, Arc>, Arc>> = Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>, Arc>::Failure { + error: crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::E(val.error()) + }); + ret = MaybePlacebo::from(result.clone()); + return ret.read(); + }; + MutableMapTrait::, Arc>::Put(rd!(m.clone()), &k, val.value()) + } else { + MutableMapTrait::, Arc>::Put(rd!(m.clone()), &k, &orig.get(&k)) + } + } + } + let mut _out1: Sequence> = crate::implementation_from_dafny::SortedSets::_default::SetToSequence::>(&s.keys()); + attrNames = _out1.clone(); + let mut _hi1: u64 = truncate!(attrNames.cardinality(), u64); + for i in integer_range(0, _hi1).map(Into::::into) { + let mut k: Sequence = attrNames.get(&int!((&i).clone())); + if !orig.contains(&k) { + let mut val: Arc, Sequence>> = _default::StructuredToAttr(&s.get(&k)); + if matches!((&val).as_ref(), Failure{ .. }) { + let mut result: Arc, Arc>, Arc>> = Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>, Arc>::Failure { + error: crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::E(val.error()) + }); + ret = MaybePlacebo::from(result.clone()); + return ret.read(); + }; + MutableMapTrait::, Arc>::Put(rd!(m.clone()), &k, val.value()) } } + let mut result: Arc, Arc>, Arc>> = Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>, Arc>::Success { + value: MutableMapTrait::, Arc>::content(rd!(m.clone())) + }); + ret = MaybePlacebo::from(result.clone()); + return ret.read(); } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(64,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(120,3) pub fn StructuredToItemDecrypt(s: &Map, Arc>, orig: &Map, Arc>, actions: &Map, Arc>) -> Arc, Arc>, Arc>> { - let mut ddbMap: Map, Arc, Sequence>>> = (&({ - let mut s = s.clone(); - let mut orig = orig.clone(); - let mut actions = actions.clone(); - Arc::new(move || -> Map, Arc, Sequence>>>{ - let mut _coll0: MapBuilder, Arc, Sequence>>> = MapBuilder::, Arc, Sequence>>>::new(); - for __compr_0 in (&orig).keys().iter().cloned() { - let mut k: Sequence = __compr_0.clone(); - if { - let x: Sequence = k.clone(); - crate::implementation_from_dafny::software::amazon::cryptography::services::dynamodb::internaldafny::types::_default::IsValid_AttributeName(&x) - } { - if orig.contains(&k) && !(crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::ReservedPrefix() <= k.clone()) { - _coll0.add(&k, &(if s.contains(&k) && actions.contains(&k) && actions.get(&k) == Arc::new(CryptoAction::ENCRYPT_AND_SIGN {}) { - _default::StructuredToAttr(&s.get(&k)) - } else { - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Sequence>::Success { - value: orig.get(&k) - }) - })) - } - } - } - _coll0.build() - }) - }))(); - _default::MapError::, Arc>>(&_default::SimplifyMapValue::, Arc>(&ddbMap)) + let mut ret = MaybePlacebo::, Arc>, Arc>>>::new(); + let mut attrNames: Sequence>; + let mut _out0: Sequence> = crate::implementation_from_dafny::SortedSets::_default::SetToSequence::>(&orig.keys()); + attrNames = _out0.clone(); + let mut m: Object, Arc>>; + let mut _nw0: Object, Arc>> = MutableMap::, Arc>::_allocate_object(); + m = _nw0.clone(); + let mut _hi0: u64 = truncate!(attrNames.cardinality(), u64); + for i in integer_range(0, _hi0).map(Into::::into) { + let mut k: Sequence = attrNames.get(&int!((&i).clone())); + if !(crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::ReservedPrefix() <= k.clone()) { + if s.contains(&k) && actions.contains(&k) && actions.get(&k) == Arc::new(CryptoAction::ENCRYPT_AND_SIGN {}) { + let mut val: Arc, Sequence>> = _default::StructuredToAttr(&s.get(&k)); + if matches!((&val).as_ref(), Failure{ .. }) { + let mut result: Arc, Arc>, Arc>> = Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>, Arc>::Failure { + error: crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::E(val.error()) + }); + ret = MaybePlacebo::from(result.clone()); + return ret.read(); + }; + MutableMapTrait::, Arc>::Put(rd!(m.clone()), &k, val.value()) + } else { + MutableMapTrait::, Arc>::Put(rd!(m.clone()), &k, &orig.get(&k)) + } + } + } + let mut result: Arc, Arc>, Arc>> = Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Arc>, Arc>::Success { + value: MutableMapTrait::, Arc>::content(rd!(m.clone())) + }); + ret = MaybePlacebo::from(result.clone()); + return ret.read(); } /// = specification/dynamodb-encryption-client/ddb-item-conversion.md#convert-ddb-item-to-structured-data /// = type=implication /// # - MUST contain a [Structured Data Terminal](../structured-encryption/structures.md#structured-data-terminal) /// # for each attribute on the DynamoDB Item, and no others. - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(72,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(152,3) pub fn ItemToStructured(item: &Map, Arc>) -> Arc, Arc>, Arc>> { let mut structuredMap: Map, Arc, Sequence>>> = (&({ let mut item = item.clone(); @@ -101727,7 +101835,7 @@ pub mod _DynamoToStruct_Compile { /// = type=implication /// # - MUST contain an Attribute for every [Structured Data Terminal](../structured-encryption/structures.md#structured-data-terminal) /// # on the Structured Data, and not other Attributes. - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(101,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(181,3) pub fn StructuredToItem(s: &Map, Arc>) -> Arc, Arc>, Arc>> { if s.keys().iter().all(({ let mut s = s.clone(); @@ -101774,7 +101882,7 @@ pub mod _DynamoToStruct_Compile { _default::MakeError::, Arc>>(&string_utf16_of("Not valid attribute names : ").concat(&attrNameList)) } } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(134,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(214,3) pub fn BigEndianPosToU32(x: &Sequence, pos: u64) -> Arc>> { if truncate!(x.cardinality(), u64) < crate::implementation_from_dafny::_StandardLibrary_Compile::_MemoryMath_Compile::_default::Add(pos, _default::LENGTH_LEN64()) { Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::>::Failure { @@ -101786,7 +101894,7 @@ pub mod _DynamoToStruct_Compile { }) } } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(143,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(223,3) pub fn BigEndianPosToU32As64(x: &Sequence, pos: u64) -> Arc>> { if truncate!(x.cardinality(), u64) < crate::implementation_from_dafny::_StandardLibrary_Compile::_MemoryMath_Compile::_default::Add(pos, _default::LENGTH_LEN64()) { Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::>::Failure { @@ -101798,7 +101906,7 @@ pub mod _DynamoToStruct_Compile { }) } } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(152,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(232,3) pub fn MakeError<_T: DafnyType>(s: &Sequence) -> Arc>> { Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::<_T, Arc>::Failure { error: Arc::new(Error::DynamoDbEncryptionException { @@ -101806,7 +101914,7 @@ pub mod _DynamoToStruct_Compile { }) }) } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(156,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(236,3) pub fn MapError<_T: DafnyType>(r: &Arc>>) -> Arc>> { if matches!(r.as_ref(), Success{ .. }) { Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::<_T, Arc>::Success { @@ -101821,11 +101929,11 @@ pub mod _DynamoToStruct_Compile { /// and the Length is not needed since we are /// working with the exact set of bytes when we /// need to deserialize. - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(163,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(243,3) pub fn TopLevelAttributeToBytes(a: &Arc) -> Arc, Sequence>> { _default::AttrToBytes(a, false, 1) } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(173,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(253,3) pub fn AttrToStructured(item: &Arc) -> Arc, Sequence>> { let mut valueOrError0: Arc, Sequence>> = _default::TopLevelAttributeToBytes(item); if valueOrError0.IsFailure() { @@ -101840,7 +101948,7 @@ pub mod _DynamoToStruct_Compile { }) } } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(183,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(263,3) pub fn StructuredToAttr(s: &Arc) -> Arc, Sequence>> { let mut valueOrError0: Arc>> = crate::implementation_from_dafny::_Wrappers_Compile::_default::Need::>(truncate!(s.typeId().cardinality(), u64) == _default::TYPEID_LEN64(), &string_utf16_of("Type ID must be two bytes")); if valueOrError0.IsFailure() { @@ -101865,7 +101973,7 @@ pub mod _DynamoToStruct_Compile { } } } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(205,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(285,3) pub fn AttrToTypeId(a: &Arc) -> TerminalTypeId { let mut _source0: Arc = a.clone(); if matches!((&_source0).as_ref(), S{ .. }) { @@ -101926,17 +102034,18 @@ pub mod _DynamoToStruct_Compile { } } } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(221,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(301,3) pub fn CharLess(x: &DafnyCharUTF16, y: &DafnyCharUTF16) -> bool { x.clone() < y.clone() } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(227,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(307,3) pub fn AttrToBytes(a: &Arc, prefix: bool, depth: u64) -> Arc, Sequence>> { let mut valueOrError0: Arc>> = crate::implementation_from_dafny::_Wrappers_Compile::_default::Need::>(depth <= crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::MAX_STRUCTURE_DEPTH(), &string_utf16_of("Depth of attribute structure to serialize exceeds limit of ").concat(&crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::MAX_STRUCTURE_DEPTH_STR())); if valueOrError0.IsFailure() { valueOrError0.PropagateFailure::>() } else { let mut valueOrError1: Arc, Sequence>> = (&({ + let mut a = a.clone(); let mut depth = depth.clone(); Arc::new(move |_source0: &Arc| -> Arc, Sequence>>{ if matches!(_source0.as_ref(), S{ .. }) { @@ -101980,7 +102089,7 @@ pub mod _DynamoToStruct_Compile { if matches!(_source0.as_ref(), M{ .. }) { let mut ___mcc_h6: Map, Arc> = _source0.M().clone(); let mut m: Map, Arc> = ___mcc_h6.clone(); - _default::MapAttrToBytes(&m, depth) + _default::MapAttrToBytes(&a, &m, depth) } else { if matches!(_source0.as_ref(), L{ .. }) { let mut ___mcc_h7: Sequence> = _source0.L().clone(); @@ -102032,7 +102141,7 @@ pub mod _DynamoToStruct_Compile { } } } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(458,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(538,3) pub fn StringSetAttrToBytes(ss: &Sequence>) -> Arc, Sequence>> { let mut asSet: Set> = crate::implementation_from_dafny::_Seq_Compile::_default::ToSet::>(ss); let mut valueOrError0: Arc>> = crate::implementation_from_dafny::_Wrappers_Compile::_default::Need::>(truncate!(asSet.cardinality(), u64) == truncate!(ss.cardinality(), u64), &string_utf16_of("String Set had duplicate values")); @@ -102057,7 +102166,7 @@ pub mod _DynamoToStruct_Compile { } } } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(475,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(555,3) pub fn NumberSetAttrToBytes(ns: &Sequence>) -> Arc, Sequence>> { let mut asSet: Set> = crate::implementation_from_dafny::_Seq_Compile::_default::ToSet::>(ns); let mut valueOrError0: Arc>> = crate::implementation_from_dafny::_Wrappers_Compile::_default::Need::>(truncate!(asSet.cardinality(), u64) == truncate!(ns.cardinality(), u64), &string_utf16_of("Number Set had duplicate values")); @@ -102098,7 +102207,7 @@ pub mod _DynamoToStruct_Compile { } } } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(501,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(581,3) pub fn BinarySetAttrToBytes(bs: &Sequence>) -> Arc, Sequence>> { let mut asSet: Set> = crate::implementation_from_dafny::_Seq_Compile::_default::ToSet::>(bs); let mut valueOrError0: Arc>> = crate::implementation_from_dafny::_Wrappers_Compile::_default::Need::>(truncate!(asSet.cardinality(), u64) == truncate!(bs.cardinality(), u64), &string_utf16_of("Binary Set had duplicate values")); @@ -102123,50 +102232,45 @@ pub mod _DynamoToStruct_Compile { } } } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(527,3) - pub fn MapAttrToBytes(m: &Map, Arc>, depth: u64) -> Arc, Sequence>> { - let mut bytesResults: Map, Arc, Sequence>>> = (&({ - let mut m = m.clone(); - let mut depth = depth.clone(); - Arc::new(move || -> Map, Arc, Sequence>>>{ - let mut _coll0: MapBuilder, Arc, Sequence>>> = MapBuilder::, Arc, Sequence>>>::new(); - for __compr_0 in (&m).keys().iter().cloned() { - let mut k: Sequence = __compr_0.clone(); - if { - let x: Sequence = k.clone(); - crate::implementation_from_dafny::software::amazon::cryptography::services::dynamodb::internaldafny::types::_default::IsValid_AttributeName(&x) - } { - if m.contains(&k) { - _coll0.add(&k, &_default::AttrToBytes(&m.get(&k), true, depth + 1)) - } - } - } - _coll0.build() - }) - }))(); - let mut valueOrError0: Arc, Sequence>> = _default::U32ToBigEndian64(truncate!(m.cardinality(), u64)); + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(639,3) + pub fn MapAttrToBytes(parent: &Arc, m: &Map, Arc>, depth: u64) -> Arc, Sequence>> { + let mut ret = MaybePlacebo::, Sequence>>>::new(); + let mut attrNames: Sequence> = crate::implementation_from_dafny::SortedSets::_default::SetToOrderedSequence2::(&m.keys(), &(Arc::new(move |x0: &DafnyCharUTF16,x1: &DafnyCharUTF16| _default::CharLess(x0, x1)) as Arc _ + Sync + Send>)); + let mut len: u64 = truncate!(attrNames.cardinality(), u64); + let mut valueOrError0: Arc, Sequence>> = _default::U32ToBigEndian64(len); if valueOrError0.IsFailure() { - valueOrError0.PropagateFailure::>() - } else { - let mut count: Sequence = valueOrError0.Extract(); - let mut valueOrError1: Arc, Sequence>, Sequence>> = _default::SimplifyMapValue::, Sequence>(&bytesResults); - if valueOrError1.IsFailure() { - valueOrError1.PropagateFailure::>() - } else { - let mut bytes: Map, Sequence> = valueOrError1.Extract(); - let mut valueOrError2: Arc, Sequence>> = _default::CollectMap(&bytes, &(seq![] as Sequence)); - if valueOrError2.IsFailure() { - valueOrError2.PropagateFailure::>() - } else { - let mut body: Sequence = valueOrError2.Extract(); - Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Sequence>::Success { - value: count.concat(&body) - }) - } - } + ret = MaybePlacebo::from(valueOrError0.PropagateFailure::>()); + return ret.read(); + }; + let mut output: Sequence = valueOrError0.Extract(); + let mut _hi0: u64 = len; + for i in integer_range(0, _hi0).map(Into::::into) { + let mut k: Sequence = attrNames.get(&int!((&i).clone())); + let mut val: Arc, Sequence>> = _default::AttrToBytes(&m.get(&k), true, depth + 1); + if matches!((&val).as_ref(), Failure{ .. }) { + let mut result: Arc, Sequence>> = Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Sequence>::Failure { + error: val.error().clone() + }); + ret = MaybePlacebo::from(result.clone()); + return ret.read(); + }; + let mut data: Arc, Sequence>> = _default::SerializeMapItem(&k, val.value()); + if matches!((&data).as_ref(), Failure{ .. }) { + let mut result: Arc, Sequence>> = Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Sequence>::Failure { + error: data.error().clone() + }); + ret = MaybePlacebo::from(result.clone()); + return ret.read(); + }; + output = output.concat(data.value()); } + let mut result: Arc, Sequence>> = Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Sequence>::Success { + value: output.clone() + }); + ret = MaybePlacebo::from(result.clone()); + return ret.read(); } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(553,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(682,3) pub fn ListAttrToBytes(l: &Sequence>, depth: u64) -> Arc, Sequence>> { let mut valueOrError0: Arc, Sequence>> = _default::U32ToBigEndian64(truncate!(l.cardinality(), u64)); if valueOrError0.IsFailure() { @@ -102184,7 +102288,7 @@ pub mod _DynamoToStruct_Compile { } } } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(595,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(724,3) pub fn U32ToBigEndian64(x: u64) -> Arc, Sequence>> { if 4294967295 < x { Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::, Sequence>::Failure { @@ -102196,7 +102300,7 @@ pub mod _DynamoToStruct_Compile { }) } } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(614,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(743,3) pub fn BigEndianToU32As32(x: &Sequence) -> Arc>> { if truncate!(x.cardinality(), u64) < _default::LENGTH_LEN64() { Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::>::Failure { @@ -102208,7 +102312,7 @@ pub mod _DynamoToStruct_Compile { }) } } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(625,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(754,3) pub fn BigEndianToU32As64(x: &Sequence) -> Arc>> { if truncate!(x.cardinality(), u64) < _default::LENGTH_LEN64() { Arc::new(crate::implementation_from_dafny::_Wrappers_Compile::Result::>::Failure { @@ -102222,7 +102326,7 @@ pub mod _DynamoToStruct_Compile { } /// The Duvet implications set-entries and set-entry-length mentioned in SerializeBinaryValue /// are also implied here for String Sets and Number Sets - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(640,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(769,3) pub fn EncodeString(s: &Sequence) -> Arc, Sequence>> { let mut valueOrError0: Arc>> = crate::implementation_from_dafny::UTF8::_default::Encode(s); if valueOrError0.IsFailure() { @@ -102240,7 +102344,7 @@ pub mod _DynamoToStruct_Compile { } } } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(656,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(785,3) pub fn CollectString(setToSerialize: &Sequence>, pos: u64, serialized: &Sequence) -> Arc, Sequence>> { let mut _r0 = setToSerialize.clone(); let mut _r1 = pos; @@ -102278,7 +102382,7 @@ pub mod _DynamoToStruct_Compile { /// # | ---------------- | ------------------------------------ | /// # | Set Entry Length | 4 | /// # | Set Entry Value | Variable. Equal to Set Entry Length. | - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(673,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(802,3) pub fn SerializeBinaryValue(b: &Sequence) -> Arc, Sequence>> { let mut valueOrError0: Arc, Sequence>> = _default::U32ToBigEndian64(truncate!(b.cardinality(), u64)); if valueOrError0.IsFailure() { @@ -102290,7 +102394,7 @@ pub mod _DynamoToStruct_Compile { }) } } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(698,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(827,3) pub fn CollectBinary(setToSerialize: &Sequence>, pos: u64, serialized: &Sequence) -> Arc, Sequence>> { let mut _r0 = setToSerialize.clone(); let mut _r1 = pos; @@ -102320,7 +102424,7 @@ pub mod _DynamoToStruct_Compile { } } } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(758,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(887,3) pub fn CollectList(listToSerialize: &Sequence>, depth: u64, serialized: &Sequence) -> Arc, Sequence>> { let mut ret = MaybePlacebo::, Sequence>>>::new(); let mut result: Sequence = serialized.clone(); @@ -102346,7 +102450,7 @@ pub mod _DynamoToStruct_Compile { /// = specification/dynamodb-encryption-client/ddb-attribute-serialization.md#map-key /// = type=implication /// # Map Key MUST be a [String Value](#string). - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(790,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(919,3) pub fn SerializeMapItem(key: &Sequence, value: &Sequence) -> Arc, Sequence>> { let mut valueOrError0: Arc>> = crate::implementation_from_dafny::UTF8::_default::Encode(key); if valueOrError0.IsFailure() { @@ -102365,12 +102469,12 @@ pub mod _DynamoToStruct_Compile { } } } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(839,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(968,3) pub fn CollectMap(mapToSerialize: &Map, Sequence>, serialized: &Sequence) -> Arc, Sequence>> { let mut keys: Sequence> = crate::implementation_from_dafny::SortedSets::_default::SetToOrderedSequence2::(&mapToSerialize.keys(), &(Arc::new(move |x0: &DafnyCharUTF16,x1: &DafnyCharUTF16| _default::CharLess(x0, x1)) as Arc _ + Sync + Send>)); _default::CollectOrderedMapSubset(&keys, mapToSerialize, 0, serialized) } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(854,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(983,3) pub fn CollectOrderedMapSubset(keys: &Sequence>, mapToSerialize: &Map, Sequence>, pos: u64, serialized: &Sequence) -> Arc, Sequence>> { let mut _r0 = keys.clone(); let mut _r1 = mapToSerialize.clone(); @@ -102404,7 +102508,7 @@ pub mod _DynamoToStruct_Compile { } } } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(875,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(1004,3) pub fn BoolToUint8(b: bool) -> u8 { if b { 1 @@ -102412,7 +102516,7 @@ pub mod _DynamoToStruct_Compile { 0 } } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(886,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(1015,3) pub fn IsUnique<_T: DafnyTypeEq>(s: &Sequence<_T>) -> bool { let mut asSet: Set<_T> = crate::implementation_from_dafny::_Seq_Compile::_default::ToSet::<_T>(s); if truncate!(asSet.cardinality(), u64) == truncate!(s.cardinality(), u64) { @@ -102421,7 +102525,7 @@ pub mod _DynamoToStruct_Compile { false } } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(900,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(1029,3) pub fn DeserializeBinarySet(serialized: &Sequence, remainingCount: u64, origSerializedSize: u64, resultSet: &Arc) -> Arc, Sequence>> { let mut _r0 = serialized.clone(); let mut _r1 = remainingCount; @@ -102479,7 +102583,7 @@ pub mod _DynamoToStruct_Compile { } } } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(934,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(1063,3) pub fn DeserializeStringSet(serialized: &Sequence, remainingCount: u64, origSerializedSize: u64, resultSet: &Arc) -> Arc, Sequence>> { let mut _r0 = serialized.clone(); let mut _r1 = remainingCount; @@ -102543,7 +102647,7 @@ pub mod _DynamoToStruct_Compile { } } } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(969,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(1098,3) pub fn DeserializeNumberSet(serialized: &Sequence, remainingCount: u64, origSerializedSize: u64, resultSet: &Arc) -> Arc, Sequence>> { let mut _r0 = serialized.clone(); let mut _r1 = remainingCount; @@ -102607,7 +102711,7 @@ pub mod _DynamoToStruct_Compile { } } } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(1003,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(1132,3) pub fn DeserializeListEntry(serialized: &Sequence, pos: u64, depth: u64, resultList: &Arc) -> Arc, u64), Sequence>> { let mut serialized_size: u64 = truncate!(serialized.cardinality(), u64); if serialized_size - pos < _default::PREFIX_LEN64() { @@ -102653,7 +102757,7 @@ pub mod _DynamoToStruct_Compile { } } } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(1064,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(1193,3) pub fn DeserializeList(serialized: &Sequence, pos: u64, remainingCount: u64, depth: u64, resultList: &Arc) -> Arc, Sequence>> { let mut ret = MaybePlacebo::, Sequence>>>::new(); let mut npos: u64 = pos; @@ -102675,7 +102779,7 @@ pub mod _DynamoToStruct_Compile { })); return ret.read(); } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(1110,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(1239,3) pub fn DeserializeMapEntry(serialized: &Sequence, pos: u64, depth: u64, resultMap: &Arc) -> Arc, u64), Sequence>> { let mut serialized_size: u64 = truncate!(serialized.cardinality(), u64); let mut orig_pos: u64 = pos; @@ -102748,7 +102852,7 @@ pub mod _DynamoToStruct_Compile { } } } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(1190,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(1319,3) pub fn DeserializeMap(serialized: &Sequence, pos: u64, remainingCount: u64, depth: u64, resultMap: &Arc) -> Arc, Sequence>> { let mut ret = MaybePlacebo::, Sequence>>>::new(); let mut npos: u64 = pos; @@ -102770,7 +102874,7 @@ pub mod _DynamoToStruct_Compile { })); return ret.read(); } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(1237,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(1366,3) pub fn BytesToAttr(value: &Sequence, typeId: &TerminalTypeId, totalBytes: &Arc>, depth: u64, pos: u64) -> Arc, Sequence>> { let mut value_size: u64 = truncate!(value.cardinality(), u64); let mut valueOrError0: Arc>> = crate::implementation_from_dafny::_Wrappers_Compile::_default::Need::>(depth <= crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::MAX_STRUCTURE_DEPTH(), &string_utf16_of("Depth of attribute structure to deserialize exceeds limit of ").concat(&crate::implementation_from_dafny::_DynamoDbEncryptionUtil_Compile::_default::MAX_STRUCTURE_DEPTH_STR())); @@ -103058,7 +103162,7 @@ pub mod _DynamoToStruct_Compile { } } } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(1359,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(1488,3) pub fn FlattenValueMap<_X: DafnyTypeEq, _Y: DafnyType>(m: &Map<_X, Arc>>>) -> Map<_X, _Y> { (&({ let mut m = m.clone(); @@ -103074,7 +103178,7 @@ pub mod _DynamoToStruct_Compile { }) }))() } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(1363,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(1492,3) pub fn FlattenErrors<_X: DafnyTypeEq, _Y: DafnyType>(m: &Map<_X, Arc>>>) -> Set> { (&({ let mut m = m.clone(); @@ -103090,7 +103194,7 @@ pub mod _DynamoToStruct_Compile { }) }))() } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(1402,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(1531,3) pub fn SimplifyMapValue<_X: DafnyTypeEq, _Y: DafnyType>(m: &Map<_X, Arc>>>) -> Arc, Sequence>> { if m.keys().iter().all(({ let mut m = m.clone(); @@ -103112,28 +103216,28 @@ pub mod _DynamoToStruct_Compile { } } /// number of bytes in an encoded count or length - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(202,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(282,3) pub fn LENGTH_LEN64() -> u64 { 4 } /// number of bytes in a TerminalTypeId - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(201,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(281,3) pub fn TYPEID_LEN64() -> u64 { 2 } /// number of bytes in an encoded boolean - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(200,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(280,3) pub fn BOOL_LEN64() -> u64 { 1 } /// number of bytes in a prefix, i.e. 2-byte type and 4-byte length - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(203,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(283,3) pub fn PREFIX_LEN64() -> u64 { 6 } } - /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(881,3) + /// dafny/DynamoDbEncryption/src/DynamoToStruct.dfy(1010,3) #[derive(PartialEq, Clone)] pub enum AttrValueAndLength { AttrValueAndLength { @@ -111499,7 +111603,7 @@ pub mod _JSON_Compile { } else { let mut c: u16 = str.get(&(start.clone() + int!(1))); if c == DafnyCharUTF16(117 as u16).0 as u16 { - if !(start.clone() + int!(6) < str.cardinality()) { + if str.cardinality() < start.clone() + int!(6) { return Arc::new(Result::, Arc>::Failure { error: Arc::new(DeserializationError::EscapeAtEOS {}) }); @@ -114281,14 +114385,14 @@ pub mod _JSON_Compile { pub fn EscapeUnicode(c: u16) -> Sequence { let mut sStr: Sequence = crate::implementation_from_dafny::_JSON_Compile::_Utils_Compile::_Str_Compile::_default::OfNat(&int!((&c).clone()), &int!(16)); let mut s: Sequence = crate::implementation_from_dafny::_UnicodeStrings_Compile::_default::ASCIIToUTF16(&sStr); - s.concat(&({ - let _initializer = { - Arc::new(move |_v0: &DafnyInt| -> u16{ - DafnyCharUTF16(32 as u16).0 as u16 - }) - }; - integer_range(Zero::zero(), int!(4) - s.cardinality()).map(move |i| _initializer(&i)).collect::>() - })) + ({ + let _initializer = { + Arc::new(move |_v0: &DafnyInt| -> u16{ + DafnyCharUTF16(48 as u16).0 as u16 + }) + }; + integer_range(Zero::zero(), int!(4) - s.cardinality()).map(move |i| _initializer(&i)).collect::>() + }).concat(&s) } /// ../submodules/MaterialProviders/libraries/src/JSON/Spec.dfy(51,3) pub fn Escape(str: &Sequence, start: &nat) -> Sequence { @@ -130845,6 +130949,7 @@ pub mod _StandardLibrary_Compile { pub use ::dafny_runtime::euclidian_division; pub use ::dafny_runtime::DafnyCharUTF16; pub use ::dafny_runtime::string_utf16_of; + pub use ::dafny_runtime::DafnyTypeEq; pub use ::std::sync::Arc; pub use crate::implementation_from_dafny::_Wrappers_Compile::Option; pub use ::dafny_runtime::_System::nat; @@ -130856,7 +130961,7 @@ pub mod _StandardLibrary_Compile { pub struct _default {} impl _default { - /// ../submodules/MaterialProviders/StandardLibrary/src/String.dfy(14,3) + /// ../submodules/MaterialProviders/StandardLibrary/src/String.dfy(15,3) pub fn Int2Digits(n: &DafnyInt, base: &DafnyInt) -> Sequence { let mut _accumulator: Sequence = seq![] as Sequence; let mut _r0 = n.clone(); @@ -130876,7 +130981,7 @@ pub mod _StandardLibrary_Compile { } } } - /// ../submodules/MaterialProviders/StandardLibrary/src/String.dfy(30,3) + /// ../submodules/MaterialProviders/StandardLibrary/src/String.dfy(31,3) pub fn Digits2String(digits: &Sequence, chars: &Sequence) -> Sequence { let mut _accumulator: Sequence = seq![] as Sequence; let mut _r0 = digits.clone(); @@ -130896,7 +131001,7 @@ pub mod _StandardLibrary_Compile { } } } - /// ../submodules/MaterialProviders/StandardLibrary/src/String.dfy(40,3) + /// ../submodules/MaterialProviders/StandardLibrary/src/String.dfy(41,3) pub fn Int2String(n: &DafnyInt, chars: &Sequence) -> Sequence { let mut base: DafnyInt = chars.cardinality(); if n.clone() == int!(0) { @@ -130909,25 +131014,22 @@ pub mod _StandardLibrary_Compile { } } } - /// ../submodules/MaterialProviders/StandardLibrary/src/String.dfy(52,3) + /// ../submodules/MaterialProviders/StandardLibrary/src/String.dfy(53,3) pub fn Base10Int2String(n: &DafnyInt) -> Sequence { crate::implementation_from_dafny::_StandardLibrary_Compile::_String_Compile::_default::Int2String(n, &crate::implementation_from_dafny::_StandardLibrary_Compile::_String_Compile::_default::Base10()) } - /// ../submodules/MaterialProviders/StandardLibrary/src/String.dfy(58,3) - pub fn HasSubString(haystack: &Sequence, needle: &Sequence) -> Arc> { + /// ../submodules/MaterialProviders/StandardLibrary/src/String.dfy(59,3) + pub fn HasSubString<_T: DafnyTypeEq>(haystack: &Sequence<_T>, needle: &Sequence<_T>) -> Arc> { let mut o = MaybePlacebo::>>::new(); - if haystack.cardinality() < needle.cardinality() { + if truncate!(haystack.cardinality(), u64) < truncate!(needle.cardinality(), u64) { o = MaybePlacebo::from(Arc::new(Option::::None {})); return o.read(); }; - if !(!(crate::implementation_from_dafny::_StandardLibrary_Compile::_UInt_Compile::_default::UINT64_MAX_LIMIT() - int!(1) < haystack.cardinality())) { - panic!("Halt") - }; let mut size: u64 = truncate!(needle.cardinality(), u64); - let mut limit: u64 = truncate!(haystack.cardinality(), u64) - size + truncate!(int!(1), u64); + let mut limit: u64 = crate::implementation_from_dafny::_StandardLibrary_Compile::_MemoryMath_Compile::_default::Add(truncate!(haystack.cardinality(), u64) - size, truncate!(int!(1), u64)); let mut _hi0: u64 = limit; for index in integer_range(truncate!(int!(0), u64), _hi0).map(Into::::into) { - if crate::implementation_from_dafny::_StandardLibrary_Compile::_Sequence_Compile::_default::SequenceEqual::(haystack, needle, index, truncate!(int!(0), u64), size) { + if crate::implementation_from_dafny::_StandardLibrary_Compile::_Sequence_Compile::_default::SequenceEqual::<_T>(haystack, needle, index, truncate!(int!(0), u64), size) { o = MaybePlacebo::from(Arc::new(Option::::Some { value: int!(index) })); @@ -130937,7 +131039,7 @@ pub mod _StandardLibrary_Compile { o = MaybePlacebo::from(Arc::new(Option::::None {})); return o.read(); } - /// ../submodules/MaterialProviders/StandardLibrary/src/String.dfy(12,3) + /// ../submodules/MaterialProviders/StandardLibrary/src/String.dfy(13,3) pub fn Base10() -> Sequence { seq![DafnyCharUTF16(48 as u16), DafnyCharUTF16(49 as u16), DafnyCharUTF16(50 as u16), DafnyCharUTF16(51 as u16), DafnyCharUTF16(52 as u16), DafnyCharUTF16(53 as u16), DafnyCharUTF16(54 as u16), DafnyCharUTF16(55 as u16), DafnyCharUTF16(56 as u16), DafnyCharUTF16(57 as u16)] } @@ -132197,20 +132299,34 @@ pub mod _Structure_Compile { } /// ../submodules/MaterialProviders/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Structure.dfy(258,3) pub fn ExtractCustomEncryptionContext(encryptionContext: &BranchKeyContext) -> Arc, Arc>> { + let mut prefixKeys: Set> = (&({ + let mut encryptionContext = encryptionContext.clone(); + Arc::new(move || -> Set>{ + let mut _coll0: SetBuilder> = SetBuilder::>::new(); + for __compr_0 in (&encryptionContext.keys()).iter().cloned() { + let mut k: Sequence = __compr_0.clone(); + if encryptionContext.keys().contains(&k) && _default::ENCRYPTION_CONTEXT_PREFIX() <= k.clone() { + _coll0.add(&k) + } + } + _coll0.build() + }) + }))(); let mut encodedEncryptionContext: Set<(Arc>>, Arc>>)> = (&({ + let mut prefixKeys = prefixKeys.clone(); let mut encryptionContext = encryptionContext.clone(); Arc::new(move || -> Set<(Arc>>, Arc>>)>{ - let mut _coll0: SetBuilder<(Arc>>, Arc>>)> = SetBuilder::<(Arc>>, Arc>>)>::new(); - for __compr_0 in (&encryptionContext).keys().iter().cloned() { - let mut k: Sequence = __compr_0.clone(); - if encryptionContext.contains(&k) && _default::ENCRYPTION_CONTEXT_PREFIX() < k.clone() { - _coll0.add(&(( + let mut _coll1: SetBuilder<(Arc>>, Arc>>)> = SetBuilder::<(Arc>>, Arc>>)>::new(); + for __compr_1 in (&prefixKeys).iter().cloned() { + let mut k: Sequence = __compr_1.clone(); + if prefixKeys.contains(&k) { + _coll1.add(&(( crate::implementation_from_dafny::UTF8::_default::Encode(&k.drop(&int!((&truncate!((&_default::ENCRYPTION_CONTEXT_PREFIX().cardinality()).clone(), u32)).clone()))), crate::implementation_from_dafny::UTF8::_default::Encode(&encryptionContext.get(&k)) ))) } } - _coll0.build() + _coll1.build() }) }))(); let mut valueOrError0: Arc>> = crate::implementation_from_dafny::_Wrappers_Compile::_default::Need::>((&encodedEncryptionContext).iter().all(({ @@ -132229,14 +132345,14 @@ pub mod _Structure_Compile { value: (&({ let mut encodedEncryptionContext = encodedEncryptionContext.clone(); Arc::new(move || -> Map{ - let mut _coll1: MapBuilder = MapBuilder::::new(); - for __compr_1 in (&encodedEncryptionContext).iter().cloned() { - let mut i: (Arc>>, Arc>>) = __compr_1.clone(); + let mut _coll2: MapBuilder = MapBuilder::::new(); + for __compr_2 in (&encodedEncryptionContext).iter().cloned() { + let mut i: (Arc>>, Arc>>) = __compr_2.clone(); if encodedEncryptionContext.contains(&i) { - _coll1.add(i.0.clone().value(), i.1.clone().value()) + _coll2.add(i.0.clone().value(), i.1.clone().value()) } } - _coll1.build() + _coll2.build() }) }))() }) @@ -140460,7 +140576,10 @@ pub mod _TestDynamoDBFilterExpr_Compile { impl _default { /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(19,3) pub fn expect_contains(haystack: &Arc, needle: &Arc, negate: bool) -> () { - if crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::does_contain(haystack, needle) != negate { + let mut val: bool; + let mut _out0: bool = crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::does_contain(haystack, needle); + val = _out0; + if val != negate { if negate { print!("{}", DafnyPrintWrapper(haystack)); print!("{}", DafnyPrintWrapper(&string_utf16_of(" should not have contained "))); @@ -140473,7 +140592,7 @@ pub mod _TestDynamoDBFilterExpr_Compile { print!("{}", DafnyPrintWrapper(&string_utf16_of("but it didn't\n"))) } }; - let mut _e00: bool = crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::does_contain(haystack, needle); + let mut _e00: bool = val; let mut _e10: bool = negate; if !(_e00 == _e10) { print!("{}", DafnyPrintWrapper(&string_utf16_of("\nLeft:\n"))); @@ -140484,7 +140603,7 @@ pub mod _TestDynamoDBFilterExpr_Compile { }; return (); } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(32,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(33,3) pub fn UnicodeLessTest() -> () { let mut A: Sequence = string_utf16_of("A"); let mut B: Sequence = string_utf16_of("퀀"); @@ -140507,24 +140626,27 @@ pub mod _TestDynamoDBFilterExpr_Compile { } return (); } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(58,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(59,3) pub fn LowLevelTests() -> () { - crate::implementation_from_dafny::_BeaconTestFixtures_Compile::_default::expect_equal::>>(&crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::ParseExpr(&string_utf16_of("and")), &seq![Arc::new(Token::And {})]); - crate::implementation_from_dafny::_BeaconTestFixtures_Compile::_default::expect_equal::>>(&crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::ParseExpr(&string_utf16_of(" AnD ")), &seq![Arc::new(Token::And {})]); - crate::implementation_from_dafny::_BeaconTestFixtures_Compile::_default::expect_equal::>>(&crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::ParseExpr(&string_utf16_of(" A AnD B ")), &seq![crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::MakeAttr(&string_utf16_of("A")), Arc::new(Token::And {}), crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::MakeAttr(&string_utf16_of("B"))]); - crate::implementation_from_dafny::_BeaconTestFixtures_Compile::_default::expect_equal::>>(&crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::ParseExpr(&string_utf16_of(" A_B AnD B_C ")), &seq![crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::MakeAttr(&string_utf16_of("A_B")), Arc::new(Token::And {}), crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::MakeAttr(&string_utf16_of("B_C"))]); + crate::implementation_from_dafny::_BeaconTestFixtures_Compile::_default::expect_equal::>>(&crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::ParseExpr(&string_utf16_of("and"), 0), &seq![Arc::new(Token::And {})]); + crate::implementation_from_dafny::_BeaconTestFixtures_Compile::_default::expect_equal::>>(&crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::ParseExpr(&string_utf16_of(" AnD "), 0), &seq![Arc::new(Token::And {})]); + crate::implementation_from_dafny::_BeaconTestFixtures_Compile::_default::expect_equal::>>(&crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::ParseExpr(&string_utf16_of(" A AnD B "), 0), &seq![crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::MakeAttr(&string_utf16_of("A")), Arc::new(Token::And {}), crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::MakeAttr(&string_utf16_of("B"))]); + crate::implementation_from_dafny::_BeaconTestFixtures_Compile::_default::expect_equal::>>(&crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::ParseExpr(&string_utf16_of(" A_B AnD B_C "), 0), &seq![crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::MakeAttr(&string_utf16_of("A_B")), Arc::new(Token::And {}), crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::MakeAttr(&string_utf16_of("B_C"))]); let mut input: Sequence> = seq![Arc::new(Token::Not {}), crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::MakeAttr(&string_utf16_of("A")), Arc::new(Token::In {}), Arc::new(Token::Open {}), crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::MakeAttr(&string_utf16_of("B")), Arc::new(Token::Comma {}), crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::MakeAttr(&string_utf16_of("C")), Arc::new(Token::Close {}), Arc::new(Token::Or {})]; - if !crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::IsIN(&input.drop(&int!(1))) { + if !crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::IsIN(&input, 1) { + panic!("Halt") + }; + if !crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::IsIN(&input.drop(&int!(1)), 0) { panic!("Halt") }; - crate::implementation_from_dafny::_BeaconTestFixtures_Compile::_default::expect_equal::>>(&crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::ConvertToPrefix(&input), &seq![Arc::new(Token::Not {}), Arc::new(Token::In {}), Arc::new(Token::Open {}), crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::MakeAttr(&string_utf16_of("A")), Arc::new(Token::Comma {}), crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::MakeAttr(&string_utf16_of("B")), Arc::new(Token::Comma {}), crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::MakeAttr(&string_utf16_of("C")), Arc::new(Token::Close {}), Arc::new(Token::Or {})]); + crate::implementation_from_dafny::_BeaconTestFixtures_Compile::_default::expect_equal::>>(&crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::ConvertToPrefix(&input, 0), &seq![Arc::new(Token::Not {}), Arc::new(Token::In {}), Arc::new(Token::Open {}), crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::MakeAttr(&string_utf16_of("A")), Arc::new(Token::Comma {}), crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::MakeAttr(&string_utf16_of("B")), Arc::new(Token::Comma {}), crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::MakeAttr(&string_utf16_of("C")), Arc::new(Token::Close {}), Arc::new(Token::Or {})]); input = seq![Arc::new(Token::And {}), Arc::new(Token::Or {}), Arc::new(Token::Not {}), Arc::new(Token::And {}), Arc::new(Token::Or {}), Arc::new(Token::Not {}), Arc::new(Token::And {}), Arc::new(Token::Or {}), Arc::new(Token::Not {})]; - crate::implementation_from_dafny::_BeaconTestFixtures_Compile::_default::expect_equal::>>(&crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::ConvertToPrefix(&input), &input); + crate::implementation_from_dafny::_BeaconTestFixtures_Compile::_default::expect_equal::>>(&crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::ConvertToPrefix(&input, 0), &input); input = seq![Arc::new(Token::Not {}), crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::MakeAttr(&string_utf16_of("A")), Arc::new(Token::In {}), Arc::new(Token::Open {}), crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::MakeAttr(&string_utf16_of("B")), Arc::new(Token::Comma {}), crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::MakeAttr(&string_utf16_of("C")), Arc::new(Token::Close {})]; - crate::implementation_from_dafny::_BeaconTestFixtures_Compile::_default::expect_equal::>>(&crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::ConvertToPrefix(&input), &seq![Arc::new(Token::Not {}), Arc::new(Token::In {}), Arc::new(Token::Open {}), crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::MakeAttr(&string_utf16_of("A")), Arc::new(Token::Comma {}), crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::MakeAttr(&string_utf16_of("B")), Arc::new(Token::Comma {}), crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::MakeAttr(&string_utf16_of("C")), Arc::new(Token::Close {})]); + crate::implementation_from_dafny::_BeaconTestFixtures_Compile::_default::expect_equal::>>(&crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::ConvertToPrefix(&input, 0), &seq![Arc::new(Token::Not {}), Arc::new(Token::In {}), Arc::new(Token::Open {}), crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::MakeAttr(&string_utf16_of("A")), Arc::new(Token::Comma {}), crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::MakeAttr(&string_utf16_of("B")), Arc::new(Token::Comma {}), crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::MakeAttr(&string_utf16_of("C")), Arc::new(Token::Close {})]); return (); } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(75,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(77,3) pub fn TestExtractAttributes() -> () { let mut attrMap: Map, Sequence> = map![(string_utf16_of("#one")) => (string_utf16_of("two")), (string_utf16_of("#three")) => (string_utf16_of("four"))]; crate::implementation_from_dafny::_BeaconTestFixtures_Compile::_default::expect_equal::>>(&crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::ExtractAttributes(&string_utf16_of(""), &Arc::new(Option::, Sequence>>::None {})), &(seq![] as Sequence>)); @@ -140584,7 +140706,7 @@ pub mod _TestDynamoDBFilterExpr_Compile { })), &seq![string_utf16_of("A"), string_utf16_of("B"), string_utf16_of("D"), string_utf16_of("E"), string_utf16_of("F")]); return (); } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(105,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(107,3) pub fn TestNoBeacons() -> () { let mut context: Arc = Arc::new(ExprContext::ExprContext { keyExpr: Arc::new(Option::>::None {}), @@ -140631,7 +140753,7 @@ pub mod _TestDynamoDBFilterExpr_Compile { }; return (); } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(122,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(124,3) pub fn TestBasicParse() -> () { let mut context: Arc = Arc::new(ExprContext::ExprContext { keyExpr: Arc::new(Option::>::None {}), @@ -140662,7 +140784,7 @@ pub mod _TestDynamoDBFilterExpr_Compile { panic!("Halt") }; let mut beaconVersion: Arc = valueOrError0.Extract(); - let mut parsed: Sequence> = crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::ParseExpr(context.filterExpr().value()); + let mut parsed: Sequence> = crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::ParseExpr(context.filterExpr().value(), 0); let mut _e00: DafnyInt = parsed.cardinality(); let mut _e10: DafnyInt = int!(7); if !(_e00.clone() == _e10.clone()) { @@ -140716,7 +140838,7 @@ pub mod _TestDynamoDBFilterExpr_Compile { }; return (); } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(150,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(152,3) pub fn TestNoBeaconFail() -> () { let mut context: Arc = Arc::new(ExprContext::ExprContext { keyExpr: Arc::new(Option::>::None {}), @@ -140747,7 +140869,7 @@ pub mod _TestDynamoDBFilterExpr_Compile { panic!("Halt") }; let mut beaconVersion: Arc = valueOrError0.Extract(); - let mut parsed: Sequence> = crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::ParseExpr(context.filterExpr().value()); + let mut parsed: Sequence> = crate::implementation_from_dafny::_DynamoDBFilterExpr_Compile::_default::ParseExpr(context.filterExpr().value(), 0); let mut _e00: DafnyInt = parsed.cardinality(); let mut _e10: DafnyInt = int!(7); if !(_e00.clone() == _e10.clone()) { @@ -140832,7 +140954,7 @@ pub mod _TestDynamoDBFilterExpr_Compile { }; return (); } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(185,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(187,3) pub fn TestBasicBeacons() -> () { let mut context: Arc = Arc::new(ExprContext::ExprContext { keyExpr: Arc::new(Option::>::None {}), @@ -140895,7 +141017,7 @@ pub mod _TestDynamoDBFilterExpr_Compile { })); return (); } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(217,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(219,3) pub fn TestMultiContextFailures() -> () { let mut context: Arc = Arc::new(ExprContext::ExprContext { keyExpr: Arc::new(Option::>::None {}), @@ -140987,19 +141109,19 @@ pub mod _TestDynamoDBFilterExpr_Compile { }; return (); } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(258,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(260,3) pub fn DS(x: &Sequence) -> Arc { Arc::new(AttributeValue::S { S: x.clone() }) } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(262,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(264,3) pub fn DN(x: &Sequence) -> Arc { Arc::new(AttributeValue::N { N: x.clone() }) } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(267,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(269,3) pub fn TestFilterCompare() -> () { let mut item1: Map, Arc> = map![(string_utf16_of("one")) => (_default::DS(&string_utf16_of("abc"))), (string_utf16_of("two")) => (_default::DS(&string_utf16_of("cde"))), (string_utf16_of("three")) => (_default::DS(&string_utf16_of("cde")))]; let mut values: Map, Arc> = map![]; @@ -141150,7 +141272,7 @@ pub mod _TestDynamoDBFilterExpr_Compile { crate::implementation_from_dafny::_BeaconTestFixtures_Compile::_default::expect_equal::, Arc>>>(&newItems, &seq![item1.clone()]); return (); } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(305,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(307,3) pub fn TestFilterFailNumeric() -> () { let mut item1: Map, Arc> = map![(string_utf16_of("one")) => (_default::DN(&string_utf16_of("800")))]; let mut values: Map, Arc> = map![(string_utf16_of(":two")) => (_default::DN(&string_utf16_of("foo")))]; @@ -141188,7 +141310,7 @@ pub mod _TestDynamoDBFilterExpr_Compile { }; return (); } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(320,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(322,3) pub fn TestFilterCompareNumeric() -> () { let mut item1: Map, Arc> = map![(string_utf16_of("one")) => (_default::DN(&string_utf16_of("800")))]; let mut values: Map, Arc> = map![(string_utf16_of(":two")) => (_default::DN(&string_utf16_of("0800.000e0")))]; @@ -141351,7 +141473,7 @@ pub mod _TestDynamoDBFilterExpr_Compile { crate::implementation_from_dafny::_BeaconTestFixtures_Compile::_default::expect_equal::, Arc>>>(&newItems, &seq![item1.clone()]); return (); } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(357,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(359,3) pub fn TestFilterIn() -> () { let mut item1: Map, Arc> = map![(string_utf16_of("one")) => (_default::DS(&string_utf16_of("abc"))), (string_utf16_of("two")) => (_default::DS(&string_utf16_of("cde"))), (string_utf16_of("three")) => (_default::DS(&string_utf16_of("cde")))]; let mut version: Arc; @@ -141419,7 +141541,7 @@ pub mod _TestDynamoDBFilterExpr_Compile { crate::implementation_from_dafny::_BeaconTestFixtures_Compile::_default::expect_equal::, Arc>>>(&newItems, &(seq![] as Sequence, Arc>>)); return (); } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(378,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(380,3) pub fn TestFilterBetweenAlpha() -> () { let mut item1: Map, Arc> = map![(string_utf16_of("one")) => (_default::DS(&string_utf16_of("abc"))), (string_utf16_of("two")) => (_default::DS(&string_utf16_of("bcd"))), (string_utf16_of("three")) => (_default::DS(&string_utf16_of("cde")))]; let mut version: Arc; @@ -141487,7 +141609,7 @@ pub mod _TestDynamoDBFilterExpr_Compile { crate::implementation_from_dafny::_BeaconTestFixtures_Compile::_default::expect_equal::, Arc>>>(&newItems, &seq![item1.clone()]); return (); } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(399,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(401,3) pub fn TestFilterBetweenNumber() -> () { let mut item1: Map, Arc> = map![(string_utf16_of("one")) => (_default::DN(&string_utf16_of("9"))), (string_utf16_of("two")) => (_default::DN(&string_utf16_of("52"))), (string_utf16_of("three")) => (_default::DN(&string_utf16_of("185")))]; let mut version: Arc; @@ -141555,7 +141677,7 @@ pub mod _TestDynamoDBFilterExpr_Compile { crate::implementation_from_dafny::_BeaconTestFixtures_Compile::_default::expect_equal::, Arc>>>(&newItems, &seq![item1.clone()]); return (); } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(419,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(421,3) pub fn TestFilterSize() -> () { let mut item1: Map, Arc> = map![(string_utf16_of("one")) => (_default::DN(&string_utf16_of("9"))), (string_utf16_of("two")) => (_default::DN(&string_utf16_of("52"))), (string_utf16_of("three")) => (_default::DN(&string_utf16_of("185")))]; let mut values: Arc, Arc>>> = Arc::new(Option::, Arc>>::Some { @@ -141626,7 +141748,7 @@ pub mod _TestDynamoDBFilterExpr_Compile { crate::implementation_from_dafny::_BeaconTestFixtures_Compile::_default::expect_equal::, Arc>>>(&newItems, &(seq![] as Sequence, Arc>>)); return (); } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(445,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(447,3) pub fn TestFilterContains() -> () { let mut item1: Map, Arc> = map![(string_utf16_of("one")) => (_default::DN(&string_utf16_of("abcdef"))), (string_utf16_of("two")) => (_default::DN(&string_utf16_of("a"))), (string_utf16_of("three")) => (_default::DN(&string_utf16_of("f"))), (string_utf16_of("four")) => (_default::DN(&string_utf16_of("cde"))), (string_utf16_of("five")) => (_default::DN(&string_utf16_of("efg")))]; let mut version: Arc; @@ -141684,7 +141806,7 @@ pub mod _TestDynamoDBFilterExpr_Compile { crate::implementation_from_dafny::_BeaconTestFixtures_Compile::_default::expect_equal::, Arc>>>(&newItems, &(seq![] as Sequence, Arc>>)); return (); } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(467,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(469,3) pub fn TestFilterBegins() -> () { let mut item1: Map, Arc> = map![(string_utf16_of("one")) => (_default::DN(&string_utf16_of("abcdef"))), (string_utf16_of("two")) => (_default::DN(&string_utf16_of("a"))), (string_utf16_of("three")) => (_default::DN(&string_utf16_of("f"))), (string_utf16_of("four")) => (_default::DN(&string_utf16_of("abcd"))), (string_utf16_of("five")) => (_default::DN(&string_utf16_of("abcdf")))]; let mut version: Arc; @@ -141742,7 +141864,7 @@ pub mod _TestDynamoDBFilterExpr_Compile { crate::implementation_from_dafny::_BeaconTestFixtures_Compile::_default::expect_equal::, Arc>>>(&newItems, &(seq![] as Sequence, Arc>>)); return (); } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(488,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(490,3) pub fn TestFilterComplex() -> () { let mut item1: Map, Arc> = map![(string_utf16_of("one")) => (_default::DN(&string_utf16_of("1"))), (string_utf16_of("two")) => (_default::DN(&string_utf16_of("2"))), (string_utf16_of("three")) => (_default::DN(&string_utf16_of("3")))]; let mut values: Arc, Arc>>> = Arc::new(Option::, Arc>>::Some { @@ -141783,7 +141905,7 @@ pub mod _TestDynamoDBFilterExpr_Compile { crate::implementation_from_dafny::_BeaconTestFixtures_Compile::_default::expect_equal::, Arc>>>(&newItems, &seq![item1.clone()]); return (); } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(510,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(512,3) pub fn TestFilterIndirectNames() -> () { let mut item1: Map, Arc> = map![(string_utf16_of("one")) => (_default::DS(&string_utf16_of("abc"))), (string_utf16_of("two")) => (_default::DS(&string_utf16_of("cde"))), (string_utf16_of("three")) => (_default::DS(&string_utf16_of("cde")))]; let mut values: Map, Arc> = map![(string_utf16_of(":uno")) => (_default::DS(&string_utf16_of("ab"))), (string_utf16_of(":dos")) => (_default::DS(&string_utf16_of("bc")))]; @@ -141887,7 +142009,7 @@ pub mod _TestDynamoDBFilterExpr_Compile { crate::implementation_from_dafny::_BeaconTestFixtures_Compile::_default::expect_equal::, Arc>>>(&newItems, &(seq![] as Sequence, Arc>>)); return (); } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(545,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(547,3) pub fn TestFilterIndirectNamesWithLoc() -> () { let mut values: Map, Arc> = map![(string_utf16_of(":uno")) => (_default::DS(&string_utf16_of("ab"))), (string_utf16_of(":dos")) => (_default::DN(&string_utf16_of("2")))]; let mut names: Map, Sequence> = map![(string_utf16_of("#eine")) => (string_utf16_of("Date")), (string_utf16_of("#zwei")) => (string_utf16_of("Month")), (string_utf16_of("#drei")) => (string_utf16_of("Year"))]; @@ -141962,7 +142084,7 @@ pub mod _TestDynamoDBFilterExpr_Compile { crate::implementation_from_dafny::_BeaconTestFixtures_Compile::_default::expect_equal::, Arc>>>(&newItems, &(seq![] as Sequence, Arc>>)); return (); } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(569,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(571,3) pub fn TestFilterAttrOps() -> () { let mut names: Map, Sequence> = map![(string_utf16_of("#fecha")) => (string_utf16_of("Date"))]; let mut values: Map, Arc> = map![(string_utf16_of(":m")) => (_default::DS(&string_utf16_of("M"))), (string_utf16_of(":s")) => (_default::DS(&string_utf16_of("N")))]; @@ -142093,7 +142215,7 @@ pub mod _TestDynamoDBFilterExpr_Compile { crate::implementation_from_dafny::_BeaconTestFixtures_Compile::_default::expect_equal::, Arc>>>(&newItems, &seq![crate::implementation_from_dafny::_BeaconTestFixtures_Compile::_default::SimpleItem()]); return (); } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(598,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(600,3) pub fn TestFilterSizeIn() -> () { let mut item1: Map, Arc> = map![(string_utf16_of("one")) => (_default::DN(&string_utf16_of("9"))), (string_utf16_of("two")) => (_default::DN(&string_utf16_of("52"))), (string_utf16_of("three")) => (_default::DN(&string_utf16_of("185")))]; let mut values: Arc, Arc>>> = Arc::new(Option::, Arc>>::Some { @@ -142154,7 +142276,7 @@ pub mod _TestDynamoDBFilterExpr_Compile { crate::implementation_from_dafny::_BeaconTestFixtures_Compile::_default::expect_equal::, Arc>>>(&newItems, &(seq![] as Sequence, Arc>>)); return (); } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(623,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(625,3) pub fn TestFilterBeacons() -> () { let mut values: Map, Arc> = map![(string_utf16_of(":val2")) => (_default::DN(&string_utf16_of("1.23"))), (string_utf16_of(":val3")) => (_default::DS(&string_utf16_of("N_MyName.T_MyTitle"))), (string_utf16_of(":val4")) => (_default::DS(&string_utf16_of("T_MyTitle"))), (string_utf16_of(":val5")) => (_default::DS(&string_utf16_of("MyName__mytitle")))]; let mut version: Arc; @@ -142256,7 +142378,7 @@ pub mod _TestDynamoDBFilterExpr_Compile { crate::implementation_from_dafny::_BeaconTestFixtures_Compile::_default::expect_equal::, Arc>>>(&newItems, &seq![crate::implementation_from_dafny::_BeaconTestFixtures_Compile::_default::SimpleItem()]); return (); } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(649,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(651,3) pub fn TestBadBetween() -> () { let mut values: Map, Arc> = map![(string_utf16_of(":val3")) => (_default::DS(&string_utf16_of("T_ATitle"))), (string_utf16_of(":val4")) => (_default::DS(&string_utf16_of("T_MyTitle")))]; let mut version: Arc; @@ -142293,7 +142415,7 @@ pub mod _TestDynamoDBFilterExpr_Compile { }; return (); } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(664,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(666,3) pub fn TestBadStandard() -> () { let mut values: Map, Arc> = map![(string_utf16_of(":val")) => (_default::DS(&string_utf16_of("foo")))]; let mut version: Arc; @@ -142411,7 +142533,7 @@ pub mod _TestDynamoDBFilterExpr_Compile { }; return (); } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(692,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(694,3) pub fn TestComparisons() -> () { let mut values: Map, Arc> = map![(string_utf16_of(":val1")) => (_default::DS(&string_utf16_of("N_"))), (string_utf16_of(":val2")) => (_default::DS(&string_utf16_of("N_MyName"))), (string_utf16_of(":val3")) => (_default::DS(&string_utf16_of("N_MyName.T_"))), (string_utf16_of(":val4")) => (_default::DS(&string_utf16_of("N_MyName.T_Title"))), (string_utf16_of(":val5")) => (_default::DS(&string_utf16_of("T_"))), (string_utf16_of(":val6")) => (_default::DS(&string_utf16_of("N_MyName.N_")))]; let mut version: Arc; @@ -142443,6 +142565,11 @@ pub mod _TestDynamoDBFilterExpr_Compile { value: values.clone() })); newItems = _out4.clone(); + if matches!((&newItems).as_ref(), Failure{ .. }) { + print!("{}", DafnyPrintWrapper(&string_utf16_of("\n"))); + print!("{}", DafnyPrintWrapper(&newItems)); + print!("{}", DafnyPrintWrapper(&string_utf16_of("\n\n"))) + }; if !matches!((&newItems).as_ref(), Success{ .. }) { panic!("Halt") }; @@ -142575,157 +142702,157 @@ pub mod _TestDynamoDBFilterExpr_Compile { } } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(32,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(33,3) #[test] pub fn UnicodeLessTest() { _default::UnicodeLessTest() } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(58,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(59,3) #[test] pub fn LowLevelTests() { _default::LowLevelTests() } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(75,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(77,3) #[test] pub fn TestExtractAttributes() { _default::TestExtractAttributes() } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(105,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(107,3) #[test] pub fn TestNoBeacons() { _default::TestNoBeacons() } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(122,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(124,3) #[test] pub fn TestBasicParse() { _default::TestBasicParse() } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(150,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(152,3) #[test] pub fn TestNoBeaconFail() { _default::TestNoBeaconFail() } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(185,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(187,3) #[test] pub fn TestBasicBeacons() { _default::TestBasicBeacons() } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(217,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(219,3) #[test] pub fn TestMultiContextFailures() { _default::TestMultiContextFailures() } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(267,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(269,3) #[test] pub fn TestFilterCompare() { _default::TestFilterCompare() } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(305,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(307,3) #[test] pub fn TestFilterFailNumeric() { _default::TestFilterFailNumeric() } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(320,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(322,3) #[test] pub fn TestFilterCompareNumeric() { _default::TestFilterCompareNumeric() } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(357,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(359,3) #[test] pub fn TestFilterIn() { _default::TestFilterIn() } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(378,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(380,3) #[test] pub fn TestFilterBetweenAlpha() { _default::TestFilterBetweenAlpha() } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(399,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(401,3) #[test] pub fn TestFilterBetweenNumber() { _default::TestFilterBetweenNumber() } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(419,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(421,3) #[test] pub fn TestFilterSize() { _default::TestFilterSize() } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(445,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(447,3) #[test] pub fn TestFilterContains() { _default::TestFilterContains() } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(467,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(469,3) #[test] pub fn TestFilterBegins() { _default::TestFilterBegins() } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(488,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(490,3) #[test] pub fn TestFilterComplex() { _default::TestFilterComplex() } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(510,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(512,3) #[test] pub fn TestFilterIndirectNames() { _default::TestFilterIndirectNames() } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(545,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(547,3) #[test] pub fn TestFilterIndirectNamesWithLoc() { _default::TestFilterIndirectNamesWithLoc() } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(569,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(571,3) #[test] pub fn TestFilterAttrOps() { _default::TestFilterAttrOps() } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(598,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(600,3) #[test] pub fn TestFilterSizeIn() { _default::TestFilterSizeIn() } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(623,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(625,3) #[test] pub fn TestFilterBeacons() { _default::TestFilterBeacons() } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(649,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(651,3) #[test] pub fn TestBadBetween() { _default::TestBadBetween() } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(664,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(666,3) #[test] pub fn TestBadStandard() { _default::TestBadStandard() } - /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(692,3) + /// dafny/DynamoDbEncryption/test/FilterExpr.dfy(694,3) #[test] pub fn TestComparisons() { _default::TestComparisons()