Binary TCP support and SHA256 support.

[n1bor]

Binary protocol support: 4 blockers preventing a Bitcoin P2P client in Aver

Environment: aver 0.27.1, repo at commit f581bc27, Linux (WSL2).

Happy to split this into 4 separate issues if you'd prefer — say the word and I'll
file them individually and link back here. Keeping them together for now because
they share one root cause and one motivating use case.

What I'm trying to build

I was having a play with Aver. So thought I would try implementing something "real". Most of below is analysis by Claude but looks accurate to me!

A command-line program in Aver that:

1. Takes the IP address of a Bitcoin node as a parameter
2. Connects to that node over the Bitcoin P2P protocol (TCP, default port 8333)
3. Listens for transaction announcements
4. Decodes each transaction and prints its details to the screen

This is a good fit for Aver on paper — transaction decoding is pure, total,
recursive parsing over a well-specified binary format, which is exactly the kind
of code verify blocks and refinement types shine on. The blocker is entirely in
getting the bytes in and out, plus one missing primitive.

The Bitcoin P2P wire format is a length-prefixed binary framing:

magic (4 bytes) | command (12 bytes, ASCII null-padded) | length (4 bytes LE) |
checksum (4 bytes) | payload (`length` bytes, arbitrary binary)

Mainnet magic is F9 BE B4 D9. The checksum is the first 4 bytes of
double-SHA-256 over the payload.

Issue 1 — Tcp.send silently corrupts binary responses

File: aver-rt/src/tcp.rs:129

Ok(String::from_utf8_lossy(&buf).into_owned())

Every byte sequence in the response that isn't valid UTF-8 is replaced with
U+FFFD REPLACEMENT CHARACTER. The replacement is lossy and irreversible — the
original bytes cannot be recovered from the returned String.

For Bitcoin specifically, the first four bytes of every single message
(F9 BE B4 D9) are not valid UTF-8, so corruption begins at offset 0 of the
first read.

The failure is silent. Tcp.send returns Result.Ok with mangled data rather
than surfacing an error, so a caller has no way to detect that it happened.

Applies to any binary protocol, not just Bitcoin — this equally breaks
Redis RESP with binary payloads, MQTT, Postgres wire protocol, DNS over TCP, etc.

Issue 2 — Tcp.readLine cannot read binary at all

File: aver-rt/src/tcp.rs:80-99

Two independent problems on the persistent-connection read path:

a) Line framing is wrong for length-prefixed protocols. read_line reads
until \n. Binary payloads contain 0x0A at arbitrary offsets, so messages get
split at meaningless boundaries. The function also strips a trailing \r\n or
\n, silently destroying those bytes when they are payload data rather than
framing.

b) It rejects non-UTF-8 outright. std::io::BufRead::read_line returns
ErrorKind::InvalidData when the bytes read aren't valid UTF-8. So unlike
Issue 1 this doesn't corrupt — it hard-fails. A Bitcoin node's first response
would return Result.Err with an I/O error string.

Note the inconsistency: the one-shot path (Tcp.send) corrupts silently while
the persistent path (Tcp.readLine) errors. Both are blockers, but they present
as completely different symptoms, which makes the underlying cause harder to
identify from the Aver side.

Missing capability: there is no way to read an exact number of bytes. Every
length-prefixed protocol needs "read the 24-byte header, decode the length
field, then read exactly that many bytes." No combination of the current API
expresses this.

Issue 3 — Tcp.writeLine cannot send arbitrary bytes

File: aver-rt/src/tcp.rs:62-77

let msg = format!("{}\r\n", line);
reader.get_mut().write_all(msg.as_bytes())

Two problems:

a) Unconditional \r\n append. Two extra bytes are added to every write.
For a length-prefixed protocol this desynchronises the stream immediately — the
peer reads the trailing \r\n as the start of the next message.

b) No way to express a non-ASCII byte. The parameter is an Aver String,
which maps to a Rust String and is therefore always valid UTF-8. as_bytes()
UTF-8-encodes it, so a codepoint like U+00F9 goes onto the wire as C3 B9, not
as the single byte F9. There is no escape hatch — no byte-string literal, no
String.fromBytes. The byte 0xF9 simply cannot be transmitted.

So the Bitcoin handshake can't even be started: the 4-byte magic prefix is
unsendable.

Issue 4 — No SHA-256, and no bitwise operators to implement one

Bitcoin requires double-SHA-256 in two places that cannot be avoided:

• the 4-byte checksum in every P2P message header
• the txid of every transaction (the identifier you'd print)

No hash primitive exists. grep -rn '"sha256"\|Crypto\.' src/ --include=*.rs
returns nothing. There is no Crypto namespace in docs/services.md — the full
namespace list is Bool, List, Vector, Result, Option, Int, Float, String, Map,
Char, Byte, Args, Console, Http, HttpServer, Disk, Tcp, Random, Time, Terminal,
Env.

And it can't be implemented in Aver. SHA-256 is defined in terms of XOR,
AND, NOT, right-rotation and right-shift on 32-bit words. Per llms.txt, Aver
has no bitwise operators — I confirmed this holds in the implementation, not
just the docs:

grep -rn "Caret\|Ampersand\|ShiftLeft\|ShiftRight\|BitAnd\|BitOr" src/lexer* src/parser* src/syntax*
→ no matches

Simulating bitwise operations arithmetically via Int.div / Int.mod is
theoretically possible but impractical: Int is i64, both functions return
Result<Int, String> (so every one of the ~64 operations per round needs
unwrapping), there's no unsigned 32-bit wrapping type, and SHA-256 runs 64
rounds per 512-bit block. The result would be enormous, unreadable, and slow —
the opposite of what Aver optimises for.

This one is independent of Issues 1-3: even with a byte-clean socket, a Bitcoin
client still can't compute a message checksum or a txid.

Suggested shape of a fix

Offered as a starting point for discussion, not a prescription — you'll have a
much better sense of how this fits Aver's design.

Byte-level TCP. Following the existing Byte namespace convention of
operating on Int rather than introducing a new primitive type:

Tcp.sendBytes   : (String, Int, List<Int>) -> Result<List<Int>, String>
Tcp.writeBytes  : (Tcp.Connection, List<Int>) -> Result<Unit, String>
Tcp.readBytes   : (Tcp.Connection, Int) -> Result<List<Int>, String>

readBytes taking an explicit count is the important one — exact-length reads
are what length-prefixed framing needs, and nothing in the current API provides
them. Vector<Int> may be the better carrier given O(1) indexed access during
parsing.

Hashing:

Crypto.sha256 : List<Int> -> List<Int>

Bitcoin needs SHA-256 and RIPEMD-160; a general-purpose namespace would likely
want SHA-512 too.

Effect classification. The new TCP methods would presumably inherit the
current classification of Tcp.connect/writeLine/readLine — unclassified,
so record/replay rather than verify trace. Crypto.sha256 is deterministic
and pure, so arguably it belongs with the pure namespaces and needs no effect
declaration at all, which would let hashing code carry ordinary verify blocks.

Alternatives I considered

• JSON-RPC to bitcoind over Http.post instead of P2P. Avoids Issues 1-3
  entirely and the node does the hashing. But there's no JSON namespace and no
  base64 for HTTP Basic auth, so both would need hand-rolling in Aver. Viable,
  and a reasonable answer if binary sockets are out of scope for the language.
• A sidecar process holding the socket and emitting hex, with Aver doing the
  decoding. Works today, but concedes that Aver can't own the network layer.
• Implementing SHA-256 arithmetically. Discounted for the reasons in Issue 4.

Issues 1-3 are runtime-level and cannot be worked around from Aver source at all.

Question

Is byte-level I/O something you'd want in Aver, or is it deliberately out of
scope? Entirely reasonable if the answer is "text protocols only" — I'd just
rather know before building on the JSON-RPC path.

Happy to split this into 4 issues, and happy to attempt a PR for any of them if
you'd point me at the direction you'd want it taken.

[n1bor]

Correction to Issue 4 above — I understated what's already in the tree, and it makes that item considerably cheaper than I made it sound.

I wrote that Aver "has no SHA-256". That's true of the language surface but wrong about the repository. sha2 is already a workspace dependency, pulled in by the
wasm-compile feature:

wasm-compile = ["dep:aver-cert", "dep:wasm-encoder", "dep:wasmprinter",
                "dep:wasmparser", "dep:wat", "dep:sha2"]

So it's already vendored, already in Cargo.lock, and already linked into any binary built with --features wasm. I'm not asking you to take on a new dependency — I'm asking to
expose a hasher the project already ships and already depends on.

What still stands from the original:

• No Crypto namespace and nothing SHA-related callable from .av code (grep -rn '"sha256"\|Crypto\.' src/ --include=*.rs returns nothing)
• No bitwise operators, so it can't be implemented in Aver either — I checked the lexer/parser, not just the docs

What I'd revise:

• Exposing Crypto.sha256 is plumbing, not a new-dependency decision
• Two things that aren't trivial: sha2 sits behind wasm-compile, so a default-feature Crypto namespace needs the dependency promoted out of that flag; and it's currently
  used at compile time for artifact certification rather than at runtime for user programs, so it needs wiring into the VM, wasm-gc and wasip2 paths separately
• SHA-256/512 is the cheap half. RIPEMD-160 would be a genuinely new dependency, and it's only needed for address derivation — so it could reasonably come later, or never

Issues 1-3 are unaffected by this; they're in the TCP layer and independent of the hashing question.

Apologies for the noise — I'd rather correct it than have you evaluate the request on a false premise.

[jasisz]

Thanks for this — and for the follow-up correction on sha2, which makes item 4 considerably cheaper.

To answer the question first: byte-level I/O is in scope. The String-only TCP surface is an accident of what got built first, not a design position — there was simply no binary use case until now. Decoding a well-specified binary format is exactly where verify should shine, so I'd rather fix the I/O layer than push you to a sidecar.

Per item:

1. Tcp.send corruption — tracked in Tcp.send silently corrupts non-UTF-8 responses, making binary protocols unreachable #763, fixed by your Add Tcp.sendBytes — a byte-clean one-shot TCP call #764 (one small comment there).

2. • 3. Exact-count reads / byte-clean writes — yes, please split these into their own issues as you offered. Direction I'd take: Tcp.readBytes(conn, n) and Tcp.writeBytes(conn, payload), both on List<Int> for consistency with sendBytes, and no framing added on the write side. One contract detail worth fixing upfront: readBytes returns exactly n bytes or Result.Err — a short read at EOF is an error, not a shorter list. Length-prefixed parsing is built on that guarantee; a partial-read escape hatch can come later if something concretely needs it.

3. SHA-256 — in scope, as a separate PR. You're right that sha2 is already vendored; promoting it out of the wasm-compile feature is fine. Crypto.sha256 : List<Int> -> List<Int>, deterministic, no effect declaration. One deliberate limitation: the prover will treat it as an opaque function — same input, same output, nothing more. That's enough for checksum and txid reasoning, and I don't plan to add bitwise operators to make it implementable in-language. RIPEMD-160 deferred until something concretely needs address derivation.

VM-first is fine for all of these, same as #764 — backend coverage can follow. And since you offered: happy to hand you readBytes/writeBytes, and Crypto.sha256 too if you feel like it — #764 shows you've got the wiring pattern down.