Skip to content

Commit 9a2ad56

Browse files
author
Grant Wuerker
committed
hacking
1 parent 1e7c7d2 commit 9a2ad56

File tree

6 files changed

+253
-166
lines changed

6 files changed

+253
-166
lines changed

‎crates/library/std/src/buf.fe

+1-1
Original file line numberDiff line numberDiff line change
@@ -215,7 +215,7 @@ pub struct MemoryBufferReader {
215215
let offset: u256 = self.read_offset(len: 1)
216216
unsafe {
217217
let value: u256 = evm::mload(offset)
218-
return u8(evm::byte(offset: 0, value))
218+
return u8(evm::shr(bits: 248, value))
219219
}
220220
}
221221

‎crates/specgen/fixtures/basic_equivalence.fe

+64
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,64 @@
1+
use std::evm
2+
use std::spec
3+
4+
// #invariant
5+
// fn de_morgan_true(a: bool, b: bool) {
6+
// spec::given_true(a and b)
7+
// spec::assert_true(not ((not a) or (not b)))
8+
// }
9+
10+
// #invariant
11+
// fn de_morgan_false(a: bool, b: bool) {
12+
// spec::given_false(a and b)
13+
// spec::assert_false(not ((not a) or (not b)))
14+
// }
15+
16+
// #invariant
17+
// fn shl_shr_255(a: u256) {
18+
// spec::given_lte(a, 255)
19+
20+
// let shl_a: u256 = evm::shl(bits: 248, value: a)
21+
// spec::assert_eq(
22+
// a,
23+
// evm::shr(bits: 248, value: shl_a)
24+
// )
25+
// }
26+
27+
// #invariant
28+
// fn shl_shr_n(a: u256, n: u256) {
29+
// spec::given_lte(a, 255)
30+
// spec::given_lte(n, 248)
31+
32+
// let shl_a: u256 = evm::shl(bits: n, value: a)
33+
// spec::assert_eq(
34+
// a,
35+
// evm::shr(bits: n, value: shl_a)
36+
// )
37+
// }
38+
39+
// #invariant
40+
// fn shl_byte(a: u256) {
41+
// spec::given_lte(a, 255)
42+
43+
// let shl_a: u256 = evm::shl(bits: 248, value: a)
44+
// spec::assert_eq(
45+
// a,
46+
// evm::byte(offset: 0, value: shl_a)
47+
// )
48+
// }
49+
50+
const FREE_MEM_PTR: u256 = 4096
51+
52+
#invariant
53+
unsafe fn read_byte(a: u8) {
54+
// evm::mstore8(offset: FREE_MEM_PTR, value: a)
55+
evm::mstore(
56+
offset: FREE_MEM_PTR,
57+
value: evm::shl(bits: 248, value: a)
58+
)
59+
60+
spec::assert_eq(
61+
a,
62+
evm::shr(bits: 248, value: evm::mload(offset: FREE_MEM_PTR))
63+
)
64+
}

‎crates/specgen/fixtures/buf.fe

+27-4
Original file line numberDiff line numberDiff line change
@@ -14,14 +14,37 @@ use std::spec
1414
// spec::assert_eq(reader.read_u8(), b)
1515
// }
1616

17+
// #invariant
18+
// fn rw_single_u8(a: u8) {
19+
// let mut buf: MemoryBuffer = MemoryBuffer::new(len: 1)
20+
// let mut reader: MemoryBufferReader = buf.reader()
21+
// let mut writer: MemoryBufferWriter = buf.writer()
22+
23+
// writer.write_u8(value: a)
24+
// spec::assert_eq(reader.read_u8(), a)
25+
// }
26+
27+
// #invariant
28+
// fn rw_single_u16(a: u16) {
29+
// let mut buf: MemoryBuffer = MemoryBuffer::new(len: 2)
30+
// let mut reader: MemoryBufferReader = buf.reader()
31+
// let mut writer: MemoryBufferWriter = buf.writer()
32+
33+
// writer.write_u16(value: a)
34+
// spec::assert_eq(reader.read_u16(), a)
35+
// }
36+
1737
#invariant
18-
fn rw_single_u8(a: u8) {
19-
let mut buf: MemoryBuffer = MemoryBuffer::new(len: 1)
38+
fn rw_u16(a: u16, b: u16) {
39+
let mut buf: MemoryBuffer = MemoryBuffer::new(len: 4)
2040
let mut reader: MemoryBufferReader = buf.reader()
2141
let mut writer: MemoryBufferWriter = buf.writer()
2242

23-
writer.write_u8(value: a)
24-
spec::assert_eq(reader.read_u8(), a)
43+
writer.write_u16(value: a)
44+
writer.write_u16(value: b)
45+
46+
spec::assert_eq(reader.read_u16(), a)
47+
spec::assert_eq(reader.read_u16(), b)
2548
}
2649

2750

‎crates/specgen/fixtures/sanity.fe

+53-54
Original file line numberDiff line numberDiff line change
@@ -1,54 +1,53 @@
11
// use std::{evm, spec}
22
use std::spec
33
use std::evm
4-
use std::buf::{MemoryBuffer, MemoryBufferWriter, MemoryBufferReader}
54

6-
#invariant
7-
fn simple1(a: u256) {
8-
spec::given_lte(a, 26)
5+
// #invariant
6+
// fn simple1(a: u256) {
7+
// spec::given_lte(a, 26)
98

10-
spec::assert_lte(a, 42)
11-
}
9+
// spec::assert_lte(a, 42)
10+
// }
1211

13-
#invariant
14-
fn simple2(a: u256) {
15-
spec::given_lte(a, 42)
12+
// #invariant
13+
// fn simple2(a: u256) {
14+
// spec::given_lte(a, 42)
1615

17-
spec::assert_ne(a, 43)
18-
}
16+
// spec::assert_ne(a, 43)
17+
// }
1918

20-
#invariant
21-
fn simple3(a: u256, b: u256) {
22-
spec::given_lte(a, b)
23-
spec::given_eq(a, 42)
19+
// #invariant
20+
// fn simple3(a: u256, b: u256) {
21+
// spec::given_lte(a, b)
22+
// spec::given_eq(a, 42)
2423

25-
spec::assert_ne(b, 26)
26-
}
24+
// spec::assert_ne(b, 26)
25+
// }
2726

28-
#invariant
29-
fn simple4(a: u256, b: u256) {
30-
spec::given_lte(a, 42)
31-
spec::given_lte(b, 26)
27+
// #invariant
28+
// fn simple4(a: u256, b: u256) {
29+
// spec::given_lte(a, 42)
30+
// spec::given_lte(b, 26)
3231

33-
spec::assert_lte(evm::add(a, b), 68)
34-
}
32+
// spec::assert_lte(evm::add(a, b), 68)
33+
// }
3534

36-
#invariant
37-
fn simple5(a: u256) {
38-
spec::given_lte(a, 42)
39-
spec::given_gte(a, 26)
35+
// #invariant
36+
// fn simple5(a: u256) {
37+
// spec::given_lte(a, 42)
38+
// spec::given_gte(a, 26)
4039

41-
spec::assert_ne(a, 25)
42-
spec::assert_ne(a, 45)
43-
}
40+
// spec::assert_ne(a, 25)
41+
// spec::assert_ne(a, 45)
42+
// }
4443

45-
#invariant
46-
fn simple6(a: u256) {
47-
spec::given_lte(a, 42)
48-
spec::given_gte(a, 42)
44+
// #invariant
45+
// fn simple6(a: u256) {
46+
// spec::given_lte(a, 42)
47+
// spec::given_gte(a, 42)
4948

50-
spec::assert_eq(a, 42)
51-
}
49+
// spec::assert_eq(a, 42)
50+
// }
5251

5352
// fn sq(_ a: u256) -> u256 {
5453
// return evm::mul(a, a)
@@ -72,25 +71,25 @@ fn simple6(a: u256) {
7271
// spec::assert_eq(c, 5)
7372
// }
7473

75-
#invariant
76-
fn simple8(a: u256, b: u256, c: u256) {
77-
spec::given_lte(a, 1023)
78-
spec::given_lte(b, 1023)
79-
spec::given_lte(c, 1023)
74+
// #invariant
75+
// fn simple8(a: u256, b: u256, c: u256) {
76+
// spec::given_lte(a, 1023)
77+
// spec::given_lte(b, 1023)
78+
// spec::given_lte(c, 1023)
8079

81-
// a + b = c
82-
spec::given_eq(evm::add(a, b), c)
83-
spec::given_eq(a, 42)
84-
spec::given_eq(c, 68)
80+
// // a + b = c
81+
// spec::given_eq(evm::add(a, b), c)
82+
// spec::given_eq(a, 42)
83+
// spec::given_eq(c, 68)
8584

86-
spec::assert_eq(b, 26)
87-
}
85+
// spec::assert_eq(b, 26)
86+
// }
8887

89-
#invariant
90-
fn simple9(a: bool, b: bool) {
91-
spec::given_false(a)
92-
spec::given_true(b)
88+
// #invariant
89+
// fn simple9(a: bool, b: bool) {
90+
// spec::given_false(a)
91+
// spec::given_true(b)
9392

94-
spec::assert_true(a or b)
95-
spec::assert_false(a and b)
96-
}
93+
// spec::assert_true(a or b)
94+
// spec::assert_false(a and b)
95+
// }

‎specs/rw-single-u8-spec.k

-107
This file was deleted.

0 commit comments

Comments
 (0)