From 507a9e22f7d6344beb15a8386aea64a5bbfe44f1 Mon Sep 17 00:00:00 2001 From: Nick Spinale Date: Fri, 24 May 2024 12:50:35 +0000 Subject: [PATCH] Add Dafny test Signed-off-by: Nick Spinale --- .reuse/dep5 | 5 + Cargo.lock | 75 +++++++- Cargo.toml | 3 + .../tests/root-task/dafny/core/Cargo.nix | 19 ++ .../tests/root-task/dafny/core/Cargo.toml | 25 +++ .../tests/root-task/dafny/core/build.rs | 21 ++ .../tests/root-task/dafny/core/src/lib.rs | 32 +++ .../tests/root-task/dafny/hacking/.gitignore | 7 + .../tests/root-task/dafny/hacking/Makefile | 61 ++++++ .../tests/root-task/dafny/hacking/shell.nix | 19 ++ .../tests/root-task/dafny/task/Cargo.nix | 18 ++ .../tests/root-task/dafny/task/Cargo.toml | 22 +++ .../tests/root-task/dafny/task/src/main.rs | 18 ++ .../tests/root-task/dafny/verified/core.dfy | 17 ++ crates/sel4-mod-in-out-dir/Cargo.nix | 16 ++ crates/sel4-mod-in-out-dir/Cargo.toml | 24 +++ crates/sel4-mod-in-out-dir/src/lib.rs | 72 +++++++ .../manifest-scope.nix | 5 + .../manual-manifests.nix | 1 + hacking/nix/scope/dafny/default.nix | 77 ++++++++ hacking/nix/scope/dafny/deps.nix | 182 ++++++++++++++++++ hacking/nix/scope/default.nix | 2 + hacking/nix/scope/world/instances/dafny.nix | 65 +++++++ hacking/nix/scope/world/instances/default.nix | 4 + 24 files changed, 786 insertions(+), 4 deletions(-) create mode 100644 crates/private/tests/root-task/dafny/core/Cargo.nix create mode 100644 crates/private/tests/root-task/dafny/core/Cargo.toml create mode 100644 crates/private/tests/root-task/dafny/core/build.rs create mode 100644 crates/private/tests/root-task/dafny/core/src/lib.rs create mode 100644 crates/private/tests/root-task/dafny/hacking/.gitignore create mode 100644 crates/private/tests/root-task/dafny/hacking/Makefile create mode 100644 crates/private/tests/root-task/dafny/hacking/shell.nix create mode 100644 crates/private/tests/root-task/dafny/task/Cargo.nix create mode 100644 crates/private/tests/root-task/dafny/task/Cargo.toml create mode 100644 crates/private/tests/root-task/dafny/task/src/main.rs create mode 100644 crates/private/tests/root-task/dafny/verified/core.dfy create mode 100644 crates/sel4-mod-in-out-dir/Cargo.nix create mode 100644 crates/sel4-mod-in-out-dir/Cargo.toml create mode 100644 crates/sel4-mod-in-out-dir/src/lib.rs create mode 100644 hacking/nix/scope/dafny/default.nix create mode 100644 hacking/nix/scope/dafny/deps.nix create mode 100644 hacking/nix/scope/world/instances/dafny.nix diff --git a/.reuse/dep5 b/.reuse/dep5 index d92aa7466..5e9d01510 100644 --- a/.reuse/dep5 +++ b/.reuse/dep5 @@ -14,6 +14,11 @@ Files: Copyright: 2023, Colias Group, LLC License: BSD-2-Clause +Files: + hacking/nix/scope/dafny/deps.nix +Copyright: 2024, Colias Group, LLC +License: BSD-2-Clause + Files: crates/examples/microkit/banscii/pds/assistant/core/assets/fonts/rock-salt/*.ttf Copyright: 2010 by Font Diner, Inc DBA Sideshow. All rights reserved. diff --git a/Cargo.lock b/Cargo.lock index 345d90ba1..9bc9b28cd 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -73,6 +73,12 @@ dependencies = [ "memchr", ] +[[package]] +name = "allocator-api2" +version = "0.2.18" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5c6cb57a04249c6480766f7f7cef5467412af1490f8d1e243141daddada3264f" + [[package]] name = "anstream" version = "0.6.13" @@ -127,6 +133,12 @@ version = "1.0.81" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0952808a6c2afd1aa8947271f3a60f1a6763c7b912d210184c5149b5cf147247" +[[package]] +name = "as-any" +version = "0.3.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5b8a30a44e99a1c83ccb2a6298c563c888952a1c9134953db26876528f84c93a" + [[package]] name = "async-unsync" version = "0.2.2" @@ -457,6 +469,19 @@ dependencies = [ "typenum", ] +[[package]] +name = "dafny_runtime" +version = "0.1.0" +source = "git+https://github.com/coliasgroup/dafny.git?tag=keep/02d0a578fdf594a38c7c72d7ad56e1a6#02d0a578fdf594a38c7c72d7ad56e1a62e464f44" +dependencies = [ + "as-any", + "hashbrown 0.14.5", + "itertools", + "num", + "once_cell", + "paste", +] + [[package]] name = "defmt" version = "0.3.6" @@ -795,11 +820,12 @@ dependencies = [ [[package]] name = "hashbrown" -version = "0.14.3" +version = "0.14.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "290f1a1d9242c78d09ce40a5e87e7554ee637af1351968159f4952f028f75604" +checksum = "e5274423e17b7c9fc20b6e7e208532f9b19825d82dfd615708b70edd83df41f1" dependencies = [ "ahash", + "allocator-api2", ] [[package]] @@ -864,7 +890,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "7b0b929d511467233429c45a44ac1dcaa21ba0f5ba11e4879e6ed28ddb4f9df4" dependencies = [ "equivalent", - "hashbrown 0.14.3", + "hashbrown 0.14.5", ] [[package]] @@ -878,6 +904,15 @@ dependencies = [ "windows-sys", ] +[[package]] +name = "itertools" +version = "0.11.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b1c173a5686ce8bfa551b3563d0c2170bf24ca44da99c7ca4bfdab5418c3fe57" +dependencies = [ + "either", +] + [[package]] name = "itoa" version = "1.0.10" @@ -1371,7 +1406,7 @@ checksum = "a6a622008b6e321afc04970976f62ee297fdbaa6f95318ca343e3eebb9648441" dependencies = [ "crc32fast", "flate2", - "hashbrown 0.14.3", + "hashbrown 0.14.5", "indexmap", "memchr", "ruzstd", @@ -1393,6 +1428,12 @@ dependencies = [ "ttf-parser", ] +[[package]] +name = "paste" +version = "1.0.15" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "57c0d7b74b563b49d38dae00a0c37d4d6de9b432382b2892f0574ddcae73fd0a" + [[package]] name = "peeking_take_while" version = "0.1.2" @@ -2387,6 +2428,14 @@ dependencies = [ "zerocopy 0.7.32", ] +[[package]] +name = "sel4-mod-in-out-dir" +version = "0.1.0" +dependencies = [ + "quote", + "syn 1.0.109", +] + [[package]] name = "sel4-newlib" version = "0.1.0" @@ -2960,6 +3009,24 @@ dependencies = [ "sel4-root-task", ] +[[package]] +name = "tests-root-task-dafny-core" +version = "0.1.0" +dependencies = [ + "dafny_runtime", + "num", + "sel4-mod-in-out-dir", +] + +[[package]] +name = "tests-root-task-dafny-task" +version = "0.1.0" +dependencies = [ + "sel4", + "sel4-root-task", + "tests-root-task-dafny-core", +] + [[package]] name = "tests-root-task-default-test-harness" version = "0.1.0" diff --git a/Cargo.toml b/Cargo.toml index 80dd5a986..afada6897 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -57,6 +57,8 @@ members = [ "crates/private/tests/root-task/backtrace", "crates/private/tests/root-task/c", "crates/private/tests/root-task/config", + "crates/private/tests/root-task/dafny/core", + "crates/private/tests/root-task/dafny/task", "crates/private/tests/root-task/default-test-harness", "crates/private/tests/root-task/loader", "crates/private/tests/root-task/panicking", @@ -111,6 +113,7 @@ members = [ "crates/sel4-microkit/macros", "crates/sel4-microkit/message", "crates/sel4-microkit/message/types", + "crates/sel4-mod-in-out-dir", "crates/sel4-newlib", "crates/sel4-one-ref-cell", "crates/sel4-panicking", diff --git a/crates/private/tests/root-task/dafny/core/Cargo.nix b/crates/private/tests/root-task/dafny/core/Cargo.nix new file mode 100644 index 000000000..b4c765c25 --- /dev/null +++ b/crates/private/tests/root-task/dafny/core/Cargo.nix @@ -0,0 +1,19 @@ +# +# Copyright 2024, Colias Group, LLC +# +# SPDX-License-Identifier: BSD-2-Clause +# + +{ mk, localCrates, dafnySource }: + +mk { + package.name = "tests-root-task-dafny-core"; + dependencies = { + inherit (localCrates) + sel4-mod-in-out-dir + # dafny_runtime + ; + dafny_runtime = dafnySource; + num = { version = "0.4"; default-features = false; features = ["alloc"]; }; + }; +} diff --git a/crates/private/tests/root-task/dafny/core/Cargo.toml b/crates/private/tests/root-task/dafny/core/Cargo.toml new file mode 100644 index 000000000..ee6a9c07b --- /dev/null +++ b/crates/private/tests/root-task/dafny/core/Cargo.toml @@ -0,0 +1,25 @@ +# +# Copyright 2023, Colias Group, LLC +# +# SPDX-License-Identifier: BSD-2-Clause +# +# +# This file is generated from './Cargo.nix'. You can edit this file directly +# if you are not using this project's Cargo manifest management tools. +# See 'hacking/cargo-manifest-management/README.md' for more information. +# + +[package] +name = "tests-root-task-dafny-core" +version = "0.1.0" +authors = ["Nick Spinale "] +edition = "2021" +license = "BSD-2-Clause" + +[dependencies] +num = { version = "0.4", default-features = false, features = ["alloc"] } +sel4-mod-in-out-dir = { path = "../../../../../sel4-mod-in-out-dir" } + +[dependencies.dafny_runtime] +git = "https://github.com/coliasgroup/dafny.git" +tag = "keep/02d0a578fdf594a38c7c72d7ad56e1a6" diff --git a/crates/private/tests/root-task/dafny/core/build.rs b/crates/private/tests/root-task/dafny/core/build.rs new file mode 100644 index 000000000..e0cec6fb1 --- /dev/null +++ b/crates/private/tests/root-task/dafny/core/build.rs @@ -0,0 +1,21 @@ +// +// Copyright 2024, Colias Group, LLC +// +// SPDX-License-Identifier: BSD-2-Clause +// + +use std::env; +use std::fs; +use std::path::PathBuf; + +const TRANSLATED_ENV: &str = "TRANSLATED"; + +fn main() { + let translated_src = env::var(TRANSLATED_ENV).unwrap(); + let out_dir = env::var("OUT_DIR").unwrap(); + let translated_dst = PathBuf::from(&out_dir).join("translated.rs"); + fs::copy(&translated_src, &translated_dst).unwrap(); + + println!("cargo:rerun-if-env-changed={TRANSLATED_ENV}"); + println!("cargo:rerun-if-changed={}", translated_src); +} diff --git a/crates/private/tests/root-task/dafny/core/src/lib.rs b/crates/private/tests/root-task/dafny/core/src/lib.rs new file mode 100644 index 000000000..cc12b522c --- /dev/null +++ b/crates/private/tests/root-task/dafny/core/src/lib.rs @@ -0,0 +1,32 @@ +// +// Copyright 2024, Colias Group, LLC +// +// SPDX-License-Identifier: BSD-2-Clause +// + +#![no_std] +#![feature(proc_macro_hygiene)] + +use dafny_runtime::DafnyInt; +use num::traits::cast::ToPrimitive; +use sel4_mod_in_out_dir::in_out_dir; + +#[rustfmt::skip] +#[in_out_dir] +mod translated; + +pub fn max(a: usize, b: usize) -> usize { + translated::_module::_default::Max(&DafnyInt::from(a), &DafnyInt::from(b)) + .to_usize() + .unwrap() +} + +#[cfg(test)] +mod tests { + use super::max; + + #[test] + fn x() { + assert_eq!(max(13, 37), 37); + } +} diff --git a/crates/private/tests/root-task/dafny/hacking/.gitignore b/crates/private/tests/root-task/dafny/hacking/.gitignore new file mode 100644 index 000000000..c25bec135 --- /dev/null +++ b/crates/private/tests/root-task/dafny/hacking/.gitignore @@ -0,0 +1,7 @@ +# +# Copyright 2024, Colias Group, LLC +# +# SPDX-License-Identifier: BSD-2-Clause +# + +/build/ diff --git a/crates/private/tests/root-task/dafny/hacking/Makefile b/crates/private/tests/root-task/dafny/hacking/Makefile new file mode 100644 index 000000000..2f10c7615 --- /dev/null +++ b/crates/private/tests/root-task/dafny/hacking/Makefile @@ -0,0 +1,61 @@ +# +# Copyright 2024, Colias Group, LLC +# +# SPDX-License-Identifier: BSD-2-Clause +# + +top_level_dir := $(TOP_LEVEL_DIR) + +build_dir := build + +dafny_link := $(build_dir)/dafny +dafny_bin := $(dafny_link)/bin/dafny + +dafny_name := core +dafny_src := ../verified/$(dafny_name).dfy +dafny_output_prefix := $(build_dir)/$(dafny_name) +dafny_output := $(dafny_output_prefix)-rust/src/$(dafny_name).rs +dafny_dst := $(build_dir)/translated.rs + +.PHONY: none +none: + +.PHONY: clean +clean: + rm -rf $(build_dir) + +FORCE: ; + +$(build_dir): + mkdir -p $@ + +$(dafny_link): FORCE | $(build_dir) + nix-build $(top_level_dir) -A pkgs.build.this.dafny -o $@ + +$(dafny_output): FORCE | $(build_dir) + $(dafny_bin) translate rs $(dafny_src) -o $(dafny_output_prefix) + +$(dafny_dst): $(dafny_output) + cp $< $@ + +# # # + +.PHONY: dafny +dafny: $(dafny_link) + +.PHONY: translate +translate: $(dafny_dst) + +.PHONY: test +test: + cargo test -p tests-root-task-dafny-core + +.PHONY: run +run: + set -eu; \ + script=$$( \ + nix-build $(top_level_dir) \ + -A worlds.aarch64.default.instances.tests.root-task.dafny.automate \ + --no-out-link \ + ); \ + $$script diff --git a/crates/private/tests/root-task/dafny/hacking/shell.nix b/crates/private/tests/root-task/dafny/hacking/shell.nix new file mode 100644 index 000000000..88b9d8155 --- /dev/null +++ b/crates/private/tests/root-task/dafny/hacking/shell.nix @@ -0,0 +1,19 @@ +# +# Copyright 2024, Colias Group, LLC +# +# SPDX-License-Identifier: BSD-2-Clause +# + +let + topLevelDir = ../../../../../..; + topLevel = import topLevelDir {}; + +in +topLevel.worlds.default.shell.overrideAttrs (self: super: { + nativeBuildInputs = (super.nativeBuildInputs or []) ++ [ + topLevel.pkgs.build.dafny + ]; + + TOP_LEVEL_DIR = toString topLevelDir; + TRANSLATED = toString ./build/translated.rs; +}) diff --git a/crates/private/tests/root-task/dafny/task/Cargo.nix b/crates/private/tests/root-task/dafny/task/Cargo.nix new file mode 100644 index 000000000..0e255f280 --- /dev/null +++ b/crates/private/tests/root-task/dafny/task/Cargo.nix @@ -0,0 +1,18 @@ +# +# Copyright 2024, Colias Group, LLC +# +# SPDX-License-Identifier: BSD-2-Clause +# + +{ mk, localCrates }: + +mk { + package.name = "tests-root-task-dafny-task"; + dependencies = { + inherit (localCrates) + sel4 + sel4-root-task + tests-root-task-dafny-core + ; + }; +} diff --git a/crates/private/tests/root-task/dafny/task/Cargo.toml b/crates/private/tests/root-task/dafny/task/Cargo.toml new file mode 100644 index 000000000..8a76a89ee --- /dev/null +++ b/crates/private/tests/root-task/dafny/task/Cargo.toml @@ -0,0 +1,22 @@ +# +# Copyright 2023, Colias Group, LLC +# +# SPDX-License-Identifier: BSD-2-Clause +# +# +# This file is generated from './Cargo.nix'. You can edit this file directly +# if you are not using this project's Cargo manifest management tools. +# See 'hacking/cargo-manifest-management/README.md' for more information. +# + +[package] +name = "tests-root-task-dafny-task" +version = "0.1.0" +authors = ["Nick Spinale "] +edition = "2021" +license = "BSD-2-Clause" + +[dependencies] +sel4 = { path = "../../../../../sel4" } +sel4-root-task = { path = "../../../../../sel4-root-task" } +tests-root-task-dafny-core = { path = "../core" } diff --git a/crates/private/tests/root-task/dafny/task/src/main.rs b/crates/private/tests/root-task/dafny/task/src/main.rs new file mode 100644 index 000000000..ad840b5a9 --- /dev/null +++ b/crates/private/tests/root-task/dafny/task/src/main.rs @@ -0,0 +1,18 @@ +// +// Copyright 2024, Colias Group, LLC +// +// SPDX-License-Identifier: BSD-2-Clause +// + +#![no_std] +#![no_main] + +use sel4_root_task::{debug_println, root_task}; + +#[root_task(heap_size = 1024 * 1024)] +fn main(_: &sel4::BootInfoPtr) -> ! { + assert_eq!(tests_root_task_dafny_core::max(13, 37), 37); + + debug_println!("TEST_PASS"); + sel4::init_thread::suspend_self() +} diff --git a/crates/private/tests/root-task/dafny/verified/core.dfy b/crates/private/tests/root-task/dafny/verified/core.dfy new file mode 100644 index 000000000..bb044840c --- /dev/null +++ b/crates/private/tests/root-task/dafny/verified/core.dfy @@ -0,0 +1,17 @@ +// +// Copyright 2024, Colias Group, LLC +// Copyright (c) Microsoft Corporation +// +// SPDX-License-Identifier: MIT +// + +method Max(a: int, b:int) returns (c: int) + ensures a < b ==> c == b + ensures b <= a ==> c == a +{ + if (a < b) { + return b; + } else { + return a; + } +} diff --git a/crates/sel4-mod-in-out-dir/Cargo.nix b/crates/sel4-mod-in-out-dir/Cargo.nix new file mode 100644 index 000000000..2a4d6db6e --- /dev/null +++ b/crates/sel4-mod-in-out-dir/Cargo.nix @@ -0,0 +1,16 @@ +# +# Copyright 2024, Colias Group, LLC +# +# SPDX-License-Identifier: BSD-2-Clause +# + +{ mk, versions }: + +mk { + package.name = "sel4-mod-in-out-dir"; + lib.proc-macro = true; + dependencies = { + inherit (versions) quote; + syn = { version = versions.syn; features = [ "full" ]; }; + }; +} diff --git a/crates/sel4-mod-in-out-dir/Cargo.toml b/crates/sel4-mod-in-out-dir/Cargo.toml new file mode 100644 index 000000000..38711ab0b --- /dev/null +++ b/crates/sel4-mod-in-out-dir/Cargo.toml @@ -0,0 +1,24 @@ +# +# Copyright 2023, Colias Group, LLC +# +# SPDX-License-Identifier: BSD-2-Clause +# +# +# This file is generated from './Cargo.nix'. You can edit this file directly +# if you are not using this project's Cargo manifest management tools. +# See 'hacking/cargo-manifest-management/README.md' for more information. +# + +[package] +name = "sel4-mod-in-out-dir" +version = "0.1.0" +authors = ["Nick Spinale "] +edition = "2021" +license = "BSD-2-Clause" + +[lib] +proc-macro = true + +[dependencies] +quote = "1.0.23" +syn = { version = "1.0.107", features = ["full"] } diff --git a/crates/sel4-mod-in-out-dir/src/lib.rs b/crates/sel4-mod-in-out-dir/src/lib.rs new file mode 100644 index 000000000..b5043c087 --- /dev/null +++ b/crates/sel4-mod-in-out-dir/src/lib.rs @@ -0,0 +1,72 @@ +// +// Copyright 2024, Colias Group, LLC +// +// SPDX-License-Identifier: BSD-2-Clause +// + +use std::env; +use std::path::Path; + +use proc_macro::TokenStream; +use quote::quote; +use syn::parse::{Error, Parse, ParseStream}; +use syn::{parse_macro_input, ItemMod, MetaNameValue, Result}; + +/// Set a module's `#[path]` relative to `$OUT_DIR`. +/// +/// The following is not supported by rustc: +/// ```ignore +/// #[path = concat!(env!("OUT_DIR"), "/foo.rs")] +/// mod foo; +/// ``` + +/// This macro does exactly that: +/// ```ignore +/// #[in_out_dir] +/// mod foo; +/// ``` + +/// This works too: +/// ```ignore +/// #[in_out_dir(relative_path = "path/to/bar.rs")] +/// mod foo; +/// ``` +#[proc_macro_attribute] +pub fn in_out_dir(attr: TokenStream, item: TokenStream) -> TokenStream { + let input = parse_macro_input!(attr as Input); + let item_mod = parse_macro_input!(item as ItemMod); + let relative_path = input + .relative_path + .unwrap_or_else(|| format!("{}.rs", item_mod.ident)); + let path = Path::new(&env::var("OUT_DIR").unwrap()).join(relative_path); + let path = path.to_str().unwrap(); + quote!( + #[path = #path] + #item_mod + ) + .into() +} + +struct Input { + relative_path: Option, +} + +impl Parse for Input { + fn parse(input: ParseStream) -> Result { + let relative_path = if input.is_empty() { + None + } else { + let name_value = input.parse::()?; + let path = name_value.path; + if !path.is_ident("relative_path") { + return Err(Error::new_spanned(path, "unrecognized argument")); + } + let lit = name_value.lit; + match lit { + syn::Lit::Str(s) => Some(s.value()), + _ => return Err(Error::new_spanned(lit, "value must be a string literal")), + } + }; + Ok(Self { relative_path }) + } +} diff --git a/hacking/cargo-manifest-management/manifest-scope.nix b/hacking/cargo-manifest-management/manifest-scope.nix index 82ca0491e..2ee305280 100644 --- a/hacking/cargo-manifest-management/manifest-scope.nix +++ b/hacking/cargo-manifest-management/manifest-scope.nix @@ -213,4 +213,9 @@ in rec { default-features = false; inherit features; }; + + dafnySource = { + git = "https://github.com/coliasgroup/dafny.git"; + tag = "keep/02d0a578fdf594a38c7c72d7ad56e1a6"; # branch dev + }; } diff --git a/hacking/cargo-manifest-management/manual-manifests.nix b/hacking/cargo-manifest-management/manual-manifests.nix index ab12e7b96..b91b5cc71 100644 --- a/hacking/cargo-manifest-management/manual-manifests.nix +++ b/hacking/cargo-manifest-management/manual-manifests.nix @@ -15,4 +15,5 @@ in { # rustls = relativeToTmpSrc "rustls/rustls"; # lock_api = relativeToTmpSrc "parking_lot/lock_api"; # volatile = relativeToTmpSrc "volatile"; + # dafny_runtime = relativeToTmpSrc "dafny/Source/DafnyRuntime/DafnyRuntimeRust"; } diff --git a/hacking/nix/scope/dafny/default.nix b/hacking/nix/scope/dafny/default.nix new file mode 100644 index 000000000..b46379d09 --- /dev/null +++ b/hacking/nix/scope/dafny/default.nix @@ -0,0 +1,77 @@ +# +# Copyright 2024, Colias Group, LLC +# +# SPDX-License-Identifier: BSD-2-Clause +# + +{ lib +, buildDotnetModule +, fetchFromGitHub +, writeScript +, jdk11 +, z3 +, sources +}: + +let + f = { useLocal ? false }: buildDotnetModule rec { + pname = "Dafny"; + version = "4.6.0"; + + src = sources.fetchGit { + url = "https://github.com/coliasgroup/dafny.git"; + rev = "02d0a578fdf594a38c7c72d7ad56e1a62e464f44"; + local = sources.localRoot + "/dafny"; + inherit useLocal; + }; + + postPatch = '' + cp ${ + writeScript "fake-gradlew-for-dafny" '' + mkdir -p build/libs/ + javac $(find -name "*.java" | grep "^./src/main") -d classes + jar cf build/libs/DafnyRuntime-${version}.jar -C classes dafny + ''} Source/DafnyRuntime/DafnyRuntimeJava/gradlew + + # Needed to fix + # "error NETSDK1129: The 'Publish' target is not supported without + # specifying a target framework. The current project targets multiple + # frameworks, you must specify the framework for the published + # application." + substituteInPlace Source/DafnyRuntime/DafnyRuntime.csproj \ + --replace TargetFrameworks TargetFramework \ + --replace "netstandard2.0;net452" net6.0 + ''; + + nativeBuildInputs = [ + jdk11 + ]; + + nugetDeps = ./deps.nix; + + # Build just these projects. Building Source/Dafny.sln includes a bunch of + # unnecessary components like tests. + projectFile = [ + "Source/Dafny/Dafny.csproj" + "Source/DafnyRuntime/DafnyRuntime.csproj" + # "Source/DafnyLanguageServer/DafnyLanguageServer.csproj" + ]; + + executables = [ "Dafny" ]; + + # Help Dafny find z3 + makeWrapperArgs = [ "--prefix PATH : ${lib.makeBinPath [ z3 ]}" ]; + + postFixup = '' + ln -s "$out/bin/Dafny" "$out/bin/dafny" || true + ''; + + passthru = { + local = f { useLocal = true; }; + remote = f { useLocal = false; }; + }; + }; + +in f { + # useLocal = true; +} diff --git a/hacking/nix/scope/dafny/deps.nix b/hacking/nix/scope/dafny/deps.nix new file mode 100644 index 000000000..0c96fca4e --- /dev/null +++ b/hacking/nix/scope/dafny/deps.nix @@ -0,0 +1,182 @@ +# This file was automatically generated by passthru.fetch-deps. +# Please dont edit it manually, your changes might get overwritten! + +{ fetchNuGet }: [ + (fetchNuGet { pname = "Boogie"; version = "3.1.3"; sha256 = "0xzc7s0rjb8dhdkdf71g6pdsnyhbl534xpwd8gbx6g16a87iqx6i"; }) + (fetchNuGet { pname = "Boogie.AbstractInterpretation"; version = "3.1.6"; sha256 = "1c6z13dz0sbkmk4ay64aihy7s7xlfdvhpcknxhw1m1b0yly5qj6b"; }) + (fetchNuGet { pname = "Boogie.BaseTypes"; version = "3.1.6"; sha256 = "1hxcpc45f32g3jpaw7mg6k9qsppcb3p20wxv4d4dc3nz0r52lrmr"; }) + (fetchNuGet { pname = "Boogie.CodeContractsExtender"; version = "3.1.6"; sha256 = "1qk7w7c40fpkvvarbgi1bkdcxpn12r0lqngpwwjw8i7nk84ni5gl"; }) + (fetchNuGet { pname = "Boogie.Concurrency"; version = "3.1.6"; sha256 = "11981gfa0n4s214yilnxqhh1clr4l78iqlws6gv01z1n6rxgbyla"; }) + (fetchNuGet { pname = "Boogie.Core"; version = "3.1.6"; sha256 = "0sgj6i1hvp90g2zfqs1aly500xnv3fq9d4cfgii5kpza8vgm7w4g"; }) + (fetchNuGet { pname = "Boogie.ExecutionEngine"; version = "3.1.6"; sha256 = "08vxxwcnkykcngihkp0bvfwkgwxb3nnqjp5f1vz4bnw708xs0ydg"; }) + (fetchNuGet { pname = "Boogie.Graph"; version = "3.1.6"; sha256 = "0fzj65pnky8i83jj2h9nszij25a46z68fy2sm3pxwlg678nmx2jz"; }) + (fetchNuGet { pname = "Boogie.Houdini"; version = "3.1.6"; sha256 = "0lfljb9brnr79hp1f0ff6fcy51ml66pjj102jk4pqpmsjwvcjx43"; }) + (fetchNuGet { pname = "Boogie.Model"; version = "3.1.6"; sha256 = "0546b27mxv97v7qilb1carbwip0q7sz9zz7sxizpww6yc3j8w8if"; }) + (fetchNuGet { pname = "Boogie.Provers.LeanAuto"; version = "3.1.6"; sha256 = "1x1f35g0kxzhxvw4icmbvkik16py47j6h04gj0ckwbny9qmglaby"; }) + (fetchNuGet { pname = "Boogie.Provers.SMTLib"; version = "3.1.6"; sha256 = "0mqlpwfxgv9dd773254rrbgbjb5mpa3xkvlq32ml752h36j8m2r9"; }) + (fetchNuGet { pname = "Boogie.VCExpr"; version = "3.1.6"; sha256 = "0p7axpjn4qg191bs7b33zf9l336bdznvxp3305z2ssnkakjx247h"; }) + (fetchNuGet { pname = "Boogie.VCGeneration"; version = "3.1.6"; sha256 = "05z2lr92hbllikv65gh7m3i879fnn6pjn2acf133sijx9b1jixdb"; }) + (fetchNuGet { pname = "CocoR"; version = "2014.12.24"; sha256 = "0ps8h7aawkcc1910qnh13llzb01pvgsjmg862pxp0p4wca2dn7a2"; }) + (fetchNuGet { pname = "JetBrains.Annotations"; version = "2021.1.0"; sha256 = "07pnhxxlgx8spmwmakz37nmbvgyb6yjrbrhad5rrn6y767z5r1gb"; }) + (fetchNuGet { pname = "MediatR"; version = "8.1.0"; sha256 = "0cqx7yfh998xhsfk5pr6229lcjcs1jxxyqz7dwskc9jddl6a2akp"; }) + (fetchNuGet { pname = "Microsoft.Bcl.AsyncInterfaces"; version = "1.1.1"; sha256 = "0a1ahssqds2ympr7s4xcxv5y8jgxs7ahd6ah6fbgglj4rki1f1vw"; }) + (fetchNuGet { pname = "Microsoft.Bcl.AsyncInterfaces"; version = "6.0.0"; sha256 = "15gqy2m14fdlvy1g59207h5kisznm355kbw010gy19vh47z8gpz3"; }) + (fetchNuGet { pname = "Microsoft.CodeAnalysis.Analyzers"; version = "3.0.0"; sha256 = "0bbl0jpqywqmzz2gagld1p2gvdfldjfjmm25hil9wj2nq1zc4di8"; }) + (fetchNuGet { pname = "Microsoft.CodeAnalysis.Common"; version = "3.7.0"; sha256 = "0882492nx6x68b0pkh3q5xaawz0b2l5x35r40722ignyjnvjydph"; }) + (fetchNuGet { pname = "Microsoft.CodeAnalysis.CSharp"; version = "3.7.0"; sha256 = "0adw6rcag8wxydzyiyhls2mxaqkay5qlz25z1fxrlv5qnchqn0n5"; }) + (fetchNuGet { pname = "Microsoft.DotNet.PlatformAbstractions"; version = "2.0.4"; sha256 = "1fdzln4im9hb55agzwchbfgm3vmngigmbpci5j89b0gqcxixmv8j"; }) + (fetchNuGet { pname = "Microsoft.Extensions.Configuration"; version = "2.0.0"; sha256 = "0yssxq9di5h6xw2cayp5hj3l9b2p0jw9wcjz73rwk4586spac9s9"; }) + (fetchNuGet { pname = "Microsoft.Extensions.Configuration"; version = "5.0.0"; sha256 = "01m9vzlq0vg0lhckj2dimwq42niwny8g3lm13c9a401hlyg90z1p"; }) + (fetchNuGet { pname = "Microsoft.Extensions.Configuration.Abstractions"; version = "2.0.0"; sha256 = "1ilz2yrgg9rbjyhn6a5zh9pr51nmh11z7sixb4p7vivgydj9gxwf"; }) + (fetchNuGet { pname = "Microsoft.Extensions.Configuration.Abstractions"; version = "5.0.0"; sha256 = "0fqxkc9pjxkqylsdf26s9q21ciyk56h1w33pz3v1v4wcv8yv1v6k"; }) + (fetchNuGet { pname = "Microsoft.Extensions.Configuration.Binder"; version = "2.0.0"; sha256 = "1prvdbma6r18n5agbhhabv6g357p1j70gq4m9g0vs859kf44nrgc"; }) + (fetchNuGet { pname = "Microsoft.Extensions.Configuration.CommandLine"; version = "5.0.0"; sha256 = "084hnz5l0vr15ay23rksqipslqnz3pp30w9hsirpx1iqdm5688mc"; }) + (fetchNuGet { pname = "Microsoft.Extensions.Configuration.FileExtensions"; version = "5.0.0"; sha256 = "1wq229r3xcmm9wh9sqdpvmfv4qpbp2zms9x6xk7g7sbb8h32hnz3"; }) + (fetchNuGet { pname = "Microsoft.Extensions.Configuration.Json"; version = "5.0.0"; sha256 = "0hq5i483bjbvprp1la9l3si82x1ydxbvkpfc7r3s7zgxg957fyp9"; }) + (fetchNuGet { pname = "Microsoft.Extensions.DependencyInjection"; version = "2.0.0"; sha256 = "018izzgykaqcliwarijapgki9kp2c560qv8qsxdjywr7byws5apq"; }) + (fetchNuGet { pname = "Microsoft.Extensions.DependencyInjection"; version = "5.0.0"; sha256 = "15sdwcyzz0qlybwbdq854bn3jk6kx7awx28gs864c4shhbqkppj4"; }) + (fetchNuGet { pname = "Microsoft.Extensions.DependencyInjection.Abstractions"; version = "2.0.0"; sha256 = "1pwrfh9b72k9rq6mb2jab5qhhi225d5rjalzkapiayggmygc8nhz"; }) + (fetchNuGet { pname = "Microsoft.Extensions.DependencyInjection.Abstractions"; version = "5.0.0"; sha256 = "17cz6s80va0ch0a6nqa1wbbbp3p8sqxb96lj4qcw67ivkp2yxiyj"; }) + (fetchNuGet { pname = "Microsoft.Extensions.DependencyModel"; version = "2.0.4"; sha256 = "041i1vlcibpzgalxxzdk81g5pgmqvmz2g61k0rqa2sky0wpvijx9"; }) + (fetchNuGet { pname = "Microsoft.Extensions.FileProviders.Abstractions"; version = "5.0.0"; sha256 = "01ahgd0b2z2zycrr2lcsq2cl59fn04bh51hdwdp9dcsdkpvnasj1"; }) + (fetchNuGet { pname = "Microsoft.Extensions.FileProviders.Physical"; version = "5.0.0"; sha256 = "00vii8148a6pk12l9jl0rhjp7apil5q5qcy7v1smnv17lj4p8szd"; }) + (fetchNuGet { pname = "Microsoft.Extensions.FileSystemGlobbing"; version = "5.0.0"; sha256 = "0lm6n9vbyjh0l17qcc2y9qwn1cns3dyjmkvbxjp0g9sll32kjpmb"; }) + (fetchNuGet { pname = "Microsoft.Extensions.Logging"; version = "2.0.0"; sha256 = "1jkwjcq1ld9znz1haazk8ili2g4pzfdp6i7r7rki4hg3jcadn386"; }) + (fetchNuGet { pname = "Microsoft.Extensions.Logging"; version = "5.0.0"; sha256 = "1qa1l18q2jh9azya8gv1p8anzcdirjzd9dxxisb4911i9m1648i3"; }) + (fetchNuGet { pname = "Microsoft.Extensions.Logging.Abstractions"; version = "5.0.0"; sha256 = "1yza38675dbv1qqnnhqm23alv2bbaqxp0pb7zinjmw8j2mr5r6wc"; }) + (fetchNuGet { pname = "Microsoft.Extensions.Options"; version = "2.0.0"; sha256 = "0g4zadlg73f507krilhaaa7h0jdga216syrzjlyf5fdk25gxmjqh"; }) + (fetchNuGet { pname = "Microsoft.Extensions.Options"; version = "5.0.0"; sha256 = "1rdmgpg770x8qwaaa6ryc27zh93p697fcyvn5vkxp0wimlhqkbay"; }) + (fetchNuGet { pname = "Microsoft.Extensions.Options.ConfigurationExtensions"; version = "2.0.0"; sha256 = "1isc3rjbzz60f7wbmgcwslx5d10hm5hisnk7v54vfi2bz7132gll"; }) + (fetchNuGet { pname = "Microsoft.Extensions.Primitives"; version = "2.0.0"; sha256 = "1xppr5jbny04slyjgngxjdm0maxdh47vq481ps944d7jrfs0p3mb"; }) + (fetchNuGet { pname = "Microsoft.Extensions.Primitives"; version = "5.0.0"; sha256 = "0swqcknyh87ns82w539z1mvy804pfwhgzs97cr3nwqk6g5s42gd6"; }) + (fetchNuGet { pname = "Microsoft.NETCore.Platforms"; version = "1.0.1"; sha256 = "01al6cfxp68dscl15z7rxfw9zvhm64dncsw09a1vmdkacsa2v6lr"; }) + (fetchNuGet { pname = "Microsoft.NETCore.Platforms"; version = "1.1.0"; sha256 = "08vh1r12g6ykjygq5d3vq09zylgb84l63k49jc4v8faw9g93iqqm"; }) + (fetchNuGet { pname = "Microsoft.NETCore.Platforms"; version = "2.1.2"; sha256 = "1507hnpr9my3z4w1r6xk5n0s1j3y6a2c2cnynj76za7cphxi1141"; }) + (fetchNuGet { pname = "Microsoft.NETCore.Platforms"; version = "3.0.0"; sha256 = "1bk8r4r3ihmi6322jmcag14jmw11mjqys202azqjzglcx59pxh51"; }) + (fetchNuGet { pname = "Microsoft.NETCore.Targets"; version = "1.0.1"; sha256 = "0ppdkwy6s9p7x9jix3v4402wb171cdiibq7js7i13nxpdky7074p"; }) + (fetchNuGet { pname = "Microsoft.NETCore.Targets"; version = "1.1.0"; sha256 = "193xwf33fbm0ni3idxzbr5fdq3i2dlfgihsac9jj7whj0gd902nh"; }) + (fetchNuGet { pname = "Microsoft.TestPlatform.Extensions.TrxLogger"; version = "17.9.0"; sha256 = "0wn38vj9i4gjw5zsl4wcivpqrmp1h5n6m1zxcfwj7yjn9hf45rz9"; }) + (fetchNuGet { pname = "Microsoft.TestPlatform.ObjectModel"; version = "17.9.0"; sha256 = "1kgsl9w9fganbm9wvlkqgk0ag9hfi58z88rkfybc6kvg78bx89ca"; }) + (fetchNuGet { pname = "Microsoft.TestPlatform.TestHost"; version = "17.9.0"; sha256 = "19ffh31a1jxzn8j69m1vnk5hyfz3dbxmflq77b8x82zybiilh5nl"; }) + (fetchNuGet { pname = "Microsoft.VisualStudio.Threading"; version = "16.7.56"; sha256 = "13x0xrsjxd86clf9cjjwmpzlyp8pkrf13riya7igs8zy93zw2qap"; }) + (fetchNuGet { pname = "Microsoft.VisualStudio.Threading.Analyzers"; version = "16.7.56"; sha256 = "04v9df0k7bsc0rzgkw4mnvi43pdrh42vk6xdcwn9m6im33m0nnz2"; }) + (fetchNuGet { pname = "Microsoft.VisualStudio.Validation"; version = "15.5.31"; sha256 = "1ah99rn922qa0sd2k3h64m324f2r32pw8cn4cfihgvwx4qdrpmgw"; }) + (fetchNuGet { pname = "Microsoft.Win32.Primitives"; version = "4.3.0"; sha256 = "0j0c1wj4ndj21zsgivsc24whiya605603kxrbiw6wkfdync464wq"; }) + (fetchNuGet { pname = "Microsoft.Win32.Registry"; version = "4.6.0"; sha256 = "0i4y782yrqqyx85pg597m20gm0v126w0j9ddk5z7xb3crx4z9f2s"; }) + (fetchNuGet { pname = "Microsoft.Win32.SystemEvents"; version = "6.0.0"; sha256 = "0c6pcj088g1yd1vs529q3ybgsd2vjlk5y1ic6dkmbhvrp5jibl9p"; }) + (fetchNuGet { pname = "Nerdbank.Streams"; version = "2.6.81"; sha256 = "06wihcaga8537ibh0mkj28m720m6vzkqk562zkynhca85nd236yi"; }) + (fetchNuGet { pname = "Newtonsoft.Json"; version = "11.0.2"; sha256 = "1784xi44f4k8v1fr696hsccmwpy94bz7kixxqlri98zhcxn406b2"; }) + (fetchNuGet { pname = "Newtonsoft.Json"; version = "13.0.1"; sha256 = "0fijg0w6iwap8gvzyjnndds0q4b8anwxxvik7y8vgq97dram4srb"; }) + (fetchNuGet { pname = "OmniSharp.Extensions.JsonRpc"; version = "0.19.5"; sha256 = "0ilcv3cxcvjkd8ngiydi69pzll07rhqdv5nq9yjnhyj142ynw2cb"; }) + (fetchNuGet { pname = "OmniSharp.Extensions.JsonRpc.Generators"; version = "0.19.5"; sha256 = "1mac4yx29ld8fyirg7n0vqn81hzdvcrl8w0l9w5xhnnm6bcd42v8"; }) + (fetchNuGet { pname = "OmniSharp.Extensions.LanguageProtocol"; version = "0.19.5"; sha256 = "1clgrbw6dlh46iiiqhavwh15xqar41az352mb5r4ln8ql3wnmk1i"; }) + (fetchNuGet { pname = "OmniSharp.Extensions.LanguageServer"; version = "0.19.5"; sha256 = "0cvxmc0r4ajnaah7lsppik61qickq7i0df4jwqaj6c6axiizhqlm"; }) + (fetchNuGet { pname = "OmniSharp.Extensions.LanguageServer.Shared"; version = "0.19.5"; sha256 = "0cczmmsmn3pj74wpasgfhjay1a817sd0zgzgqvvnckxxzq3n463h"; }) + (fetchNuGet { pname = "RangeTree"; version = "3.0.1"; sha256 = "19si88v2r0rc7kai1avwhigcvh3x3c916vrvqlyb59sn4f27pbm2"; }) + (fetchNuGet { pname = "runtime.any.System.Collections"; version = "4.3.0"; sha256 = "0bv5qgm6vr47ynxqbnkc7i797fdi8gbjjxii173syrx14nmrkwg0"; }) + (fetchNuGet { pname = "runtime.any.System.Diagnostics.Tracing"; version = "4.3.0"; sha256 = "00j6nv2xgmd3bi347k00m7wr542wjlig53rmj28pmw7ddcn97jbn"; }) + (fetchNuGet { pname = "runtime.any.System.Globalization"; version = "4.3.0"; sha256 = "1daqf33hssad94lamzg01y49xwndy2q97i2lrb7mgn28656qia1x"; }) + (fetchNuGet { pname = "runtime.any.System.IO"; version = "4.3.0"; sha256 = "0l8xz8zn46w4d10bcn3l4yyn4vhb3lrj2zw8llvz7jk14k4zps5x"; }) + (fetchNuGet { pname = "runtime.any.System.Reflection"; version = "4.3.0"; sha256 = "02c9h3y35pylc0zfq3wcsvc5nqci95nrkq0mszifc0sjx7xrzkly"; }) + (fetchNuGet { pname = "runtime.any.System.Reflection.Extensions"; version = "4.3.0"; sha256 = "0zyri97dfc5vyaz9ba65hjj1zbcrzaffhsdlpxc9bh09wy22fq33"; }) + (fetchNuGet { pname = "runtime.any.System.Reflection.Primitives"; version = "4.3.0"; sha256 = "0x1mm8c6iy8rlxm8w9vqw7gb7s1ljadrn049fmf70cyh42vdfhrf"; }) + (fetchNuGet { pname = "runtime.any.System.Resources.ResourceManager"; version = "4.3.0"; sha256 = "03kickal0iiby82wa5flar18kyv82s9s6d4xhk5h4bi5kfcyfjzl"; }) + (fetchNuGet { pname = "runtime.any.System.Runtime"; version = "4.3.0"; sha256 = "1cqh1sv3h5j7ixyb7axxbdkqx6cxy00p4np4j91kpm492rf4s25b"; }) + (fetchNuGet { pname = "runtime.any.System.Runtime.Handles"; version = "4.3.0"; sha256 = "0bh5bi25nk9w9xi8z23ws45q5yia6k7dg3i4axhfqlnj145l011x"; }) + (fetchNuGet { pname = "runtime.any.System.Runtime.InteropServices"; version = "4.3.0"; sha256 = "0c3g3g3jmhlhw4klrc86ka9fjbl7i59ds1fadsb2l8nqf8z3kb19"; }) + (fetchNuGet { pname = "runtime.any.System.Text.Encoding"; version = "4.3.0"; sha256 = "0aqqi1v4wx51h51mk956y783wzags13wa7mgqyclacmsmpv02ps3"; }) + (fetchNuGet { pname = "runtime.any.System.Text.Encoding.Extensions"; version = "4.3.0"; sha256 = "0lqhgqi0i8194ryqq6v2gqx0fb86db2gqknbm0aq31wb378j7ip8"; }) + (fetchNuGet { pname = "runtime.any.System.Threading.Tasks"; version = "4.3.0"; sha256 = "03mnvkhskbzxddz4hm113zsch1jyzh2cs450dk3rgfjp8crlw1va"; }) + (fetchNuGet { pname = "runtime.debian.8-x64.runtime.native.System.Security.Cryptography.OpenSsl"; version = "4.3.0"; sha256 = "16rnxzpk5dpbbl1x354yrlsbvwylrq456xzpsha1n9y3glnhyx9d"; }) + (fetchNuGet { pname = "runtime.fedora.23-x64.runtime.native.System.Security.Cryptography.OpenSsl"; version = "4.3.0"; sha256 = "0hkg03sgm2wyq8nqk6dbm9jh5vcq57ry42lkqdmfklrw89lsmr59"; }) + (fetchNuGet { pname = "runtime.fedora.24-x64.runtime.native.System.Security.Cryptography.OpenSsl"; version = "4.3.0"; sha256 = "0c2p354hjx58xhhz7wv6div8xpi90sc6ibdm40qin21bvi7ymcaa"; }) + (fetchNuGet { pname = "runtime.native.System"; version = "4.0.0"; sha256 = "1ppk69xk59ggacj9n7g6fyxvzmk1g5p4fkijm0d7xqfkig98qrkf"; }) + (fetchNuGet { pname = "runtime.native.System"; version = "4.3.0"; sha256 = "15hgf6zaq9b8br2wi1i3x0zvmk410nlmsmva9p0bbg73v6hml5k4"; }) + (fetchNuGet { pname = "runtime.native.System.Security.Cryptography.OpenSsl"; version = "4.3.0"; sha256 = "18pzfdlwsg2nb1jjjjzyb5qlgy6xjxzmhnfaijq5s2jw3cm3ab97"; }) + (fetchNuGet { pname = "runtime.opensuse.13.2-x64.runtime.native.System.Security.Cryptography.OpenSsl"; version = "4.3.0"; sha256 = "0qyynf9nz5i7pc26cwhgi8j62ps27sqmf78ijcfgzab50z9g8ay3"; }) + (fetchNuGet { pname = "runtime.opensuse.42.1-x64.runtime.native.System.Security.Cryptography.OpenSsl"; version = "4.3.0"; sha256 = "1klrs545awhayryma6l7g2pvnp9xy4z0r1i40r80zb45q3i9nbyf"; }) + (fetchNuGet { pname = "runtime.osx.10.10-x64.runtime.native.System.Security.Cryptography.OpenSsl"; version = "4.3.0"; sha256 = "0zcxjv5pckplvkg0r6mw3asggm7aqzbdjimhvsasb0cgm59x09l3"; }) + (fetchNuGet { pname = "runtime.rhel.7-x64.runtime.native.System.Security.Cryptography.OpenSsl"; version = "4.3.0"; sha256 = "0vhynn79ih7hw7cwjazn87rm9z9fj0rvxgzlab36jybgcpcgphsn"; }) + (fetchNuGet { pname = "runtime.ubuntu.14.04-x64.runtime.native.System.Security.Cryptography.OpenSsl"; version = "4.3.0"; sha256 = "160p68l2c7cqmyqjwxydcvgw7lvl1cr0znkw8fp24d1by9mqc8p3"; }) + (fetchNuGet { pname = "runtime.ubuntu.16.04-x64.runtime.native.System.Security.Cryptography.OpenSsl"; version = "4.3.0"; sha256 = "15zrc8fgd8zx28hdghcj5f5i34wf3l6bq5177075m2bc2j34jrqy"; }) + (fetchNuGet { pname = "runtime.ubuntu.16.10-x64.runtime.native.System.Security.Cryptography.OpenSsl"; version = "4.3.0"; sha256 = "1p4dgxax6p7rlgj4q73k73rslcnz4wdcv8q2flg1s8ygwcm58ld5"; }) + (fetchNuGet { pname = "runtime.unix.Microsoft.Win32.Primitives"; version = "4.3.0"; sha256 = "0y61k9zbxhdi0glg154v30kkq7f8646nif8lnnxbvkjpakggd5id"; }) + (fetchNuGet { pname = "runtime.unix.System.Diagnostics.Debug"; version = "4.3.0"; sha256 = "1lps7fbnw34bnh3lm31gs5c0g0dh7548wfmb8zz62v0zqz71msj5"; }) + (fetchNuGet { pname = "runtime.unix.System.IO.FileSystem"; version = "4.3.0"; sha256 = "14nbkhvs7sji5r1saj2x8daz82rnf9kx28d3v2qss34qbr32dzix"; }) + (fetchNuGet { pname = "runtime.unix.System.Private.Uri"; version = "4.3.0"; sha256 = "1jx02q6kiwlvfksq1q9qr17fj78y5v6mwsszav4qcz9z25d5g6vk"; }) + (fetchNuGet { pname = "runtime.unix.System.Runtime.Extensions"; version = "4.3.0"; sha256 = "0pnxxmm8whx38dp6yvwgmh22smknxmqs5n513fc7m4wxvs1bvi4p"; }) + (fetchNuGet { pname = "Serilog"; version = "2.12.0"; sha256 = "0lqxpc96qcjkv9pr1rln7mi4y7n7jdi4vb36c2fv3845w1vswgr4"; }) + (fetchNuGet { pname = "Serilog.Extensions.Logging"; version = "3.0.1"; sha256 = "069qy7dm5nxb372ij112ppa6m99b4iaimj3sji74m659fwrcrl9a"; }) + (fetchNuGet { pname = "Serilog.Settings.Configuration"; version = "3.1.0"; sha256 = "1cj5am4n073331gbfm2ylqb9cadl4q3ppzgwmm5c8m1drxpiwkb5"; }) + (fetchNuGet { pname = "Serilog.Sinks.Debug"; version = "2.0.0"; sha256 = "1i7j870l47gan3gpnnlzkccn5lbm7518cnkp25a3g5gp9l0dbwpw"; }) + (fetchNuGet { pname = "Serilog.Sinks.File"; version = "5.0.0"; sha256 = "097rngmgcrdfy7jy8j7dq3xaq2qky8ijwg0ws6bfv5lx0f3vvb0q"; }) + (fetchNuGet { pname = "System.AppContext"; version = "4.1.0"; sha256 = "0fv3cma1jp4vgj7a8hqc9n7hr1f1kjp541s6z0q1r6nazb4iz9mz"; }) + (fetchNuGet { pname = "System.Buffers"; version = "4.3.0"; sha256 = "0fgns20ispwrfqll4q1zc1waqcmylb3zc50ys9x8zlwxh9pmd9jy"; }) + (fetchNuGet { pname = "System.Collections"; version = "4.3.0"; sha256 = "19r4y64dqyrq6k4706dnyhhw7fs24kpp3awak7whzss39dakpxk9"; }) + (fetchNuGet { pname = "System.Collections.Immutable"; version = "1.7.0"; sha256 = "1gik4sn9jsi1wcy1pyyp0r4sn2g17cwrsh24b2d52vif8p2h24zx"; }) + (fetchNuGet { pname = "System.Collections.Immutable"; version = "1.7.1"; sha256 = "1nh4nlxfc7lbnbl86wwk1a3jwl6myz5j6hvgh5sp4krim9901hsq"; }) + (fetchNuGet { pname = "System.CommandLine"; version = "2.0.0-beta4.22272.1"; sha256 = "1iy5hwwgvx911g3yq65p4zsgpy08w4qz9j3h0igcf7yci44vw8yd"; }) + (fetchNuGet { pname = "System.Configuration.ConfigurationManager"; version = "6.0.0"; sha256 = "0sqapr697jbb4ljkq46msg0xx1qpmc31ivva6llyz2wzq3mpmxbw"; }) + (fetchNuGet { pname = "System.Diagnostics.Debug"; version = "4.3.0"; sha256 = "00yjlf19wjydyr6cfviaph3vsjzg3d5nvnya26i2fvfg53sknh3y"; }) + (fetchNuGet { pname = "System.Diagnostics.Tracing"; version = "4.3.0"; sha256 = "1m3bx6c2s958qligl67q7grkwfz3w53hpy7nc97mh6f7j5k168c4"; }) + (fetchNuGet { pname = "System.Drawing.Common"; version = "6.0.0"; sha256 = "02n8rzm58dac2np8b3xw8ychbvylja4nh6938l5k2fhyn40imlgz"; }) + (fetchNuGet { pname = "System.Dynamic.Runtime"; version = "4.0.11"; sha256 = "1pla2dx8gkidf7xkciig6nifdsb494axjvzvann8g2lp3dbqasm9"; }) + (fetchNuGet { pname = "System.Globalization"; version = "4.0.11"; sha256 = "070c5jbas2v7smm660zaf1gh0489xanjqymkvafcs4f8cdrs1d5d"; }) + (fetchNuGet { pname = "System.Globalization"; version = "4.3.0"; sha256 = "1cp68vv683n6ic2zqh2s1fn4c2sd87g5hpp6l4d4nj4536jz98ki"; }) + (fetchNuGet { pname = "System.IO"; version = "4.1.0"; sha256 = "1g0yb8p11vfd0kbkyzlfsbsp5z44lwsvyc0h3dpw6vqnbi035ajp"; }) + (fetchNuGet { pname = "System.IO"; version = "4.3.0"; sha256 = "05l9qdrzhm4s5dixmx68kxwif4l99ll5gqmh7rqgw554fx0agv5f"; }) + (fetchNuGet { pname = "System.IO.FileSystem"; version = "4.0.1"; sha256 = "0kgfpw6w4djqra3w5crrg8xivbanh1w9dh3qapb28q060wb9flp1"; }) + (fetchNuGet { pname = "System.IO.FileSystem.Primitives"; version = "4.3.0"; sha256 = "0j6ndgglcf4brg2lz4wzsh1av1gh8xrzdsn9f0yznskhqn1xzj9c"; }) + (fetchNuGet { pname = "System.IO.Pipelines"; version = "4.7.3"; sha256 = "0djp59x56klidi04xx8p5jc1nchv5zvd1d59diphqxwvgny3aawy"; }) + (fetchNuGet { pname = "System.Linq"; version = "4.1.0"; sha256 = "1ppg83svb39hj4hpp5k7kcryzrf3sfnm08vxd5sm2drrijsla2k5"; }) + (fetchNuGet { pname = "System.Linq.Async"; version = "6.0.1"; sha256 = "10ira8hmv0i54yp9ggrrdm1c06j538sijfjpn1kmnh9j2xk5yzmq"; }) + (fetchNuGet { pname = "System.Linq.Expressions"; version = "4.1.0"; sha256 = "1gpdxl6ip06cnab7n3zlcg6mqp7kknf73s8wjinzi4p0apw82fpg"; }) + (fetchNuGet { pname = "System.Memory"; version = "4.5.4"; sha256 = "14gbbs22mcxwggn0fcfs1b062521azb9fbb7c113x0mq6dzq9h6y"; }) + (fetchNuGet { pname = "System.Net.WebSockets"; version = "4.3.0"; sha256 = "1gfj800078kggcgl0xyl00a6y5k4wwh2k2qm69rjy22wbmq7fy4p"; }) + (fetchNuGet { pname = "System.ObjectModel"; version = "4.0.12"; sha256 = "1sybkfi60a4588xn34nd9a58png36i0xr4y4v4kqpg8wlvy5krrj"; }) + (fetchNuGet { pname = "System.Private.Uri"; version = "4.3.0"; sha256 = "04r1lkdnsznin0fj4ya1zikxiqr0h6r6a1ww2dsm60gqhdrf0mvx"; }) + (fetchNuGet { pname = "System.Reactive"; version = "4.4.1"; sha256 = "0gx8jh3hny2y5kijz5k9pxiqw481d013787c04zlhps21ygklw4a"; }) + (fetchNuGet { pname = "System.Reflection"; version = "4.1.0"; sha256 = "1js89429pfw79mxvbzp8p3q93il6rdff332hddhzi5wqglc4gml9"; }) + (fetchNuGet { pname = "System.Reflection"; version = "4.3.0"; sha256 = "0xl55k0mw8cd8ra6dxzh974nxif58s3k1rjv1vbd7gjbjr39j11m"; }) + (fetchNuGet { pname = "System.Reflection.Emit"; version = "4.0.1"; sha256 = "0ydqcsvh6smi41gyaakglnv252625hf29f7kywy2c70nhii2ylqp"; }) + (fetchNuGet { pname = "System.Reflection.Emit.ILGeneration"; version = "4.0.1"; sha256 = "1pcd2ig6bg144y10w7yxgc9d22r7c7ww7qn1frdfwgxr24j9wvv0"; }) + (fetchNuGet { pname = "System.Reflection.Emit.Lightweight"; version = "4.0.1"; sha256 = "1s4b043zdbx9k39lfhvsk68msv1nxbidhkq6nbm27q7sf8xcsnxr"; }) + (fetchNuGet { pname = "System.Reflection.Extensions"; version = "4.0.1"; sha256 = "0m7wqwq0zqq9gbpiqvgk3sr92cbrw7cp3xn53xvw7zj6rz6fdirn"; }) + (fetchNuGet { pname = "System.Reflection.Metadata"; version = "1.6.0"; sha256 = "1wdbavrrkajy7qbdblpbpbalbdl48q3h34cchz24gvdgyrlf15r4"; }) + (fetchNuGet { pname = "System.Reflection.Primitives"; version = "4.0.1"; sha256 = "1bangaabhsl4k9fg8khn83wm6yial8ik1sza7401621jc6jrym28"; }) + (fetchNuGet { pname = "System.Reflection.Primitives"; version = "4.3.0"; sha256 = "04xqa33bld78yv5r93a8n76shvc8wwcdgr1qvvjh959g3rc31276"; }) + (fetchNuGet { pname = "System.Reflection.TypeExtensions"; version = "4.1.0"; sha256 = "1bjli8a7sc7jlxqgcagl9nh8axzfl11f4ld3rjqsyxc516iijij7"; }) + (fetchNuGet { pname = "System.Resources.ResourceManager"; version = "4.0.1"; sha256 = "0b4i7mncaf8cnai85jv3wnw6hps140cxz8vylv2bik6wyzgvz7bi"; }) + (fetchNuGet { pname = "System.Resources.ResourceManager"; version = "4.3.0"; sha256 = "0sjqlzsryb0mg4y4xzf35xi523s4is4hz9q4qgdvlvgivl7qxn49"; }) + (fetchNuGet { pname = "System.Runtime"; version = "4.1.0"; sha256 = "02hdkgk13rvsd6r9yafbwzss8kr55wnj8d5c7xjnp8gqrwc8sn0m"; }) + (fetchNuGet { pname = "System.Runtime"; version = "4.3.0"; sha256 = "066ixvgbf2c929kgknshcxqj6539ax7b9m570cp8n179cpfkapz7"; }) + (fetchNuGet { pname = "System.Runtime.Caching"; version = "6.0.0"; sha256 = "0wh98a77cby4i3h2mar241k01105x661kh03vlyd399shxkfk60a"; }) + (fetchNuGet { pname = "System.Runtime.CompilerServices.Unsafe"; version = "4.4.0"; sha256 = "0a6ahgi5b148sl5qyfpyw383p3cb4yrkm802k29fsi4mxkiwir29"; }) + (fetchNuGet { pname = "System.Runtime.CompilerServices.Unsafe"; version = "4.7.0"; sha256 = "16r6sn4czfjk8qhnz7bnqlyiaaszr0ihinb7mq9zzr1wba257r54"; }) + (fetchNuGet { pname = "System.Runtime.CompilerServices.Unsafe"; version = "4.7.1"; sha256 = "119br3pd85lq8zcgh4f60jzmv1g976q1kdgi3hvqdlhfbw6siz2j"; }) + (fetchNuGet { pname = "System.Runtime.Extensions"; version = "4.1.0"; sha256 = "0rw4rm4vsm3h3szxp9iijc3ksyviwsv6f63dng3vhqyg4vjdkc2z"; }) + (fetchNuGet { pname = "System.Runtime.Extensions"; version = "4.3.0"; sha256 = "1ykp3dnhwvm48nap8q23893hagf665k0kn3cbgsqpwzbijdcgc60"; }) + (fetchNuGet { pname = "System.Runtime.Handles"; version = "4.0.1"; sha256 = "1g0zrdi5508v49pfm3iii2hn6nm00bgvfpjq1zxknfjrxxa20r4g"; }) + (fetchNuGet { pname = "System.Runtime.Handles"; version = "4.3.0"; sha256 = "0sw2gfj2xr7sw9qjn0j3l9yw07x73lcs97p8xfc9w1x9h5g5m7i8"; }) + (fetchNuGet { pname = "System.Runtime.InteropServices"; version = "4.1.0"; sha256 = "01kxqppx3dr3b6b286xafqilv4s2n0gqvfgzfd4z943ga9i81is1"; }) + (fetchNuGet { pname = "System.Runtime.InteropServices"; version = "4.3.0"; sha256 = "00hywrn4g7hva1b2qri2s6rabzwgxnbpw9zfxmz28z09cpwwgh7j"; }) + (fetchNuGet { pname = "System.Runtime.InteropServices.RuntimeInformation"; version = "4.0.0"; sha256 = "0glmvarf3jz5xh22iy3w9v3wyragcm4hfdr17v90vs7vcrm7fgp6"; }) + (fetchNuGet { pname = "System.Runtime.Numerics"; version = "4.3.0"; sha256 = "19rav39sr5dky7afygh309qamqqmi9kcwvz3i0c5700v0c5cg61z"; }) + (fetchNuGet { pname = "System.Security.AccessControl"; version = "4.6.0"; sha256 = "1wl1dyghi0qhpap1vgfhg2ybdyyhy9vc2a7dpm1xb30vfgmlkjmf"; }) + (fetchNuGet { pname = "System.Security.AccessControl"; version = "6.0.0"; sha256 = "0a678bzj8yxxiffyzy60z2w1nczzpi8v97igr4ip3byd2q89dv58"; }) + (fetchNuGet { pname = "System.Security.Cryptography.ProtectedData"; version = "6.0.0"; sha256 = "05kd3a8w7658hjxq9vvszxip30a479fjmfq4bq1r95nrsvs4hbss"; }) + (fetchNuGet { pname = "System.Security.Permissions"; version = "6.0.0"; sha256 = "0jsl4xdrkqi11iwmisi1r2f2qn5pbvl79mzq877gndw6ans2zhzw"; }) + (fetchNuGet { pname = "System.Security.Principal.Windows"; version = "4.6.0"; sha256 = "1jmfzfz1n8hp63s5lja5xxpzkinbp6g59l3km9h8avjiisdrg5wm"; }) + (fetchNuGet { pname = "System.Text.Encoding"; version = "4.0.11"; sha256 = "1dyqv0hijg265dwxg6l7aiv74102d6xjiwplh2ar1ly6xfaa4iiw"; }) + (fetchNuGet { pname = "System.Text.Encoding"; version = "4.3.0"; sha256 = "1f04lkir4iladpp51sdgmis9dj4y8v08cka0mbmsy0frc9a4gjqr"; }) + (fetchNuGet { pname = "System.Text.Encoding.CodePages"; version = "4.5.1"; sha256 = "1z21qyfs6sg76rp68qdx0c9iy57naan89pg7p6i3qpj8kyzn921w"; }) + (fetchNuGet { pname = "System.Text.Encoding.Extensions"; version = "4.3.0"; sha256 = "11q1y8hh5hrp5a3kw25cb6l00v5l5dvirkz8jr3sq00h1xgcgrxy"; }) + (fetchNuGet { pname = "System.Threading"; version = "4.0.11"; sha256 = "19x946h926bzvbsgj28csn46gak2crv2skpwsx80hbgazmkgb1ls"; }) + (fetchNuGet { pname = "System.Threading"; version = "4.3.0"; sha256 = "0rw9wfamvhayp5zh3j7p1yfmx9b5khbf4q50d8k5rk993rskfd34"; }) + (fetchNuGet { pname = "System.Threading.Channels"; version = "4.7.1"; sha256 = "038fyrriypwzsj5fwgnkw79hm5ya0x63r724yizgahbxf512chr2"; }) + (fetchNuGet { pname = "System.Threading.Tasks"; version = "4.0.11"; sha256 = "0nr1r41rak82qfa5m0lhk9mp0k93bvfd7bbd9sdzwx9mb36g28p5"; }) + (fetchNuGet { pname = "System.Threading.Tasks"; version = "4.3.0"; sha256 = "134z3v9abw3a6jsw17xl3f6hqjpak5l682k2vz39spj4kmydg6k7"; }) + (fetchNuGet { pname = "System.Threading.Tasks.Extensions"; version = "4.5.3"; sha256 = "0g7r6hm572ax8v28axrdxz1gnsblg6kszq17g51pj14a5rn2af7i"; }) + (fetchNuGet { pname = "System.Windows.Extensions"; version = "6.0.0"; sha256 = "1wy9pq9vn1bqg5qnv53iqrbx04yzdmjw4x5yyi09y3459vaa1sip"; }) + (fetchNuGet { pname = "Tomlyn"; version = "0.16.2"; sha256 = "1i928q6a7l65mk7wj2vvfclyvxamdjxg4dbj3g6g95inrfgvidah"; }) +] diff --git a/hacking/nix/scope/default.nix b/hacking/nix/scope/default.nix index 7d3936a62..53d33d810 100644 --- a/hacking/nix/scope/default.nix +++ b/hacking/nix/scope/default.nix @@ -145,6 +145,8 @@ superCallPackage ../rust-utils {} self // capdl-tool = callBuildBuildPackage ./capdl-tool {}; + dafny = callBuildBuildPackage ./dafny {}; + ### local tools mkTool = rootCrate: buildCrateInLayersHere { diff --git a/hacking/nix/scope/world/instances/dafny.nix b/hacking/nix/scope/world/instances/dafny.nix new file mode 100644 index 000000000..a2a824b43 --- /dev/null +++ b/hacking/nix/scope/world/instances/dafny.nix @@ -0,0 +1,65 @@ +# +# Copyright 2024, Colias Group, LLC +# +# SPDX-License-Identifier: BSD-2-Clause +# + +{ lib +, runCommand + +, dafny + +, sources +, crates +, crateUtils +, seL4Modifications +, mkTask + +, mkInstance + +, canSimulate +}: + +let + verifiedSrcDir = lib.cleanSource (sources.srcRoot + "/crates/private/tests/root-task/dafny/verified"); + verifiedName = "core"; + verifiedSrc = "${verifiedSrcDir}/${verifiedName}.dfy"; + + translated = runCommand "translated.rs" { + nativeBuildInputs = [ dafny ]; + } '' + dafny translate rs ${verifiedSrc} -o ${verifiedName} + mv ${verifiedName}-rust/src/${verifiedName}.rs $out + ''; + # TODO + # --standard-libraries \ + +in +mkInstance { + rootTask = mkTask rec { + rootCrate = crates.tests-root-task-dafny-task; + release = false; + + layers = [ + crateUtils.defaultIntermediateLayer + { + crates = [ "sel4-root-task" ]; + modifications = seL4Modifications; + } + ]; + + lastLayerModifications.modifyDerivation = drv: drv.overrideAttrs (attrs: { + nativeBuildInputs = (attrs.nativeBuildInputs or []) ++ [ + dafny + ]; + + TRANSLATED = translated; + }); + }; + + extraPlatformArgs = lib.optionalAttrs canSimulate { + canAutomateSimply = true; + }; +} // { + inherit translated; +} diff --git a/hacking/nix/scope/world/instances/default.nix b/hacking/nix/scope/world/instances/default.nix index ea5d4cf6f..bcebd3d92 100644 --- a/hacking/nix/scope/world/instances/default.nix +++ b/hacking/nix/scope/world/instances/default.nix @@ -206,6 +206,10 @@ in rec { inherit canSimulate; }); + dafny = maybe haveFullRuntime (callPackage ./dafny.nix { + inherit canSimulate; + }); + default-test-harness = maybe (haveFullRuntime && haveUnwindingSupport) (mkInstance { rootTask = mkTask { rootCrate = crates.tests-root-task-default-test-harness;