diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy index 60163f417..6045f22db 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy @@ -153,6 +153,83 @@ module CompoundBeacon { partFromPrefix(parts, value) } + function method PartsToString(p : seq) : string + { + var beaconParts := Seq.Map((s : BeaconPart) => s.getPrefix(), p); + if |beaconParts| == 0 then + "" + else + Join(beaconParts, "") + } + + function method CPartToString(s : ConstructorPart) : string + { + if s.required then + s.part.getPrefix() + else + "[" + s.part.getPrefix() + "]" + } + + function method CPartsToString(p : seq) : string + { + var beaconParts := Seq.Map((s : ConstructorPart) => CPartToString(s), p); + if |beaconParts| == 0 then + "" + else + Join(beaconParts, "") + } + + function method CListToString(p : ConstructorList) : string + { + var beaconParts := Seq.Map((s : Constructor) => CPartsToString(s.parts), p); + Join(beaconParts, ", ") + } + + // Can this constructor produce this list of parts? + // e.g. if the constructor has A_.B_ then + // these are ok : A_foo, B_foo, A_foo.B_foo + // these are bad : B_foo.A_foo, A_foo.A_foo + // that is, we can skip a arbitrary number of parts, + // but once we match a part, the rest of inParts must be able to directly follow + predicate method CanConstruct(con : seq, inParts : seq, matched : bool := false) + { + if |inParts| == 0 then + true + else if |con| == 0 then + false + else if con[0].part == inParts[0] then + CanConstruct(con[1..], inParts[1..], true) + else if !con[0].required || !matched then + CanConstruct(con[1..], inParts, matched) + else + false + } + + // Fail unless one of these constructor can make a beacon composed of this sequence of parts + predicate method {:tailrecursion} IsValidPartOrder(candidates : seq, inParts : seq) + { + if |candidates| == 0 then + false + else if CanConstruct(candidates[0].parts, inParts) then + true + else + IsValidPartOrder(candidates[1..], inParts) + } + + // Fail unless it is possible to construct a beacon composed of this sequence of parts + function method ValidatePartOrder(inParts : seq, orig : string) : Result + { + if IsValidPartOrder(construct, inParts) then + Success(true) + else + var msg := + "Compound Beacon value '" + orig + + "' cannot be constructed from any available constructor for " + base.name + + " value parsed as " + PartsToString(inParts) + + " available constructors are " + CListToString(construct) + "."; + Failure(E(msg)) + } + // find the part whose prefix matches this value function method {:tailrecursion} partFromPrefix(p : seq, value : string) : (ret : Result) @@ -221,6 +298,8 @@ module CompoundBeacon { Failure(E("CompoundBeacon " + base.name + " can only be queried as a string, not as " + AttrTypeToStr(value))) else var parts := Split(value.S, split); + var partsUsed :- Seq.MapWithResult(s => getPartFromPrefix(s), parts); + var _ :- ValidatePartOrder(partsUsed, value.S); var beaconParts :- Seq.MapWithResult(s => FindAndCalcPart(s, keys), parts); var lastIsPrefix :- justPrefix(Seq.Last(parts)); if !forEquality && lastIsPrefix then diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy index 385ae4738..5a020226f 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy @@ -157,6 +157,46 @@ module TestBaseBeacon { } + method {:test} TestCompoundQueries() { + var context := ExprContext ( + None, + Some("Mixed = :mixed"), + None, + None + ); + var version := GetLotsaBeacons(); + var src := GetLiteralSource([1,2,3,4,5], version); + var beaconVersion :- expect C.ConvertVersionWithSource(FullTableConfig, version, src); + + context := context.(values := Some(map[":mixed" := DDB.AttributeValue.S("N_MyName.Y_1984")])); + var newContext :- expect Beaconize(beaconVersion, context, DontUseKeyId); + context := context.(values := Some(map[":mixed" := DDB.AttributeValue.S("N_MyName")])); + newContext :- expect Beaconize(beaconVersion, context, DontUseKeyId); + context := context.(values := Some(map[":mixed" := DDB.AttributeValue.S("Y_1984")])); + newContext :- expect Beaconize(beaconVersion, context, DontUseKeyId); + context := context.(values := Some(map[":mixed" := DDB.AttributeValue.S("T_foo")])); + newContext :- expect Beaconize(beaconVersion, context, DontUseKeyId); + context := context.(values := Some(map[":mixed" := DDB.AttributeValue.S("M_bar")])); + newContext :- expect Beaconize(beaconVersion, context, DontUseKeyId); + context := context.(values := Some(map[":mixed" := DDB.AttributeValue.S("T_foo.M_bar")])); + newContext :- expect Beaconize(beaconVersion, context, DontUseKeyId); + + context := context.(values := Some(map[":mixed" := DDB.AttributeValue.S("N_MyName.N_MyName")])); + var badContext := Beaconize(beaconVersion, context, DontUseKeyId); + expect badContext.Failure?; + expect badContext.error == E("Compound Beacon value 'N_MyName.N_MyName' cannot be constructed from any available constructor for Mixed value parsed as N_N_ available constructors are N_Y_, T_[M_]."); + + context := context.(values := Some(map[":mixed" := DDB.AttributeValue.S("Y_1984.N_MyName")])); + badContext := Beaconize(beaconVersion, context, DontUseKeyId); + expect badContext.Failure?; + expect badContext.error == E("Compound Beacon value 'Y_1984.N_MyName' cannot be constructed from any available constructor for Mixed value parsed as Y_N_ available constructors are N_Y_, T_[M_]."); + + context := context.(values := Some(map[":mixed" := DDB.AttributeValue.S("M_bar.T_foo")])); + badContext := Beaconize(beaconVersion, context, DontUseKeyId); + expect badContext.Failure?; + expect badContext.error == E("Compound Beacon value 'M_bar.T_foo' cannot be constructed from any available constructor for Mixed value parsed as M_T_ available constructors are N_Y_, T_[M_]."); + } + method {:test} TestQueryBeacons() { var context := ExprContext ( None, @@ -173,7 +213,7 @@ module TestBaseBeacon { ":NameTitle" := DDB.AttributeValue.S("N_MyName.T_MyTitle"), ":NameTitleN" := DDB.AttributeValue.S("N_MyName"), ":NameTitleT" := DDB.AttributeValue.S("T_MyTitle"), - ":NameTitleTN" := DDB.AttributeValue.S("T_MyTitle.N_MyName"), + ":NameTitleTN" := DDB.AttributeValue.S("N_MyName.T_MyTitle"), ":NameTitleField" := DDB.AttributeValue.S("MyName__mytitle"), ":YearName" := DDB.AttributeValue.S("Y_1984.N_MyName") ]), @@ -187,7 +227,7 @@ module TestBaseBeacon { ":Mixed" := DDB.AttributeValue.S("N_" + Name_beacon + ".Y_1984"), ":Name" := DDB.AttributeValue.S(Name_beacon), ":NameTitle" := DDB.AttributeValue.S("N_" + Name_beacon + ".T_" + Title_beacon), - ":NameTitleTN" := DDB.AttributeValue.S("T_" + Title_beacon + ".N_" + Name_beacon), + ":NameTitleTN" := DDB.AttributeValue.S("N_" + Name_beacon + ".T_" + Title_beacon), ":NameTitleN" := DDB.AttributeValue.S("N_" + Name_beacon), ":NameTitleT" := DDB.AttributeValue.S("T_" + Title_beacon), ":NameTitleField" := DDB.AttributeValue.S(NameTitle_beacon),