GitLab

Made a gc access lemma stronger (old one was too weak for the proof)

updated _CoqProject file

generalized rdcss_minor to return boolean indicating if the n1 matches the value read at the second location lln

    Now both the left and right reference point to an integer. rdcss_minor takes as input the pair of references and three values (m1, n1, n2). It atomically does the following:

    If the left value equals m1 and the right value equals n1, then the right value is updated to n2.