chore: add externs for os and language (#1149)

Author: ajewellamz

AwsCryptographicMaterialProviders/Makefile

@@ -27,6 +27,7 @@ RUST_OTHER_FILES := \
 	runtimes/rust/src/hmac.rs \
 	runtimes/rust/src/kms.rs \
 	runtimes/rust/src/local_cmc.rs \
+	runtimes/rust/src/oslang.rs \
 	runtimes/rust/src/random.rs \
 	runtimes/rust/src/rsa.rs \
 	runtimes/rust/src/sets.rs \

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/test/Keyrings/TestMultiKeyring.dfy

@@ -3,6 +3,7 @@
 
 include "../../src/Index.dfy"
 include "../TestUtils.dfy"
+include "../../../../../StandardLibrary/src/Time.dfy"
 
 module TestMultiKeyring {
   import opened Wrappers
@@ -12,6 +13,7 @@ module TestMultiKeyring {
   import AwsCryptographyPrimitivesTypes
   import MaterialProviders
   import Types = AwsCryptographyMaterialProvidersTypes
+  import Time
 
   method getInputEncryptionMaterials(encryptionContext: Types.EncryptionContext) returns (res: Types.EncryptionMaterials) {
 
@@ -47,7 +49,7 @@ module TestMultiKeyring {
 
   method {:test} TestHappyCase()
   {
-
+    var time := Time.GetAbsoluteTime();
     var mpl :- expect MaterialProviders.MaterialProviders();
 
     var encryptionContext := TestUtils.SmallEncryptionContext(TestUtils.SmallEncryptionContextVariation.A);
@@ -99,6 +101,12 @@ module TestMultiKeyring {
     //# (structures.md#encryption-materials) returned by the last OnEncrypt
     //# call.
     expect |encryptionMaterialsOut.materials.encryptedDataKeys| == 2;
+
+    time := Time.PrintTimeSinceShortChained(time);
+    for i := 0 to 100 {
+      encryptionMaterialsOut :- expect multiKeyring.OnEncrypt(Types.OnEncryptInput(materials:=encryptionMaterials));
+    }
+    Time.PrintTimeSinceShort(time);
   }
 
   method {:test} TestChildKeyringFailureEncrypt() {

AwsCryptographicMaterialProviders/runtimes/rust/src/lib.rs

@@ -39,6 +39,7 @@ pub mod ecdsa;
 pub mod hmac;
 pub mod kms;
 pub mod local_cmc;
+pub mod oslang;
 pub mod random;
 pub mod rsa;
 pub mod sets;

AwsCryptographicMaterialProviders/runtimes/rust/src/oslang.rs

@@ -0,0 +1,38 @@
+// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+
+#![deny(warnings, unconditional_panic)]
+#![deny(nonstandard_style)]
+#![deny(clippy::all)]
+#![allow(dead_code)]
+#![allow(non_snake_case)]
+
+impl crate::implementation_from_dafny::OsLang::_default {
+    pub fn GetLanguageShort() -> ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>
+    {
+        dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string("Rust")
+    }
+    pub fn GetLanguageLong() -> ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>
+    {
+        dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string("Rust")
+    }
+    pub fn GetOsShort() -> ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>
+    {
+        let os = match std::env::consts::OS {
+            "macos" => "MacOS",
+            "windows" => "Windows",
+            "openbsd" => "Unix",
+            "linux" => "Unix",
+            "freebsd" => "Unix",
+            "netbsd" => "Unix",
+            _ => "Other"
+        };
+        dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(os)
+    }
+    pub fn GetOsLong() -> ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>
+    {
+        let os = format!("{} {}", std::env::consts::OS, std::env::consts::ARCH);
+        dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&os)
+    }
+                
+}

AwsCryptographyPrimitives/Makefile

@@ -21,6 +21,7 @@ RUST_OTHER_FILES := \
         runtimes/rust/src/ecdh.rs \
         runtimes/rust/src/ecdsa.rs \
         runtimes/rust/src/hmac.rs \
+        runtimes/rust/src/oslang.rs \
         runtimes/rust/src/random.rs \
         runtimes/rust/src/rsa.rs \
         runtimes/rust/src/sets.rs \

AwsCryptographyPrimitives/runtimes/rust/.gitignore

@@ -23,6 +23,7 @@ src/digest.rs
 src/ecdh.rs
 src/ecdsa.rs
 src/hmac.rs
+src/oslang.rs
 src/random.rs
 src/rsa.rs
 src/sets.rs

AwsCryptographyPrimitives/runtimes/rust/copy_externs.sh

@@ -12,6 +12,7 @@ cp $SRC/digest.rs src
 cp $SRC/ecdh.rs src
 cp $SRC/ecdsa.rs src
 cp $SRC/hmac.rs src
+cp $SRC/oslang.rs src
 cp $SRC/random.rs src
 cp $SRC/rsa.rs src
 cp $SRC/sets.rs src

AwsCryptographyPrimitives/runtimes/rust/src/lib.rs

@@ -27,6 +27,7 @@ pub mod digest;
 pub mod ecdh;
 pub mod ecdsa;
 pub mod hmac;
+pub mod oslang;
 pub mod random;
 pub mod rsa;
 pub mod sets;

ComAmazonawsDynamodb/Makefile

@@ -16,6 +16,7 @@ RUST_OTHER_FILES := \
         runtimes/rust/src/concurrent_call.rs \
         runtimes/rust/src/dafny_libraries.rs \
         runtimes/rust/src/ddb.rs \
+        runtimes/rust/src/oslang.rs \
         runtimes/rust/src/sets.rs \
         runtimes/rust/src/time.rs \
         runtimes/rust/src/uuid.rs

ComAmazonawsDynamodb/runtimes/rust/.gitignore

@@ -7,6 +7,7 @@ src/dafny_libraries.rs
 src/deps.rs
 src/implementation_from_dafny.rs
 src/sets.rs
+src/oslang.rs
 src/standard_library_conversions.rs
 src/standard_library_externs.rs
 src/time.rs