Unverified bedrock2 wrapper functions are incorrect on divstep

[JasonGross]

fiat-crypto/src/Bedrock/Standalone/Stringification.v

Lines 108 to 137 in 4be7fee

	(** TODO: Is there a better way to do this? *)
	(** TODO: FIXME: This is currently incorrect when outputs contain mixed integers and pointers *)
	Definition wrap_call
	{p : parameters}
	{t}
	(indata : type.for_each_lhs_of_arrow var_data t)
	(outdata : base_var_data (type.final_codomain t))
	(f : func)
	(insizes : type.for_each_lhs_of_arrow access_sizes t)
	(outsizes : base_access_sizes (type.final_codomain t))
	: string
	:= let innames := ToString.OfPHOAS.names_list_of_input_var_data indata in
	let outnames := ToString.OfPHOAS.names_list_of_base_var_data outdata in
	let '(name, (args, rets, _body)) := f in
	let '(precall, all_args)
	:= match rets, outnames with
	| nil, _ | _, nil => (name, outnames ++ innames)
	| cons _ _, cons r0 _
	=> let r0 := List.last outnames r0 in
	let outnames' := List.removelast outnames in
	(("*" ++ r0 ++ " = " ++ name)%string, outnames' ++ innames)
	end%list in
	((precall ++ "(")
	++ (String.concat
	", "
	(List.map
	(** TODO: Is there a better way to do this? *)
	(fun n => "(uintptr_t)" ++ n)
	all_args))
	++ ")")%string.

divstep contains mixed integers and lists in the output. Can @jadephilipoom or @andres-erbsen help me write a better version of this? Roughly, I need to somehow perform the same algorithm as make_innames + make_outnames + translate_func + c_func to print the function prototype, except instead of starting with a function nat -> string and getting out ltypes, I already have strings where each ltype should be (and they are not parameterized by nat, but instead are already in type.for_each_lhs_of_arrow / type-indexed structures. How can I get this to work?

[andres-erbsen]

I think https://github.com/mit-plv/bedrock2/blob/master/bedrock2/src/bedrock2/ToCString.v#L118-L129 is the relevant code in bedrock2 (and it could be changed if it would make things significantly easier)

[JasonGross]

I think this one is more of a concern:

fiat-crypto/src/Bedrock/Field/Translation/Func.v

Lines 43 to 87 in 0592f00

	(* Translates functions in 3 steps:
	1) load any lists from the arguments
	2) call translate_cmd to translate the function body and get the
	return values
	3) store the return values in the designated variables (with
	lists being written into memory)
	The reason for the load/translate/store pattern is so that, for
	the inductive proof of translate_cmd, there is no need to reason
	about the memory. Since fiat-crypto doesn't do any list
	manipulations in the middle of functions, but only uses lists in
	arguments/return values, it's a convenient formalization. *)
	Definition translate_func {t}
	(e : API.Expr t)
	(* argument variables *)
	(argnames : type.for_each_lhs_of_arrow ltype t)
	(* lengths of argument lists *)
	(lengths : type.for_each_lhs_of_arrow list_lengths t)
	(* integer sizes of argument lists *)
	(argsizes : type.for_each_lhs_of_arrow access_sizes t)
	(* return variables *)
	(rets : base_ltype (type.final_codomain t))
	(* integer sizes of return lists *)
	(retsizes : base_access_sizes (type.final_codomain t))
	: list string * list string * cmd (* bedrock function *)
	* list_lengths (type.base (type.final_codomain t)) (* output list lengths *) :=
	(* load arguments *)
	let load_args_out := load_arguments 0%nat argnames lengths argsizes in
	let nextn := fst (fst load_args_out) in
	let args := snd (fst load_args_out) in
	let load_args_cmd := snd load_args_out in
	(* translate *)
	let out := translate_func' (e _) nextn args in
	(* store return values *)
	let store_rets := store_return_values (snd (fst out)) rets retsizes in
	(* make new arguments for pointers to returned lists *)
	let part := extract_listnames rets in
	let out_ptrs := flatten_listonly_base_ltype (fst part) in
	let innames := out_ptrs ++ flatten_argnames argnames in
	let outnames := flatten_listexcl_base_ltype (snd part) in
	(* assemble executable body: load arguments, function body, store rets *)
	let body := cmd.seq (cmd.seq load_args_cmd (snd out)) (snd store_rets) in
	(* assemble func (arg varnames, return varnames, executable body),
	also add in output list lengths *)
	(innames, outnames, body, fst store_rets).