Add Dafny test

Signed-off-by: Nick Spinale <[email protected]>

.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.

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",

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"]; };
+  };
+}

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 <[email protected]>"]
+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"

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);
+}

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);
+    }
+}

crates/private/tests/root-task/dafny/hacking/.gitignore

@@ -0,0 +1,7 @@
+#
+# Copyright 2024, Colias Group, LLC
+#
+# SPDX-License-Identifier: BSD-2-Clause
+#
+
+/build/

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

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;
+})

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
+    ;
+  };
+}