Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Ghost Constraint Stabilization #1271

Merged
merged 66 commits into from
Jan 13, 2023
Merged

Ghost Constraint Stabilization #1271

merged 66 commits into from
Jan 13, 2023

Commits on Nov 28, 2022

  1. recognize and reject extern specs which define bodies for their methods

    @juliand665
    juliand665 committed Nov 28, 2022
    Configuration menu
    Copy the full SHA
    3e8cfef View commit details
    Browse the repository at this point in the history

  2. support multiple constraints in ghost constraints

    @juliand665
    juliand665 committed Nov 28, 2022
    Configuration menu
    Copy the full SHA
    6e4fcdb View commit details
    Browse the repository at this point in the history

  3. correctly support purity ghost constraints 

    turns out the previous implementation was flawed in that it made the function pure whether or not the constraint held
    @juliand665
    juliand665 committed Nov 28, 2022
    Configuration menu
    Copy the full SHA
    352baa8 View commit details
    Browse the repository at this point in the history

  4. require at least one bound for ghost constraints

    @juliand665
    juliand665 committed Nov 28, 2022
    Configuration menu
    Copy the full SHA
    10613be View commit details
    Browse the repository at this point in the history

  5. report example structure only when it makes sense

    @juliand665
    juliand665 committed Nov 28, 2022
    Configuration menu
    Copy the full SHA
    ab1f109 View commit details
    Browse the repository at this point in the history

  6. add compiletests for ghost constraint purity

    @juliand665
    juliand665 committed Nov 28, 2022
    Configuration menu
    Copy the full SHA
    b5e3776 View commit details
    Browse the repository at this point in the history

  7. auto-format prusti-specs crate

    @juliand665
    juliand665 committed Nov 28, 2022
    Configuration menu
    Copy the full SHA
    18ac669 View commit details
    Browse the repository at this point in the history

  8. unify handling of bodies in extern specs and check more places

    @juliand665
    juliand665 committed Nov 28, 2022
    Configuration menu
    Copy the full SHA
    99a17bf View commit details
    Browse the repository at this point in the history

  9. add unit test for bodies in extern specs

    @juliand665
    juliand665 committed Nov 28, 2022
    Configuration menu
    Copy the full SHA
    0112241 View commit details
    Browse the repository at this point in the history

  10. update unit tests

    @juliand665
    juliand665 committed Nov 28, 2022
    Configuration menu
    Copy the full SHA
    44358db View commit details
    Browse the repository at this point in the history

Commits on Dec 7, 2022

  1. parse new syntax for ghost constraints/conditional spec refinements

    @juliand665
    juliand665 committed Dec 7, 2022
    Configuration menu
    Copy the full SHA
    3535dbb View commit details
    Browse the repository at this point in the history

  2. add failing test for extraneous comma before specs

    @juliand665
    juliand665 committed Dec 7, 2022
    Configuration menu
    Copy the full SHA
    f30d131 View commit details
    Browse the repository at this point in the history

  3. update example in error note

    @juliand665
    juliand665 committed Dec 7, 2022
    Configuration menu
    Copy the full SHA
    5a6ab38 View commit details
    Browse the repository at this point in the history

  4. remove ghost constraint feature flag 

    you can still introduce unsound behavior with them, but they're far from the only way to do so, and absolutely necessary for prusti std
    @juliand665
    juliand665 committed Dec 7, 2022
    Configuration menu
    Copy the full SHA
    6c30fef View commit details
    Browse the repository at this point in the history

  5. rename ghost constraints to conditional spec refinements in user-faci… 

    …ng strings & comments
    @juliand665
    juliand665 committed Dec 7, 2022
    Configuration menu
    Copy the full SHA
    4a5dc33 View commit details
    Browse the repository at this point in the history

  6. formatting

    @juliand665
    juliand665 committed Dec 7, 2022
    Configuration menu
    Copy the full SHA
    eae12e0 View commit details
    Browse the repository at this point in the history

  7. address clippy's concerns

    @juliand665
    juliand665 committed Dec 7, 2022
    Configuration menu
    Copy the full SHA
    b187acc View commit details
    Browse the repository at this point in the history

Commits on Dec 11, 2022

  1. add unit test for trait impls with generic arguments 

    removed a check preventing use of this feature previously; this effectively formalizes it as working
    @juliand665
    juliand665 committed Dec 11, 2022
    Configuration menu
    Copy the full SHA
    d0e3fd2 View commit details
    Browse the repository at this point in the history

Commits on Dec 12, 2022

  1. improve test

    @juliand665
    juliand665 committed Dec 12, 2022
    Configuration menu
    Copy the full SHA
    a9cb317 View commit details
    Browse the repository at this point in the history

Commits on Dec 16, 2022

  1. desugaring fixes 

    expressions are not implicitly in parentheses, creating very strange errors when desugaring e.g. a + b to &a + b
    @juliand665
    juliand665 committed Dec 16, 2022
    Configuration menu
    Copy the full SHA
    d4069dd View commit details
    Browse the repository at this point in the history

  2. conditional spec refinements -> type-conditional spec refinements

    @juliand665
    juliand665 committed Dec 16, 2022
    Configuration menu
    Copy the full SHA
    c9ae6ef View commit details
    Browse the repository at this point in the history

  3. rename ghost constraints to type-conditional spec refinements everywhere

    @juliand665
    juliand665 committed Dec 16, 2022
    Configuration menu
    Copy the full SHA
    5e85a13 View commit details
    Browse the repository at this point in the history

  4. update test to reflect that generics are supported 

    not thoroughly tested, but let's not let perfect be the enemy of good enough
    @juliand665
    juliand665 committed Dec 16, 2022
    Configuration menu
    Copy the full SHA
    76e6f65 View commit details
    Browse the repository at this point in the history

  5. update test to reflect that generics are supported 

    not thoroughly tested, but let's not let perfect be the enemy of good enough
    @juliand665
    juliand665 committed Dec 16, 2022
    Configuration menu
    Copy the full SHA
    c1c8cc0 View commit details
    Browse the repository at this point in the history

Commits on Dec 17, 2022

  1. adjust join_spans testing-specific behavior 

    testing-specific workaround is now only present when cfg(test) is active
    @juliand665
    juliand665 committed Dec 17, 2022
    Configuration menu
    Copy the full SHA
    32b342c View commit details
    Browse the repository at this point in the history

  2. make typecondspec parser more robust, require comma again

    @juliand665
    juliand665 committed Dec 17, 2022
    Configuration menu
    Copy the full SHA
    33669ea View commit details
    Browse the repository at this point in the history

  3. update overlooked holdover of old ghost constraint term

    @juliand665
    juliand665 committed Dec 17, 2022
    Configuration menu
    Copy the full SHA
    9d2fe45 View commit details
    Browse the repository at this point in the history

  4. fix typo

    @juliand665
    juliand665 committed Dec 17, 2022
    Configuration menu
    Copy the full SHA
    3cc4388 View commit details
    Browse the repository at this point in the history

  5. update compiletests to new typecondspec syntax

    @juliand665
    juliand665 committed Dec 17, 2022
    Configuration menu
    Copy the full SHA
    c080ee7 View commit details
    Browse the repository at this point in the history

  6. Merge remote-tracking branch 'upstream/master'

    @juliand665
    juliand665 committed Dec 17, 2022
    Configuration menu
    Copy the full SHA
    d9a78b8 View commit details
    Browse the repository at this point in the history

  7. update preparser tests to include the new parentheses

    @juliand665
    juliand665 committed Dec 17, 2022
    Configuration menu
    Copy the full SHA
    6c4076b View commit details
    Browse the repository at this point in the history

  8. update cargo test

    @juliand665
    juliand665 committed Dec 17, 2022
    Configuration menu
    Copy the full SHA
    bb01b49 View commit details
    Browse the repository at this point in the history

  9. update more compiletests

    @juliand665
    juliand665 committed Dec 17, 2022
    Configuration menu
    Copy the full SHA
    6c6ba20 View commit details
    Browse the repository at this point in the history

  10. update more compiletests

    @juliand665
    juliand665 committed Dec 17, 2022
    Configuration menu
    Copy the full SHA
    f4dfa7e View commit details
    Browse the repository at this point in the history

Commits on Dec 19, 2022

  1. allow merge clauses for extern trait specs 

    implemented by simply tacking on our bound to the existing clause
    @juliand665
    juliand665 committed Dec 19, 2022
    Configuration menu
    Copy the full SHA
    13e8fb2 View commit details
    Browse the repository at this point in the history

  2. allow extern_spec to take a module argument & apply to free functions 

    the module argument is not valid on impls, since those already work with qualified type paths
    @juliand665
    juliand665 committed Dec 19, 2022
    Configuration menu
    Copy the full SHA
    d038693 View commit details
    Browse the repository at this point in the history

  3. update tests

    @juliand665
    juliand665 committed Dec 19, 2022
    Configuration menu
    Copy the full SHA
    b60dae2 View commit details
    Browse the repository at this point in the history

  4. allow trailing commas in where clauses on extern specs on traits

    @juliand665
    juliand665 committed Dec 19, 2022
    Configuration menu
    Copy the full SHA
    94f8d4c View commit details
    Browse the repository at this point in the history

Commits on Dec 20, 2022

  1. ignore lifetimes in pure function substs

    @juliand665
    juliand665 committed Dec 20, 2022
    Configuration menu
    Copy the full SHA
    c243fc5 View commit details
    Browse the repository at this point in the history

  2. ignore lifetimes in extern spec sanity check too

    @juliand665
    juliand665 committed Dec 20, 2022
    Configuration menu
    Copy the full SHA
    501a737 View commit details
    Browse the repository at this point in the history

Commits on Dec 29, 2022

  1. always use lifetimes from args instead of generics 

    generic lifetimes are erased during trait impl resolution
    @juliand665
    juliand665 committed Dec 29, 2022
    Configuration menu
    Copy the full SHA
    b3be7e8 View commit details
    Browse the repository at this point in the history

  2. clippy

    @juliand665
    juliand665 committed Dec 29, 2022
    Configuration menu
    Copy the full SHA
    8d2d8bc View commit details
    Browse the repository at this point in the history

Commits on Jan 4, 2023

  1. update user guide with new typecondspec syntax

    @juliand665
    juliand665 committed Jan 4, 2023
    Configuration menu
    Copy the full SHA
    379e2da View commit details
    Browse the repository at this point in the history

  2. add regression test for trait resolution with references

    @juliand665
    juliand665 committed Jan 4, 2023
    Configuration menu
    Copy the full SHA
    811ac31 View commit details
    Browse the repository at this point in the history

  3. update broken link

    @juliand665
    juliand665 committed Jan 4, 2023
    Configuration menu
    Copy the full SHA
    23dbd7d View commit details
    Browse the repository at this point in the history

Commits on Jan 5, 2023

  1. use lifetimes from substs when possible

    @juliand665
    juliand665 committed Jan 5, 2023
    Configuration menu
    Copy the full SHA
    be6cee0 View commit details
    Browse the repository at this point in the history

  2. erase lifetimes only when resolved method differs

    @juliand665
    juliand665 committed Jan 5, 2023
    Configuration menu
    Copy the full SHA
    317ab08 View commit details
    Browse the repository at this point in the history

Commits on Jan 6, 2023

  1. tiny fix 

    got lost in the refactor; i blame copilot lol
    @juliand665
    juliand665 committed Jan 6, 2023
    Configuration menu
    Copy the full SHA
    9897e55 View commit details
    Browse the repository at this point in the history

  2. fix some test indentation

    @juliand665
    juliand665 committed Jan 6, 2023
    Configuration menu
    Copy the full SHA
    b00c103 View commit details
    Browse the repository at this point in the history

  3. remove unnecessary derive

    @juliand665
    juliand665 committed Jan 6, 2023
    Configuration menu
    Copy the full SHA
    2634786 View commit details
    Browse the repository at this point in the history

  4. rename missed test folders

    @juliand665
    juliand665 committed Jan 6, 2023
    Configuration menu
    Copy the full SHA
    6ff4c4a View commit details
    Browse the repository at this point in the history

  5. improve generic trait tests

    @juliand665
    juliand665 committed Jan 6, 2023
    Configuration menu
    Copy the full SHA
    333c869 View commit details
    Browse the repository at this point in the history

Commits on Jan 8, 2023

  1. update comment

    @juliand665
    juliand665 committed Jan 8, 2023
    Configuration menu
    Copy the full SHA
    6433cd9 View commit details
    Browse the repository at this point in the history

  2. drop unhelpful comment

    @juliand665
    juliand665 committed Jan 8, 2023
    Configuration menu
    Copy the full SHA
    3943e37 View commit details
    Browse the repository at this point in the history

  3. remove outdated comment 

    better no information than inaccurate information!
    @juliand665
    juliand665 committed Jan 8, 2023
    Configuration menu
    Copy the full SHA
    021f88f View commit details
    Browse the repository at this point in the history

  4. fix spans for binary ops 

    while preserving the safety of parenthesizing incoming LHS/RHS
    @juliand665
    juliand665 committed Jan 8, 2023
    Configuration menu
    Copy the full SHA
    2d523eb View commit details
    Browse the repository at this point in the history

  5. obsolete #[generic]/#[concrete] for traits 

    the latter didn't work anyway, and now that we have type-cond-specs, we know we won't need it, so we can drop the annotations entirely.
    @juliand665
    juliand665 committed Jan 8, 2023
    Configuration menu
    Copy the full SHA
    46a863d View commit details
    Browse the repository at this point in the history

  6. update tests for trait parameter attribute removal

    @juliand665
    juliand665 committed Jan 8, 2023
    Configuration menu
    Copy the full SHA
    e5b96df View commit details
    Browse the repository at this point in the history

  7. update preparser cfg tests

    @juliand665
    juliand665 committed Jan 8, 2023
    Configuration menu
    Copy the full SHA
    0684867 View commit details
    Browse the repository at this point in the history

  8. rewrite self type in newly-allowed where clauses 

    where clauses on traits
    @juliand665
    juliand665 committed Jan 8, 2023
    Configuration menu
    Copy the full SHA
    eb01178 View commit details
    Browse the repository at this point in the history

Commits on Jan 12, 2023

  1. bump cache version 

    we were getting spurious failures for the core proof tests from old data
    @juliand665
    juliand665 committed Jan 12, 2023
    Configuration menu
    Copy the full SHA
    6072933 View commit details
    Browse the repository at this point in the history

  2. mangle function names for extern specs

    @juliand665
    juliand665 committed Jan 12, 2023
    Configuration menu
    Copy the full SHA
    f8c3954 View commit details
    Browse the repository at this point in the history

  3. flatten extern spec modules 

    it's like they were never there! no more use crate::*;
    @juliand665
    juliand665 committed Jan 12, 2023
    Configuration menu
    Copy the full SHA
    d1e49e7 View commit details
    Browse the repository at this point in the history

  4. update tests

    @juliand665
    juliand665 committed Jan 12, 2023
    Configuration menu
    Copy the full SHA
    e29553c View commit details
    Browse the repository at this point in the history

  5. only mangle free functions 

    keep the changes to a minimum
    @juliand665
    juliand665 committed Jan 12, 2023
    Configuration menu
    Copy the full SHA
    c1743f7 View commit details
    Browse the repository at this point in the history

Commits on Jan 13, 2023

  1. Merge branch 'master' into master

    @juliand665
    juliand665 authored Jan 13, 2023
    Configuration menu
    Copy the full SHA
    c0561fa View commit details
    Browse the repository at this point in the history