hacking

crates/library/std/src/buf.fe

@@ -215,7 +215,7 @@ pub struct MemoryBufferReader {
         let offset: u256 = self.read_offset(len: 1)
         unsafe {
             let value: u256 = evm::mload(offset)
-            return u8(evm::byte(offset: 0, value))
+            return u8(evm::shr(bits: 248, value))
         }
     }
 

crates/specgen/fixtures/basic_equivalence.fe

@@ -0,0 +1,64 @@
+use std::evm
+use std::spec
+
+// #invariant
+// fn de_morgan_true(a: bool, b: bool) {
+//     spec::given_true(a and b)
+//     spec::assert_true(not ((not a) or (not b)))
+// }
+
+// #invariant
+// fn de_morgan_false(a: bool, b: bool) {
+//     spec::given_false(a and b)
+//     spec::assert_false(not ((not a) or (not b)))
+// }
+
+// #invariant
+// fn shl_shr_255(a: u256) {
+//     spec::given_lte(a, 255)
+
+//     let shl_a: u256 = evm::shl(bits: 248, value: a)
+//     spec::assert_eq(
+//         a,
+//         evm::shr(bits: 248, value: shl_a)
+//     )
+// }
+
+// #invariant
+// fn shl_shr_n(a: u256, n: u256) {
+//     spec::given_lte(a, 255)
+//     spec::given_lte(n, 248)
+
+//     let shl_a: u256 = evm::shl(bits: n, value: a)
+//     spec::assert_eq(
+//         a,
+//         evm::shr(bits: n, value: shl_a)
+//     )
+// }
+
+// #invariant
+// fn shl_byte(a: u256) {
+//     spec::given_lte(a, 255)
+
+//     let shl_a: u256 = evm::shl(bits: 248, value: a)
+//     spec::assert_eq(
+//         a,
+//         evm::byte(offset: 0, value: shl_a)
+//     )
+// }
+
+const FREE_MEM_PTR: u256 = 4096
+
+#invariant
+unsafe fn read_byte(a: u8) {
+    // evm::mstore8(offset: FREE_MEM_PTR, value: a)
+    evm::mstore(
+        offset: FREE_MEM_PTR, 
+        value: evm::shl(bits: 248, value: a)
+    )
+
+    spec::assert_eq(
+        a,
+        evm::shr(bits: 248, value: evm::mload(offset: FREE_MEM_PTR))
+    )
+}

crates/specgen/fixtures/buf.fe

@@ -14,14 +14,37 @@ use std::spec
 //     spec::assert_eq(reader.read_u8(), b)
 // }
 
+// #invariant
+// fn rw_single_u8(a: u8) {
+//     let mut buf: MemoryBuffer = MemoryBuffer::new(len: 1)
+//     let mut reader: MemoryBufferReader = buf.reader()
+//     let mut writer: MemoryBufferWriter = buf.writer()
+
+//     writer.write_u8(value: a)
+//     spec::assert_eq(reader.read_u8(), a)
+// }
+
+// #invariant
+// fn rw_single_u16(a: u16) {
+//     let mut buf: MemoryBuffer = MemoryBuffer::new(len: 2)
+//     let mut reader: MemoryBufferReader = buf.reader()
+//     let mut writer: MemoryBufferWriter = buf.writer()
+
+//     writer.write_u16(value: a)
+//     spec::assert_eq(reader.read_u16(), a)
+// }
+
 #invariant
-fn rw_single_u8(a: u8) {
-    let mut buf: MemoryBuffer = MemoryBuffer::new(len: 1)
+fn rw_u16(a: u16, b: u16) {
+    let mut buf: MemoryBuffer = MemoryBuffer::new(len: 4)
     let mut reader: MemoryBufferReader = buf.reader()
     let mut writer: MemoryBufferWriter = buf.writer()
 
-    writer.write_u8(value: a)
-    spec::assert_eq(reader.read_u8(), a)
+    writer.write_u16(value: a)
+    writer.write_u16(value: b)
+
+    spec::assert_eq(reader.read_u16(), a)
+    spec::assert_eq(reader.read_u16(), b)
 }
 
 

crates/specgen/fixtures/sanity.fe

@@ -1,54 +1,53 @@
 // use std::{evm, spec}
 use std::spec
 use std::evm
-use std::buf::{MemoryBuffer, MemoryBufferWriter, MemoryBufferReader}
 
-#invariant
-fn simple1(a: u256) {
-    spec::given_lte(a, 26)
+// #invariant
+// fn simple1(a: u256) {
+//     spec::given_lte(a, 26)
 
-    spec::assert_lte(a, 42)
-}
+//     spec::assert_lte(a, 42)
+// }
 
-#invariant
-fn simple2(a: u256) {
-    spec::given_lte(a, 42)
+// #invariant
+// fn simple2(a: u256) {
+//     spec::given_lte(a, 42)
 
-    spec::assert_ne(a, 43)
-}
+//     spec::assert_ne(a, 43)
+// }
 
-#invariant
-fn simple3(a: u256, b: u256) {
-    spec::given_lte(a, b)
-    spec::given_eq(a, 42)
+// #invariant
+// fn simple3(a: u256, b: u256) {
+//     spec::given_lte(a, b)
+//     spec::given_eq(a, 42)
 
-    spec::assert_ne(b, 26)
-}
+//     spec::assert_ne(b, 26)
+// }
 
-#invariant
-fn simple4(a: u256, b: u256) {
-    spec::given_lte(a, 42)
-    spec::given_lte(b, 26)
+// #invariant
+// fn simple4(a: u256, b: u256) {
+//     spec::given_lte(a, 42)
+//     spec::given_lte(b, 26)
 
-    spec::assert_lte(evm::add(a, b), 68)
-}
+//     spec::assert_lte(evm::add(a, b), 68)
+// }
 
-#invariant
-fn simple5(a: u256) {
-    spec::given_lte(a, 42)
-    spec::given_gte(a, 26)
+// #invariant
+// fn simple5(a: u256) {
+//     spec::given_lte(a, 42)
+//     spec::given_gte(a, 26)
 
-    spec::assert_ne(a, 25)
-    spec::assert_ne(a, 45)
-}
+//     spec::assert_ne(a, 25)
+//     spec::assert_ne(a, 45)
+// }
 
-#invariant
-fn simple6(a: u256) {
-    spec::given_lte(a, 42)
-    spec::given_gte(a, 42)
+// #invariant
+// fn simple6(a: u256) {
+//     spec::given_lte(a, 42)
+//     spec::given_gte(a, 42)
 
-    spec::assert_eq(a, 42)
-}
+//     spec::assert_eq(a, 42)
+// }
 
 // fn sq(_ a: u256) -> u256 {
 //     return evm::mul(a, a)
@@ -72,25 +71,25 @@ fn simple6(a: u256) {
 //     spec::assert_eq(c, 5)
 // }
 
-#invariant
-fn simple8(a: u256, b: u256, c: u256) {
-    spec::given_lte(a, 1023)
-    spec::given_lte(b, 1023)
-    spec::given_lte(c, 1023)
+// #invariant
+// fn simple8(a: u256, b: u256, c: u256) {
+//     spec::given_lte(a, 1023)
+//     spec::given_lte(b, 1023)
+//     spec::given_lte(c, 1023)
 
-    // a + b = c
-    spec::given_eq(evm::add(a, b), c)
-    spec::given_eq(a, 42)
-    spec::given_eq(c, 68)
+//     // a + b = c
+//     spec::given_eq(evm::add(a, b), c)
+//     spec::given_eq(a, 42)
+//     spec::given_eq(c, 68)
 
-    spec::assert_eq(b, 26)
-}
+//     spec::assert_eq(b, 26)
+// }
 
-#invariant
-fn simple9(a: bool, b: bool) {
-    spec::given_false(a)
-    spec::given_true(b)
+// #invariant
+// fn simple9(a: bool, b: bool) {
+//     spec::given_false(a)
+//     spec::given_true(b)
 
-    spec::assert_true(a or b)
-    spec::assert_false(a and b)
-}
+//     spec::assert_true(a or b)
+//     spec::assert_false(a and b)
+// }