typed-rust: lower make-bytevector to a fresh owned vec!
ober
52786620e5673bd6555e23fffaaa7e71b8ab9734
--- a/docs/jerboa-to-rust.md +++ b/docs/jerboa-to-rust.md @@ -83,10 +83,14 @@ Landed: byte access `buf[(i) as usize] as u64`. With the bitwise primitives and same-module recursion this is enough to express a constant-time `equal?` (XOR-accumulate fold) entirely in Typed Jerboa; see - `tests/fixtures/typed/rust-ct-equal.ss`. Bytevector construction - (`make-bytevector`) and in-place mutation (`bytevector-u8-set!`, - `bytevector-copy!`) are not yet lowered -- they need the mutable-ownership - model that the current Clone-heavy lowering does not yet provide. + `tests/fixtures/typed/rust-ct-equal.ss`. +- `make-bytevector` is checked as `(Nat -> Bytes)` / `(Nat Nat -> Bytes)` (the + fill defaults to a literal `0`) and lowers to a fresh owned buffer `vec![(fill) + as u8; (size) as usize]`; see `tests/fixtures/typed/rust-make-bytevector.ss`. + In-place mutation (`bytevector-u8-set!`, `bytevector-copy!`) is the next step + and needs the mutable-ownership model that the current Clone-heavy lowering + does not yet provide -- the plan is a `let mut` buffer mutated inside an + effectful `for` loop (the construct half is now in place). - `string->utf8` / `utf8->string` cross the text/binary boundary. `string->utf8` is `(String -> Bytes)` and lowers to `(s).as_bytes().to_vec()`; `utf8->string` is `(Bytes -> String)` and lowers to lossy decode --- a/docs/typed-jerboa.md +++ b/docs/typed-jerboa.md @@ -234,7 +234,10 @@ Current landing: `(Bytes Nat -> Nat)` and lowers to indexed access `buf[(i) as usize] as u64`; combined with the bitwise primitives and same-module recursion, this is enough to express a constant-time `equal?` (XOR-accumulate fold) entirely in Typed - Jerboa — see `tests/fixtures/typed/rust-ct-equal.ss`. `string->utf8` + Jerboa — see `tests/fixtures/typed/rust-ct-equal.ss`. `make-bytevector` is + checked as `(Nat -> Bytes)` / `(Nat Nat -> Bytes)` (fill defaults to `0`) and + lowers to a fresh owned `vec![(fill) as u8; (size) as usize]`; in-place + mutation is still future work. `string->utf8` (`String -> Bytes`) and `utf8->string` (`Bytes -> String`) cross the text/binary boundary, lowering to `as_bytes().to_vec()` and a lossy `from_utf8_lossy` decode, so a constant-time auth-token comparison ports too --- a/lib/jerboa/typed/checker.ss +++ b/lib/jerboa/typed/checker.ss @@ -1277,6 +1277,35 @@ (append acc-errors start-errors end-errors body-errors range-errors invariant-errors)))))))]))) + (def (infer-make-bytevector args env type-names expr) + ;; (make-bytevector size) or (make-bytevector size fill). Size and fill are + ;; numeric; the result is a fresh Bytes buffer. A missing fill defaults to a + ;; literal 0 so the emitter always sees both operands. + (if (or (< (length args) 1) (> (length args) 2)) + (values #f + (list (error-at expr 'bad-primitive-arity + "make-bytevector needs a size and an optional fill" + expr))) + (let*-values + ([(size-ir size-errors) (infer-expression (car args) env type-names)] + [(fill-ir fill-errors) + (if (= (length args) 2) + (infer-expression (cadr args) env type-names) + (values (make-typed-ir-lit 'Nat (expr-source expr) 0) '()))]) + (let* ([operand-errors + (operand-type-errors 'numeric + (list (ir-type size-ir) (ir-type fill-ir)) + (list expr expr) expr)] + [ok? (and size-ir fill-ir + (null? size-errors) (null? fill-errors) + (null? operand-errors))]) + (values + (and ok? + (make-typed-ir-call 'Bytes (expr-source expr) + 'make-bytevector 'make-bytevector + (list size-ir fill-ir) '())) + (append size-errors fill-errors operand-errors)))))) + (def (bad-constructor-arity expr name expected args) (list (error-at expr 'bad-call-arity "typed constructor arity does not match" @@ -1607,6 +1636,8 @@ (infer-shift head args env type-names expr)] [(for/fold) (infer-for-fold args env type-names expr)] + [(make-bytevector) + (infer-make-bytevector args env type-names expr)] [(option-some) (infer-option-some args env type-names expr)] [(option-none) --- a/lib/jerboa/typed/core.ss +++ b/lib/jerboa/typed/core.ss @@ -111,6 +111,10 @@ string-length string-append bytevector-length + bytevector-u8-ref + string->utf8 + utf8->string + make-bytevector debug-string record-ctor record-pred --- a/lib/jerboa/typed/rust.ss +++ b/lib/jerboa/typed/rust.ss @@ -1302,6 +1302,18 @@ (emit-expression (cadr args)) ") as usize] as u64)")) + ;; (make-bytevector size fill) -> a fresh owned buffer; the checker always + ;; supplies a fill operand (defaulting to a literal 0), so both are present. + (def (emit-make-bytevector args) + (unless (= (length args) 2) + (error 'typed-rust "make-bytevector expects size and fill operands" args)) + (string-append + "vec![(" + (emit-expression (cadr args)) + ") as u8; (" + (emit-expression (car args)) + ") as usize]")) + ;; borrow the String's bytes and copy into an owned Vec<u8> (no move, so the ;; source String stays usable under the Clone-heavy ownership model) (def (emit-string->utf8 args) @@ -1545,6 +1557,7 @@ [(bytevector-u8-ref) (emit-bytevector-u8-ref args)] [(string->utf8) (emit-string->utf8 args)] [(utf8->string) (emit-utf8->string args)] + [(make-bytevector) (emit-make-bytevector args)] [(debug-string) (emit-debug-string args)] [(record-ctor) (let ([record (lookup-name (ir-call-info-ref ir 'record) new file mode 100644 --- /dev/null +++ b/tests/fixtures/typed/rust-make-bytevector.ss @@ -0,0 +1,20 @@ +(typed-library (sample typed make-bytevector) + (export zero-buf filled-buf buf-len first-or-zero) + + ;; a fresh zero-filled buffer of length n (fill defaults to 0) + (def (zero-buf (n : Nat)) : Bytes + (make-bytevector n)) + + ;; a buffer of length n filled with the given byte + (def (filled-buf (n : Nat) (b : Nat)) : Bytes + (make-bytevector n b)) + + ;; round-trips construct + length: a freshly-made buffer reports its size + (def (buf-len (n : Nat)) : Nat + (bytevector-length (make-bytevector n 255))) + + ;; construct, then read back the fill byte at index 0 (0 for an empty buffer) + (def (first-or-zero (n : Nat) (b : Nat)) : Nat + (if (> n 0) + (bytevector-u8-ref (make-bytevector n b) 0) + 0))) --- a/tests/test-typed-checker.ss +++ b/tests/test-typed-checker.ss @@ -683,6 +683,38 @@ acc)))) '(bad-for-fold)) +(test "make-bytevector returns Bytes with an explicit fill" + (error-kinds + '(typed-library (body mkbv-ok) + (export f) + (def (f (n : Nat) (b : Nat)) : Bytes + (make-bytevector n b)))) + '()) + +(test "make-bytevector fill defaults to 0 when omitted" + (error-kinds + '(typed-library (body mkbv-default) + (export f) + (def (f (n : Nat)) : Bytes + (make-bytevector n)))) + '()) + +(test "make-bytevector rejects a non-numeric size" + (error-kinds + '(typed-library (body mkbv-bad-size) + (export f) + (def (f (s : String)) : Bytes + (make-bytevector s)))) + '(operand-type-mismatch)) + +(test "make-bytevector rejects too many operands" + (error-kinds + '(typed-library (body mkbv-bad-arity) + (export f) + (def (f (n : Nat) (b : Nat)) : Bytes + (make-bytevector n b b)))) + '(bad-primitive-arity)) + (test "record constructor and accessor calls" (error-kinds '(typed-library (body record-ok) --- a/tests/test-typed-rust.ss +++ b/tests/test-typed-rust.ss @@ -218,6 +218,21 @@ (define for-fold-rust (typed-library-form->rust-string for-fold-form)) +;; make-bytevector: a fresh owned buffer, the construct half of byte-buffer +;; plumbing (mutation lands next). Fill defaults to 0 when omitted. +(define mkbv-form + '(typed-library (sample typed mkbv) + (export zero-buf filled-buf buf-len) + (def (zero-buf (n : Nat)) : Bytes + (make-bytevector n)) + (def (filled-buf (n : Nat) (b : Nat)) : Bytes + (make-bytevector n b)) + (def (buf-len (n : Nat)) : Nat + (bytevector-length (make-bytevector n 255))))) + +(define mkbv-rust + (typed-library-form->rust-string mkbv-form)) + (define return-form '(typed-library (sample typed return-values) (export greeting echo-text echo-bytes) @@ -505,6 +520,16 @@ (substring? for-fold-rust "for i in (start)..(end)")) #t) +(test "rust lowers make-bytevector to a fresh vec!" + (and (substring? mkbv-rust "pub fn zero_buf(n: u64) -> Vec<u8>") + ;; omitted fill defaults to a literal 0 + (substring? mkbv-rust "vec![(0u64) as u8; (n) as usize]") + ;; explicit fill flows through + (substring? mkbv-rust "vec![(b) as u8; (n) as usize]") + ;; construct + length round-trips + (substring? mkbv-rust "(vec![(255u64) as u8; (n) as usize]).len() as u64")) + #t) + (test "rust emits handle registry for record and variant ABI" (and (substring? handle-rust "fn jt_store_handle<T: Any + Send>(value: T) -> u64") (substring? handle-rust "fn jt_clone_handle<T: Any + Clone>(id: u64) -> Option<T>")