kata-containers/regorus
1
0
Fork 0
mirror of https://github.com/microsoft/regorus.git synced 2026-08-05 02:16:11 +00:00
Code Issues Packages Projects Releases Wiki Activity

Progress to cargo build success

Browse Source
This commit is contained in:
Jay Lorch
2026-03-03 16:35:05 -08:00
parent 1f2a2ecb41
commit 90894aa8e1
2 changed files with 9 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

8
src/number.rs
View File

@@ -37,6 +37,7 @@ use vstd::std_specs::cmp::*;
use crate::*;
#[cfg(verus_keep_ghost)]
use crate::verusspec::bigint::*;
use crate::verusspec::float::*;
@@ -335,6 +336,7 @@ impl Serialize for Number {
verus! {
#[cfg(verus_keep_ghost)]
impl FromSpecImpl<BigInt> for Number {
open spec fn obeys_from_spec() -> bool
{
@@ -353,6 +355,7 @@ impl From<BigInt> for Number {
}
}
#[cfg(verus_keep_ghost)]
impl FromSpecImpl<u64> for Number {
open spec fn obeys_from_spec() -> bool
{
@@ -371,6 +374,7 @@ impl From<u64> for Number {
}
}
#[cfg(verus_keep_ghost)]
impl FromSpecImpl<usize> for Number {
open spec fn obeys_from_spec() -> bool
{
@@ -389,6 +393,7 @@ impl From<usize> for Number {
}
}
#[cfg(verus_keep_ghost)]
impl FromSpecImpl<u128> for Number {
open spec fn obeys_from_spec() -> bool
{
@@ -411,6 +416,7 @@ impl From<u128> for Number {
}
}
#[cfg(verus_keep_ghost)]
impl FromSpecImpl<i64> for Number {
open spec fn obeys_from_spec() -> bool
{
@@ -429,6 +435,7 @@ impl From<i64> for Number {
}
}
#[cfg(verus_keep_ghost)]
impl FromSpecImpl<i128> for Number {
open spec fn obeys_from_spec() -> bool
{
@@ -447,6 +454,7 @@ impl From<i128> for Number {
}
}
#[cfg(verus_keep_ghost)]
impl FromSpecImpl<f64> for Number {
open spec fn obeys_from_spec() -> bool
{

1
src/verusspec/mod.rs
View File

@@ -1,3 +1,4 @@
#[cfg(verus_keep_ghost)]
pub(crate) mod bigint;
pub(crate) mod float;
pub(crate) mod utils;