pyrox.dev
1{
2 lib,
3 pkgs,
4 ...
5}:
6{
7 name = "owi";
8
9 meta.maintainers = with lib.maintainers; [ ethancedwards8 ];
10
11 nodes.machine = {
12 environment.systemPackages = with pkgs; [ owi ];
13
14 environment.etc."owipass.rs".source = pkgs.writeText "owi.rs" ''
15 use owi_sym::Symbolic;
16
17 fn mean_one(x: i32, y: i32) -> i32 {
18 (x + y)/2
19 }
20
21 fn mean_two(x: i32, y: i32) -> i32 {
22 (y + x)/2
23 }
24
25 fn main() {
26 let x = i32::symbol();
27 let y = i32::symbol();
28 // proving the commutative property of addition!
29 owi_sym::assert(mean_one(x, y) == mean_two(x, y))
30 }
31 '';
32
33 environment.etc."owifail.rs".source = pkgs.writeText "owi.rs" ''
34 use owi_sym::Symbolic;
35
36 fn mean_wrong(x: i32, y: i32) -> i32 {
37 (x + y) / 2
38 }
39
40 fn mean_correct(x: i32, y: i32) -> i32 {
41 (x & y) + ((x ^ y) >> 1)
42 }
43
44 fn main() {
45 let x = i32::symbol();
46 let y = i32::symbol();
47 owi_sym::assert(mean_wrong(x, y) == mean_correct(x, y))
48 }
49 '';
50 };
51
52 testScript =
53 { nodes, ... }:
54 ''
55 start_all()
56
57 # testing
58 machine.succeed("owi rust --fail-on-assertion-only /etc/owipass.rs")
59 machine.fail("owi rust --fail-on-assertion-only /etc/owifail.rs")
60 '';
61}