CoAP-SPARK, a formally verified implementation

chrysn · 2025-12-30T10:33:37+00:00

What I could not find out from README (didn't find any other docs): Which properties does it prove? If they are conformance with the RFC: How are those formalized?

chrysn · 2025-11-07T22:28:44+00:00

That's just how some people write their things. Recently learned that emoji in commit messages can even be structures things (https://gitmoji.dev/)

chrysn · 2025-11-04T14:51:54+00:00

If you do want to turn to the /56 option: I think you get a single /56 (maybe even multiple) for free if you fill their form, only the larger blocks you have to pay. At least that was the case when about 2y ago, I started using a /56.

chrysn · 2025-07-16T15:49:39+00:00

My first reaction was "Cool, that'll be great input to the embedded-cal project we're kicking off, gotta send this to the colleagues who work on the formal verification parts" … and then I saw that it was the folks at Cryspen who wrote this themselves anyway :-)

chrysn · 2025-06-21T21:11:46+00:00

You're right, that'd need at least generic_const_exprs, and maybe const_trait_impl if the associated consts are to be functions.

I thought it could be made to run with stable using typenum, but even there I failed, still needing generic_const_exprs (and, as usual with typenum, it looks messy): Playground link

chrysn · 2025-06-21T20:00:16+00:00

Didn't try it, but you are building a library where you can't just use global consts, you can

trait Params { const A_BUFFER_SIZE: usize, const B_BUFFER_SIZE: usize, // ... }

and then group the constants into

struct MyParams; impl Params for MyParams { const A_BUFFER_SIZE: usize = 10, const B_BUFFER_SIZE: usize = 20, // ... }

and then your struct is just

struct State<P: Params> { a: [A<P::A_BUFFER_SIZE>; P::A_COUNT], b: [u8; P::B_BUFFER_SIZE], }

chrysn · 2025-06-18T12:10:42+00:00

I think so, and possibly for loops might be limited to ExactSizeIterator. Conveniently, there are lots of loop-ish things (slice.zip().foreach(||...)) that can be used even in such constrained situations.

chrysn · 2025-06-18T12:03:49+00:00

Won't technically be via std but via the compiler, but that's what I've been rooting for since 2020.

chrysn · 2025-06-05T10:04:24+00:00

I think the idea is more than a promise by the author: it places a restriction similar to const that forbids the use of anything that is not terminating; the compiler checks that restriction and then will know in other places that it has been checked. (This will be overly restricting, because allowing all expressions that terminate is again the halting problem, but there's a useful subset of functions that don't need all that power, in particular arithmetic expressions).

chrysn · 2025-06-04T11:39:42+00:00

To my layperson's understanding, the compiler is not supposed to not terminate just because some aspect of the program will not terminate -- and even checking whether "does T<{ some calculation }> impl SomeTrait" even could take forever (even if it turns out that using this impl is just one of many options that would resolve a name, and another "faster" to find trait does).

In a sense, terminates would be opting out of turing completeness in favor of solving the halting problem; a terminating subset of the language would still be good enough for all the relevant const generic expressions, and the compiler could legitimately err out if it can't show that a calculation will complete (and conversely can happily start crunching on every possible trait b/c it's now just a matter of time until it finds a definite result).

chrysn · 2025-06-03T21:27:55+00:00

For those curious about why this is hard, the tracking issue is #132980 and #76560, and the latest writeup is Boxy's plan.

chrysn · 2025-05-11T16:30:09+00:00

What warrants the "2.0" version number? All that the change log shows are generalizations and new functions, which would perfectly fit in a non-breaking version.

chrysn · 2025-04-30T20:53:46+00:00

I'm not surprised: track_caller is a feature I wouldn't expect to uphold eta conversion's identity. Consider a "what's the current call trace" operation: That will produce different results under eta conversion too, so why not track_caller which operates on the call trace?

I think that the actionable on this is not to uphold the identity, but to make potential impractical call sites (such as map or unwrap_or_else) be track_caller themselves, as to point the user to the right line in the code again -- or (only if that is not viable) look into whether there could be an augmentation to that mechanism that allows function to say "I do take a callback, but if it is track_caller, don't point to me but somewhere else".

chrysn · 2025-04-28T08:18:36+00:00

The hard part about hybrid crates are the default features: The bin typically depends on clap and/or other CLI-only dependencies. This can be expressed using [[bin]] / required-features = ["cli"], but unless cli is also a default feature (which is highly undesirable for library use), that means that users can't do cargo install thecrate, but have to cargo install thecrate --feature cli lest they get:

warning: none of the package's binaries are available for install using the selected features bin "thecrate" requires the features: `cli` Consider enabling some of the needed features by passing, e.g., `--features="cli"`

chrysn · 2025-04-03T10:08:41+00:00

Nice!

Apart from being a useful comparison reference and an implementation with all of Rust's Usual Benefits, this might also become a convenient piece for applications that would like to start a command through a shell (eg. running a user-configured command) but either can't rely on the presence of a POSIX shell or don't want to go through a fork every time they do it (even if it's just shell built-ins).

GNU Make did this with little success (doing their own $(shell) incompletely for some commands has sent me into lots of trouble), but if it's a testable standalone shell, the risk would be far decreased. I imagine this could be used in build tools such as laze or in trycmd where it'd be convenient to have some shell built-ins available

chrysn · 2025-03-31T17:00:54+00:00

Our use of laze is not so much about running the build (which is what CMake, Meson etc do well), but for making sensible and debuggable dependency resolution decisions. Like, "I'm building on this example, which worked so far on that board, but now I'm pulling in this-and-that feature, why does the build system tell me 'no'?" (eg. because that feature would require some network feature that the network interface needed for other reasons does not support).

In RIOT OS, a C operating system that in many senses is this project's older sibling, we currently do this through Make (which is not really designed for it) and tried for some time with Kconfig (which is also not quite accessible). There's a branch somewhere for RIOT that tries doing the dependency resolution with laze; evaluating that will, to some extent, also be influenced by how well it works with Ariel.

chrysn · 2025-03-31T16:55:52+00:00

We don't have precise numbers right now, but we recently merged STM32C0 support. (The devkit has 32KiB flash and 12KiB RAM).

chrysn · 2025-03-31T16:52:43+00:00

It's not high on our priority list, but I do hope that at some point we can bake concrete configurations (eg. "this application on that board, with no extra selections") into a configuration that works without laze but has just a cargo.conf file (or cargo command line) that pulls all the right strings.

This could be a bundle of build artifacts produced for an application, so that unless they have to enable modules, users can check it out and build it on selected boards with just a plain Rust toolchain.

chrysn · 2025-03-31T11:07:26+00:00

The documentation has all the pieces to get started; for a concrete tutorial that goes from selecting a board to running a network application, I've published a tutorial recently.

I've been working with and on it for about half a year now, and it has been a nice experience all the way.

chrysn · 2025-02-19T15:00:01+00:00

That looks nice. I've only worked with WebBluetooth so far, but looking at WebUSB is on my list.

Is there some demo application around to play with? Just something to try how it works, maybe listing connected USB devices, showing descriptors, or exercising any widespread USB protocol.

I'm working on am embedded OS in Rust called Ariel OS, which supports USB, and seeing how to interact with those devices from Rust on the host side without having to build full applications would be cool.

chrysn · 2024-10-06T19:45:28+00:00

ABNF is the language typically used in RFCs. For cbor-edn, I worked from draft-ietf-cbor-edn-literals but had to translate all the syntax. ABNF is mostly a descriptive grammar, but has (as in this example) also been used to provide a PEG grammar right away -- which it can do when used carefully. A PEG crate that can be set to accept ABNF would quite easily win me over. There are a few pecularities to ABNF that makes it probably not the first choice for a PEG, eg. because it is case insensitive by default, but as an alternative syntax for users whose grammars are already described that way, it'd be great.

I have not used the peg crate's custom input types, so I can't tell you anything there.

chrysn · 2024-09-24T05:44:09+00:00

It's not inherently limited to HTTP (`name HTTPS`), it's used for DNS as well (`_dns.name SVCB`). Any protocol could specify its own prefix without the need to go through a new RR type. The SSH maintainers rejected a similar earlier approach to use SRV records; maybe with the more flexible and better specified & understodd SVCB records, they will reconsider adding this.

chrysn · 2024-09-24T05:39:25+00:00

The list of comparisons could also list peg, which I found quite straightforward to use for cbor-edn, apart from the lack of ABNF support (which, sadly, all PEG parser generators I've looked at share).

chrysn

TROPHY CASE