Require length of Loc and Jump encodings to be independent of offset

[myreen]

Currently the lab_to_target pass contains a recursive functions with a clock that can signal that the compiler should give up.

cakeml/compiler/backend/lab_to_targetScript.sml

Lines 236 to 244 in 40f98ca

	val remove_labels_def = Define `
	remove_labels init_clock c pos labs ffis sec_list =
	(* Here init_clock puts an upper limit on the number of times the
	lengths can be adjusted. In many cases, clock = 0 should be
	enough. If this were to hit the clock limit for large values of
	init_clock, then something is badly wrong. Worth testing with
	the clock limit set to low values to see how many iterations
	are used. *)
	remove_labels_loop init_clock c pos labs ffis (enc_sec_list c.encode sec_list)`;

This function should not be recursive and should not use a clock.

To remove the clock, one needs to assume that the length of encodings of Loc and Jump are independent of the label/jump offset. Concretely, enc_ok_def should change:

cakeml/compiler/encoders/asm/asmPropsScript.sml

Lines 25 to 43 in 40f98ca

	val offset_monotonic_def = Define `
	offset_monotonic enc c a1 a2 i1 i2 <=>
	asm_ok i1 c /\ asm_ok i2 c ==>
	(0w <= a1 /\ 0w <= a2 /\ a1 <= a2 ==> LENGTH (enc i1) <= LENGTH (enc i2)) /\
	(a1 < 0w /\ a2 < 0w /\ a2 <= a1 ==> LENGTH (enc i1) <= LENGTH (enc i2))`
	val enc_ok_def = Define `
	enc_ok (c : 'a asm_config) <=>
	(* code alignment and length *)
	(2 EXP c.code_alignment = LENGTH (c.encode (Inst Skip))) /\
	(!w. (LENGTH (c.encode w) MOD 2 EXP c.code_alignment = 0) /\
	LENGTH (c.encode w) <> 0) /\
	(* label instantiation predictably affects length of code *)
	(!w1 w2. offset_monotonic c.encode c w1 w2 (Jump w1) (Jump w2)) /\
	(!cmp r ri w1 w2.
	offset_monotonic c.encode c w1 w2
	(JumpCmp cmp r ri w1) (JumpCmp cmp r ri w2)) /\
	(!w1 w2. offset_monotonic c.encode c w1 w2 (Call w1) (Call w2)) /\
	(!w1 w2 r. offset_monotonic c.encode c w1 w2 (Loc r w1) (Loc r w2))`

and the implementation and verification of remove_labels should make use of the change.

[tanyongkiam]

Could you sketch how the offset_monotonic condition should be used in lab_to_target?

From what I'm reading, isn't it still possible that the length of a Jump/Loc instruction could increase when w1 increases to w2 and that could require another loop around in remove_labels?

[myreen]

I'd like it to be:

offset_monotonic enc c a1 a2 i1 i2 <=> 
(asm_ok i1 c /\ asm_ok i2 c ==> LENGTH (enc i1) = LENGTH (enc i2))

I think offset_monotonic should be renamed to enc_length_ignores_offset or similar.

[xrchz]

This should be taken into account by #1080 and is superseded by that.