replace borrow with theory expression

[aep]

a theory can now finally contain an expression body

pub theory small(x) -> bool (x < 10)

borrow is now deprecated and will eventually be completely removed. to carry type state, simply use expressive theories

pub dothings(int mut * x)
    where small(*x)
    model small(*x)

this change also rewrites string using integrity theories

string is renamed to buffer, to make the name string available for a unicode implementation. buffer holds null terminated data, which may be something not a string.

this change also rewrites slice using integrity theories

mut_slice should now be passed by by value rather than pointer. the state is internally held as pointer. this makes the api more composable.

[jwerle]

this is huge!

[aep]

Do you intend to implement string again?

@jwerle no. i dont have time to implement unicode support. if someone else wants to contribute that, that would be great of course. (#44)

[jwerle]

@aep I'll take a look! I did some stuff over here before: https://github.com/jwerle/libutf8