typed→rust: bytevector-append + integer->le-bytes primitives
ober
54906f8e9f98cf17514dc17f71db60747c92a996
--- a/lib/jerboa/typed/checker.ss +++ b/lib/jerboa/typed/checker.ss @@ -372,6 +372,14 @@ (cons 'utf8->string (make-typed-call-sig (list 'Bytes) 'String '() 'utf8->string '())) + ;; concatenate two byte strings into a fresh owned buffer. + (cons 'bytevector-append + (make-typed-call-sig (list 'Bytes 'Bytes) 'Bytes '() + 'bytevector-append '())) + ;; an Int as its 8-byte little-endian i64 encoding (Rust i64::to_le_bytes). + (cons 'integer->le-bytes + (make-typed-call-sig (list 'Int) 'Bytes '() + 'integer->le-bytes '())) ;; base-2 logarithm on a float (the entropy/log-likelihood primitive); ;; callers cast integers up with exact->inexact first. (cons 'log2 --- a/lib/jerboa/typed/core.ss +++ b/lib/jerboa/typed/core.ss @@ -125,6 +125,8 @@ bytevector-u8-ref string->utf8 utf8->string + bytevector-append + integer->le-bytes make-bytevector exact->inexact log2 --- a/lib/jerboa/typed/rust.ss +++ b/lib/jerboa/typed/rust.ss @@ -1407,6 +1407,26 @@ [(hkdf-sha256) (emit-hkdf-sha256 args)] [else (error 'typed-rust "unknown crypto primitive" prim)])) + ;; (bytevector-append a b) -> a fresh owned buffer a ++ b. Clone the first so + ;; the source Bytes stay usable (Clone-heavy ownership), then extend. + (def (emit-bytevector-append args) + (unless (= (length args) 2) + (error 'typed-rust "bytevector-append expects two Bytes operands" args)) + (string-append + "{ let mut __v = (" + (emit-expression (car args)) + ").clone(); __v.extend_from_slice(" + (bytes-slice (cadr args)) + "); __v }")) + + ;; (integer->le-bytes n) -> the 8-byte little-endian i64 encoding, matching + ;; Rust's i64::to_le_bytes (secmon serializes timestamps this way). + (def (emit-integer->le-bytes args) + (unless (= (length args) 1) + (error 'typed-rust "integer->le-bytes expects one Int operand" args)) + (string-append + "(((" (emit-expression (car args)) ") as i64).to_le_bytes().to_vec())")) + (def (emit-equality args) (unless (= (length args) 2) (error 'typed-rust "equal? expects two operands" args)) @@ -1643,6 +1663,8 @@ [(bytevector-u8-ref) (emit-bytevector-u8-ref args)] [(string->utf8) (emit-string->utf8 args)] [(utf8->string) (emit-utf8->string args)] + [(bytevector-append) (emit-bytevector-append args)] + [(integer->le-bytes) (emit-integer->le-bytes args)] [(make-bytevector) (emit-make-bytevector args)] [(exact->inexact) (emit-to-float args)] [(log2) (emit-log2 args)]