Skip to content

Commit 09dd03b

Browse files
johnchandlerburnhamsamuelburnhamarthurpaulinogabriel-barrett
authored
Jcb/compilation roundtrip (#282)
* refactor module organization, env types, and add richer scc result * tmp rustfmt * rust, const sorting and expr compilation * compile_const * wip: compiler structure, but erroring * compiling Env in 11.32 seconds * clippy and warnings * manual stack management for compile_expr to avoid overflow * xclippy warnings * compilation in 6.65s, total pipeline in 16.8s * remove cons_list * ci: Add comparative benchmark report (#265) * feat: Add Json serde for Benchmark API * (WIP) Add comparison report and PR comment workflow * Add one-shot benches and markdown report * Export benchmark API in ix library * Add env var overrides for config settings * Finish report pretty-printer * Fix `bench.yml` * Scope permissions with app token * Fix security alert * Fixup * Start `Ixon` serde in Aiur (#268) This patch implements (and changes) enough of the code base as a PoC of being able to provably bootstrap the precise Ixon whose hash is stated as an argument of the claim (as input of the Aiur entrypoint call). This is done by reading the bytes from the `IOBuffer`, deserializing it and then serializing and hashing the respective bytes. Deserialization followed by serialization was the chosen solution because serialization is, in principle, cheaper. Thus the deserialization can be tagged as `#[unconstrained]` for extra speed. Furthermore, the unconstrained tag is now more rigorous: an unconstrained function can no longer call a constrained function. As an extra, the IxVM code has been split into multiple smaller Aiur toplevels to enable parallel elaboration by Lean. --------- Co-authored-by: Gabriel Barreto <gabriel.aquino.barreto@gmail.com> * chore: Clean up Benchmark API (#267) * chore: Test benchmark PR * Refactor blake3 bench to use Criterion * chore: Refactoring * More fixes * Lifted unconstrained restriction (#273) * lifted unconstrained restriction * filtered queries of multiplicity 0 * constrained inside unconstrained test * Progress on serialize and deserialize (#276) * Ixon.UVar * deserialize Ixon.EVar and Ixon.Blob * some fixes * small fix * progress on serialize * wip * fixes and deserialize for more cases * more fixes * removed stream input from `serialize` * uvar, evar * `u64_get_trimmed_le` rewritten --------- Co-authored-by: Arthur Paulino <arthurleonardo.ap@gmail.com> * IxVM file split (#278) * rust compiler (#263) * refactor module organization, env types, and add richer scc result * tmp rustfmt * rust, const sorting and expr compilation * compile_const * wip: compiler structure, but erroring * compiling Env in 11.32 seconds * clippy and warnings * manual stack management for compile_expr to avoid overflow * xclippy warnings * compilation in 6.65s, total pipeline in 16.8s * remove cons_list * review comments * Pointer pattern (#280) * Pointer pattern * elab new Pattern.pointer constructor * pointer match test --------- Co-authored-by: Arthur Paulino <arthurleonardo.ap@gmail.com> * decompilation pipeline working * fix failing condense.rs tests * parallelize decoding * xclippy warnings --------- Co-authored-by: Samuel Burnham <45365069+samuelburnham@users.noreply.github.com> Co-authored-by: Arthur Paulino <arthurleonardo.ap@gmail.com> Co-authored-by: Gabriel Barreto <gabriel.aquino.barreto@gmail.com>
1 parent b4b8dc4 commit 09dd03b

10 files changed

Lines changed: 2043 additions & 316 deletions

File tree

‎src/ix.rs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
pub mod address;
22
pub mod compile;
33
pub mod condense;
4+
pub mod decompile;
45
pub mod env;
56
pub mod graph;
67
pub mod ground;

‎src/ix/address.rs‎

Lines changed: 11 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,24 +1,31 @@
11
use blake3::Hash;
2+
use core::array::TryFromSliceError;
23
use std::cmp::{Ordering, PartialOrd};
34
use std::hash::{Hash as StdHash, Hasher};
45

56
#[derive(Debug, Clone, PartialEq, Eq)]
67
pub struct Address {
7-
pub hash: Hash,
8+
hash: Hash,
89
}
910

1011
impl Address {
12+
pub fn from_slice(input: &[u8]) -> Result<Self, TryFromSliceError> {
13+
Ok(Address { hash: Hash::from_slice(input)? })
14+
}
1115
pub fn hash(input: &[u8]) -> Self {
1216
Address { hash: blake3::hash(input) }
1317
}
1418
pub fn hex(&self) -> String {
1519
self.hash.to_hex().as_str().to_owned()
1620
}
21+
pub fn as_bytes(&self) -> &[u8; 32] {
22+
self.hash.as_bytes()
23+
}
1724
}
1825

1926
impl Ord for Address {
2027
fn cmp(&self, other: &Address) -> Ordering {
21-
self.hash.as_bytes().cmp(other.hash.as_bytes())
28+
self.as_bytes().cmp(other.as_bytes())
2229
}
2330
}
2431

@@ -29,7 +36,7 @@ impl PartialOrd for Address {
2936
}
3037
impl StdHash for Address {
3138
fn hash<H: Hasher>(&self, state: &mut H) {
32-
self.hash.as_bytes().hash(state);
39+
self.as_bytes().hash(state);
3340
}
3441
}
3542

@@ -60,7 +67,7 @@ pub mod tests {
6067
for b in &mut bytes {
6168
*b = u8::arbitrary(g);
6269
}
63-
Address { hash: Hash::from_slice(&bytes).unwrap() }
70+
Address::from_slice(&bytes).unwrap()
6471
}
6572
}
6673
impl Arbitrary for MetaAddress {

‎src/ix/compile.rs‎

Lines changed: 56 additions & 80 deletions
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,7 @@ pub struct CompileState {
3838
#[derive(Default)]
3939
pub struct BlockCache {
4040
pub exprs: FxHashMap<Expr, MetaAddress>,
41-
pub univs: FxHashMap<Level, MetaAddress>,
41+
pub univs: FxHashMap<Level, Address>,
4242
pub cmps: FxHashMap<(Name, Name), Ordering>,
4343
}
4444

@@ -156,7 +156,7 @@ pub fn compile_name(
156156
Ok(cached.clone())
157157
} else {
158158
let addr = match name.as_data() {
159-
NameData::Anonymous => store_ixon(&Ixon::NAnon, stt)?,
159+
NameData::Anonymous(_) => store_ixon(&Ixon::NAnon, stt)?,
160160
NameData::Str(n, s, _) => {
161161
let n2 = compile_name(n, stt)?;
162162
let s2 = store_string(s, stt)?;
@@ -178,54 +178,36 @@ pub fn compile_level(
178178
univs: &[Name],
179179
cache: &mut BlockCache,
180180
stt: &CompileState,
181-
) -> Result<MetaAddress, CompileError> {
181+
) -> Result<Address, CompileError> {
182182
if let Some(cached) = cache.univs.get(level) {
183-
Ok(cached.clone())
184-
} else {
185-
let (data_ixon, meta_ixon) = match level.as_data() {
186-
LevelData::Zero => (Ixon::UZero, Ixon::Meta(Metadata::default())),
187-
LevelData::Succ(x) => {
188-
let MetaAddress { data, meta } = compile_level(x, univs, cache, stt)?;
189-
let nodes = vec![Metadatum::Link(meta)];
190-
(Ixon::USucc(data), Ixon::Meta(Metadata { nodes }))
191-
},
192-
LevelData::Max(x, y) => {
193-
let MetaAddress { data: data_x, meta: meta_x } =
194-
compile_level(x, univs, cache, stt)?;
195-
let MetaAddress { data: data_y, meta: meta_y } =
196-
compile_level(y, univs, cache, stt)?;
197-
let nodes = vec![Metadatum::Link(meta_x), Metadatum::Link(meta_y)];
198-
(Ixon::UMax(data_x, data_y), Ixon::Meta(Metadata { nodes }))
199-
},
200-
LevelData::Imax(x, y) => {
201-
let MetaAddress { data: data_x, meta: meta_x } =
202-
compile_level(x, univs, cache, stt)?;
203-
let MetaAddress { data: data_y, meta: meta_y } =
204-
compile_level(y, univs, cache, stt)?;
205-
let nodes = vec![Metadatum::Link(meta_x), Metadatum::Link(meta_y)];
206-
(Ixon::UIMax(data_x, data_y), Ixon::Meta(Metadata { nodes }))
207-
},
208-
LevelData::Param(n) => match univs.iter().position(|x| x == n) {
209-
Some(i) => {
210-
let data = Ixon::UVar(Nat::from_le_bytes(&i.to_le_bytes()));
211-
let n_addr = compile_name(n, stt)?;
212-
let nodes = vec![Metadatum::Link(n_addr)];
213-
(data, Ixon::Meta(Metadata { nodes }))
214-
},
215-
None => {
216-
return Err(CompileError::LevelParam(n.clone(), univs.to_vec()));
217-
},
218-
},
219-
LevelData::Mvar(x) => {
220-
return Err(CompileError::LevelMVar(x.clone()));
221-
},
222-
};
223-
let data = store_ixon(&data_ixon, stt)?;
224-
let meta = store_ixon(&meta_ixon, stt)?;
225-
let address = MetaAddress { data, meta };
226-
cache.univs.insert(level.clone(), address.clone());
227-
Ok(address)
183+
return Ok(cached.clone());
228184
}
185+
let data_ixon = match level.as_data() {
186+
LevelData::Zero(_) => Ixon::UZero,
187+
LevelData::Succ(x, _) => Ixon::USucc(compile_level(x, univs, cache, stt)?),
188+
LevelData::Max(x, y, _) => {
189+
let x = compile_level(x, univs, cache, stt)?;
190+
let y = compile_level(y, univs, cache, stt)?;
191+
Ixon::UMax(x, y)
192+
},
193+
LevelData::Imax(x, y, _) => {
194+
let x = compile_level(x, univs, cache, stt)?;
195+
let y = compile_level(y, univs, cache, stt)?;
196+
Ixon::UIMax(x, y)
197+
},
198+
LevelData::Param(n, _) => match univs.iter().position(|x| x == n) {
199+
Some(i) => Ixon::UVar(Nat::from_le_bytes(&i.to_le_bytes())),
200+
None => {
201+
return Err(CompileError::LevelParam(n.clone(), univs.to_vec()));
202+
},
203+
},
204+
LevelData::Mvar(x, _) => {
205+
return Err(CompileError::LevelMVar(x.clone()));
206+
},
207+
};
208+
let addr = store_ixon(&data_ixon, stt)?;
209+
cache.univs.insert(level.clone(), addr.clone());
210+
Ok(addr)
229211
}
230212

231213
pub fn compare_level(
@@ -235,32 +217,32 @@ pub fn compare_level(
235217
y_ctx: &[Name],
236218
) -> Result<SOrd, CompileError> {
237219
match (x.as_data(), y.as_data()) {
238-
(LevelData::Mvar(e), _) | (_, LevelData::Mvar(e)) => {
220+
(LevelData::Mvar(e, _), _) | (_, LevelData::Mvar(e, _)) => {
239221
Err(CompileError::LevelMVar(e.clone()))
240222
},
241-
(LevelData::Zero, LevelData::Zero) => Ok(SOrd::eq(true)),
242-
(LevelData::Zero, _) => Ok(SOrd::lt(true)),
243-
(_, LevelData::Zero) => Ok(SOrd::gt(true)),
244-
(LevelData::Succ(x), LevelData::Succ(y)) => {
223+
(LevelData::Zero(_), LevelData::Zero(_)) => Ok(SOrd::eq(true)),
224+
(LevelData::Zero(_), _) => Ok(SOrd::lt(true)),
225+
(_, LevelData::Zero(_)) => Ok(SOrd::gt(true)),
226+
(LevelData::Succ(x, _), LevelData::Succ(y, _)) => {
245227
compare_level(x, y, x_ctx, y_ctx)
246228
},
247-
(LevelData::Succ(_), _) => Ok(SOrd::lt(true)),
248-
(_, LevelData::Succ(_)) => Ok(SOrd::gt(true)),
249-
(LevelData::Max(xl, xr), LevelData::Max(yl, yr)) => {
229+
(LevelData::Succ(_, _), _) => Ok(SOrd::lt(true)),
230+
(_, LevelData::Succ(_, _)) => Ok(SOrd::gt(true)),
231+
(LevelData::Max(xl, xr, _), LevelData::Max(yl, yr, _)) => {
250232
SOrd::try_compare(compare_level(xl, yl, x_ctx, y_ctx)?, || {
251233
compare_level(xr, yr, x_ctx, y_ctx)
252234
})
253235
},
254-
(LevelData::Max(_, _), _) => Ok(SOrd::lt(true)),
255-
(_, LevelData::Max(_, _)) => Ok(SOrd::gt(true)),
256-
(LevelData::Imax(xl, xr), LevelData::Imax(yl, yr)) => {
236+
(LevelData::Max(_, _, _), _) => Ok(SOrd::lt(true)),
237+
(_, LevelData::Max(_, _, _)) => Ok(SOrd::gt(true)),
238+
(LevelData::Imax(xl, xr, _), LevelData::Imax(yl, yr, _)) => {
257239
SOrd::try_compare(compare_level(xl, yl, x_ctx, y_ctx)?, || {
258240
compare_level(xr, yr, x_ctx, y_ctx)
259241
})
260242
},
261-
(LevelData::Imax(_, _), _) => Ok(SOrd::lt(true)),
262-
(_, LevelData::Imax(_, _)) => Ok(SOrd::gt(true)),
263-
(LevelData::Param(x), LevelData::Param(y)) => {
243+
(LevelData::Imax(_, _, _), _) => Ok(SOrd::lt(true)),
244+
(_, LevelData::Imax(_, _, _)) => Ok(SOrd::gt(true)),
245+
(LevelData::Param(x, _), LevelData::Param(y, _)) => {
264246
match (
265247
x_ctx.iter().position(|n| x == n),
266248
y_ctx.iter().position(|n| y == n),
@@ -372,14 +354,14 @@ pub fn compile_data_value(
372354
pub fn compile_kv_map(
373355
kv: &Vec<(Name, LeanDataValue)>,
374356
stt: &CompileState,
375-
) -> Result<Address, CompileError> {
357+
) -> Result<Vec<(Address, DataValue)>, CompileError> {
376358
let mut list = Vec::with_capacity(kv.len());
377359
for (name, data_value) in kv {
378360
let n = compile_name(name, stt)?;
379361
let d = compile_data_value(data_value, stt)?;
380362
list.push((n, d));
381363
}
382-
store_ixon(&Ixon::meta(vec![Metadatum::KVMap(list)]), stt)
364+
Ok(list)
383365
}
384366
pub fn compile_ref(
385367
name: &Name,
@@ -406,7 +388,7 @@ pub fn compile_expr(
406388
) -> Result<MetaAddress, CompileError> {
407389
enum Frame<'a> {
408390
Compile(&'a Expr),
409-
Mdata(Address),
391+
Mdata(Vec<(Address, DataValue)>),
410392
App,
411393
Lam(Address, BinderInfo),
412394
All(Address, BinderInfo),
@@ -430,8 +412,8 @@ pub fn compile_expr(
430412
stack.push(Frame::Cache(expr.clone()));
431413
match expr.as_data() {
432414
ExprData::Mdata(kv, inner, _) => {
433-
let md = compile_kv_map(kv, stt)?;
434-
stack.push(Frame::Mdata(md));
415+
let kvs = compile_kv_map(kv, stt)?;
416+
stack.push(Frame::Mdata(kvs));
435417
stack.push(Frame::Compile(inner));
436418
},
437419
ExprData::Bvar(idx, _) => {
@@ -441,27 +423,22 @@ pub fn compile_expr(
441423
},
442424
ExprData::Sort(univ, _) => {
443425
let u = compile_level(univ, univ_ctx, cache, stt)?;
444-
let data = store_ixon(&Ixon::ESort(u.data), stt)?;
445-
let meta =
446-
store_ixon(&Ixon::meta(vec![Metadatum::Link(u.meta)]), stt)?;
426+
let data = store_ixon(&Ixon::ESort(u), stt)?;
427+
let meta = store_ixon(&Ixon::meta(vec![]), stt)?;
447428
result.push(MetaAddress { meta, data })
448429
},
449430
ExprData::Const(name, lvls, _) => {
450431
let n = compile_name(name, stt)?;
451432
let mut lds = Vec::with_capacity(lvls.len());
452-
let mut lms = Vec::with_capacity(lvls.len());
453433
for l in lvls {
454434
let u = compile_level(l, univ_ctx, cache, stt)?;
455-
lds.push(u.data);
456-
lms.push(u.meta);
435+
lds.push(u);
457436
}
458437
match mut_ctx.get(name) {
459438
Some(idx) => {
460439
let data = store_ixon(&Ixon::ERec(idx.clone(), lds), stt)?;
461-
let meta = store_ixon(
462-
&Ixon::meta(vec![Metadatum::Link(n), Metadatum::Links(lms)]),
463-
stt,
464-
)?;
440+
let meta =
441+
store_ixon(&Ixon::meta(vec![Metadatum::Link(n)]), stt)?;
465442
result.push(MetaAddress { data, meta })
466443
},
467444
None => {
@@ -472,7 +449,6 @@ pub fn compile_expr(
472449
&Ixon::meta(vec![
473450
Metadatum::Link(n),
474451
Metadatum::Link(addr.meta.clone()),
475-
Metadatum::Links(lms),
476452
]),
477453
stt,
478454
)?;
@@ -524,10 +500,10 @@ pub fn compile_expr(
524500
ExprData::Mvar(..) => return Err(CompileError::ExprMVar),
525501
}
526502
},
527-
Frame::Mdata(md) => {
503+
Frame::Mdata(kv) => {
528504
let inner = result.pop().unwrap();
529505
let meta = store_ixon(
530-
&Ixon::meta(vec![Metadatum::Link(md), Metadatum::Link(inner.meta)]),
506+
&Ixon::meta(vec![Metadatum::KVMap(kv), Metadatum::Link(inner.meta)]),
531507
stt,
532508
)?;
533509
result.push(MetaAddress { data: inner.data, meta });

‎src/ix/condense.rs‎

Lines changed: 19 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -175,10 +175,9 @@ mod tests {
175175
(&c, &[]),
176176
]);
177177
let sccs = compute_sccs(&g);
178-
assert_eq!(
179-
scc_to_vec(&sccs),
180-
vec![vec![n("A")], vec![n("B")], vec![n("C")]]
181-
);
178+
let mut res = vec![vec![n("A")], vec![n("B")], vec![n("C")]];
179+
res.sort();
180+
assert_eq!(scc_to_vec(&sccs), res);
182181
}
183182

184183
#[test]
@@ -194,10 +193,12 @@ mod tests {
194193
(&d, slice::from_ref(&c)),
195194
]);
196195
let sccs = compute_sccs(&g);
197-
assert_eq!(
198-
scc_to_vec(&sccs),
199-
vec![vec![n("A"), n("B")], vec![n("C"), n("D")]]
200-
);
196+
let mut res = vec![vec![n("A"), n("B")], vec![n("C"), n("D")]];
197+
for scc in &mut res {
198+
scc.sort();
199+
}
200+
res.sort();
201+
assert_eq!(scc_to_vec(&sccs), res);
201202
}
202203

203204
#[test]
@@ -223,13 +224,15 @@ mod tests {
223224
]);
224225

225226
let sccs = compute_sccs(&graph);
226-
assert_eq!(
227-
scc_to_vec(&sccs),
228-
vec![
229-
vec![n("A"), n("B"), n("E")],
230-
vec![n("C"), n("D"), n("H")],
231-
vec![n("F"), n("G")],
232-
]
233-
);
227+
let mut res = vec![
228+
vec![n("A"), n("B"), n("E")],
229+
vec![n("C"), n("D"), n("H")],
230+
vec![n("F"), n("G")],
231+
];
232+
for scc in &mut res {
233+
scc.sort();
234+
}
235+
res.sort();
236+
assert_eq!(scc_to_vec(&sccs), res,);
234237
}
235238
}

0 commit comments

Comments
 (0)