Administrivia: Canadian Common CV
Lots of work this weekend trying to figure out the toolchain we'll use for getting BPF hacked onto our thing. I've decided to use netcat (the OG version) as the base for hacking. So far, I've got it attaching an EBPF filter onto the socket, and communicating between the user and the kernel using a map. That doesn't sound like a lot but it's the better part of a day and a half of reading. Next up, figuring out how to get the socket info (going to need to patch the kernel), and add a new helper to send arbitrary data.
Term is coming to a close. Submitted an admittedly rough draft of the C to BPF compilation write up yesterday. The models look good, and the compilation scheme is okay, but the analysis is admittedly weak. Taking a day off before getting back into the EBPF RPC backpressure work tomorrow.
Completed ACL2 proofs for loop precondition, termination, and postconditions for the simple "countdown" loop. Ended up re-working the loop "if" test to consume "then" and "else" terms, and added a nop to make the number of instructions equal for both branches. Now that I have a this work I can proceed to the writeup. Did most of the initial proof work using the proof builder, but I was able to give enough hints to the theorem prover to automate the loop theorem in the end.
Yesterday, I said I thought I needed to add a loop check at the beginning in order to handle the case where the initial value was zero, in order to make the induction work. However, in this case, I just asserted as a precondition a positive value, which means that the base case checks out because we have a contradition in the premises, and we specify a case split at value > 1 for the inductive case; where the value <= 1, and > 0, is effectively another base case, and for any values v > 1, we can appeal to the inductive hypothesis.
Working on ACL2 proofs for first simple wasm program; We set a value to some positive number and a loop repeats until that value is zero. We want to show that if that loop terminates (that is, if the stepper function reduces the program to "nil"), that the value in the store is zero. Right now, we enter the loop even if the value is set to zero, which means that we'll miss the zero check and the loop will run forever. In order to do an induction proof (using (dec-induct x)) we will need to rewrite the program so it terminates at zero.
Currently, however, we have a bunch of theorems that make handling it easy to "interpret" the program in blocks: we have theorems that handle initialization, loop entry, and loop body itself, and loop test. We compose these theorems together to have a "big mama" theorem that describes how one run through the program deals with some value x at a time.
A good result tonight. This was the first time I've used the "induct by two natural numbers" method; By defining an induction principle that reduces the value by 1, but the stepper count by "length of block", we're able to get a pretty slick proof of that "if this loop terminates, you have the answer you expect" result we were looking for. I've hit some caveats: 1) stepper count needs to be the same, regardless of whether we're taking the loop or exiting (right now they take different steps, which means we can't satisfy particular conditions about the # of steps we have) and 2) we need a way to show that if a number is inside our legal range (0..maxsize), if it's greater than 1, decrementing it by 1 keeps it in that range, and therefore, we're allowed the term from inside a i32-val.