Skip to content

Commit c66f268

Browse files
alex-chewShubham Chaturvedi
authored and
Shubham Chaturvedi
committed
feat: Rust codegen for Constraints (#582)
*Issue #, if available:* #533 *Description of changes:* This PR implements Rust library codegen for input validation of supported constraint traits (`@required`, `@length`, `@range`). Notes: * Unlike in Java and C#, library users may directly construct the generated operation input structures in Rust (in order to aid in idiomatic usage, especially w.r.t. pattern matching, like the AWS SDK for Rust does) and are not restricted to using the builder pattern. Therefore, the builder can't take sole responsibility for validation; instead, validation happens whenever an operation is called. * Unlike other target languages, Rust is limited in its ability to propagate arbitrary errors up the call stack unless the API is designed for doing so. Our models don't define a specific error shape for validation, so in order to represent validation errors in the generated `Error` enum, we generate a `ValidationError` variant that only exists on the Rust side. When converting to Dafny, we upcast the error into the `Opaque` variant; when converting from Dafny, we downcast it back after checking that doing so is safe using `dafny_runtime::is_object!`. * By Polymorph's design, values crossing the boundary from Dafny-compiled code are assumed to be "valid", but the `WrappedSimpleConstraintsTest` intentionally breaks this assumption in order to test the constraint validation logic, forcing invalid values across the boundary by (ab)using `{:axiom}`. This would be okay except that the Dafny tests in the Constraints test model *also* pass across malformed UTF-8 for `@DafnyUtf8Bytes` strings (which is not a constraint trait). The Rust type conversion process does not allow for failure when converting values from Dafny (doing so would be a major refactor and probably some performance impact), so I've isolated the malformed UTF-8 test assertions and used a bit of `sed` to simply disable them for Rust specifically, while allowing the other languages to continue testing them.
1 parent d97d83f commit c66f268

40 files changed

+3162
-50
lines changed

TestModels/Constraints/Makefile

Lines changed: 15 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,8 @@ CORES=2
55

66
ENABLE_EXTERN_PROCESSING=1
77

8+
TRANSPILE_TESTS_IN_RUST=1
9+
810
include ../SharedMakefile.mk
911

1012
PROJECT_SERVICES := \
@@ -24,13 +26,19 @@ TRANSLATION_RECORD_GO := \
2426
# This project has no dependencies
2527
# DEPENDENT-MODELS:=
2628

27-
# First, export DAFNY_VERSION=4.2
28-
# Three separate items, because 'make polymorph_code_gen' doesn't quite work
29-
polymorph:
30-
npm i --no-save prettier@3 prettier-plugin-java@2.5
31-
make polymorph_dafny
32-
make polymorph_java
33-
make polymorph_dotnet
29+
clean: _clean
30+
rm -rf $(LIBRARY_ROOT)/runtimes/java/src/main/dafny-generated
31+
rm -rf $(LIBRARY_ROOT)/runtimes/java/src/main/smithy-generated
32+
rm -rf $(LIBRARY_ROOT)/runtimes/java/src/test/dafny-generated
33+
34+
# Patch out tests that Rust codegen doesn't support
35+
transpile_rust: | transpile_implementation_rust transpile_dependencies_rust remove_unsupported_rust_tests
36+
37+
remove_unsupported_rust_tests:
38+
$(MAKE) _sed_file \
39+
SED_FILE_PATH=$(LIBRARY_ROOT)/runtimes/rust/src/implementation_from_dafny.rs \
40+
SED_BEFORE_STRING='let mut allowBadUtf8BytesFromDafny: bool = true' \
41+
SED_AFTER_STRING='let mut allowBadUtf8BytesFromDafny: bool = false'
3442

3543
# Python
3644

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
[package]
2+
name = "simple_constraints"
3+
version = "0.1.0"
4+
edition = "2021"
5+
6+
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
7+
8+
[features]
9+
wrapped-client = []
10+
11+
[dependencies]
12+
aws-smithy-runtime = {version = "1.7.1", features=["client"]}
13+
aws-smithy-runtime-api = {version = "1.7.2", features=["client"]}
14+
aws-smithy-types = "1.2.4"
15+
dafny_runtime = { path = "../../../dafny-dependencies/dafny_runtime_rust"}
16+
17+
[dependencies.tokio]
18+
version = "1.26.0"
19+
features = ["full"]
20+
21+
[dev-dependencies]
22+
simple_constraints = { path = ".", features = ["wrapped-client"] }
23+
24+
[lib]
25+
path = "src/implementation_from_dafny.rs"
Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
1+
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0
3+
// Do not modify this file. This file is machine generated, and any changes to it will be overwritten.
4+
use aws_smithy_types::error::operation::BuildError;
5+
6+
#[derive(::std::clone::Clone, ::std::fmt::Debug, ::std::cmp::PartialEq)]
7+
pub struct Client {
8+
pub(crate) dafny_client: ::dafny_runtime::Object<dyn crate::r#simple::constraints::internaldafny::types::ISimpleConstraintsClient>
9+
}
10+
11+
impl Client {
12+
/// Creates a new client from the service [`Config`](crate::Config).
13+
#[track_caller]
14+
pub fn from_conf(
15+
conf: crate::types::simple_constraints_config::SimpleConstraintsConfig,
16+
) -> Result<Self, BuildError> {
17+
let inner =
18+
crate::simple::constraints::internaldafny::_default::SimpleConstraints(
19+
&crate::conversions::simple_constraints_config::_simple_constraints_config::to_dafny(conf),
20+
);
21+
if matches!(
22+
inner.as_ref(),
23+
crate::_Wrappers_Compile::Result::Failure { .. }
24+
) {
25+
// TODO: convert error - the potential types are not modeled!
26+
return Err(BuildError::other(
27+
::aws_smithy_types::error::metadata::ErrorMetadata::builder()
28+
.message("Invalid client config")
29+
.build(),
30+
));
31+
}
32+
Ok(Self {
33+
dafny_client: ::dafny_runtime::upcast_object()(inner.Extract())
34+
})
35+
}
36+
}
37+
38+
mod get_constraints;
Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,49 @@
1+
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0
3+
// Do not modify this file. This file is machine generated, and any changes to it will be overwritten.
4+
impl crate::client::Client {
5+
/// Constructs a fluent builder for the [`GetConstraints`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder) operation.
6+
///
7+
/// - The fluent builder is configurable:
8+
/// - [`blob_less_than_or_equal_to_ten(impl Into<Option<::aws_smithy_types::Blob>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::blob_less_than_or_equal_to_ten) / [`set_blob_less_than_or_equal_to_ten(Option<::aws_smithy_types::Blob>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::set_blob_less_than_or_equal_to_ten): (undocumented)<br>
9+
/// - [`greater_than_one(impl Into<Option<::std::primitive::i32>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::greater_than_one) / [`set_greater_than_one(Option<::std::primitive::i32>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::set_greater_than_one): (undocumented)<br>
10+
/// - [`less_than_ten(impl Into<Option<::std::primitive::i32>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::less_than_ten) / [`set_less_than_ten(Option<::std::primitive::i32>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::set_less_than_ten): (undocumented)<br>
11+
/// - [`list_less_than_or_equal_to_ten(impl Into<Option<::std::vec::Vec<::std::string::String>>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::list_less_than_or_equal_to_ten) / [`set_list_less_than_or_equal_to_ten(Option<::std::vec::Vec<::std::string::String>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::set_list_less_than_or_equal_to_ten): (undocumented)<br>
12+
/// - [`map_less_than_or_equal_to_ten(impl Into<Option<::std::collections::HashMap<::std::string::String, ::std::string::String>>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::map_less_than_or_equal_to_ten) / [`set_map_less_than_or_equal_to_ten(Option<::std::collections::HashMap<::std::string::String, ::std::string::String>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::set_map_less_than_or_equal_to_ten): (undocumented)<br>
13+
/// - [`my_blob(impl Into<Option<::aws_smithy_types::Blob>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::my_blob) / [`set_my_blob(Option<::aws_smithy_types::Blob>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::set_my_blob): (undocumented)<br>
14+
/// - [`my_list(impl Into<Option<::std::vec::Vec<::std::string::String>>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::my_list) / [`set_my_list(Option<::std::vec::Vec<::std::string::String>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::set_my_list): (undocumented)<br>
15+
/// - [`my_list_of_utf8_bytes(impl Into<Option<::std::vec::Vec<::std::string::String>>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::my_list_of_utf8_bytes) / [`set_my_list_of_utf8_bytes(Option<::std::vec::Vec<::std::string::String>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::set_my_list_of_utf8_bytes): (undocumented)<br>
16+
/// - [`my_map(impl Into<Option<::std::collections::HashMap<::std::string::String, ::std::string::String>>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::my_map) / [`set_my_map(Option<::std::collections::HashMap<::std::string::String, ::std::string::String>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::set_my_map): (undocumented)<br>
17+
/// - [`my_string(impl Into<Option<::std::string::String>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::my_string) / [`set_my_string(Option<::std::string::String>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::set_my_string): (undocumented)<br>
18+
/// - [`my_utf8_bytes(impl Into<Option<::std::string::String>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::my_utf8_bytes) / [`set_my_utf8_bytes(Option<::std::string::String>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::set_my_utf8_bytes): (undocumented)<br>
19+
/// - [`non_empty_blob(impl Into<Option<::aws_smithy_types::Blob>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::non_empty_blob) / [`set_non_empty_blob(Option<::aws_smithy_types::Blob>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::set_non_empty_blob): (undocumented)<br>
20+
/// - [`non_empty_list(impl Into<Option<::std::vec::Vec<::std::string::String>>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::non_empty_list) / [`set_non_empty_list(Option<::std::vec::Vec<::std::string::String>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::set_non_empty_list): (undocumented)<br>
21+
/// - [`non_empty_map(impl Into<Option<::std::collections::HashMap<::std::string::String, ::std::string::String>>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::non_empty_map) / [`set_non_empty_map(Option<::std::collections::HashMap<::std::string::String, ::std::string::String>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::set_non_empty_map): (undocumented)<br>
22+
/// - [`non_empty_string(impl Into<Option<::std::string::String>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::non_empty_string) / [`set_non_empty_string(Option<::std::string::String>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::set_non_empty_string): (undocumented)<br>
23+
/// - [`one_to_ten(impl Into<Option<::std::primitive::i32>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::one_to_ten) / [`set_one_to_ten(Option<::std::primitive::i32>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::set_one_to_ten): (undocumented)<br>
24+
/// - [`string_less_than_or_equal_to_ten(impl Into<Option<::std::string::String>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::string_less_than_or_equal_to_ten) / [`set_string_less_than_or_equal_to_ten(Option<::std::string::String>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::set_string_less_than_or_equal_to_ten): (undocumented)<br>
25+
/// - [`my_ten_to_ten(impl Into<Option<::std::primitive::i64>>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::my_ten_to_ten) / [`set_my_ten_to_ten(Option<::std::primitive::i64>)`](crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::set_my_ten_to_ten): (undocumented)<br>
26+
/// - On success, responds with [`GetConstraintsOutput`](crate::operation::get_constraints::GetConstraintsOutput) with field(s):
27+
/// - [`blob_less_than_or_equal_to_ten(Option<::aws_smithy_types::Blob>)`](crate::operation::get_constraints::GetConstraintsOutput::blob_less_than_or_equal_to_ten): (undocumented)
28+
/// - [`greater_than_one(Option<::std::primitive::i32>)`](crate::operation::get_constraints::GetConstraintsOutput::greater_than_one): (undocumented)
29+
/// - [`less_than_ten(Option<::std::primitive::i32>)`](crate::operation::get_constraints::GetConstraintsOutput::less_than_ten): (undocumented)
30+
/// - [`list_less_than_or_equal_to_ten(Option<::std::vec::Vec<::std::string::String>>)`](crate::operation::get_constraints::GetConstraintsOutput::list_less_than_or_equal_to_ten): (undocumented)
31+
/// - [`map_less_than_or_equal_to_ten(Option<::std::collections::HashMap<::std::string::String, ::std::string::String>>)`](crate::operation::get_constraints::GetConstraintsOutput::map_less_than_or_equal_to_ten): (undocumented)
32+
/// - [`my_blob(Option<::aws_smithy_types::Blob>)`](crate::operation::get_constraints::GetConstraintsOutput::my_blob): (undocumented)
33+
/// - [`my_list(Option<::std::vec::Vec<::std::string::String>>)`](crate::operation::get_constraints::GetConstraintsOutput::my_list): (undocumented)
34+
/// - [`my_list_of_utf8_bytes(Option<::std::vec::Vec<::std::string::String>>)`](crate::operation::get_constraints::GetConstraintsOutput::my_list_of_utf8_bytes): (undocumented)
35+
/// - [`my_map(Option<::std::collections::HashMap<::std::string::String, ::std::string::String>>)`](crate::operation::get_constraints::GetConstraintsOutput::my_map): (undocumented)
36+
/// - [`my_string(Option<::std::string::String>)`](crate::operation::get_constraints::GetConstraintsOutput::my_string): (undocumented)
37+
/// - [`my_utf8_bytes(Option<::std::string::String>)`](crate::operation::get_constraints::GetConstraintsOutput::my_utf8_bytes): (undocumented)
38+
/// - [`non_empty_blob(Option<::aws_smithy_types::Blob>)`](crate::operation::get_constraints::GetConstraintsOutput::non_empty_blob): (undocumented)
39+
/// - [`non_empty_list(Option<::std::vec::Vec<::std::string::String>>)`](crate::operation::get_constraints::GetConstraintsOutput::non_empty_list): (undocumented)
40+
/// - [`non_empty_map(Option<::std::collections::HashMap<::std::string::String, ::std::string::String>>)`](crate::operation::get_constraints::GetConstraintsOutput::non_empty_map): (undocumented)
41+
/// - [`non_empty_string(Option<::std::string::String>)`](crate::operation::get_constraints::GetConstraintsOutput::non_empty_string): (undocumented)
42+
/// - [`one_to_ten(Option<::std::primitive::i32>)`](crate::operation::get_constraints::GetConstraintsOutput::one_to_ten): (undocumented)
43+
/// - [`string_less_than_or_equal_to_ten(Option<::std::string::String>)`](crate::operation::get_constraints::GetConstraintsOutput::string_less_than_or_equal_to_ten): (undocumented)
44+
/// - [`that_ten_to_ten(Option<::std::primitive::i64>)`](crate::operation::get_constraints::GetConstraintsOutput::that_ten_to_ten): (undocumented)
45+
/// - On failure, responds with [`SdkError<GetConstraintsError>`](crate::operation::get_constraints::GetConstraintsError)
46+
pub fn get_constraints(&self) -> crate::operation::get_constraints::builders::GetConstraintsFluentBuilder {
47+
crate::operation::get_constraints::builders::GetConstraintsFluentBuilder::new(self.clone())
48+
}
49+
}
Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0
3+
// Do not modify this file. This file is machine generated, and any changes to it will be overwritten.
4+
pub mod client;
5+
6+
pub mod error;
7+
8+
pub mod get_constraints;
9+
10+
pub mod simple_constraints_config;
Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0
3+
// Do not modify this file. This file is machine generated, and any changes to it will be overwritten.
4+
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
5+
// SPDX-License-Identifier: Apache-2.0
6+
// Do not modify this file. This file is machine generated, and any changes to it will be overwritten.
7+
#[allow(dead_code)]
8+
9+
pub fn to_dafny(
10+
value: &crate::client::Client,
11+
) ->
12+
::dafny_runtime::Object<dyn crate::r#simple::constraints::internaldafny::types::ISimpleConstraintsClient>
13+
{
14+
value.dafny_client.clone()
15+
}
16+
17+
#[allow(dead_code)]
18+
pub fn from_dafny(
19+
dafny_value: ::dafny_runtime::Object<
20+
dyn crate::r#simple::constraints::internaldafny::types::ISimpleConstraintsClient
21+
>,
22+
) -> crate::client::Client {
23+
crate::client::Client { dafny_client: dafny_value }
24+
}
Lines changed: 99 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,99 @@
1+
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0
3+
// Do not modify this file. This file is machine generated, and any changes to it will be overwritten.
4+
/// Wraps up an arbitrary Rust Error value as a Dafny Error
5+
pub fn to_opaque_error<E: 'static>(value: E) ->
6+
::std::rc::Rc<crate::r#simple::constraints::internaldafny::types::Error>
7+
{
8+
let error_obj: ::dafny_runtime::Object<dyn::std::any::Any> = ::dafny_runtime::Object(Some(
9+
::std::rc::Rc::new(::std::cell::UnsafeCell::new(value)),
10+
));
11+
::std::rc::Rc::new(
12+
crate::r#simple::constraints::internaldafny::types::Error::Opaque {
13+
obj: error_obj,
14+
},
15+
)
16+
}
17+
18+
/// Wraps up an arbitrary Rust Error value as a Dafny Result<T, Error>.Failure
19+
pub fn to_opaque_error_result<T: ::dafny_runtime::DafnyType, E: 'static>(value: E) ->
20+
::std::rc::Rc<
21+
crate::_Wrappers_Compile::Result<
22+
T,
23+
::std::rc::Rc<crate::r#simple::constraints::internaldafny::types::Error>
24+
>
25+
>
26+
{
27+
::std::rc::Rc::new(crate::_Wrappers_Compile::Result::Failure {
28+
error: to_opaque_error(value),
29+
})
30+
}
31+
pub fn to_dafny(
32+
value: crate::types::error::Error,
33+
) -> ::std::rc::Rc<crate::r#simple::constraints::internaldafny::types::Error> {
34+
::std::rc::Rc::new(match value {
35+
crate::types::error::Error::SimpleConstraintsException { message } =>
36+
crate::r#simple::constraints::internaldafny::types::Error::SimpleConstraintsException {
37+
message: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&message),
38+
},
39+
crate::types::error::Error::CollectionOfErrors { list, message } =>
40+
crate::r#simple::constraints::internaldafny::types::Error::CollectionOfErrors {
41+
message: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&message),
42+
list: ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(&list, |e| to_dafny(e.clone()))
43+
},
44+
crate::types::error::Error::ValidationError(inner) =>
45+
crate::r#simple::constraints::internaldafny::types::Error::Opaque {
46+
obj: {
47+
let rc = ::std::rc::Rc::new(inner) as ::std::rc::Rc<dyn ::std::any::Any>;
48+
// safety: `rc` is new, ensuring it has refcount 1 and is uniquely owned.
49+
// we should use `dafny_runtime_conversions::rc_struct_to_dafny_class` once it
50+
// accepts unsized types (https://github.com/dafny-lang/dafny/pull/5769)
51+
unsafe { ::dafny_runtime::Object::from_rc(rc) }
52+
},
53+
},
54+
crate::types::error::Error::Opaque { obj } =>
55+
crate::r#simple::constraints::internaldafny::types::Error::Opaque {
56+
obj: ::dafny_runtime::Object(obj.0)
57+
},
58+
})
59+
}
60+
61+
#[allow(dead_code)]
62+
pub fn from_dafny(
63+
dafny_value: ::std::rc::Rc<
64+
crate::r#simple::constraints::internaldafny::types::Error,
65+
>,
66+
) -> crate::types::error::Error {
67+
match ::std::borrow::Borrow::borrow(&dafny_value) {
68+
crate::r#simple::constraints::internaldafny::types::Error::SimpleConstraintsException { message } =>
69+
crate::types::error::Error::SimpleConstraintsException {
70+
message: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(&message),
71+
},
72+
crate::r#simple::constraints::internaldafny::types::Error::CollectionOfErrors { list, message } =>
73+
crate::types::error::Error::CollectionOfErrors {
74+
message: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(&message),
75+
list: ::dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(&list, |e| from_dafny(e.clone()))
76+
},
77+
crate::r#simple::constraints::internaldafny::types::Error::Opaque { obj } =>
78+
crate::types::error::Error::Opaque {
79+
obj: obj.clone()
80+
},
81+
crate::r#simple::constraints::internaldafny::types::Error::Opaque { obj } =>
82+
{
83+
use ::std::any::Any;
84+
if ::dafny_runtime::is_object!(obj, crate::types::error::ValidationError) {
85+
let typed = ::dafny_runtime::cast_object!(obj.clone(), crate::types::error::ValidationError);
86+
crate::types::error::Error::ValidationError(
87+
// safety: dafny_class_to_struct will increment ValidationError's Rc
88+
unsafe {
89+
::dafny_runtime::dafny_runtime_conversions::object::dafny_class_to_struct(typed)
90+
}
91+
)
92+
} else {
93+
crate::types::error::Error::Opaque {
94+
obj: obj.clone()
95+
}
96+
}
97+
},
98+
}
99+
}

0 commit comments

Comments
 (0)