feat: Distill the `EvaluationProgram` #183

winston-h-zhang · 2024-08-01T01:24:38Z

This PR adds the distilled program and distilled memory to loam. Here are the changes:

Implemented cons/car/cdr/atom/quote, as well as tests.
Implemented the distilled program.
Implemented the memory distillation process.
Added tests for inconsistent memory.
Added debugging and printing infrastructure for ascent, and for memory distillation.

src/loam/evaluation.rs

src/loam/allocation.rs

porcuquine · 2024-08-02T20:42:42Z

src/loam/allocation.rs

+ascent! {
+    #![trace]
+
+    struct DistilledAllocationProgram {


This looks pretty good! However, I think you were too aggressive and removed some non-signal relations. In particular, as far as I can tell, there are no surviving hashing rules (or related relations). You can see from first principles that this cannot be correct, since a proof will necessarily prove the hashes. If that weren't the case, it would be possible to falsify the digests.

This would actually be a useful test to add. I'm not being rhetorical, it would strengthen the test suite for memory in general. The test would be to replace digests with random values. If correctly constrained by rules that check the digests, such a randomization should fail. But I think in this DistilledAllocationProgram it will go undetected.

Do you mean "assert" in the literal sense, so that a rule takes a join of the digest and relations, and then checks the hash? Otherwise I don't think there's an easy way to write the distilled program to support this, because you have to check the 3 cases of digest/relation/full pointers. For example, if I only want to register a cons_rel if I have a cons_mem but not a cons_digest_mem, ascent doesn't let me write something like:

cons_rel(car, cdr, cons) <-- cons_mem(car, cdr, addr), let cons = Ptr(Tag::Cons.elt(), *addr), !cons_digest_mem(value, addr);

We should discuss further on zulip @porcuquine

src/loam/distilled_evaluation.rs

src/loam/allocation.rs

porcuquine · 2024-08-02T23:55:07Z

src/loam/distilled_evaluation.rs

-    relation eval_car(Ptr, Ptr, Ptr); // (expr, env, body)
+    relation eval_car_cdr(Ptr, Ptr, Ptr, bool); // (expr, env, body, is_car)

-    eval_input(body, env), eval_car(expr, env, body) <-- 
-        eval_input(expr, env), cons_rel(op, tail, expr), if op.is_car(),
+    eval_input(body, env), eval_car_cdr(expr, env, body, is_car) <-- 
+        eval_input(expr, env), cons_rel(op, tail, expr), if op.is_car_cdr(), let is_car = op.is_car(),
        cons_rel(body, end, tail), if end.is_nil();

    eval(expr, env, car) <--
-        eval_car(expr, env, body),
+        eval_car_cdr(expr, env, body, true),
+        eval(body, env, evaled),
+        cons_rel(car, cdr, evaled);
+
+    eval(expr, env, cdr) <--
+        eval_car_cdr(expr, env, body, false),


I think this can be taken further. This is really eval_unop, I think. Instead of a bool, you can include op (a Ptr), as in fold and friends. Later, we could remove the tag and just use the symbol address as an optimization.

Yup, same thoughts

src/loam/evaluation.rs

src/loam/mod.rs

src/loam/allocation.rs

src/loam/memory.rs

winston-h-zhang · 2024-09-04T04:10:10Z

I'm going to rename test_distilled to test_second_phase and clean up the testing code slightly.

porcuquine

This looks good to me. I didn't scrutinize the actual evaluation programs closely again, but I did review them over time as the work built up. Since that's all in flux anyway, I think this is good to merge now.

Let's try to keep PRs smaller, more focused, and less long-lived now that we're in the next phase of development. Good work.

src/loam/memory.rs

…tion/debugging infra

porcuquine · 2024-09-05T23:43:43Z

🎉