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

feat: Compute matching patterns for automatic induction #5835

Open
wants to merge 47 commits into
base: master
Choose a base branch
from
Open

feat: Compute matching patterns for automatic induction #5835

wants to merge 47 commits into from

Commits on Oct 12, 2024

  1. chore: Improve trigger/induction code 

    # Conflicts:
#	Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrForallStmt.cs
    @RustanLeino
    RustanLeino committed Oct 12, 2024
    Configuration menu
    Copy the full SHA
    8c4c4a6 View commit details
    Browse the repository at this point in the history

  2. Compute triggers for automatic induction 

    # Conflicts:
#	Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs
#	Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrForallStmt.cs
    @RustanLeino
    RustanLeino committed Oct 12, 2024
    Configuration menu
    Copy the full SHA
    e62d2b6 View commit details
    Browse the repository at this point in the history

  3. Improve induction heuristics

    @RustanLeino
    RustanLeino committed Oct 12, 2024
    Configuration menu
    Copy the full SHA
    ad1c724 View commit details
    Browse the repository at this point in the history

  4. chore: Change “ghost method” to “lemma”

    @RustanLeino
    RustanLeino committed Oct 12, 2024
    Configuration menu
    Copy the full SHA
    29d715a View commit details
    Browse the repository at this point in the history

Commits on Oct 14, 2024

  1. chore: Improve C#

    @RustanLeino
    RustanLeino committed Oct 14, 2024
    Configuration menu
    Copy the full SHA
    4cfbe21 View commit details
    Browse the repository at this point in the history

  2. Also consider codatatype equality as a greatest focal predicate

    @RustanLeino
    RustanLeino committed Oct 14, 2024
    Configuration menu
    Copy the full SHA
    b17c662 View commit details
    Browse the repository at this point in the history

  3. Show tooltips for any quantifier rewrite substitutions

    @RustanLeino
    RustanLeino committed Oct 14, 2024
    Configuration menu
    Copy the full SHA
    cee8d58 View commit details
    Browse the repository at this point in the history

  4. feat!: Auto-induction for twostate lemmas but not ghost methods

    @RustanLeino
    RustanLeino committed Oct 14, 2024
    Configuration menu
    Copy the full SHA
    dda37cb View commit details
    Browse the repository at this point in the history

Commits on Oct 16, 2024

  1. fix: Don’t consider arrow-typed variables for auto induction

    @RustanLeino
    RustanLeino committed Oct 16, 2024
    Configuration menu
    Copy the full SHA
    fa79ba3 View commit details
    Browse the repository at this point in the history

  2. feat: allow ternary expressions in triggers

    @RustanLeino
    RustanLeino committed Oct 16, 2024
    Configuration menu
    Copy the full SHA
    0028a3a View commit details
    Browse the repository at this point in the history

  3. Compute and use triggers for induction hypotheses

    @RustanLeino
    RustanLeino committed Oct 16, 2024
    Configuration menu
    Copy the full SHA
    394c635 View commit details
    Browse the repository at this point in the history

  4. Tooltip named expressions from trigger selection

    @RustanLeino
    RustanLeino committed Oct 16, 2024
    Configuration menu
    Copy the full SHA
    659d4ba View commit details
    Browse the repository at this point in the history

  5. chore: Remove deprecated semi-colons

    @RustanLeino
    RustanLeino committed Oct 16, 2024
    Configuration menu
    Copy the full SHA
    6b5b207 View commit details
    Browse the repository at this point in the history

  6. Add tests for ternary expressions in triggers

    @RustanLeino
    RustanLeino committed Oct 16, 2024
    Configuration menu
    Copy the full SHA
    3fc56d3 View commit details
    Browse the repository at this point in the history

  7. Adjust resource count in test

    @RustanLeino
    RustanLeino committed Oct 16, 2024
    Configuration menu
    Copy the full SHA
    73d2d61 View commit details
    Browse the repository at this point in the history

  8. Merge branch 'master' into triggers-for-auto-induction

    @RustanLeino
    RustanLeino committed Oct 16, 2024
    Configuration menu
    Copy the full SHA
    73406c6 View commit details
    Browse the repository at this point in the history

  9. Add release notes

    @RustanLeino
    RustanLeino committed Oct 16, 2024
    Configuration menu
    Copy the full SHA
    f4815f4 View commit details
    Browse the repository at this point in the history

Commits on Oct 17, 2024

  1. Help proof

    @RustanLeino
    RustanLeino committed Oct 17, 2024
    Configuration menu
    Copy the full SHA
    e4e4ce8 View commit details
    Browse the repository at this point in the history

  2. Update test, which no longer exhausts resources

    @RustanLeino
    RustanLeino committed Oct 17, 2024
    Configuration menu
    Copy the full SHA
    3a0f1c0 View commit details
    Browse the repository at this point in the history

  3. Improve proofs

    @RustanLeino
    RustanLeino committed Oct 17, 2024
    Configuration menu
    Copy the full SHA
    703c661 View commit details
    Browse the repository at this point in the history

Commits on Oct 20, 2024

  1. Fix typo in method name

    @RustanLeino
    RustanLeino committed Oct 20, 2024
    Configuration menu
    Copy the full SHA
    54e9ddb View commit details
    Browse the repository at this point in the history

  2. Remove unnecessary assertion

    @RustanLeino
    RustanLeino committed Oct 20, 2024
    Configuration menu
    Copy the full SHA
    b46f0dc View commit details
    Browse the repository at this point in the history

  3. Remove unnecessary $’s

    @RustanLeino
    RustanLeino committed Oct 20, 2024
    Configuration menu
    Copy the full SHA
    022685c View commit details
    Browse the repository at this point in the history

  4. Improve C# and comments

    @RustanLeino
    RustanLeino committed Oct 20, 2024
    Configuration menu
    Copy the full SHA
    4cb3f5a View commit details
    Browse the repository at this point in the history

  5. Revert tooltip printing of trigger named expressions

    @RustanLeino
    RustanLeino committed Oct 20, 2024
    Configuration menu
    Copy the full SHA
    a213285 View commit details
    Browse the repository at this point in the history

  6. Improve and document methods that compute/report induction triggers

    @RustanLeino
    RustanLeino committed Oct 20, 2024
    Configuration menu
    Copy the full SHA
    72c15fe View commit details
    Browse the repository at this point in the history

  7. Incomplete attempt at specifying behavior

    @RustanLeino
    RustanLeino committed Oct 20, 2024
    Configuration menu
    Copy the full SHA
    704af8c View commit details
    Browse the repository at this point in the history

Commits on Oct 23, 2024

  1. doc: Align :induction documentation with actual behavior 

    We don't accept {:induction X} for arbitrary Xs, and bound variables must be in order.
    @cpitclaudel
    cpitclaudel committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    9e9dd80 View commit details
    Browse the repository at this point in the history

  2. Remove unnecessary $s

    @cpitclaudel
    cpitclaudel committed Oct 23, 2024
    Configuration menu
    Copy the full SHA
    8a792b1 View commit details
    Browse the repository at this point in the history

Commits on Oct 24, 2024

  1. Move :inductionPattern attribute generation to ComputeInductionTriggers 

    … and rename it to :inductionTrigger.
    @cpitclaudel
    cpitclaudel committed Oct 24, 2024
    Configuration menu
    Copy the full SHA
    7c6ab84 View commit details
    Browse the repository at this point in the history

  2. Allow users to disable trigger generation with an empty inductionTrigger

    @cpitclaudel
    cpitclaudel committed Oct 24, 2024
    Configuration menu
    Copy the full SHA
    766ac5b View commit details
    Browse the repository at this point in the history

  3. Update documentation 

    - Mention --manual-lemma-induction
- Mention {:inductionTrigger}
    @cpitclaudel
    cpitclaudel committed Oct 24, 2024
    Configuration menu
    Copy the full SHA
    a3702d2 View commit details
    Browse the repository at this point in the history

  4. Add one more test for induction triggers

    @cpitclaudel
    cpitclaudel committed Oct 24, 2024
    Configuration menu
    Copy the full SHA
    ffe54af View commit details
    Browse the repository at this point in the history

  5. Document {:inductionTrigger}

    @cpitclaudel
    cpitclaudel committed Oct 24, 2024
    Configuration menu
    Copy the full SHA
    8c7b06c View commit details
    Browse the repository at this point in the history

Commits on Oct 30, 2024

  1. Always report “inductionTrigger”, not just in DEBUG build

    @RustanLeino
    RustanLeino committed Oct 30, 2024
    Configuration menu
    Copy the full SHA
    769d6cd View commit details
    Browse the repository at this point in the history

  2. Fix format of expected test output

    @RustanLeino
    RustanLeino committed Oct 30, 2024
    Configuration menu
    Copy the full SHA
    2c7fcc9 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' into triggers-for-auto-induction 

    # Conflicts:
#	Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs
#	Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrForallStmt.cs
#	Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo
#	Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo
#	Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo
#	Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo
#	Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo
#	Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo
#	Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo
#	Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect
    @RustanLeino
    RustanLeino committed Oct 30, 2024
    Configuration menu
    Copy the full SHA
    62e771c View commit details
    Browse the repository at this point in the history

Commits on Oct 31, 2024

  1. Use underscore name for generated attributes 

    * By using _inductionTrigger for generated triggers, the Dafny machinery for cloning things into refinement modules works correctly
* Tooltips only show things not already in the program text
    @RustanLeino
    RustanLeino committed Oct 31, 2024
    Configuration menu
    Copy the full SHA
    af0223b View commit details
    Browse the repository at this point in the history

  2. Update tests

    @RustanLeino
    RustanLeino committed Oct 31, 2024
    Configuration menu
    Copy the full SHA
    6cdaa08 View commit details
    Browse the repository at this point in the history

  3. Update tests and expected output

    @RustanLeino
    RustanLeino committed Oct 31, 2024
    Configuration menu
    Copy the full SHA
    a1149c9 View commit details
    Browse the repository at this point in the history

  4. Fix previous code edit

    @RustanLeino
    RustanLeino committed Oct 31, 2024
    Configuration menu
    Copy the full SHA
    c447ffa View commit details
    Browse the repository at this point in the history

  5. Merge branch 'master' into triggers-for-auto-induction

    @RustanLeino
    RustanLeino committed Oct 31, 2024
    Configuration menu
    Copy the full SHA
    3d8d0e7 View commit details
    Browse the repository at this point in the history

  6. Update standard libraries

    @RustanLeino
    RustanLeino committed Oct 31, 2024
    Configuration menu
    Copy the full SHA
    63683d1 View commit details
    Browse the repository at this point in the history

  7. Merge branch 'master' into triggers-for-auto-induction

    @RustanLeino
    RustanLeino committed Oct 31, 2024
    Configuration menu
    Copy the full SHA
    808a2b3 View commit details
    Browse the repository at this point in the history

  8. Merge branch 'master' into triggers-for-auto-induction 

    # Conflicts:
#	Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo
#	Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo
#	Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo
#	Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo
#	Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo
#	Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo
#	Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo
    @RustanLeino
    RustanLeino committed Oct 31, 2024
    Configuration menu
    Copy the full SHA
    43bdbd3 View commit details
    Browse the repository at this point in the history

  9. Update standard library

    @RustanLeino
    RustanLeino committed Oct 31, 2024
    Configuration menu
    Copy the full SHA
    3652ff3 View commit details
    Browse the repository at this point in the history

Commits on Nov 1, 2024

  1. Update standard library

    @RustanLeino
    RustanLeino committed Nov 1, 2024
    Configuration menu
    Copy the full SHA
    b070751 View commit details
    Browse the repository at this point in the history