Milnes strings

[briangmilnes]

I have 'thickened' strings quite a bit. There are additions to the end of FStar.String.fst that define a partial string equality and string equality and provide a string difference (for upcoming Final testing framework). The added functions are in FStar.String.Base and quite a few proofs in FStar.String.Properties. As well as as a decidable equality class on streq.

FStar.String.Properties has 36 proofs showing the relationships between streq, streq' (it's boolean equivalent), lengths, indexes and the string differencer first_diff.

This, as expected, does not seem to increase proof times.

I did not include Base and Properties into FStar.String.fsti, so it's questionable if I have the right form here. And is it right to name the property streq and the boolean streq'?

I also added a tests/validate-time/Test.FStar.String.fst to test this.

And adjusted fstar.mk to allow overwriting of WARN_ERROR so I could cut down some warnings in validate-time tests.

[briangmilnes]

Still have the github writing to the slack channel problem, so my fix did not take.

[nikswamy]

Hi Brian, Thanks for this PR. A few comments:

1. I don't think we need streq and the equality class for strings. Strings already have decidable equality (they are eqtype) and an equality instance is given here https://github.com/FStarLang/FStar/blob/master/ulib/FStar.Class.Eq.fst#L43

2. I would rename FStar.String.Base to FStar.String.FirstDiff and remove the changes to FStar.String.fsti. By declaring these in FStar.String.fsti you are effectively assuming them as primitives in FStar.String, although you have given implementations in FStar.String.Base

3. I'll leave some other more localized comments

[briangmilnes]

Will do although I had problems proving with =, I'll try again. That's why there is a streq. Is there a definition of = on strings somewhere that I did not find?

On Mon, Oct 21, 2024 at 2:48 PM nikswamy @.***> wrote:

@.**** commented on this pull request.

In ulib/FStar.String.fsti https://github.com/FStarLang/FStar/pull/3576#discussion_r1809579436:

+val streq_upto' s1 (s2: string{strlen s1 = strlen s2}) (pos: nat{streq_upto s1 s2 pos}) :

• Tot (b:bool{b <==> streq s1 s2})

• +val streq' (s1 s2: string) : Tot (b:bool{b <==> streq s1 s2})

• +/// Return the first difference position upto a pos as an option. +val first_diff' s1 s2

• (pos: nat{pos <= strlen s1 /\ pos <= strlen s2 /\ streq_upto s1 s2 pos}) :
• Tot (o : (option (pos: nat{pos <= (min (strlen s1) (strlen s2))})) {
• (None? o ==> strlen s1 = strlen s2 /\ streq_upto s1 s2 (strlen s1)) /\
• (Some? o ==>
• streq_upto_min s1 s2 ((Some?.v o) - 1) /\
• (((Some?.v o) = strlen s1 \/ (Some?.v o) = strlen s2) /\ strlen s1 <> strlen s2)
• \/
• (((Some?.v o) < strlen s1 /\ (Some?.v o) < strlen s2) /\
• (index s1 (Some?.v o) <> (index s2 (Some?.v o)))))

This big refinement formula here is a duplicate of the formula in first_diff. Refactoring them into a single definition is better than copying it

— Reply to this email directly, view it on GitHub https://github.com/FStarLang/FStar/pull/3576#pullrequestreview-2383367394, or unsubscribe https://github.com/notifications/unsubscribe-auth/ACKMDK4FKGRDFFYSDUYZX6LZ4VZBFAVCNFSM6AAAAABQA3CT7WVHI2DSMVQWIX3LMV43YUDVNRWFEZLROVSXG5CSMV3GSZLXHMZDGOBTGM3DOMZZGQ . You are receiving this because you authored the thread.Message ID: @.***>