Code

Add Prusti-ish frontend to Creusot#932

Code

Open

dewert99 wants to merge 102 commits intocreusot-rs:mastercreusot-rs/creusot:masterfrom dewert99:prustidewert99/creusot:prustiCopy head branch name to clipboard

+7,662-36

Commits

Commits on Oct 20, 2022

• Initial implementation of Prusti to Creusot conversion

  dewert99

  committed
  a62f47c

  Copy full SHA for a62f47c

• Fixed handling of after_expiry

  dewert99

  committed
  03312a2

  Copy full SHA for 03312a2

Commits on Oct 21, 2022

• Merge remote-tracking branch 'origin/master' into prusti

  Show description for 5944625
  dewert99

  committed
  5944625

  Copy full SHA for 5944625

• Fixed tests after merge

  dewert99

  committed
  9d02456

  Copy full SHA for 9d02456

• Merge remote-tracking branch 'origin/641' into prusti

  dewert99

  committed
  128a82e

  Copy full SHA for 128a82e

Commits on Oct 22, 2022

• Added support for prusti logical functions (TODO treat them differently when they are called)

  dewert99

  committed
  482418c

  Copy full SHA for 482418c

Commits on Oct 29, 2022

• Added support for calling logical functions with home signatures.

  Show description for a54842a
  dewert99

  committed
  a54842a

  Copy full SHA for a54842a

• Switched logical calls to trait methods to use the implementors logical signature if possible

  dewert99

  committed
  f175b29

  Copy full SHA for f175b29

Commits on Oct 31, 2022

• Improved handling of associated types

  dewert99

  committed
  a0bb4aa

  Copy full SHA for a0bb4aa

Commits on Nov 1, 2022

• Fixed introduced issue with regular creusot functions

  dewert99

  committed
  f4bb934

  Copy full SHA for f4bb934

Commits on Nov 2, 2022

• Added curr and expiry stubs

  dewert99

  committed
  0e4c737

  Copy full SHA for 0e4c737

• Merge remote-tracking branch 'origin/master' into prusti

  dewert99

  committed
  c36c45a

  Copy full SHA for c36c45a

Commits on Nov 4, 2022

• Switched prusti import to prusti_prelude and added support for implications

  dewert99

  committed
  64728a5

  Copy full SHA for 64728a5

Commits on Nov 7, 2022

• Fixed some quantifiers and box dereferences and added work around for functions logical functions that take "made up" references

  dewert99

  committed
  332144e

  Copy full SHA for 332144e

• Fixed issue with lifetimes bound in impl block and added prusti versions of predicate and law

  dewert99

  committed
  dfc2bdc

  Copy full SHA for dfc2bdc

Commits on Nov 17, 2022

• Tricked at_expiry into using an early-bound lifetime

  dewert99

  committed
  23d39fe

  Copy full SHA for 23d39fe

• Hacky patch to help avoid subtly wrong uses of <&mut T>::shallow_model()

  dewert99

  committed
  92267df

  Copy full SHA for 92267df

Commits on Jun 6, 2023

• Merge branch 'master' into prusti

  Show description for cecc51b
  dewert99

  committed
  cecc51b

  Copy full SHA for cecc51b

Commits on Jun 7, 2023

• Switch translation to work with new rustc

  dewert99

  committed
  7c28341

  Copy full SHA for 7c28341

Commits on Jun 8, 2023

• Mostly got tests passing again

  dewert99

  committed
  c99e72a

  Copy full SHA for c99e72a

Commits on Jun 9, 2023

• Switched to a more precise region tracking system and fixed remaining test

  dewert99

  committed
  daecf8d

  Copy full SHA for daecf8d

• Extracted away pearlite

  dewert99

  committed
  8cecdaa

  Copy full SHA for 8cecdaa

• Improved support for constructors

  dewert99

  committed
  a6d4a60

  Copy full SHA for a6d4a60

• Switched behaviour when calling function without a "home-signature" to assume everything has a home in the current time-slice

  dewert99

  committed
  f595c95

  Copy full SHA for f595c95

• Improve error messages

  dewert99

  committed
  7c6ec37

  Copy full SHA for 7c6ec37

Commits on Jun 19, 2023

• Refactor to support outlive based requirements

  dewert99

  committed
  e6e0dac

  Copy full SHA for e6e0dac

Commits on Jun 20, 2023

• Fixed handling of shared references and boxes.

  dewert99

  committed
  1fe9ad4

  Copy full SHA for 1fe9ad4

• Prevented making references to invalid types

  dewert99

  committed
  7910fbf

  Copy full SHA for 7910fbf

Commits on Jun 21, 2023

• Started copy types to be coerced into the current time slice if they live long enough

  dewert99

  committed
  0907116

  Copy full SHA for 0907116

• Allowed copy types to be coerced into the current time slice if they live long enough in more places

  dewert99

  committed
  f683ec9

  Copy full SHA for f683ec9

• Added smallvec dependency

  dewert99

  committed
  89a6d29

  Copy full SHA for 89a6d29

• Fixed issue where copy types could be coerced into a time slice in the past

  dewert99

  committed
  bbed4eb

  Copy full SHA for bbed4eb

• Made unspecified home signatures default to using 'curr everywhere

  dewert99

  committed
  21b4e12

  Copy full SHA for 21b4e12

• Extracted constants

  dewert99

  committed
  dde9f05

  Copy full SHA for dde9f05

Commits on Jun 22, 2023

• Added zombie lint to be more strict and prevent types with invalid homes to exist at all

  dewert99

  committed
  373f03c

  Copy full SHA for 373f03c

• Improved lint handling

  dewert99

  committed
  2d1994a

  Copy full SHA for 2d1994a

• Fixed issue with at_expiry

  dewert99

  committed
  63a8fe4

  Copy full SHA for 63a8fe4

• Switched zombie lint to used non type based information, this makes it stricter, but also less likely to report duplicate errors

  dewert99

  committed
  2e957f3

  Copy full SHA for 2e957f3

• Added test

  dewert99

  committed
  d948039

  Copy full SHA for d948039

Commits on Jun 27, 2023

• Merge branch 'master' into prusti

  dewert99

  committed
  0d19502

  Copy full SHA for 0d19502

• Blessed changes to tests caused by merge

  dewert99

  committed
  6f63c56

  Copy full SHA for 6f63c56

Commits on Jun 28, 2023

• Allowed logic funtions to infer some outlive relations based on type well formedness

  dewert99

  committed
  75736f8

  Copy full SHA for 75736f8

• Fixed bug with when calling functions with 'curr in there signature

  dewert99

  committed
  348dd5f

  Copy full SHA for 348dd5f

• Fixed bug with at_expiry

  dewert99

  committed
  55d326c

  Copy full SHA for 55d326c

Commits on Jun 29, 2023

• Fixed bug with normalization

  dewert99

  committed
  7ba49c4

  Copy full SHA for 7ba49c4

Commits on Jul 2, 2023

• Refactored, improved 'static support and added snapshot feature

  dewert99

  committed
  6f7691e

  Copy full SHA for 6f7691e

Commits on Jul 4, 2023

• Fixed bug with quantifiers

  dewert99

  committed
  1345678

  Copy full SHA for 1345678

• Made equality require types to be valid

  dewert99

  committed
  45986a8

  Copy full SHA for 45986a8

• Fixed bug with tuples

  dewert99

  committed
  31a28be

  Copy full SHA for 31a28be

Commits on Jul 12, 2023

• Allowed de-referencing an &'a &mut T to an &'a T

  dewert99

  committed
  9a8c29a

  Copy full SHA for 9a8c29a

Commits on Sep 16, 2023

• Merge branch 'master' into prusti

  Show description for af857cc
  dewert99

  committed
  af857cc

  Copy full SHA for af857cc

Commits on Sep 23, 2023

• Update to support newer rustc (Note: failing tests)

  dewert99

  committed
  55d3b8e

  Copy full SHA for 55d3b8e

Commits on Oct 7, 2023

• Switch to translation that follows design from thesis

  dewert99

  committed
  518c7ec

  Copy full SHA for 518c7ec

Commits on Oct 10, 2023

• Added more lints

  dewert99

  committed
  813d483

  Copy full SHA for 813d483

• Added missing test files

  dewert99

  committed
  d1d4620

  Copy full SHA for d1d4620

Commits on Oct 11, 2023

• Prevented using at_expiry with a state_set parameter in a logic function

  dewert99

  committed
  3a4e224

  Copy full SHA for 3a4e224

• Prevented using after_expiry with a state_set parameter in a logic function

  dewert99

  committed
  f78dfea

  Copy full SHA for f78dfea

• Fixed test

  dewert99

  committed
  09309f5

  Copy full SHA for 09309f5

• Added support for ghost functions

  dewert99

  committed
  7deef66

  Copy full SHA for 7deef66

Commits on Oct 13, 2023

• Fixed bug with implicit outlives constraints and added explicit constraints to logic functions

  dewert99

  committed
  b0d9367

  Copy full SHA for b0d9367

Commits on Oct 14, 2023

• Refactored out type for states

  dewert99

  committed
  20c0399

  Copy full SHA for 20c0399

Commits on Oct 15, 2023

• Refactor

  dewert99

  committed
  c5feeb8

  Copy full SHA for c5feeb8

Commits on Oct 16, 2023

• Switch to using more SSO types

  dewert99

  committed
  cf35a14

  Copy full SHA for cf35a14

• Added "Plain" (todo derive)

  dewert99

  committed
  5b303f0

  Copy full SHA for 5b303f0

• Merge branch 'master' into prusti

  Show description for 5f21aa8
  dewert99

  committed
  5f21aa8

  Copy full SHA for 5f21aa8

• fixed merge

  dewert99

  committed
  2acf68d

  Copy full SHA for 2acf68d

Commits on Oct 18, 2023

• Merge remote-tracking branch 'origin/master' into prusti

  dewert99

  committed
  4e1cef9

  Copy full SHA for 4e1cef9

Commits on Nov 1, 2023

• Removed old WithStatic feature

  dewert99

  committed
  fbc9e18

  Copy full SHA for fbc9e18

Commits on Nov 2, 2023

• Started refactor to avoid using rustc_infer, and allowed joining zombies

  dewert99

  committed
  711c57b

  Copy full SHA for 711c57b

Commits on Nov 9, 2023

• Continued the refactor to avoid using rustc_infer

  dewert99

  committed
  2235ec6

  Copy full SHA for 2235ec6

• Revert Cargo.toml IDE hack

  dewert99

  committed
  88f10ab

  Copy full SHA for 88f10ab

Commits on Jan 13, 2024

• Merge remote-tracking branch 'origin/master' into prusti

  Show description for d969deb
  dewert99

  committed
  d969deb

  Copy full SHA for d969deb

• Started trying to allow type parameters to be instantiated with Zombie

  dewert99

  committed
  373f9ef

  Copy full SHA for 373f9ef

Commits on Jan 15, 2024

• Added failing tests and stubs to prepare for SnapEq

  dewert99

  committed
  ee6afd8

  Copy full SHA for ee6afd8

Commits on Jan 18, 2024

• Improved handling for instantiating type param with zombie

  dewert99

  committed
  e4c60fe

  Copy full SHA for e4c60fe

• Added SnapEq handling

  dewert99

  committed
  fdd8e7d

  Copy full SHA for fdd8e7d

Commits on Jan 19, 2024

• Improved types produced by when converting to zombie

  dewert99

  committed
  16fa4fd

  Copy full SHA for 16fa4fd

Commits on Jan 24, 2024

• Clean-up and rename at_expiry->at

  dewert99

  committed
  7810615

  Copy full SHA for 7810615

Commits on Jan 25, 2024

• Renamed and improved handling of global states

  Show description for 9670325
  dewert99

  committed
  9670325

  Copy full SHA for 9670325

• Merge remote-tracking branch 'origin/master' into prusti

  Show description for 78e99e8
  dewert99

  committed
  78e99e8

  Copy full SHA for 78e99e8

• bless

  dewert99

  committed
  3e273cb

  Copy full SHA for 3e273cb

• Clean up

  dewert99

  committed
  d69fa0d

  Copy full SHA for d69fa0d

• Rustfmt and re-bless tests

  dewert99

  committed
  41bbc35

  Copy full SHA for 41bbc35

Commits on Jan 29, 2024

• Merge remote-tracking branch 'origin/master' into prusti

  Show description for 0355cc0
  dewert99

  committed
  0355cc0

  Copy full SHA for 0355cc0

Commits on Feb 7, 2024

• Merge remote-tracking branch 'origin/master' into prusti

  Show description for 732f8f8
  dewert99

  committed
  732f8f8

  Copy full SHA for 732f8f8

Commits on Feb 8, 2024

• Handle rustc update

  dewert99

  committed
  aa44a8a

  Copy full SHA for aa44a8a

Commits on Mar 14, 2024

• Merge remote-tracking branch 'origin/master' into prusti

  Show description for 471dc66
  dewert99

  committed
  471dc66

  Copy full SHA for 471dc66

Commits on Mar 15, 2024

• Handle rustc update

  dewert99

  committed
  573b92a

  Copy full SHA for 573b92a

• Merge remote-tracking branch 'origin/master' into prusti

  Show description for 14ef4fd
  dewert99

  committed
  14ef4fd

  Copy full SHA for 14ef4fd

Commits on Mar 20, 2024

• Merge branch 'creusot-rs:master' into prusti

  dewert99

  authored
  8a15dfc

  Copy full SHA for 8a15dfc

Commits on May 24, 2024

• Merge tag 'refs/tags/v0.1' into prusti

  Show description for cf52904
  dewert99

  committed
  cf52904

  Copy full SHA for cf52904

• Handed rustc update

  dewert99

  committed
  93c696a

  Copy full SHA for 93c696a

• Fix tests

  dewert99

  committed
  d7cb970

  Copy full SHA for d7cb970

Commits on Jun 24, 2024

• Add description to creusot-contracts

  Show description for 6e9a7c7
  xldenis

  committed
  6e9a7c7

  Copy full SHA for 6e9a7c7

• Fix the mlcfg script

  Show description for e80700d
  

  arnaudgolfouse

  authored and

  xldenis

  committed
  e80700d

  Copy full SHA for e80700d

• upgrade why3 and cleanup the session for the red_black_tree test

  Show description for 390a1be
  

  Armael

  authored and

  xldenis

  committed
  390a1be

  Copy full SHA for 390a1be

• Fix metadata load path

  Show description for 92bb6a4
  xldenis

  committed
  92bb6a4

  Copy full SHA for 92bb6a4

Commits on Jun 25, 2024

• Bump versions

  

  Xavier Denis

  authored and

  xldenis

  committed
  277c9cb

  Copy full SHA for 277c9cb

• It is better to use the repository field in Cargo.toml

  Show description for 428b5ec
  

  szabgab

  authored and

  xldenis

  committed
  428b5ec

  Copy full SHA for 428b5ec

Commits on Jul 13, 2024

• Merge tag 'refs/tags/v0.1.1' into prusti

  dewert99

  committed
  d30d5f9

  Copy full SHA for d30d5f9

Commits on Sep 7, 2024

• Merge tag 'v0.2.0' into prusti

  Show description for 1e7bfd9
  dewert99

  committed
  1e7bfd9

  Copy full SHA for 1e7bfd9

• Handle rustc update

  dewert99

  committed
  9fb4bac

  Copy full SHA for 9fb4bac