Proposal: add a marker for strictly non-turing-complete functions

[Evrey]

As the title says, this is a proposal for a new type of function, which is guaranteed to not be turing-complete (TC). I think that this will be a highly useful addition to Zig, especially for professional software development in fields with very strict coding rules. But let's first see what y'all think before fleshing anything out.

Syntax-wise this would just appear as perhaps an extra keyword. This keyword could be anything: finite, pure, nontc,… I'll use finite in this proposal, but that's far from a final decision.

Why?

A non-TC function is 100% guaranteed to finish computation in finite time. In other words: It never hangs. There are many situations where certain guarantees about worst-case code runtimes are desirable, such as…

• … for batches in hard real-time operating systems. The Curiosity rover got stuck in a reboot loop once, thanks to a starving watchdog timer reset process.
• … for validation of user inputs. Surprisingly many user inputs are accidentally turing-complete languages.

Being non-TC further opens the doors for a hypothetical later addition of even stricter annotations:

• For example a nopanic marker that guarantees that no code path down that function is able to trigger a panic. Though really it should be a marker that rules out all noreturn calls down the path. Extra tricky when it comes to reading or writing memory, as segfaults could happen, which are potentially noreturn.
• Given the rules of non-TC functions, it's not too difficult to figure out the time complexity of a function. The finite annotation can then be expanded to further restrict the worst-case time complexity. After all, exponential time complexity in a non-TC function may still effectively be the same as just hanging.

Syntax Examples

Writing a guaranteed non-TC function will be as simple as that:

// This function is guaranteed to finish computation in finite time.
// Typing code here that may e.g. potentially result in an endless loop
// will trigger a compile error.
const f = finite fn(x: i32) i32 {
    // non-TC code here
}

Assuming nopanic and time complexity annotations to be added later, it all may look like this:

// This function will never panic or exit the process.
// It will finish computation in quadratic time, depending on `x`.
// It will never get stuck in an endless loop.
// When refactoring the code inside, any changes that break these
// assumptions will result in compile errors.
const f = nopanic finite(x * x) fn(x: i32) i32 {
    // code that e.g. includes two nested counted loops over x
}

How?

I can see two ways of implementing the TC checks. One is simple, very strict, and is also a non-TC problem to solve. The other way, well, I'll come back to that later.

In computer science, there are a bunch of minimal toy programming languages for experimentation, among them GOTO, WHILE, and LOOP. Of these, LOOP is the most powerful programming language that is non-TC. Its control structures are limited to counted loops, function calls, and branches. This will form the basis for the simple implementation.

The Simple Strategy

The rules for a finite fn are as follows:

• It can only call other finite fns.
  • A finite fn cannot have any recursion with the simple non-TC check.
• The only allowed control structures inside a finite fn are:
  • if, it's just O(1).
  • switch, as it's best case O(1), average case O(log(n)), and worst case O(n), depending on what code the compiler generates. All finite.
  • for, which is equivalent to LOOP: A counted loop with O(n) time complexity. All variants are allowed: Labelled for, normal for, for else, inline for.
  • break, as it just cuts for loops short.
  • continue, as it cannot increase the runtime of a for loop. Just cuts an iteration of a loop body short.
  • defer and errdefer, also just O(1).
  • catch and try, which are just glorified ifs.
  • There should be no harm in also allowing suspend and resume. They are pretty much calls and returns with a bit of magic attached.

In other words, the only disallowed control structures are while and calling non-TC functions. while is capable of creating infinite loops, just as unbounded recursion is. Recursion is ruled out, as checking recursion bounds is the same problem to solve as checking bounds on a while loop.

The Complex Strategy

To allow while loops and recursion, we could in theory add a theorem prover and run it for a maximum amount of time. I.e. we could try solving the halting problem. This could be combined with the already existing @setEvalBranchQuota setting.

Complexity Bounds

I already annotated the non-TC control structures with their time complexities. So in theory it shouldn't be too difficult to later add syntax for complexity bounds that the compiler checks against your code. What this syntax may look like is open for debate, however.

• We may do something that directly refers to specific inputs.
  • finite(a * b) — quadratic-ish time based on e.g. two slices
  • finite(min(a, b)) — linear time, e.g. a slice equality check
  • finite(a + b) — linear time, e.g. walking over two slices in a sequence or in lock step
  • If we have a slice a as input, should we take a-the-bound to mean the length of a-the-slice?
  • Given some integer x, it's just x in the time complexity bounds.
  • What about struct fields, are they fine? Would be too limited if not. finite(x.a + k), for example.
  • Is calling non-TC functions at comptime for finite rules okay? Or do we just offer pseudo functions for stuff like min and sqrt and log? I think pseudo will do, but calling any functions for e.g. querying container lengths would be neat.
• We may allow anonymous/generic complexity rules.
  • finite(_) — linear time, unknown bound, e.g. for a strlen impl that goes on until e.g. the calculated length overflows or the code segfaults
  • If we only have generic bounds, we may accept any identifiers, independently of what function args are named
  • finite(n * m)
  • finite(sqrt(n))
• Or just use generic keywords for generic complexities:
  • finite(linear)
  • finite(const)
  • finite(log)
  • …

Of course there's also the possibility to not just specify time complexity, but also memory complexity. Just as a potentially hanging function thanks to user inputs is undesirable, so is a function OOMing the process because of questionable user inputs. However, figuring out rules for computing memory complexity is yet another beast to tackle that is way out of scope for this proposal here.

It may be favourable to go for the generic keywords for generic complexities, possibly composable as pseudo functions like log(log). This could make it much easier to compare the computed complexity of a function vs. the annotated one. It's allowed to write a function body that does the same or better as the given annotation, but doing worse is not allowed and triggers a compile error.

Interoperability

Any fn can call any finite fn. This also means that when assigning function pointers to variables, any finite fn can be assigned to any fn pointer variable, as long as the type signatures match. No explicit type casting needed. However, the opposite is not true.

Other Potential Applications

Zig preaches the »no surprise control flow« rule. That's the reason why operators aren't overloadable. I'm not a fan of that, I often write linear algebra code, and doing so without operators is tedious and hard to read. However, I understand the reasoning behind forbidden overloads and agree in general.

I think a finite fn would open up a possibility for a good operator overloading compromise. Potentially even nopanic finite fn. Given that, when you see operators put to use in some linear algebra code, you may no longer know whether or not a function call may happen. But at least you can be comfortable that the operator code will finish quickly and that it won't crash your program. The rules can be arbitrarily harsh, e.g. finite(linear) fn operator_add(…) …, which would allow loop-based scalar code for vectors, or O(1) SIMD code.

Downsides

Of course that's a bit to add to the Zig compiler. Once a finite fn is encountered, it has to walk down the AST looking for disallowed control flow structures, worst case throwing a theorem prover at the AST. Theorem prover or not, this will increase compile times.

Further more, to really make this useful at all, finite annotations have to be added all over the stdlib. This will likely take way more time than implementing the new syntax and may even be the biggest deal-breaker.

Zig also added async functions lately, in a way that strictly avoids »coloured functions«. However, this non-TC proposal here has the very purpose of adding »coloured functions«. Though it shall be noted that magical rules only apply when a non-TC function wants to call another function. A normal function can still call whatever it wants to however it wants to.

Upsides

I will, however, highlight the potential gains again. Adding finite and maybe even nopanic will greatly help users in developing robust and secure software. It'll make accidental turing-completeness a thing of the past and thus greatly reduce vectors for DoS attacks.

Together with time complexity bounds, designing realtime systems in Zig will be easier than ever. This would not only be interesting for hard realtime systems such as spaceprobe operating systems, but also for the development of soft realtime systems, such as video game engines.

finite can also be utilised as a hint for comptime evaluation, where the compiler may just blindly evaluate all e.g. worst-case quadratic time functions, independently of whatever @setEvalBranchQuota says.

If, much later, we may add a theorem prover to also allow complicated non-TC checks to allow recursion or while, this opens the door for the addition of contracts. requires, ensures, and invariant annotations that must be finite expressions and would be checked and enforced at comptime, zero runtime assertions generated. Comptime contracts would allow for a lot more code optimisations and even robuster Zig code.

Open Questions

External Functions

When declaring external functions, it may be useful to be able to add finite rules, although the compiler is not able to check whether these rules are actually true. One example case would be adding something like finite(linear) to strlen. In general this would also be useful for annotating intrinsics, like SIMD intrinsics. (Did I mention that adding rules to the stdlib will be a potentially massive amount of work?)

How should external annotations be added, though? Convert headers once and add them in manually? Or allow aliasing function decls with such annotations, so you can have converted C headers in one file and time complexity annotations in another?

Memory Complexity

As mentioned, memory complexity bounds would be neat. But this needs additional rules for the compiler to figure out.

Mixed Time Complexity

Sometimes in high perf code you see functions that dynamically branch between two algorithms to solve the same problem. The reason for that is simple. Imagine you have one branch solving the problem in O(log(n)), and the other one solving it in O(exp(n)). These two graphs have an intersection point. Before that point exp(n) does actually better, and after it obviously log(n) outperforms exp(n). Such functions try to guess the intersection point and branch there.

How would one annotate this function now?

As stated above, if a function claims to be finite(log), then implementing it in a way that performs worse results in a compiler error. So if we were to mark this branching function as finite, it would have to claim being finite(exp). Unless we figure out some syntax that is able to express this branching. The big-O notation can express differences between worst, best, and average case complexities. We could add this, too, possibly like this:

// Simple solution: Claim worst-case exponential and best-case logarithmic.
// But what we really ideally want is something that says:
//   »`exp` inside, but only where doing better than `log`, trust me«
// … so that we can mark `f` as just `finite(log)`.
const f =
finite(
  min_t: log(x),
  max_t: exp(x),
)
fn(x: i32) i32 {
  if x <= N { return f_exp(x); }
  else      { return f_log(x); }
}

This also answers the question of how one would annotate memory complexities. Add extra fields m, min_m, etc. A simple finite(x) would then be an alias for finite(max_t: x).

Call Cost Annotations

The finite rules are simple expressions and can thus be evaluated for some input. Data comes in, a number comes out. We could utilise this to create a new @ intrinsic that performs this function selection for us.

For example, we could rewrite the function f above as follows:

// Dynamically calling one of many functions based on time complexity.
// This generates an `if x <= N` jumping to the estimated best-case implementation.
// Given that the compiler can understand this snippet without throwing theorem
// provers around, `f` can now actually be marked with the best-case time complexity
// of all implementation candidates.
const f = finite(log) fn(x: i32) i32 {
  return @callMinTime(
    // list of function candidates
    // may include non-finite functions with an assumed infinite cost
    [f_log, f_exp],
    // argument list
    x,
  );
}

Now, this approach is not perfect. For example, two functions with the same on-paper complexity may perform very differently, simply because one does e.g. more data moves than the other. Whether and how we could tackle this, e.g. by allowing scaling constants that on paper get crossed out, is also an open question.

Of course all this assumes us going for such complexity annotations in the first place, as opposed to doing just the simplest first step of having a bare finite fn of an unspecified complexity.

[rohlem]

This is an interesting idea, and it sounds like it would solve real world use cases to me.

That being said, I feel like the surface area at which this interacts with the rest of the language is quite minimal.
Why should this be part of the language, or rather, what downsides would there be to implementing this complexity analysis in an external tool to run as part of a build process? (To ensure integrity with compiler output, this process could run as a validator on some form of IR emitted by the Zig compiler.)

The one effect mentioned in the proposal would be maybe allowing operator overloading with these stricter rules - I think it's fair to regard that as a separate, subsequent proposal.

(Technically this proposal is a sort-of-superset of timeconst from #1776 , however I believe constant-time code sections supporting a limited set of operations are much less involved to prove / generate than the plethora of complexity classes expressible here.)

[Evrey]

Why should this be part of the language, or rather, what downsides would there be to implementing this complexity analysis in an external tool to run as part of a build process?

I honestly see no reason why it couldn't be an external tool, apart from stuff like safe operator overloading. But I do see reason why this, tool or language extension, could benefit from being integrated into Zig as a standard thing.

One way or another, people would have to write such complexity annotations for the stdlib and more. And if Zig or that external tool don't come with ready-to-be-used definitions for the stdlib, I see two things happening:

• Writing all the rules for dependencies is tedious, so many devs may not use such a feature in favour of just getting stuff done.
• People do try writing their own rules against the stdlib, many of which will contain little mistakes, and many of which will be duplicate efforts.

If this feature would be integrated as a language extension, stdlib support is pretty much guaranteed from version 1.0 onwards. And if it's an external tool, but an official one shipping with Zig builds, then development of the tool is more likely to be kept in sync with stdlib changes and additions as well.

Plus, if it's added as an external tool feature first, people could try it out, find pain points, find more opportunities, and then maybe it'll later still be more tightly integrated into the language, depending on the gained experience.

[ghost]

In other words, the only disallowed control structures are while and calling non-TC functions.

Ahem. You can't count from one to ten in Zig without using a while loop (#358) 😎.

It would be a nice proposal in a language that provides more high-level constructs with specific constraints. And to be really useful, the stricter (and much more difficult) version of the proposal with time complexity guarantees would be needed, IMO. Knowing that a function is finite is a rather loose upper bound. Factoring numbers by trial division is finite.

[vkcz]

Extension to the big-O-like performance-indication system proposed here: the ability to use, as a function in the cost formula, the complexity assigned to a particular other operation, so as to handle different implementations/implementations with complicated formulae of an operator or finite function.

[Evrey]

@zzyxyzz Oh, damn, i forgot that for can't run over ranges in Zig. That's a big problem with regards to the practicality of the non-theorem-prover version. I guess one could also allow while loops, if the loop condition itself only runs over finite functions, and if nobody else mutates the data fed into the loop condition. May work well enough for most number generating iterators.

And to be really useful, the stricter […] version of the proposal with time complexity guarantees would be needed

Indeed. I see the bare finite-without-bounds case as a mere careful »try it out« without putting in too much effort.

It would be a nice proposal in a language that provides more high-level constructs with specific constraints.

In the little idealistic world inside my head, every programming language would be powerful enough to run basic proofs over software. No matter whether it's a systems programming language or some small scripting language. And I think that in a language that can already tell you how much memory a specific function call would consume, having the ability to express time and possibly even memory costs would fit in nicely.

@vkcz Yeah, that does sound useful.

[kprotty]

You can't count from one to ten in Zig without using a while loop

@zzyxyzz Once can do it with a for loop given the range is known at comptime.

for ([_]u0{0} ** 10) |_, i| {
    // use i + 1
}

[matu3ba]

@Evrey
You problem must likely be solved by 1.codegen to zig or 2.static analysis of the typed ZIR. Plus any other code that is used must be analyzed beforehand.

Your hope of wide scale is in vain, because loop termination is not trivially provable (Halting problem).

Further the verification scales quadratically with code size, so one needs special tooling like cogent (which works only for limited complexity).

1. Usually keywords are reserved for control-flow, but this rule does not hold strictly for noalias (performance optimisation based on absence of aliasing pointer access). There needs to be a decision eventually how to deal with performance optimisations.
2. I would suggest putting such markers into special formatted comments above the function and use it in another parser as to not interfere too much with the main compiler development.
3. Such markers would make excellent documentation.
4. Proof systems are not standartised, because their performance is low. Static analysis is the best you can do during compilation time, but this is very slow (Rust). Though I believe we can do it faster than Rust.
5. It does not make sense to couple them tightly, unless you can do performance optimisations based on that.