Asserting Implications
31 points by matklad
31 points by matklad
One advantage of using an if statement is that you can often get better coverage information from a test harness than with a single boolean condition. Besides the universal assertion itself (“for all x meeting this condition…”), it’s likely that there’s an implicit existential assertion (“there exists some x that meets this condition…”). If the assertion condition is never triggered in tests. then you likely want to know that, since it could potentially mean that you have a gap in test coverage, or that there’s a stronger assertion that you actually want (“there are no x meeting this condition…”).
On the other hand, sometimes it’s fine if there’s no code path triggering that condition at present. It could protect against a future regression or redesign, or simply defensive programming.
// Before:
assert(header_b != null or replica.commit_min == replica.op_checkpoint);
// After:
if (header_b == null) assert(replica.commit_min == replica.op_checkpoint);
It seems like the invariant being asserted here is that either header_b is null, or header_b is not null and replica.commit_min == replica.op_checkpoint. So for me that reads most clearly as
assert( (header_b == null) or (header_b != null and replica.commit_min == replica.op_checkpoint) );
YMMV!
It should maybe be noted that it slightly changes the semantics if you have a short circuiting or implementation, though that is probably something that is a really good idea to not rely on.
Unrelated, it is nice to see a good old over-painting of a fresco instead of using some generative “AI” to make a header image.
It should maybe be noted that it slightly changes the semantics if you have a short circuiting or implementation, though that is probably something that is a really good idea to not rely on.
I think it doesn’t? In both versions, b is evaluated iff a s true. If assert itself is inlined (which it should be), then a good compiler shouldn’t be able tell the difference between two versions:
if (!(!a or b)) unreachable;
if (a) if (!b) unreachable;
Random Zig related tidbit: and, or, if are control flow operators, so they are keywords. ! doesn’t affect control flow, so it’s just a sigil.
Yeah when I read it back I found out I got confused, it relies on short circuiting, since if you don’t have it will have different semantics.
I guess the use of if here is pretty much a implementation of short circuiting.
If a is an expression that the compiler cannot see through, for example, a function call defined in a different translation unit, then the compiler will not be able to omit evaluating if (a) since it may have side effects. On the other hand, in assert() the evaluation of the entire expression is omitted if assertions are disabled. At least that’s how it works in C/C++.
In Zig, assert is a normal function:
pub fn assert(ok: bool) void {
if (!ok) unreachable; // assertion failure
}
Isn’t there a compile-time switch to disable it? In most languages/libraries I’m aware of, assertions can be disabled in “release” builds.
Also: in Kotlin — my current language crush — you could trivially implement a implies b as an infix function.
There’s compile time switch to flip between unreachable = trap and unreachable = UB, and the latter will cause the compiler to elide non-side-effecting conditions. Side effects will be preserved though, as with any function call.
The same goes for, e.g. log calls — compiler can omit formatting calls depending on the comptime log-level, and it (or LLVM rather) can elide non-side-effecting arguments, but all side-effects will be preserved.
Zig doesn’t have the class of language features to express the assert/log level pattern. Control flow is always a keyword, there are no macros, auto closures, code pre-processors or some such. So, if you want to semantically elide evaluation, you have to write an if at the call site. We do that a bunch at TigerBeetle:
pub fn push(list: *DoublyLinkedList, node: *Node) void {
if (constants.verify) assert(!list.contains(node));
if (constants.verify) list.verify();
We also don’t support disabling assertions, so for us assert has a slightly different meaning than normally in Zig, it is always a runtime check. So, if you maliciously tamper with TigerBeetle’s data file (flipping some bits and updating the corresponding checksums along the path to root), the thing will die with an assertion failure, and we do rely on that semantics (well, if you maliciously tamper with data file enough you can, of course, cause silent data loss, as TB is non-byzantine, but most changes would be caught by an assertion elsewhere).
Also: in Kotlin — my current language crush — you could trivially implement a implies b as an infix function.
Kotlin’s cool (I was part-time on Kotlin/native team many moons ago), but I don’t think you can? implies must not only be infix, but also lazy. So the best you can do is something like a implies { b }, unless Kotlin gained autoclosures since last time I’ve looked at it!
and the latter will cause the compiler to elide non-side-effecting conditions.
Is everything inline in Zig? If not, then I believe more accurately this means the compiler will elide what it can see has no side effects. In other words, it may still have to keep a call to a function without any side effects if it cannot see its definition.
Is everything inline in Zig?
First-order answer is yes. Zig doesn’t do separate compilation.
Also with regards to zig it does not seem to have easy access to a eager or like for example Rust has with | since that only works for integers and
@as(bool, @bitCast(@intFromBool(a) | @intFromBool(b)))
is not as easy to write.
While lobsters allows and even encourages posting your own content (that’s what authored-by is for!), promoting almost exclusively your own content is frowned upon. Given that four out of your last ten stories are self-promo, you might want to wait to let others to post your stuff :-)
(Yes, that one had to circle for a while before landing.)
Thanks for the reminder, but I do think that 4/10 recent and 4/5 total are on the different sides of “almost exclusively” boundary :P
That being said, yes, part of our posting of TigerBeetle stuff is self promotion. We write and post this because we find the ideas valuable and worth spreading, that is the purpose. But people getting curious about TB in general is also an intended side effect.
I am feeling slightly conflicted here, as there’s an obvious conflict of interest. The rule of thumb that I follow is “would I post this to lobste.rs if I discovered it elsewhere?”.
I don’t think the conflict of interest is a problem here, “self promotion” is definitionally a conflict of interest and it is explicitly allowed. The community has effectively waived its conflict of interest objection within the exception carved out by that rule.
And given that the “rule of thumb” is less than 1/4 (#comments + #posts) you’re clearly within the exception. Even if you weren’t numerically, I don’t think anyone would legitimately debate that you’re here engaging in good faith as a member of the community and within the exception as part of why it’s a “rule of thumb” and not a “bright line rule”.
You should also account for comments.
(Yes, that one had to circle for a while before landing.)
Anyway, for what it’s worth, this comes across as a very cheap shot.