Skip to content

Commit 4bb93b7

Browse files
author
Grant Wuerker
committed
hacking
1 parent b4ecfc6 commit 4bb93b7

File tree

12 files changed

+132
-126
lines changed

12 files changed

+132
-126
lines changed

‎crates/proof-service/fixtures/basic_equivalence.fe‎ renamed to ‎crates/fe/fixtures/basic_equivalence.fe‎

File renamed without changes.

‎crates/proof-service/fixtures/buf.fe‎ renamed to ‎crates/fe/fixtures/buf.fe‎

File renamed without changes.

‎crates/proof-service/fixtures/sanity.fe‎ renamed to ‎crates/fe/fixtures/sanity.fe‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -74,7 +74,7 @@ fn sq(_ a: u256) -> u256 {
7474
fn simple8(a: u256, b: u256, c: u256) {
7575
spec::given_eq(a, 42)
7676
spec::given_eq(c, 68)
77-
spec::given_lte(c, 1023)
77+
spec::given_eq(b, 1023)
7878

7979
// a + b = c
8080
spec::given_eq(evm::add(a, b), c)

‎crates/fe/src/task/prove.rs‎

Lines changed: 7 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,11 @@
11
#![cfg(feature = "solc-backend")]
2-
use std::fs;
3-
use std::io::{Error, Write};
4-
use std::path::Path;
5-
62
use clap::Args;
73
use fe_common::diagnostics::print_diagnostics;
8-
use fe_parser::ast::SmolStr;
94
use fe_proof_service::invariant::Invariant;
10-
use fe_proof_service::ProofServer;
5+
use fe_proof_service::ProofClient;
116

12-
const DEFAULT_OUTPUT_DIR_NAME: &str = "prove";
13-
const DEFAULT_INGOT: &str = "main";
7+
// const DEFAULT_OUTPUT_DIR_NAME: &str = "prove";
8+
// const DEFAULT_INGOT: &str = "main";
149

1510
#[derive(Args)]
1611
#[clap(about = "Generate specs for the current project")]
@@ -45,9 +40,11 @@ fn single_file_invariants(prove_arg: &ProveArgs) -> Vec<Invariant> {
4540

4641
pub fn prove(prove_arg: ProveArgs) {
4742
let invariants = single_file_invariants(&prove_arg);
48-
let server = ProofServer::new("127.0.0.1:7878");
43+
let server = ProofClient::new("127.0.0.1:7878");
4944

5045
for invariant in invariants {
51-
server.prove_invariant(invariant)
46+
let name = invariant.name.clone();
47+
let status = server.check_invariant(invariant);
48+
println!("{} (status: {})", &name, &status)
5249
}
5350
}

‎crates/kevm-proof-service/db.yaml‎

Lines changed: 11 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -1,33 +1,18 @@
1-
8487165461598368627:
2-
name: read_byte_shl_248
3-
complete: true
4-
8340690516531694925:
5-
name: shl_shr_248
6-
complete: true
7-
6859094145672656092:
8-
name: shl_shr_n
9-
complete: true
10-
1178386169830789967:
11-
name: de_morgan_true
12-
complete: true
13-
8335179070820156628:
14-
name: de_morgan_false
15-
complete: true
161
5577730546396304772:
172
name: simple1
183
complete: true
4+
6899393809540637772:
5+
name: simple10
6+
complete: true
197
8550010896920530121:
208
name: simple2
219
complete: true
22-
11277133206842314137:
23-
name: simple10
24-
complete: false
10+
8815378979428746437:
11+
name: simple6
12+
complete: true
2513
1316233277346233274:
2614
name: simple4
2715
complete: true
28-
5794060644489626698:
29-
name: simple6
30-
complete: false
3116
3765551559799037737:
3217
name: simple3
3318
complete: true
@@ -37,15 +22,12 @@
3722
5801784128720014789:
3823
name: simple9
3924
complete: true
40-
6899393809540637772:
41-
name: simple10
42-
complete: true
4325
10197623413532063304:
4426
name: simple8
4527
complete: false
46-
8815378979428746437:
47-
name: simple6
48-
complete: true
49-
4420712366820074710:
50-
name: rw_single_u16
28+
8128742196276399630:
29+
name: simple8
5130
complete: false
31+
6899926631315549094:
32+
name: simple8
33+
complete: true

‎crates/kevm-proof-service/server.state‎

Lines changed: 5 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -1,34 +1,18 @@
1-
SystemTime { tv_sec: 1686773923, tv_nsec: 119329865 }
1+
SystemTime { tv_sec: 1686938059, tv_nsec: 232547015 }
22
queue:
3-
name: rw_u8 id: 5409945868159526208 status: Proving
4-
name: rw_single_u8 id: 13520367379030342094 status: Proving
5-
name: rw_u16 id: 7310750552394920380 status: Proving
6-
name: rw_u256 id: 6262901239181954336 status: Proving
7-
name: rw_mix id: 3205383054861803913 status: Proving
83

94
execution pool:
10-
5409945868159526208
11-
13520367379030342094
12-
3205383054861803913
13-
7310750552394920380
14-
6262901239181954336
155

166
db:
17-
id: 8487165461598368627 entry: (name: read_byte_shl_248 complete: true)
18-
id: 8340690516531694925 entry: (name: shl_shr_248 complete: true)
19-
id: 6859094145672656092 entry: (name: shl_shr_n complete: true)
20-
id: 1178386169830789967 entry: (name: de_morgan_true complete: true)
21-
id: 8335179070820156628 entry: (name: de_morgan_false complete: true)
227
id: 5577730546396304772 entry: (name: simple1 complete: true)
8+
id: 6899393809540637772 entry: (name: simple10 complete: true)
239
id: 8550010896920530121 entry: (name: simple2 complete: true)
24-
id: 11277133206842314137 entry: (name: simple10 complete: false)
10+
id: 8815378979428746437 entry: (name: simple6 complete: true)
2511
id: 1316233277346233274 entry: (name: simple4 complete: true)
26-
id: 5794060644489626698 entry: (name: simple6 complete: false)
2712
id: 3765551559799037737 entry: (name: simple3 complete: true)
2813
id: 17173750684762914309 entry: (name: simple5 complete: true)
2914
id: 5801784128720014789 entry: (name: simple9 complete: true)
30-
id: 6899393809540637772 entry: (name: simple10 complete: true)
3115
id: 10197623413532063304 entry: (name: simple8 complete: false)
32-
id: 8815378979428746437 entry: (name: simple6 complete: true)
33-
id: 4420712366820074710 entry: (name: rw_single_u16 complete: false)
16+
id: 8128742196276399630 entry: (name: simple8 complete: false)
17+
id: 6899926631315549094 entry: (name: simple8 complete: true)
3418

‎crates/kevm-proof-service/src/main.rs‎

Lines changed: 17 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,10 @@
1-
use fe_proof_service::{invariant::Invariant, serde_json};
1+
use fe_proof_service::{invariant::Invariant, serde_json, ProofStatus};
22
use std::{
33
fs,
4-
io::BufReader,
4+
io::{BufRead, BufReader, BufWriter, Write},
55
net::{TcpListener, TcpStream},
6+
thread,
7+
time::Duration,
68
};
79

810
use server_impl::Server;
@@ -23,8 +25,17 @@ fn main() {
2325
}
2426

2527
fn connection_handler(server: &mut Server, mut stream: TcpStream) {
26-
let buf_reader = BufReader::new(&mut stream);
27-
let invariant: Invariant =
28-
serde_json::from_reader(buf_reader).expect("unable to decode invariant");
29-
server.add_invariant(invariant)
28+
let mut stream_clone = stream.try_clone().unwrap();
29+
30+
let mut reader = BufReader::new(&mut stream);
31+
let mut writer = BufWriter::new(&mut stream_clone);
32+
33+
let invariant: Invariant = {
34+
let mut invariant_encoded = String::new();
35+
reader.read_line(&mut invariant_encoded).unwrap();
36+
serde_json::from_str(&invariant_encoded).expect("unable to decode invariant")
37+
};
38+
39+
let status = server.check_invariant(invariant);
40+
serde_json::to_writer(&mut writer, &status).expect("unable to decode invariant");
3041
}

‎crates/kevm-proof-service/src/server_impl/db.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -68,7 +68,7 @@ impl Db {
6868
self.entries.insert(id, entry);
6969
}
7070

71-
pub fn get(&mut self, id: u64) -> Option<&DbEntry> {
71+
pub fn get(&self, id: u64) -> Option<&DbEntry> {
7272
self.entries.get(&id)
7373
}
7474

‎crates/kevm-proof-service/src/server_impl/mod.rs‎

Lines changed: 34 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,10 @@ use std::{
77
time::{self, Duration},
88
};
99

10-
use fe_proof_service::invariant::Invariant;
10+
use fe_proof_service::{
11+
invariant::{Invariant, InvariantHeader},
12+
ProofStatus,
13+
};
1114
use indexmap::{indexmap, IndexMap};
1215
use kevm::KSpecExecPool;
1316
use smol_str::SmolStr;
@@ -16,10 +19,7 @@ mod db;
1619
mod queue;
1720

1821
use self::{db::Db, queue::Spec};
19-
use self::{
20-
db::DbEntry,
21-
queue::{ProofStatus, Queue},
22-
};
22+
use self::{db::DbEntry, queue::Queue};
2323

2424
pub struct Server {
2525
state: Arc<Mutex<ServerState>>,
@@ -41,9 +41,12 @@ impl Server {
4141
Self { state }
4242
}
4343

44-
pub fn add_invariant(&mut self, invariant: Invariant) {
44+
pub fn check_invariant(&mut self, invariant: Invariant) -> ProofStatus {
45+
let id = invariant.id();
4546
let spec = Spec::new_from_invariant(invariant);
46-
self.state.lock().unwrap().add_spec(spec)
47+
self.state.lock().unwrap().add_spec(spec);
48+
self.state.lock().unwrap().update();
49+
self.state.lock().unwrap().proof_status(id)
4750
}
4851

4952
// pub fn display<W>(&self, mut writer: W)
@@ -110,11 +113,30 @@ impl ServerState {
110113
self.queue.push_spec(spec)
111114
}
112115

116+
pub fn proof_status(&self, invariant_id: u64) -> ProofStatus {
117+
if let Some(entry) = self.db.get(invariant_id) {
118+
if entry.complete {
119+
ProofStatus::Complete
120+
} else {
121+
ProofStatus::Incomplete
122+
}
123+
} else {
124+
for spec in &self.queue.specs {
125+
if spec.invariant_id == invariant_id {
126+
return spec.status;
127+
}
128+
}
129+
130+
panic!("missing invariant")
131+
}
132+
}
133+
113134
pub fn update(&mut self) {
114135
let mut first_indices: IndexMap<u64, usize> = indexmap! {};
115136

116137
let mut renames: Vec<(usize, SmolStr)> = vec![];
117138
let mut removals: Vec<usize> = vec![];
139+
let mut db_changed = false;
118140

119141
for (index, spec) in self.queue.specs.iter_mut().enumerate() {
120142
if let Some(first_index) = first_indices.get(&spec.invariant_id) {
@@ -157,18 +179,21 @@ impl ServerState {
157179
self.db
158180
.update(spec.invariant_id, DbEntry::new(spec.name.clone(), true));
159181
removals.push(index);
182+
db_changed = true
160183
}
161184
ProofStatus::Incomplete => {
162185
self.db
163186
.update(spec.invariant_id, DbEntry::new(spec.name.clone(), false));
164187
removals.push(index);
188+
db_changed = true
165189
}
166190
}
167191
}
168192
}
169193

170-
// todo only write if updated
171-
self.db.write();
194+
if db_changed {
195+
self.db.write();
196+
}
172197

173198
for (index, name) in renames {
174199
self.queue.specs[index].name = name

‎crates/kevm-proof-service/src/server_impl/queue.rs‎

Lines changed: 5 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -1,36 +1,12 @@
1-
use std::{
2-
fmt::Display,
3-
fs,
4-
io::Write,
5-
sync::{Arc, Mutex},
6-
thread,
7-
};
1+
use std::fmt::Display;
82

9-
use fe_proof_service::invariant::{Invariant, InvariantBody};
3+
use fe_proof_service::{
4+
invariant::{Invariant, InvariantBody},
5+
ProofStatus,
6+
};
107
use kevm::{KSpec, KSpecType};
118
use smol_str::SmolStr;
129

13-
#[derive(PartialEq, Eq)]
14-
pub enum ProofStatus {
15-
New,
16-
Ready,
17-
Proving,
18-
Complete,
19-
Incomplete,
20-
}
21-
22-
impl Display for &ProofStatus {
23-
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
24-
match self {
25-
ProofStatus::New => write!(f, "New"),
26-
ProofStatus::Ready => write!(f, "Ready"),
27-
ProofStatus::Proving => write!(f, "Proving"),
28-
ProofStatus::Complete => write!(f, "Complete"),
29-
ProofStatus::Incomplete => write!(f, "Incomplete"),
30-
}
31-
}
32-
}
33-
3410
pub struct Spec {
3511
pub name: SmolStr,
3612
pub k_spec: KSpec,

0 commit comments

Comments
 (0)