Verification of "path" package

[HSMF]

In this PR, we verify the following functions of the path package:

• path.Clean
• path.Split

In order to verify this package, we switched out every occurrence of string with string_byte which is an alias for []byte. This is because Gobra does not yet support strings.

The main part of the work is on path.Clean, which is verified for safety and correctness. We verify that Clean adheres to the functional specification SpecClean

Open questions

In path_spec, there currently are two unverified functions ("axioms"), both marked as trusted and provided without body:

• axiomStringByteAcc: An assumption that it is always fine to restore full permissions to the string. This is not the biggest problem since the original source uses immutable strings anyways but before finalizing this, we should try to get rid of this assumption.
• axiomEqualGhostEqualPath: the assumption that for our Path struct, if a == b then a === b

[HSMF]

axiomStringByteAcc is no longer required: ca00895

[jcp19]

Is there any non-trivial dependency between this PR and PR #8? Otherwise, we might want to put in this PR only the changes that have to do with package path

[HSMF]

axiomEqualGhostEqualPath is no longer required: 54e3603

[HSMF]

Below is a table that summarizes the syntactical rewrites that we had to do to verify path. See comment on bytes.

rewrites (click to expand)

Line comments are stripped in this table

	before	after
133	return b.s[:b.w]	res = b.s[:b.w] return res
142	return string_byte(b.buf[:b.w])	res = string_byte(b.buf[:b.w]) return res
185	if path == "" { return "." }	if len(path) == 0 { res = string_byte{'.'} return res }
286	for /* @ ( unfolding Lazybuf(&out, R41) in @ */ out.w /* @)@ */ > dotdot && out.index( /* @ unfolding Lazybuf(&out, R41) in @ */ out.w) != '/' {	cond := /* @ ( unfolding Lazybuf(&out, R41) in @ */ out.w /* @)@ */ > dotdot && out.index( /* @ unfolding Lazybuf(&out, R41) in @ */ out.w) != '/' for cond {
300	}	cond = /* @ ( unfolding Lazybuf(&out, R41) in @ */ out.w /* @)@ */ > dotdot && out.index( /* @ unfolding Lazybuf(&out, R41) in @ */ out.w) != '/' }
372	return "."	res = string_byte{'.'} return res
381	return out.string()	res = out.string() return res
424	return path[:i+1], path[i+1:]	dir = path[:i+1] file = path[i+1:] return dir, file
447	if len(buf) > 0 || e != "" {	if len(buf) > 0 || len(e) != 0 {
485	if path == "" { return "." }	if len(path) == 0 { return string_byte{'.'} }