This file lists what Resid's compiler, runtime and tools guarantee, how each guarantee is checked, and what is explicitly not guaranteed. Every "Guaranteed" row names the tests that fail if the guarantee breaks; run them with:

./boot.sh                      # self-compile fixed point
tests/conformance/run.sh       # language cases, including err_* rejections
tests/runtime/run.sh           # runtime properties (C harnesses over rt.ll)
tests/pkg/run.sh               # package signing, trust and ceilings
tests/provenance/run.sh        # signed provenance trailers and residc verify
tests/tls/run.sh               # TLS server authentication over committed fixtures
tests/http/run.sh              # lib/httpserv.resid request parsing and limits

• Untrusted library code compiled into a program: it must not gain capabilities (file system, processes, environment, arguments, network, terminal, clock, display) that the program did not grant it, or reach the runtime's memory internals at all.
• Untrusted package sources (a registry, a mirror, a copied archive): a dependency must be exactly what a trusted key signed, and must be the package that was asked for.
• Untrusted input data handled by a compiled program: it must not cause out-of-bounds memory access.
• A binary from elsewhere that claims to be a Resid build: its signature must be checked against a key the verifier already trusts, and what the verifier re-derived must be told apart from what the signer merely wrote down.
• Out of scope: an attacker who can write the local build tree (target/, the key files, the compiler binary), timing and other side channels, and denial of service (a malformed input may abort the process).

Effects that are not capabilities (ambient by design): writing to stdout/stderr, reading stdin (resid_read_line, resid_read_byte), OS randomness, and the runtime's own allocation and aborts. There is no extern and no in-process FFI: a program reaches the OS only through providers and the builtins above. Code in another language runs only as a native module (below), in a process that cannot reach the OS at all.

A native module is code from another language (LLVM IR text) bound with @link("m"). The guarantees below hold for any artifact, hostile ones included. The test fixtures are in tests/conformance/native/.

Not guaranteed:

• Correctness of native code. The process boundary contains it; it does not make it right. A reply is checked for its type, never its meaning.
• Kernel enforcement. The sandbox is only as strong as the kernel's seccomp. A kernel without seccomp, or one with a hole in an allowed system call, is outside this model, like other kernel bugs.
• Denial of service. Native code can spend its 60 s of CPU or exhaust memory (the host is first in line for the OOM killer). Both are out of scope here, as elsewhere.
• Timing and other side channels, as elsewhere. rdrand is not blocked: OS randomness is not a capability.
• The build tree. -rt still links an arbitrary extra C file without checks. It is a builder's flag, and an attacker who can write the build tree is out of scope.

The runtime is Resid (runtime/rt/), built on the compiler-only raw memory primitives, with no C library underneath; and the compiler performs in-place updates of values it proves unshared (ownership analysis, loop regions). Both are covered by the conformance suite and the self-compile, not by a proof.

A package archive (RESIDPKG1) holds every .resid, .toml and .ll (native module) file of the package, sorted, so its SHA-256 covers the sources, the manifest's name, version, dependencies and capabilities, and resid.lock.

A registry named by [registry] url is untrusted input exactly like a local directory, and the transport widens nothing: the archive's SHA-256 is checked against resid.lock and any -sha256 sidecar, trust still comes from a pinned key, a keyring key or a signed index, and the archive must be the package that was asked for. A fetch that succeeds is never itself a reason to trust anything.

resid-pkg serve is the publish side of the same layout, and is deliberately small: loopback only, GET and HEAD, no listing, and no request path may name a file outside the registry directory. Uploads are opt-in (--upload <keyring> --index-key <key>) and take only an archive signed by a keyring key; a client still trusts the index signature and the archive hash, never the server. Its HTTP is lib/httpserv.resid's, so the HTTP server guarantees below apply to it, and four worker regions share the listener. With --cert and --key it serves over TLS 1.3 through lib/tlswire.resid, so the TLS server guarantees apply too.

Not guaranteed: path dependencies without a pinned key are trusted as local source (spec §28.3); the package signature is not a COSE structure and does not name the publisher key; require_signatures does not extend to path dependencies, which the spec exempts as local source; and resid build does not fetch https:// itself, so a TLS registry is pulled with resid-fetch into a directory that [registry] path names.

The server parses requests from untrusted peers. It is plain Resid over List(Int) byte buffers, so the memory-safety rows above cover it; the rows here are about what it accepts.

| A client that connects and stalls -- silent, mid-head, or mid-handshake -- costs the server a descriptor, not a worker: http_accept_loop and tls_accept_loop are event loops over every connection they hold, so other clients are answered at once however many stall. | client.py (answered past 60 stalled clients), tls (served past 30 stalled handshakes) | | Each loop holds at most HttpLimits.open_max connections (1024); past it, the one that has waited longest for its request is dropped for the newcomer, so stalled connections cannot keep new ones out. | roundtrip (crowd evicted) | | A request is parsed once it is whole; how far it has been checked is remembered, so one sent a byte at a time costs linear work. A TLS handshake step is attempted only when a new record is complete, and a handshake past 64 KiB or 16 records is refused. | roundtrip (slow client cut off) |

Not guaranteed: a handler's own time is unbounded and runs on its loop, so a slow handler delays that loop's other connections (spawn more loops for more cores); and a flood of new connections can still crowd out waiting ones through eviction (denial of service is out of scope above).

Capabilities: reading the key and the chain is filesystem(readonly) and happens in the caller (lib/tlskey.resid); serving is network(readonly) and binds nothing. A server that exposes a port other machines can reach needs the full network grant, as before.

The private key is read, never written, never printed, and not kept past the call. What this language cannot do is check the key file's mode: there is no stat verb, so a mode check is not expressible here. Keeping a key file owner-only is the operator's job, and a deployment that cannot do that should not be running this.

The direction of the TLS 1.3 traffic secrets is the one mistake that a test cannot be built around: a client that uses its own application secret for both directions completes the handshake and then opens no application record at all. The client reads with the server's application traffic secret and writes with its own.

Not guaranteed:

• Only ecdsa_secp256r1_sha256, ecdsa_secp384r1_sha384 and ed25519 are produced. RSA signing, session resumption (PSK or tickets), client certificates, encrypted ClientHello, record compression and 0-RTT are not implemented. A client offering none of the server key's algorithm is refused rather than served with a signature the certificate does not cover.
• No session ticket is ever sent, so every connection pays a full handshake. That is the safe direction to be wrong in.
• This repository's own client verifies the CertificateVerify schemes ECDSA P-256/SHA-256, ECDSA P-384/SHA-384, Ed25519 and RSA-PSS with SHA-256/384/512 (rsaEncryption and RSASSA-PSS keys), each only with a certificate key of the matching kind (tls_scheme_alg).
• The key file's permissions are not checked (see above).
• Constant time is checked for the operations listed under "Cryptography library" below, on the shipped (optimized, LTO) code; the TLS record layer, handshake and key schedule around them are not separately checked.

Release binaries carry a COSE_Sign1 (Ed25519) trailer over a record that binds the source files, the binary and its sidecars by SHA-256. residc verify checks the signature and the hashes, then reports the record as evidence (what it re-derived) and attestation (what only the signer says), and names where the key it trusted came from. The graph tools (resid-why, resid-graph, resid-debug) do not verify provenance themselves; run residc verify before trusting their inputs.

Not guaranteed: toolchain and profile are attestation only, and compiler is evidence only when the residc running verify is the builder (otherwise it is a hash the reader may compare by hand); a local key verifies the signature exactly as an anchored one does, and is only named as local -- --anchored is the switch that refuses it; the graph cross-check applies only to builds that carry a signed graph artifact (debug and check profiles); --sources compares against the paths the record names, so a build from another directory needs its relative layout reproduced.

Certificates are compared as moments on the timeline, not as packed integers: x509_valid_now takes an Instant and converts the certificate's UTCTime/GeneralizedTime through lib/calendar.resid, so a certificate's notBefore cannot drift from what the rest of the language calls the same day. A time this cannot read rejects rather than comparing against a moment it did not read.

| Certificates are parsed strictly (x509_parse: DER only, inner and outer signature algorithms byte-equal, well-formed and duplicate-free extensions) and verified for ECDSA with SHA-256/384/512 on P-256 or P-384 keys, RSA PKCS#1 v1.5 with SHA-256/384/512, RSA-PSS with SHA-256/384/512 (any salt length; MGF1 must use the message hash; hashAlgorithm and maskGenAlgorithm must be present, since their defaults are SHA-1) and Ed25519. An id-RSASSA-PSS key only verifies PSS. AMD's published SEV ARK/ASK chains (Milan, Genoa) and the AWS Nitro root verify. | rsa_pkcs1, rsa_pss, pss parameter check, the x509 section of tests/crypto/run.sh | | A certificate may only sign for another if it says CA:TRUE and allows keyCertSign. A leaf handed over as an intermediate cannot issue. | leaf must not be a CA, issuer CA checks | | A store carrying CRLs enforces them: a certificate the issuer's current CRL lists is refused. | good.der, bad.der | | A CRL is used only if it is signed by the issuing CA and inside its thisUpdate..nextUpdate window, so a stale CRL cannot certify anything. | a stale CRL must not be usable | | revocation_required refuses a certificate that no current CRL covers, so "no revocation information" never reads as "not revoked". | good.der under revocation_required, revocation_required must refuse a stale CRL | | CRLs and roots are loaded separately, so a bundle of CRLs is never mistaken for a set of trust anchors. | (loading) |

Not guaranteed:

• Revocation evidence comes from the store's CRLs and OCSP responses; no stapled OCSP response in the handshake is read. A store with neither for an issuer has no revocation information about that issuer's certificates, and revocation_required is the switch that makes that a refusal rather than an acceptance.
• A pinned certificate (trust_store_has) is accepted without any chain, so it is not covered by a CRL: pinning is an explicit decision to trust those exact bytes, revocability included.
• A trust anchor is not itself checked for revocation.
• require_signatures does not extend to path dependencies, which spec §28.3 exempts as local source.
• P-521, SHA-1 (in any signature), SHA-3, DSA, RSA below 2048 bits and ECDSA over curves other than P-256 and P-384 are not verified: such a certificate is refused, not accepted on another algorithm's terms.
• Constant time is checked with valgrind on x86-64 only, and covers secret-dependent control flow and addresses, not variable-latency instructions (the only divides in the checked binary are on public indices in the AES key schedule and in the allocator, found by reading its disassembly rather than by a test). The checks need valgrind installed; without it tests/ct/run.sh reports itself skipped.

build/boot/seed.ll is committed LLVM IR of the compiler. ./boot.sh links it, rebuilds the compiler from source twice and requires all three IR outputs to be byte-identical, so the seed is exactly what the source compiles to under itself. This does not rule out a seed that reproduces itself while miscompiling (the "trusting trust" problem): no independent second compiler of the current source is maintained.