rust: Annotates literals with their type.

[armfazh]

Cargo clippy reports unnecessary literal casting, instead do annotate every literal with its type. This change does not affect any static cast.

[1] https://rust-lang.github.io/rust-clippy/master/index.html#/unnecessary_cast

[JasonGross]

Please update the autogenerated files (you should be able to download them from CI on the summary page here for generated-files-bookworm, or you can run make)

[armfazh]

It looks like one additonal cast must be added in the intermediate representation:

For example:

fiat_p256_subborrowx_u64(&mut x104, &mut x105, x103, x96, 0xffffffff_u32);

With the current patch, every literal has its own type annotation (which corresponds to the bitsize of the value). However, there should be another cast to u64 since it will be used to invoke the fiat_p256_subborrowx_u64 function.

Previously, there wasn't an issue as the rust compiler automatically converts these constants.

I couldn't find where to include this additional cast (note that for C, all constants are casted to u64, when they used as parameters of a function). It seems that this cast must come from the intermediate representation tree. @JasonGross , could you please look into this issue?

[JasonGross]

The cast for the third argument should be inserted at

fiat-crypto/src/Stringification/IR.v

Line 1353 in 37dd5af

let '(e3, _) := result_upcast (t:=tZ) (Some (int.of_zrange_relaxed (relax_zrange r[0 ~> 2 ^ s - 1]))) (e3, r3) in

fiat-crypto/src/Stringification/IR.v

Lines 1040 to 1044 in 37dd5af

	Definition result_upcast {t}
	: int.option.interp t -> arith_expr_for_base t -> arith_expr_for_base t
	:= if upcast_on_assignment
	then cast (always:=false)
	else fun _ e => e.

C says that this is false, though:

fiat-crypto/src/Stringification/C.v

Lines 557 to 558 in 37dd5af

	; upcast_on_assignment := false
	; upcast_on_funcall := false

while Rust says true

fiat-crypto/src/Stringification/Rust.v

Lines 382 to 383 in 37dd5af

	; upcast_on_assignment := true
	; upcast_on_funcall := true

so I don't see how the casts are getting there in the C code. But continuing on, we have

fiat-crypto/src/Stringification/IR.v

Lines 566 to 590 in 37dd5af

	Fixpoint cast {always:bool} {t}
	: int.option.interp t -> arith_expr_for_base t -> arith_expr_for_base t
	:= match t with
	| tZ => Zcast (always:=always)
	| base.type.type_base _
	| base.type.unit
	=> fun _ x => x
	| base.type.prod A B
	=> fun '(r1, r2) '(e1, e2) => (@cast always A r1 e1,
	@cast always B r2 e2)
	| base.type.list A
	=> fun r1 ls
	=> match r1 with
	| Some r1 => List.map (fun '(r, e) => @cast always A r e)
	(List.combine r1 ls)
	| None => ls
	end
	| base.type.option A
	=> fun r1 ls
	=> match r1 with
	| Some r1 => Option.map (fun '(r, e) => @cast always A r e)
	(Option.combine r1 ls)
	| None => ls
	end
	end.

fiat-crypto/src/Stringification/IR.v

Lines 462 to 478 in 37dd5af

	Definition Zcast {always : bool}
	: option int.type -> arith_expr_for_base tZ -> arith_expr_for_base tZ
	:= fun desired_type '(e, known_type)
	=> let eq_known_type_desired_type
	:= (known_type <- known_type;
	desired_type <- desired_type;
	Some (int.type_beq known_type desired_type))%option in
	match always, language_specific_cast_adjustment, desired_type, eq_known_type_desired_type with
	| true, _, Some desired_type, _ (* if we always insert the cast, and there's a cast, then insert it *)
	| _, true, Some desired_type, Some false (* if we are doing language-specific casts and we know the desired type and it's not the same as the known type, insert it *)
	| _, true, Some desired_type, None (* if we are doing language-specific casts and we know the desired type and there was no known type, insert it *)
	=> (Z_static_cast desired_type @@@ e, Some desired_type)
	| false, false, _, _ (* if we're not doing cast insertion (neither by forcing nor by language-specific casts), don't insert a cast *)
	| _, true, Some _, Some true (* if we're doing language-specific casts but the new type is the same as the known type, we don't need to insert a cast *)
	| _, _, None, _ (* if we don't know the type to insert, we can't insert a cast *)
	=> (e, known_type)
	end%core%Cexpr%bool.

I expect Zcast to give us

fiat-crypto/src/Stringification/IR.v

Line 471 in 37dd5af

| _, true, Some desired_type, Some false (* if we are doing language-specific casts and we know the desired type and it's not the same as the known type, insert it *)

so we should be getting a cast at

fiat-crypto/src/Stringification/IR.v

Line 473 in 37dd5af

=> (Z_static_cast desired_type @@@ e, Some desired_type)

I don't have time to dig into this more at the moment, but if you're down to try a bit more adventurous debugging, there are a bunch of debugging examples in SlowPrimeSynthesisExamples, if you pick one that's reasonably close to what you want, change a line like

fiat-crypto/src/SlowPrimeSynthesisExamples.v

Line 422 in 37dd5af

Local Existing Instance C.OutputCAPI.

to use Rust rather than C, then you can investigate what's going on. You can either try to do controlled reduction like many of the examples in there do, or you can install https://github.com/coq-community/reduction-effects and do printf-debugging with lazy or cbv by inserting printing effects.