Code

SMT context pruning#3440

Code

Merged

nikswamy merged 78 commits intomasterFStarLang/FStar:masterfrom nik_context_pruningFStarLang/FStar:nik_context_pruningCopy head branch name to clipboardSep 5, 2024

+5,447-2,081

Commits

Commits on Aug 16, 2024

• --ext profile_context, for information about which modules are used in an SMT query, relative to what is explicitly opened

  nikswamy

  committed
  15b6b58

  Copy full SHA for 15b6b58

Commits on Aug 19, 2024

• some basic components for context pruning

  nikswamy

  committed
  ab508d2

  Copy full SHA for ab508d2

Commits on Aug 21, 2024

• checkpoint; before adding dependence tracking of hashed symbols in SMT encoding

  nikswamy

  committed
  0fd5b46

  Copy full SHA for 0fd5b46

Commits on Aug 22, 2024

• --ext context_pruning works on most of ulib

  nikswamy

  committed
  7c3942d

  Copy full SHA for 7c3942d

Commits on Aug 25, 2024

• revising solver state, work in progress

  nikswamy

  committed
  d960422

  Copy full SHA for d960422

• snapshot

  nikswamy

  committed
  05825b6

  Copy full SHA for 05825b6

• restoring support for unsat cores

  nikswamy

  committed
  ba25548

  Copy full SHA for ba25548

Commits on Aug 26, 2024

• fixing hint recovery

  nikswamy

  committed
  9778e60

  Copy full SHA for 9778e60

• simpler treatement of SolverState.reset; prepping for using_facts_from

  nikswamy

  committed
  94d260f

  Copy full SHA for 94d260f

• supporting using_facts_from

  nikswamy

  committed
  546515d

  Copy full SHA for 546515d

• remove support for pending lemmas in Env

  nikswamy

  committed
  c384953

  Copy full SHA for c384953

• merging master in

  nikswamy

  committed
  e77870c

  Copy full SHA for e77870c

• snapshot

  nikswamy

  committed
  e042dd8

  Copy full SHA for e042dd8

• bump rlimit on a ModifiesGen proof

  nikswamy

  committed
  3bec9c8

  Copy full SHA for 3bec9c8

Commits on Aug 27, 2024

• preserve missing pushes

  nikswamy

  committed
  0d77e13

  Copy full SHA for 0d77e13

• revise the placement of push in the solver state

  nikswamy

  committed
  65a49e2

  Copy full SHA for 65a49e2

• removing some redundant state

  nikswamy

  committed
  71832aa

  Copy full SHA for 71832aa

• try disabling pruning state

  nikswamy

  committed
  31cd977

  Copy full SHA for 31cd977

• remove assumptions list in pruning state, unnecessary

  nikswamy

  committed
  fb26e5e

  Copy full SHA for fb26e5e

Commits on Aug 28, 2024

• pruning works on most of ulib

  nikswamy

  committed
  1c37ce5

  Copy full SHA for 1c37ce5

• snap

  nikswamy

  committed
  b308369

  Copy full SHA for b308369

• tighten pruning rules for l_quant_interp; fix a couple of proofs in ulib to with with context_pruning

  nikswamy

  committed
  6781db7

  Copy full SHA for 6781db7

• fix snapshot/rollback in SolverState for use from interactive mode; allow using_facts_from and pruning to compose

  nikswamy

  committed
  f8ba0f6

  Copy full SHA for f8ba0f6

Commits on Aug 29, 2024

• support z3refresh

  nikswamy

  committed
  7495aef

  Copy full SHA for 7495aef

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

  nikswamy

  committed
  b762a32

  Copy full SHA for b762a32

• context_pruning disables hints

  nikswamy

  committed
  381d578

  Copy full SHA for 381d578

• enable context pruning in ulib

  nikswamy

  committed
  8ebf35c

  Copy full SHA for 8ebf35c

• some restarts to stabilize UInt128

  nikswamy

  committed
  314c7ff

  Copy full SHA for 314c7ff

• enable context pruning in tests

  nikswamy

  committed
  c75c69c

  Copy full SHA for c75c69c

• retain top-level "assume" facts in context pruning

  nikswamy

  committed
  346531b

  Copy full SHA for 346531b

• supporting top-level squash & assumption uniformly; adding a disregard_using_facts_from

  nikswamy

  committed
  4a4aa81

  Copy full SHA for 4a4aa81

• try tests/hacl with disabling using facts from

  nikswamy

  committed
  6087043

  Copy full SHA for 6087043

• stabilizing Sequence.Base with an rlimit bump and a restart; tweak RefNew with an int inhabitant

  nikswamy

  committed
  497b04d

  Copy full SHA for 497b04d

Commits on Aug 30, 2024

• be less permissive with adding assumptions and ambient squashes to the environment

  nikswamy

  committed
  fbff8e9

  Copy full SHA for fbff8e9

• adding ambient squash assumptions unconditionally to root set

  nikswamy

  committed
  817de71

  Copy full SHA for 817de71

• avoid quadratically many pruning state reconstructions

  nikswamy

  committed
  27b39b3

  Copy full SHA for 27b39b3

• stabilize a proof in FStar.Seq.Permutation

  nikswamy

  committed
  4ec41c1

  Copy full SHA for 4ec41c1

• stabilize UInt128 non-linear arith; disable context pruning in legacy/LowStar.ToFStarBuffer

  nikswamy

  committed
  c59af11

  Copy full SHA for c59af11

• remove debugging spew

  nikswamy

  committed
  c9ff187

  Copy full SHA for c9ff187

• merge master in and snap

  nikswamy

  committed
  ee41b2a

  Copy full SHA for ee41b2a

• restart for a flaky proof in FStar.Matrix

  nikswamy

  committed
  56ac4b1

  Copy full SHA for 56ac4b1

• restart for a proof in Lib.Vec.Lemmas

  nikswamy

  committed
  4955b35

  Copy full SHA for 4955b35

• comments in SolverState.fsti

  nikswamy

  committed
  00e5af6

  Copy full SHA for 00e5af6

• snapshot

  nikswamy

  committed
  7d1c650

  Copy full SHA for 7d1c650

• Working around a quirk in the SMT Encoding with normalizes squash p, when p has a top-level constructor that is a formula or ==

  nikswamy

  committed
  1d727d0

  Copy full SHA for 1d727d0

• disable context_pruning for an example that relies on some non-standard unfolding behavior

  nikswamy

  committed
  1c67d6d

  Copy full SHA for 1c67d6d

• enable context_pruning for examples

  nikswamy

  committed
  0aed09e

  Copy full SHA for 0aed09e

• Revert "Working around a quirk in the SMT Encoding with normalizes squash p, when p has a top-level constructor that is a formula or =="

  Show description for 507ef63
  nikswamy

  committed
  507ef63

  Copy full SHA for 507ef63

• fix ambient assumption pruning to work both on squash and any top-level refinement; workarounds reverted

  nikswamy

  committed
  d8f4c10

  Copy full SHA for d8f4c10

Commits on Aug 31, 2024

• silly bug; fix ordering of patterns

  nikswamy

  committed
  8ecb00b

  Copy full SHA for 8ecb00b

• merge in master, bump checked file version number

  nikswamy

  committed
  27f77ad

  Copy full SHA for 27f77ad

• tweak FStar.Buffer

  nikswamy

  committed
  87e7b5d

  Copy full SHA for 87e7b5d

• handle retain assumptions when combining using_facts_from with context_pruning; retaing Prims.cache_version_number as a proof of inhabitation of int

  nikswamy

  committed
  699681f

  Copy full SHA for 699681f

• respect using_facts_from in tests/hacl; add a z3refresh to stabilize proofs in Lib.Vec.Lemmas and Lib.Sequence

  nikswamy

  committed
  45d9fc0

  Copy full SHA for 45d9fc0

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

  nikswamy

  committed
  e086779

  Copy full SHA for e086779

Commits on Sep 3, 2024

• snap

  nikswamy

  committed
  1f0d997

  Copy full SHA for 1f0d997

• nudge a known-flaky proof in AlgWP

  nikswamy

  committed
  de3837d

  Copy full SHA for de3837d

• some comments and clenup in SolverState.fst

  nikswamy

  committed
  3ed34df

  Copy full SHA for 3ed34df

• revert a couple of changes to examples

  nikswamy

  committed
  d682cab

  Copy full SHA for d682cab

• set context pruning in .fst.config.json files for use in vscode

  nikswamy

  committed
  8c81d8e

  Copy full SHA for 8c81d8e

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

  nikswamy

  committed
  70026f5

  Copy full SHA for 70026f5

• fix a comment and bug in SolverState---given_decls at a level does not include decls at prior levels:an exception is the top-most level for pruned query

  nikswamy

  committed
  635daa3

  Copy full SHA for 635daa3

• comments in FStar.SMTEncoding.Pruning.fsti

  nikswamy

  committed
  f924ec4

  Copy full SHA for f924ec4

• use rbset instead of list of triggers in Pruning; add comments

  nikswamy

  committed
  907d266

  Copy full SHA for 907d266

• silly typo, removed from the wrong map

  nikswamy

  committed
  7039e65

  Copy full SHA for 7039e65

Commits on Sep 4, 2024

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

  nikswamy

  committed
  5573de3

  Copy full SHA for 5573de3

• consolidate free names exclusion list in Pruning

  nikswamy

  committed
  a4f20c8

  Copy full SHA for a4f20c8

• one proof seems to take very long with context_pruning and is much faster with an unsat core, disabling context pruning for it for now

  nikswamy

  committed
  9a36d9e

  Copy full SHA for 9a36d9e

• and it goes through almost instantly with a restart-solver to reset the context

  nikswamy

  committed
  6195723

  Copy full SHA for 6195723

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

  nikswamy

  committed
  94d5b48

  Copy full SHA for 94d5b48

Commits on Sep 5, 2024

• merge master in & snap

  nikswamy

  committed
  a6a739e

  Copy full SHA for a6a739e

• remove support for hint_hook

  nikswamy

  committed
  cfca097

  Copy full SHA for cfca097

• snap

  nikswamy

  committed
  6d5ec04

  Copy full SHA for 6d5ec04

• remove an unused field in SMTEncoding.Env

  nikswamy

  committed
  963f1c3

  Copy full SHA for 963f1c3

• remove an unused file; remove some needless changes

  nikswamy

  committed
  0c581cd

  Copy full SHA for 0c581cd

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

  nikswamy

  committed
  fe954fc

  Copy full SHA for fe954fc

• merge master in and snapshot

  nikswamy

  committed
  1c74bcb

  Copy full SHA for 1c74bcb

• snap

  nikswamy

  committed
  84bce00

  Copy full SHA for 84bce00