Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

chore(TestModels): Add constraints inside list, map and union #485

Draft
wants to merge 13 commits into
base: main-1.x
Choose a base branch
from
Draft

chore(TestModels): Add constraints inside list, map and union #485

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
7f2d7cc
Add files to test constraints in container shapes
rishav-karanjit Jul 23, 2024
0b6f104
Pushing runtime to debug
rishav-karanjit Jul 23, 2024
ac04b6f
Push some more runtime
rishav-karanjit Jul 23, 2024
50e43e2
Revert "Push some more runtime"
rishav-karanjit Jul 23, 2024
5e0fedb
Revert "Pushing runtime to debug"
rishav-karanjit Jul 23, 2024
3fb9994
Change success to failure
rishav-karanjit Jul 23, 2024
5ed43b5
Update list and map with constraint
rishav-karanjit Jul 25, 2024
0ba698e
Add length trait to map
rishav-karanjit Jul 25, 2024
e3b91ba
Some fix
rishav-karanjit Jul 25, 2024
9a734f8
Add union with contraint
rishav-karanjit Jul 25, 2024
245b138
Revert back union test model changes
rishav-karanjit Jul 25, 2024
01a0b47
Add MyUnionWithConstraint
rishav-karanjit Jul 25, 2024
e2a5293
Some fix
rishav-karanjit Jul 25, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
22 changes: 22 additions & 0 deletions TestModels/Constraints/Model/Constraints.smithy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -96,6 +96,11 @@ list ListLessThanOrEqualToTen {
member: String
}

@length(min: 1, max: 10)
list ListWithConstraint {
member: MyString
Copy link
Member Author

@rishav-karanjit rishav-karanjit Aug 12, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Self commenting a note posterity:
MyString has constraint @length(min: 1, max: 10)

Other aggregate shapes that was added also has similar constraint

}

@length(min: 1, max: 10)
map MyMap {
key: String,
Expand All @@ -114,6 +119,12 @@ map MapLessThanOrEqualToTen {
value: String,
}

@length(min: 1, max: 10)
map MapWithConstraint {
key: MyString,
value: MyString,
}

// we don't do patterns yet
// @pattern("^[A-Za-z]+$")
// string Alphabetic
Expand Down Expand Up @@ -156,9 +167,11 @@ structure GetConstraintsInput {
MyList: MyList,
NonEmptyList: NonEmptyList,
ListLessThanOrEqualToTen: ListLessThanOrEqualToTen,
ListWithConstraint: ListWithConstraint,
MyMap: MyMap,
NonEmptyMap: NonEmptyMap,
MapLessThanOrEqualToTen: MapLessThanOrEqualToTen,
MapWithConstraint : MapWithConstraint,
// Alphabetic: Alphabetic,
OneToTen: OneToTen,
myTenToTen: TenToTen,
Expand All @@ -168,6 +181,7 @@ structure GetConstraintsInput {
// MyComplexUniqueList: MyComplexUniqueList,
MyUtf8Bytes: Utf8Bytes,
MyListOfUtf8Bytes: ListOfUtf8Bytes,
MyUnionWithConstraint: UnionWithConstraint
}

structure GetConstraintsOutput {
Expand All @@ -180,9 +194,11 @@ structure GetConstraintsOutput {
MyList: MyList,
NonEmptyList: NonEmptyList,
ListLessThanOrEqualToTen: ListLessThanOrEqualToTen,
ListWithConstraint: ListWithConstraint,
MyMap: MyMap,
NonEmptyMap: NonEmptyMap,
MapLessThanOrEqualToTen: MapLessThanOrEqualToTen,
MapWithConstraint : MapWithConstraint,
// Alphabetic: Alphabetic,
OneToTen: OneToTen,
thatTenToTen: TenToTen,
Expand All @@ -192,6 +208,12 @@ structure GetConstraintsOutput {
// MyComplexUniqueList: MyComplexUniqueList,
MyUtf8Bytes: Utf8Bytes,
MyListOfUtf8Bytes: ListOfUtf8Bytes,
MyUnionWithConstraint: UnionWithConstraint
}

union UnionWithConstraint {
IntegerValue: OneToTen,
StringValue: MyString
}

// See Comment in traits.smithy
Expand Down
5 changes: 4 additions & 1 deletion TestModels/Constraints/src/SimpleConstraintsImpl.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,17 +25,20 @@ module SimpleConstraintsImpl refines AbstractSimpleConstraintsOperations {
MyList := input.MyList,
NonEmptyList := input.NonEmptyList,
ListLessThanOrEqualToTen := input.ListLessThanOrEqualToTen,
ListWithConstraint := input.ListWithConstraint,
MyMap := input.MyMap,
NonEmptyMap := input.NonEmptyMap,
MapLessThanOrEqualToTen := input.MapLessThanOrEqualToTen,
MapWithConstraint := input.MapWithConstraint,
// Alphabetic := input.Alphabetic,
OneToTen := input.OneToTen,
GreaterThanOne := input.GreaterThanOne,
LessThanTen := input.LessThanTen,
// MyUniqueList := input.MyUniqueList,
// MyComplexUniqueList := input.MyComplexUniqueList,
MyUtf8Bytes := input.MyUtf8Bytes,
MyListOfUtf8Bytes := input.MyListOfUtf8Bytes
MyListOfUtf8Bytes := input.MyListOfUtf8Bytes,
MyUnionWithConstraint := input.MyUnionWithConstraint
);

return Success(res);
Expand Down
19 changes: 18 additions & 1 deletion TestModels/Constraints/test/Helpers.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,9 +33,11 @@ module Helpers {
MyList := Some(["00", "11"]),
NonEmptyList := Some(["00", "11"]),
ListLessThanOrEqualToTen := Some(["00", "11"]),
ListWithConstraint := Some(["0", "123", "MaxTenChar"]),
MyMap := Some(map["0" := "1", "2" := "3"]),
NonEmptyMap := Some(map["0" := "1", "2" := "3"]),
MapLessThanOrEqualToTen := Some(map["0" := "1", "2" := "3"]),
MapWithConstraint := Some(map["0" := "1", "123" := "345", "MaxTenChar" := "0123456789"]),
// Alphabetic := Some("alphabetic"),
OneToTen := Some(3),
myTenToTen := Some(3),
Expand All @@ -44,7 +46,8 @@ module Helpers {
// MyUniqueList := Some(["one", "two"]),
// MyComplexUniqueList := Some(myComplexUniqueList),
MyUtf8Bytes := Some(PROVIDER_ID),
MyListOfUtf8Bytes := Some([PROVIDER_ID, PROVIDER_ID])
MyListOfUtf8Bytes := Some([PROVIDER_ID, PROVIDER_ID]),
MyUnionWithConstraint := Some(IntegerValue(1))
)
}

Expand Down Expand Up @@ -163,6 +166,13 @@ module Helpers {
myListLessThanOrEqualToTen
}

function method ForceListWithConstraint(value : seq<string> ) : ListWithConstraint
{
assume {:axiom} IsValid_ListWithConstraint(value);
var myListWithConstraint: ListWithConstraint := value;
myListWithConstraint
}

function method ForceMyMap(value : map<string, string>) : MyMap
{
assume {:axiom} IsValid_MyMap(value);
Expand All @@ -184,6 +194,13 @@ module Helpers {
myMapLessThanOrEqualToTen
}

function method ForceMapWithConstraint(value : map<string, string> ) : MapWithConstraint
{
assume {:axiom} IsValid_MapWithConstraint(value);
var myMapWithConstraint: MapWithConstraint := value;
myMapWithConstraint
}

function method ForceGreaterThanOne(value : int) : GreaterThanOne
{
assume {:axiom} ValidInt32(value);
Expand Down
82 changes: 81 additions & 1 deletion TestModels/Constraints/test/WrappedSimpleConstraintsTest.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,12 +25,15 @@ module WrappedSimpleConstraintsTest {
TestGetConstraintWithMyList(client);
TestGetConstraintWithNonEmptyList(client);
TestGetConstraintWithListLessThanOrEqualToTen(client);
TestGetConstraintWithListWithConstraint(client);
TestGetConstraintWithMyMap(client);
TestGetConstraintWithNonEmptyMap(client);
TestGetConstraintWithMapLessThanOrEqualToTen(client);
TestGetConstraintWithMapWithConstraint(client);
TestGetConstraintWithGreaterThanOne(client);
TestGetConstraintWithUtf8Bytes(client);
TestGetConstraintWithListOfUtf8Bytes(client);
TestGetConstraintWithMyUnionWithConstraint(client);
}

method TestGetConstraintWithValidInputs(client: ISimpleConstraintsClient)
Expand Down Expand Up @@ -367,6 +370,25 @@ module WrappedSimpleConstraintsTest {
expect ret.Failure?;
}

method TestGetConstraintWithListWithConstraint(client: ISimpleConstraintsClient)
requires client.ValidState()
modifies client.Modifies
ensures client.ValidState()
{
var input := GetValidInput();
input := input.(ListWithConstraint := Some(ForceListWithConstraint(["1"])));
var ret := client.GetConstraints(input := input);
expect ret.Success?;

input := input.(ListWithConstraint := Some(ForceListWithConstraint(["0", "1", "0123456789"])));
ret := client.GetConstraints(input := input);
expect ret.Success?;

input := input.(ListWithConstraint := Some(ForceListWithConstraint(["0", "1", "MoreThen10Character"])));
ret := client.GetConstraints(input := input);
expect ret.Failure?;
}

// @length(min: 1, max: 10)
method TestGetConstraintWithMyMap(client: ISimpleConstraintsClient)
requires client.ValidState()
Expand Down Expand Up @@ -402,7 +424,7 @@ module WrappedSimpleConstraintsTest {
var ret := client.GetConstraints(input := input);
expect ret.Failure?;

input := input.(NonEmptyMap := Some(ForceNonEmptyMap(map["1" := "a"])));
input := input.(NonEmptyMap := Some(ForceNonEmptyMap(map["01234567890" := "a"])));
ret := client.GetConstraints(input := input);
expect ret.Success?;

Expand Down Expand Up @@ -439,6 +461,25 @@ module WrappedSimpleConstraintsTest {
expect ret.Failure?;
}

method TestGetConstraintWithMapWithConstraint(client: ISimpleConstraintsClient)
requires client.ValidState()
modifies client.Modifies
ensures client.ValidState()
{
var input := GetValidInput();
input := input.(MapWithConstraint := Some(ForceMapWithConstraint(map["1" := "a"])));
var ret := client.GetConstraints(input := input);
expect ret.Success?;

input := input.(MapWithConstraint := Some(ForceMapWithConstraint(map["0123456789" := "a", "b" := "abcdefghij", "IamAtTenCh" := "Metooooooo"])));
ret := client.GetConstraints(input := input);
expect ret.Success?;

input := input.(MapWithConstraint := Some(ForceMapWithConstraint(map["0123456789012" := "a", "b" := "abcdefghijklm", "IamAtMoreThenTenCh" := "Metooooooooooo"])));
ret := client.GetConstraints(input := input);
expect ret.Failure?;
}

// @range(min: 1)
method TestGetConstraintWithGreaterThanOne(client: ISimpleConstraintsClient)
requires client.ValidState()
Expand Down Expand Up @@ -565,4 +606,43 @@ module WrappedSimpleConstraintsTest {
ret := client.GetConstraints(input := input);
expect ret.Failure?;
}

method TestGetConstraintWithMyUnionWithConstraint(client: ISimpleConstraintsClient)
requires client.ValidState()
modifies client.Modifies
ensures client.ValidState()
{
var input := GetValidInput();
input := input.(MyUnionWithConstraint := Some(IntegerValue(0)));
var ret := client.GetConstraints(input := input);
expect ret.Success?;

input := input.(MyUnionWithConstraint := Some(IntegerValue(5)));
ret := client.GetConstraints(input := input);
expect ret.Success?;

input := input.(MyUnionWithConstraint := Some(IntegerValue(10)));
ret := client.GetConstraints(input := input);
expect ret.Success?;

input := input.(MyUnionWithConstraint := Some(StringValue("0")));
ret := client.GetConstraints(input := input);
expect ret.Success?;

input := input.(MyUnionWithConstraint := Some(StringValue("IamAtTenCh")));
ret := client.GetConstraints(input := input);
expect ret.Success?;

input := input.(MyUnionWithConstraint := Some(IntegerValue(1000)));
ret := client.GetConstraints(input := input);
expect ret.Failure?;

input := input.(MyUnionWithConstraint := Some(IntegerValue(-1000)));
ret := client.GetConstraints(input := input);
expect ret.Failure?;

input := input.(MyUnionWithConstraint := Some(StringValue("MoreThen10Character")));
ret := client.GetConstraints(input := input);
expect ret.Failure?;
}
}
2 changes: 1 addition & 1 deletion TestModels/Union/test/SimpleUnionImplTest.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,4 +50,4 @@ module SimpleUnionImplTest {
expect ret.union.value.Value?;
expect ret.union.value.Value == 10;
}
}
}
Loading