[Ur] couldn't prove field name disjointness compile error

Daniel Patterson dbpatterson at riseup.net
Thu Dec 31 16:51:40 EST 2009


I was adding password salting to a demo of user authentication that I
was working on (code here:
http://patch-tag.com/r/dbp/ur-play/snapshot/current/content/pretty/userpass.ur
), with the following function:

and login r =
    user <- oneOrNoRows (SELECT * FROM u WHERE (u.User = {[r.User]}));
    case user of
        None => main()
      | Some us =>
        if us.Password = Hash.sha512 (Basis.strcat
(us.Salt)(r.Password)) then
            rs <- Random.str 30;
            setCookie c {Value = {Session = rs },
                         Expires = None,
                         Secure = False};
            dml (INSERT INTO s (LoggedIn, User, Session)
                 VALUES (CURRENT_TIMESTAMP, {[r.User]}, {[rs]} ));
...

(appologies if the the line with the if got wrapped)

and it errors with the following:

userpass.ur:35:4-35:15: Couldn't prove field name disjointness
    Con 1:  [#Password = Basis.string]
    Con 2:  ([#Salt = Basis.string]) ++ <UNIF:U898::{Type}>
Hnormed 1:  [#Password = Basis.string]
Hnormed 2:  ([#Salt = Basis.string]) ++ <UNIF:U898::{Type}>
userpass.ur:35:44-35:53: Couldn't prove field name disjointness
    Con 1:  [#Salt = Basis.string]
    Con 2:  ([#Password = Basis.string]) ++ <UNIF:U898::{Type}>
Hnormed 1:  [#Salt = Basis.string]
Hnormed 2:  ([#Password = Basis.string]) ++ <UNIF:U898::{Type}>

Is this something that I can fix with explicit typing (if so how)? I'm
confused because it is saying that they are disjointed (which I read as
mismatched types), but they are all Basis.string's (which is what strcat
takes)...

Thanks,
Daniel



More information about the Ur mailing list