Allow const source buffers for EBufBlit

[tahina-pro]

In FStarLang/pulse#326, I am introducing Pulse mutable slices, and I am turning slices into immutable slices. For their C implementation, I am introducing const array pointers.
Then, I tried to refine the signature of corresponding memcpy operations so that the source pointer can be const. However, Karamel rejects me with:

blit requires a non-const pointer

This PR solves this issue by weakening the checks in lib/Check.ml to allow immutable source buffers. The destination buffer must still be mutable, though.

Everest green CI: https://github.com/project-everest/everest/actions/runs/13336176953

[msprotz]

Looks good to me! Thanks so much.

You might want to check other buffer operations like EBufFill to see if they require the same treatment.

[tahina-pro]

Thanks Jonathan!
EBufFill requires no source buffer, only a destination buffer, and as far as I understand, Checker.check still requires it to be non-const, as expected:

karamel/lib/Checker.ml

Lines 398 to 402 in 481d456

	| EBufFill (e1, e2, e3) ->
	let t1, c1 = infer_buffer env e1 in
	check env t1 e2;
	check_mut env "fill" c1;
	check_array_index env e3;

(and similarly for infer')