Milnes strings

ocaml/fstar-lib/FStarC_Parser_LexFStar.ml

@@ -473,6 +473,7 @@ match%sedlex lexbuf with
  | "#print-effects-graph" -> PRAGMA_PRINT_EFFECTS_GRAPH
  | "__SOURCE_FILE__" -> STRING (L.source_file lexbuf)
  | "__LINE__" -> INT (string_of_int (L.current_line lexbuf), false)
+ | "__FL__"   -> STRING ((L.source_file lexbuf) ^ "(" ^ (string_of_int (L.current_line lexbuf)) ^ ")")
 
  | Plus anywhite -> token lexbuf
  | newline -> L.new_line lexbuf; token lexbuf

tests/Makefile

@@ -21,6 +21,7 @@ ALL_TEST_DIRS += vale
 ALL_TEST_DIRS += hacl
 ALL_TEST_DIRS += simple_hello
 ALL_TEST_DIRS += dune_hello
+ALL_TEST_DIRS += validation-time
 HAS_OCAML := $(shell which ocamlfind 2>/dev/null)
 
 ifneq (,$(HAS_OCAML))

tests/validation-time/Makefile

@@ -0,0 +1,22 @@
+#
+# This does nothing but the default validation as these are validation time test modules.
+# Most are let _ = assert(...) which is extremely cool to test at validation time! 
+# 
+
+WARN_ERROR=--warn_error -321
+FSTAR_HOME=../..
+FSTAR_FILES=$(wildcard *.fst)
+FSTAR_EXAMPLES=$(realpath ../../examples)
+include $(FSTAR_EXAMPLES)/Makefile.include
+
+all: verify-all
+
+include $(FSTAR_HOME)/examples/Makefile.common
+
+verify-all: $(CACHE_DIR) $(addsuffix .checked, $(addprefix $(CACHE_DIR)/, $(FSTAR_FILES)))
+
+clean:
+	$(call msg, "CLEAN")
+	$(Q)rm -f .depend
+	$(Q)rm -rf _cache
+	$(Q)rm -rf _output

tests/validation-time/README.md

@@ -0,0 +1,5 @@
+
+  This directory contains tests that run on Make all which only validate F* files.
+ This allows validation time tests. If any validation fails, the file's tests fail.
+
+  Tests for an F* module FStar.M can be named Test.FStar.M.fst by default.

tests/validation-time/Test.FStar.String.fst

@@ -0,0 +1,89 @@
+module Test.FStar.String
+
+open FStar.String
+open FStar.Tactics.V2
+open FStar.IO
+
+
+open FStar.String
+open FStar.Class.Printable
+
+let _ = assert(streq "" "")
+let _ = assert(streq "A" "A")
+
+///   Is this caused by strlen being UTF8 characters instead of bytes?
+///  And there is no byte length.
+let _ = assert(strlen "A" = 1) by compute()
+let _ = assert(~(streq "A" "AB")) by compute()
+let _ = assert(streq_upto "A" "AB" 0)
+let _ = assert(streq_upto "AB" "AB" 0)
+
+[@@expect_failure]
+let _ = assert(streq_upto "AB" "AB" 1)
+
+let _ = assert(streq_upto "AB" "AB" 1) by compute()
+
+[@@expect_failure]
+let _ = assert(streq_upto "AB" "AB" 2)
+let _ = assert(streq_upto "AB" "AB" 2) by compute()
+
+[@@expect_failure]
+let _ = assert(~ (streq "A" "B"))
+let _ = assert(~(streq "A" "AB")) by compute()
+[@@expect_failure]
+let _ = assert(~(streq "AB" "Ab")) by compute()
+
+///  The boolean form is hidden behind the interface.
+[@@expect_failure]
+let _ = assert(~ (streq "A" "B")) by compute()
+let _ = assert(streq' "" "") by compute()
+[@@expect_failure]
+let _ = assert(not (streq' "" "A")) by compute()
+
+
+/// Of course by compute can't prove things it can't see a definition on.
+/// So once you hide it behind an interface it can't run it.
+/// So I need a test module but this goes in before Final so no tests yet.
+[@@expect_failure]
+let _ = assert(lines "" 0 = (0,0))  by compute()
+
+[@@expect_failure]
+let _ = assert(lines "A" 0 = (0,0)) by compute()
+let _ = assert(strlen "A" = 1)      by compute()
+
+let strlen_A_1 () : Lemma (strlen "A" = 1) = assert(strlen "A" = 1) by compute()
+[@@expect_failure]
+let _ = assert(strlen_A_1(); lines "A" 1 = (0,1)) by compute()
+
+[@@expect_failure]
+let _ = assert(strlen "A\n" = 2) by compute();
+        assert(lines "A\n" 1 = (0,1)) by compute()
+
+[@@expect_failure]
+let _ = assert(strlen "AB\nC\nD" = 6) by compute();
+        assert(lines  "AB\nC\nD" 0 = (0,0)) by compute()
+
+[@@expect_failure]
+let _ = assert(strlen "AB\nC\nD" = 6) by compute();
+        assert(lines  "AB\nC\nD" 1 = (0,1)) by compute()
+
+[@@expect_failure]
+let _ = assert(strlen "AB\nC\nD" = 6) by compute();
+        assert(lines  "AB\nC\nD" 2 = (0,2)) by compute()
+
+[@@expect_failure]
+let _ = assert(strlen "AB\nC\nD" = 6) by compute();
+        assert(lines  "AB\nC\nD" 3 = (1,0)) by compute()
+
+[@@expect_failure]
+let _ = assert(strlen "AB\nC\nD" = 6) by compute();
+        assert(lines  "AB\nC\nD" 4 = (1,1)) by compute()
+
+[@@expect_failure]
+let _ = assert(strlen "AB\nC\nD" = 6) by compute();
+        assert(lines  "AB\nC\nD" 5 = (2,0)) by compute()
+
+[@@expect_failure]
+let _ = assert(strlen "AB\nC\nD" = 6) by compute();
+        assert(lines  "AB\nC\nD" 6 = (2,1)) by compute()
+

tests/validation-time/Test.LexemeFL.fst

@@ -0,0 +1,13 @@
+///  A new lexeme __FL__ has been added to show file and line (file(line)) to make writing tests easier.
+/// This file is line sensitive any edit will change the value of __FL__.
+module Test.LexemeFL
+open FStar.Tactics.V2
+open FStar.String
+module LT = FStar.List.Tot
+// Kinda funky to get a good validation time test, added Strings in other PR will fix this.
+// The lexer is sending back some strange character that we have to adjust.
+let fl = __FL__ 
+let _ = assert(fl <> "")
+let fl'  = string_of_list (list_of_string "Test.LexemFL.fst(11)")
+let _ = assert((strlen fl') = 20) by compute()
+let _ = assert(fl' = "Test.LexemFL.fst(11)") by compute()

ulib/FStar.String.Base.fst

@@ -0,0 +1,77 @@
+(*
+   Copyright 2024 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+
+module FStar.String.Base
+
+open FStar.String
+
+let rec streq_upto' s1 (s2: string{strlen s1 = strlen s2})  (pos: nat{streq_upto s1 s2 pos}) :
+  Tot (b:bool{b <==> streq s1 s2})
+  (decreases strlen s1 - pos)
+=     
+ if pos = strlen s1 
+ then true
+ else if index s1 pos = index s2 pos
+ then streq_upto' s1 s2 (pos+1)
+ else false
+
+let streq' (s1 s2: string) : Tot (b:bool{b <==> streq s1 s2})
+=
+  if strlen s1 <> strlen s2
+  then false
+  else streq_upto' s1 s2 0 
+
+let rec 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)))))
+        })
+       (decreases (strlen s1 - pos))
+=
+ if pos = strlen s1 && pos = strlen s2
+ then None
+ else if pos >= (strlen s1) || pos >= (strlen s2)
+ then Some pos
+ else begin 
+   if (index s1 pos) <> (index s2 pos) 
+   then Some pos
+   else first_diff' s1 s2 (pos+1)
+ end
+
+let first_diff s1 s2 = first_diff' s1 s2 0
+
+let rec lines' s (upto:nat{upto <= strlen s}) 
+           lastnewline lines chars (pos: nat{pos <= upto && pos <= strlen s}) :
+  Tot (nat & nat) 
+      (decreases upto - pos)
+= if pos = upto 
+  then (if lastnewline then (lines+1, chars) else (lines, chars))
+  else if index s pos = '\n'  
+  then lines' s upto true  lines  0 (pos + 1)
+  else (if lastnewline 
+        then lines' s upto false (lines+1) chars    (pos + 1)
+        else lines' s upto false lines    (chars+1) (pos + 1))
+
+///  Return the line and character upto pos counting each starting at zero.
+let lines (s: string) (upto:nat{upto <= strlen s}) : Tot (nat & nat) = 
+  lines' s upto false 0 0 0
+

ulib/FStar.String.Eq.fst

@@ -0,0 +1,49 @@
+(*
+   Copyright 2024 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+
+module FStar.String.Eq
+
+open FStar.List.Tot.Properties
+module EqRaw = FStar.Class.Eq.Raw
+module Eq  = FStar.Class.Eq
+
+open FStar.String
+open FStar.String.Base
+open FStar.String.Properties
+
+let decides_eqtype (#a:eqtype) (f : a -> a -> bool) : prop =
+  forall x y. f x y <==> x = y
+
+let streq'_decides_deq () :
+ Lemma (decides_eqtype streq')
+= introduce forall x y. streq' x y <==> x == y
+  with streq'_iff_eq x y
+
+instance streq'_is_deq : EqRaw.deq string = {
+  eq = streq'
+}
+
+///  Propeq properties 
+
+let streq'_decides_eq () :
+ Lemma (Eq.decides_eq streq')
+= introduce forall x y. streq' x y <==> x == y
+  with streq'_iff_propeq x y
+
+instance streq'_is_eq : Eq.deq string = {
+  raw    = streq'_is_deq;
+  eq_dec = streq'_decides_deq ()
+}