vstd: Add no-std build mode #772

zhaofengli · 2023-08-25T01:19:26Z

This PR adds a #![no_std] build mode for vstd. It can be activated by passing --vstd-no-std and optionally --vstd-no-alloc to vargo.

zhaofengli · 2023-08-30T16:23:53Z

Rebased after #733. Since Cargo.toml was added to vstd, it makes sense to use the std and alloc features like other crates in the ecosystem instead of negative features as before.

Tested that a default build using vargo produces a std-enabled vstd build, and with --vstd-no-std a no-std build.

utaal · 2023-08-30T20:00:29Z

Hi @zhaofengli, and thank you for the PR! I'll try and get to it quickly (likely, in a day or two).

Otherwise fails when alloc is disabled.

This is more idiomatic compared to negative features (non_std, non_global_allocator). By default, those features are enabled in Cargo.toml and will be opted-into by vstd_build. * fixup no-std after 803

utaal · 2023-09-12T18:31:27Z

Thank you for rebasing, and sorry for the delay!

utaal · 2023-09-12T18:33:31Z

One question: is it correct that with this PR there isn't a way when building to set alloc or std individually? If so, why are they two separate features? As something we can use in the future?

zhaofengli · 2023-09-12T22:59:58Z

One question: is it correct that with this PR there isn't a way when building to set alloc or std individually? If so, why are they two separate features? As something we can use in the future?

I just moved disabling alloc to a separate flag in vargo. Now both --vstd-no-std and --vstd-no-alloc are required for a no-std build without a global allocator available.

source/pervasive/bytes.rs

utaal · 2023-09-14T12:34:19Z

Thank you! Looks good. Just one last check on the #[trigger] annotations (in a comment).

utaal · 2023-09-18T11:03:48Z

There seem to be a couple more fixes needed:

making sure that vstd is re-built when the --vstd-no-* flags change;
fixes the build for --vstd-no-std without --vstd-no-alloc;
adding #[verifier::spinoff_prover] as explained in the comment.

I made these fixes and opened a PR against this branch: mars-research#1
I cannot otherwise make edits on this branch. If they look good to you, please merge them in, so that this PR gets updated.

This reverts commit a43d536.

* ensures vstd is rebuilt when the `--vstd-no*` flags change * use the `alloc` crate when necessary for `--vstd-no-std` without `--vstd-no-alloc`

zhaofengli · 2023-09-18T16:52:55Z

Thanks for the fixes! I've merged the commits.

utaal · 2023-09-18T20:29:34Z

@tjhance you added some of the extern crate alloc; imports, and made changes to use alloc::* types when necessary before. Can you take a look and check that my changes in bb7bf7a seem reasonable?

utaal

Looks good to me. I'd like for @tjhance to have a look too, in particular at the changes that involve using the alloc crate.

tjhance · 2023-09-18T21:18:02Z

source/pervasive/std_specs/vec.rs

@@ -222,6 +222,7 @@ pub fn ex_vec_as_slice<T, A: Allocator>(vec: &Vec<T, A>) -> (slice: &[T])
    vec.as_slice()
 }

+#[cfg(feature = "std")]


why's this needed? is split_off not available with just alloc?

Good catch! I went over vstd and did the following:

Removed the gate in question, changed std::clone::Clone to core::clone::Clone

Removed redundant extern crate alloc

Made the gate on string more fine-grained (string slices can be used without alloc)

(Sorry for the late reply, was away yesterday)

tjhance

looks fine to me

utaal · 2023-09-21T10:01:49Z

Merged as d2fd642

zhaofengli changed the title ~~vstd: Fix no-std compilation~~ vstd: Add no-std build mode Aug 25, 2023

tjhance requested a review from utaal August 29, 2023 13:34

zhaofengli force-pushed the vstd-no-std branch from 6af219d to 8a24f2e Compare August 30, 2023 16:19

zhaofengli added 3 commits September 12, 2023 10:40

vstd/bytes: Make sure triggers are consistent

a43d536

Otherwise fails when alloc is disabled.

vstd: Fix no-std compilation, use std and alloc features

e4a18ff

This is more idiomatic compared to negative features (non_std, non_global_allocator). By default, those features are enabled in Cargo.toml and will be opted-into by vstd_build. * fixup no-std after 803

vstd_build: Allow disabling std and alloc

5d6d650

zhaofengli force-pushed the vstd-no-std branch from 8a24f2e to bcaf627 Compare September 12, 2023 16:40

vargo: Allow disabling std and alloc in vstd

631ff6a

zhaofengli force-pushed the vstd-no-std branch from bcaf627 to 631ff6a Compare September 12, 2023 22:58

utaal reviewed Sep 14, 2023

View reviewed changes

source/pervasive/bytes.rs Outdated Show resolved Hide resolved

utaal mentioned this pull request Sep 18, 2023

Some fixes for vstd: Add no-std build mode mars-research/verus#1

Merged

utaal added 3 commits September 18, 2023 10:52

Revert "vstd/bytes: Make sure triggers are consistent"

16e45f7

This reverts commit a43d536.

fix various issues with --vstd-no-std and --vstd-no-alloc

bb7bf7a

* ensures vstd is rebuilt when the `--vstd-no*` flags change * use the `alloc` crate when necessary for `--vstd-no-std` without `--vstd-no-alloc`

stabilize proofs for *_to_from_le_bytes with spinoff_prover

0ce9f9d

utaal requested a review from tjhance September 18, 2023 20:28

utaal approved these changes Sep 18, 2023

View reviewed changes

tjhance reviewed Sep 18, 2023

View reviewed changes

tjhance approved these changes Sep 18, 2023

View reviewed changes

zhaofengli added 3 commits September 20, 2023 13:13

vstd/vec: Allow Vec::split_off with alloc

ea449c2

vstd/string: Support StrSlice in no-std+no-alloc

56318b9

vstd: Pull in alloc crate once based on feature

e33eca6

utaal added a commit that referenced this pull request Sep 21, 2023

Merge branch 'vstd-no-std' (#772)

d2fd642

utaal closed this Sep 21, 2023

zhaofengli mentioned this pull request Nov 2, 2023

vstd/bytes: Stabilize proofs #878

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

vstd: Add no-std build mode #772

vstd: Add no-std build mode #772

zhaofengli commented Aug 25, 2023 •

edited

Loading

zhaofengli commented Aug 30, 2023

utaal commented Aug 30, 2023 •

edited

Loading

utaal commented Sep 12, 2023

utaal commented Sep 12, 2023

zhaofengli commented Sep 12, 2023

utaal commented Sep 14, 2023

utaal commented Sep 18, 2023 •

edited

Loading

zhaofengli commented Sep 18, 2023

utaal commented Sep 18, 2023

utaal left a comment

tjhance Sep 18, 2023

zhaofengli Sep 20, 2023

tjhance left a comment

utaal commented Sep 21, 2023

vstd: Add no-std build mode #772

vstd: Add no-std build mode #772

Conversation

zhaofengli commented Aug 25, 2023 • edited Loading

zhaofengli commented Aug 30, 2023

utaal commented Aug 30, 2023 • edited Loading

utaal commented Sep 12, 2023

utaal commented Sep 12, 2023

zhaofengli commented Sep 12, 2023

utaal commented Sep 14, 2023

utaal commented Sep 18, 2023 • edited Loading

zhaofengli commented Sep 18, 2023

utaal commented Sep 18, 2023

utaal left a comment

Choose a reason for hiding this comment

tjhance Sep 18, 2023

Choose a reason for hiding this comment

zhaofengli Sep 20, 2023

Choose a reason for hiding this comment

tjhance left a comment

Choose a reason for hiding this comment

utaal commented Sep 21, 2023

zhaofengli commented Aug 25, 2023 •

edited

Loading

utaal commented Aug 30, 2023 •

edited

Loading

utaal commented Sep 18, 2023 •

edited

Loading