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