From 91af3ed11166bc8f06c791d62c86a408926c3d5a Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Tue, 2 Apr 2024 10:55:01 -0700 Subject: [PATCH 1/2] chore: add example of tail recursion --- .../src/ParseJsonManifests.dfy | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) diff --git a/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/ParseJsonManifests.dfy b/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/ParseJsonManifests.dfy index e676e2109..e3ea0ffc1 100644 --- a/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/ParseJsonManifests.dfy +++ b/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/ParseJsonManifests.dfy @@ -41,8 +41,23 @@ module {:options "-functionSyntax:4"} ParseJsonManifests { } by method { // This function ideally would be`{:tailrecursion}` - // but it is not simple to here is a method - // so that it does not explode with huge numbers of tests. + // immediately below is an example of how to make it tail recursive + // However, we're leaving this as "by method" to provide an example of how to do that + + // function {:tailrecursion} BuildEncryptTestVector2( + // keys: KeyVectors.KeyVectorsClient, + // obj: seq<(string, JSON)>, + // acc : seq := [] + // ) + // : Result, string> + // { + // if |obj| == 0 then + // Success(acc) + // else + // var encryptVector :- ToEncryptTestVector(keys, obj[0].0, obj[0].1); + // BuildEncryptTestVector2(keys, obj[1..], acc + [encryptVector]) + // } + var i: nat := |obj|; var vectors := []; From f511db08ce2cb9a01b49715a91289e037887bbfd Mon Sep 17 00:00:00 2001 From: Andrew Jewell <107044381+ajewellamz@users.noreply.github.com> Date: Tue, 2 Apr 2024 16:32:32 -0400 Subject: [PATCH 2/2] Update TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/ParseJsonManifests.dfy Co-authored-by: seebees --- .../src/ParseJsonManifests.dfy | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/ParseJsonManifests.dfy b/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/ParseJsonManifests.dfy index e3ea0ffc1..0c30ef191 100644 --- a/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/ParseJsonManifests.dfy +++ b/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/ParseJsonManifests.dfy @@ -41,8 +41,10 @@ module {:options "-functionSyntax:4"} ParseJsonManifests { } by method { // This function ideally would be`{:tailrecursion}` - // immediately below is an example of how to make it tail recursive - // However, we're leaving this as "by method" to provide an example of how to do that + // at the time this did not seem simple. + // Here is an example of how to make it tail recursive that may work. + // However, we're leaving this as "by method" + // to avoid changing anything and to provide an example of how to do that // function {:tailrecursion} BuildEncryptTestVector2( // keys: KeyVectors.KeyVectorsClient,