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

Protect top-level nullary axioms #1645

Merged
merged 65 commits into from
Feb 8, 2019
Merged

Protect top-level nullary axioms #1645

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
65 commits
Select commit Hold shift + click to select a range
f6354d6
wip
nikswamy Jan 29, 2019
7067c48
merging in context profiles
nikswamy Jan 29, 2019
e87ba63
thunking top-level nullary functions
nikswamy Jan 29, 2019
b4ceb9d
snap
nikswamy Jan 29, 2019
c3e8649
fixing a flaky proof in FStar.Math.Lemmas
nikswamy Jan 29, 2019
ac9a7b0
fixing a flaky nl arith proof in LowStar.BufferView
nikswamy Jan 29, 2019
842a19e
need to explicitly prove the equality of refinements with trefl
nikswamy Jan 30, 2019
1a8ace5
a more reliable test for squashed types in the SMT encoding on post u…
nikswamy Jan 30, 2019
03d80d9
temporarily disable benton examples from test suite
nikswamy Jan 30, 2019
26315d5
temporarily disable array.pos from test suite
nikswamy Jan 30, 2019
2f4c8b2
hints and snap
nikswamy Jan 30, 2019
be037d6
permissions
nikswamy Jan 30, 2019
a8f6dc8
refactoring fv to turn thunking to an even lower level
nikswamy Jan 30, 2019
e3cfb59
forcing thunk just before printing to SMT
nikswamy Jan 30, 2019
6f7d073
snap
nikswamy Jan 30, 2019
cb35ce4
Revert "need to explicitly prove the equality of refinements with trefl"
nikswamy Jan 30, 2019
b345388
Revert "temporarily disable array.pos from test suite"
nikswamy Jan 30, 2019
b18c9e3
Revert "temporarily disable benton examples from test suite"
nikswamy Jan 30, 2019
1913e5e
Merge remote-tracking branch 'origin/master' into _nik_thunk_top_leve…
nikswamy Jan 30, 2019
66f8679
spelling out a proof in Benton2004 (with @tahina-pro)
nikswamy Jan 31, 2019
0cff08e
a new option --protect_top_level_axioms to toggle the thunking of nul…
nikswamy Jan 31, 2019
d5098ba
snap
nikswamy Jan 31, 2019
6c3d93b
perm
nikswamy Jan 31, 2019
b2be6a1
explicitly squashing a top-level nullary term to make itambient
nikswamy Jan 31, 2019
126eca2
enabling the new --protect_top_level_axioms flag for all F* tasks, wi…
nikswamy Jan 31, 2019
bc2b979
merging in nik_double_z3
nikswamy Jan 31, 2019
7ca1d13
snap
nikswamy Feb 1, 2019
049c5fc
also thunk equations of nullary symbols
nikswamy Feb 1, 2019
4094722
snap
nikswamy Feb 1, 2019
270e65a
intro_ambient explicitly used in LowStar.Monotonic.Buffer
nikswamy Feb 1, 2019
2855063
tweak
nikswamy Feb 1, 2019
6d6fbff
merging master in
nikswamy Feb 4, 2019
3b85752
snap
nikswamy Feb 4, 2019
4294b99
adjusting some flaky proofs
nikswamy Feb 4, 2019
ade4eed
triggering nullary guarded assumptions with an explicit intro_ambient
nikswamy Feb 5, 2019
cd37767
snap
nikswamy Feb 5, 2019
679d0cf
introducing a top-level `ambient` trigger for nullary terms
nikswamy Feb 5, 2019
0bcdfd2
increase rlimit for FStar.UInt128
nikswamy Feb 5, 2019
ffaf544
allow suppressing SMT verification failures into warnings; disable pr…
nikswamy Feb 5, 2019
b45e8c1
disable seplogic examples
nikswamy Feb 5, 2019
b5c3808
enable protect_top_level_axioms again
nikswamy Feb 5, 2019
533b691
setting a soft timeout to prevent cancelled builds
nikswamy Feb 5, 2019
1af5a88
disable warn_error +19
nikswamy Feb 5, 2019
b32b796
disable csl; retry without hard timeout
nikswamy Feb 5, 2019
b94f5d6
10 min z3 timeout
nikswamy Feb 6, 2019
38a6622
brittle proof in preorders/Protocol
nikswamy Feb 6, 2019
4a0ad6a
remove special treatment of MiniParse.Impl.Int
nikswamy Feb 6, 2019
38d8fab
Merge remote-tracking branch 'origin/master' into nik_thunk_top_level…
nikswamy Feb 6, 2019
3152050
restore csl to examples
nikswamy Feb 6, 2019
4fff0a9
trying to stabilize Protocol.fst
nikswamy Feb 6, 2019
e462974
restore most of seplogic, but disable SL.Examples.fst
nikswamy Feb 6, 2019
095a3e3
Merge remote-tracking branch 'origin/master' into nik_thunk_top_level…
nikswamy Feb 6, 2019
cc89869
[CI] regenerate hints + ocaml snapshot
Feb 6, 2019
495a73e
remove double include of fstar.mk
nikswamy Feb 6, 2019
3d0b1aa
forbid cache hits except when running a fresh query (i.e., when using…
nikswamy Feb 6, 2019
7fecc60
hints and snap
nikswamy Feb 6, 2019
6e81856
turn protect_top_level_axioms on by default
nikswamy Feb 6, 2019
b384e43
[CI] regenerate hints + ocaml snapshot
Feb 6, 2019
0f09306
Merge commit 'b384e43bee6506927a17593d8e556496f266f500' into nik_thun…
Feb 6, 2019
f710f04
Revert "turn protect_top_level_axioms on by default"
nikswamy Feb 6, 2019
5d61a61
merge upstream
nikswamy Feb 6, 2019
e78f6a2
merging master in
nikswamy Feb 8, 2019
829c3d0
snap
nikswamy Feb 8, 2019
e1c4c9b
some cleanup for PR 1645
nikswamy Feb 8, 2019
a6684d0
snap
nikswamy Feb 8, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
3 changes: 3 additions & 0 deletions CHANGES.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -89,6 +89,9 @@ Guidelines for the changelog:
we only found a couple of instances of this. So, for now, we are going with the
hoisting workaround.

* The encoding of nullary constants changed. See the documentation
in https://github.com/FStarLang/FStar/pull/1645

## Calculational proofs

* F\* now supports proofs in calculational style, i.e. where an
Expand Down
4 changes: 2 additions & 2 deletions doc/tutorial/code/exercises/Ex01a.fst.hints
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@
"projection_inverse_FStar.Pervasives.V_v"
],
0,
"20ca5f4cc25ea9cd59d5bdda58aa55f8"
"3d9859b0aba8f54756ef51d9298cc4e7"
],
[
"Ex01a.checkedRead",
Expand All @@ -27,7 +27,7 @@
1,
[ "@query", "projection_inverse_BoxBool_proj_0" ],
0,
"e2fdf12465a1e6dfefc1f6a0c2cea903"
"aae5fb4b95e175d2f4b48cbe420b08b5"
]
]
]
4 changes: 2 additions & 2 deletions doc/tutorial/code/exercises/Ex03a.fst.hints
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@
"well-founded-ordering-on-nat"
],
0,
"d14e2bfc1216a3a71ca6b99ded166595"
"7ea07a9c2a6bd4228933182cf6a656db"
],
[
"Ex03a.factorial",
Expand All @@ -31,7 +31,7 @@
"well-founded-ordering-on-nat"
],
0,
"1ffda84295714712458ce7b8eeaede08"
"d9b6ef96085883433069a1721045fd5e"
]
]
]
4 changes: 2 additions & 2 deletions doc/tutorial/code/exercises/Ex03b.fst.hints
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@
"well-founded-ordering-on-nat"
],
0,
"20a54bf2ab3d0ea5c49059d746218fde"
"b5b249c5241e3c23d0fb938ac4ba21a8"
],
[
"Ex03b.fibonacci",
Expand All @@ -31,7 +31,7 @@
"well-founded-ordering-on-nat"
],
0,
"6281613df44af7de3400823b783e7f79"
"e15457c89cbf0ac27de3861e4c9a61c6"
]
]
]
4 changes: 2 additions & 2 deletions doc/tutorial/code/exercises/Ex03c.fst.hints
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@
"well-founded-ordering-on-nat"
],
0,
"d34d7591f8b6712187541ccbe8783c9e"
"572cbdb4d34d622d0772a5ec1301203f"
],
[
"Ex03c.fibonacci",
Expand All @@ -35,7 +35,7 @@
"well-founded-ordering-on-nat"
],
0,
"eeb748f467b2dc971f5113f1517c6bfe"
"15d300876ef3d2b140fd70e76cf59cc8"
]
]
]
8 changes: 4 additions & 4 deletions doc/tutorial/code/exercises/Ex04a.fst.hints
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@
"subterm_ordering_Prims.Cons"
],
0,
"336c6ff04a35bcba6303945143d7b67d"
"ff097d8394e42809856bb32c233827d1"
],
[
"Ex04a.append",
Expand All @@ -30,7 +30,7 @@
"fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
],
0,
"7761b28d05065c0d5fbbb964064056cc"
"e93b003830a13c263bbf7a6010fbc778"
],
[
"Ex04a.length",
Expand All @@ -47,7 +47,7 @@
"subterm_ordering_Prims.Cons"
],
0,
"fbbcea7afb92a0ba13ef04f155d61d8f"
"37c7646acdf917d49616392202531230"
],
[
"Ex04a.append",
Expand All @@ -61,7 +61,7 @@
"fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
],
0,
"1af9b64027d6619e4095c97ef47834c0"
"fd4f44962b752fe9910536a84cb3352c"
]
]
]
8 changes: 4 additions & 4 deletions doc/tutorial/code/exercises/Ex04b.fst.hints
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@
"subterm_ordering_Prims.Cons"
],
0,
"cf01619030eb6fb6acba47acbb4d319a"
"1aea5b84c103bce4bed627122efd538e"
],
[
"Ex04b.append",
Expand All @@ -31,7 +31,7 @@
"projection_inverse_Prims.Cons_tl", "subterm_ordering_Prims.Cons"
],
0,
"3d48da192254f76ec5736d2ebeed3c67"
"c13ae9c90fd3cdc347f99bd05c6a1db5"
],
[
"Ex04b.length",
Expand All @@ -48,7 +48,7 @@
"subterm_ordering_Prims.Cons"
],
0,
"114baddf6dba4a05e0179c2e4d8b2a27"
"58f4cdae94ae9b6c77c872a4732d41f3"
],
[
"Ex04b.append",
Expand All @@ -62,7 +62,7 @@
"fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
],
0,
"891ebc1d079ec9b0f477b9c1ea4a8e5f"
"e51fe1e1f1c183265bb6f35be834d312"
]
]
]
8 changes: 4 additions & 4 deletions doc/tutorial/code/exercises/Ex04c.fst.hints
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@
"fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
],
0,
"2d353b19428615bec90330b74cb9c0c1"
"21fdbcccecfb9bdb29c656de138052e0"
],
[
"Ex04c.mem",
Expand All @@ -28,7 +28,7 @@
"fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
],
0,
"b56770fa12d59c7b8905fd4e55e9b004"
"054a8f4cfd3f2d3b25f72f137843aafd"
],
[
"Ex04c.append",
Expand All @@ -42,7 +42,7 @@
"fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
],
0,
"b7864436e6e766b10d47911bee30a457"
"4aab2243bf89f54e223f1f61e03b44ba"
],
[
"Ex04c.mem",
Expand All @@ -57,7 +57,7 @@
"fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
],
0,
"ecd33b1b33f66ce841b41912a3b26207"
"fc3c8372e568c99a2986e219f852db1b"
]
]
]
12 changes: 6 additions & 6 deletions doc/tutorial/code/exercises/Ex04e.fst.hints
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@
1,
[ "@query" ],
0,
"d9b427f279d450f93100fe50f8627a63"
"beee3122ba71ad7d9b397ef8334e7848"
],
[
"Ex04e.__proj__Some__item__v",
Expand All @@ -21,7 +21,7 @@
"refinement_interpretation_Ex04e_Tm_refine_5940fa0a1398f97ef02a98908357b71e"
],
0,
"42244429b7878d922947acf7ce4e1499"
"03939f3798f545d2c52308d7de1c6aab"
],
[
"Ex04e.find",
Expand All @@ -35,7 +35,7 @@
"fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
],
0,
"3507eb0ddcb192e26218a7ca7a8f2de0"
"53c81725d78ce370e40f16b74c404e0a"
],
[
"Ex04e.option",
Expand All @@ -44,7 +44,7 @@
1,
[ "@query" ],
0,
"a5902c42ba56ae6cdf94457bb69c4129"
"2d7393453a20ec825644a06198e1a35a"
],
[
"Ex04e.__proj__Some__item__v",
Expand All @@ -57,7 +57,7 @@
"refinement_interpretation_Ex04e_Tm_refine_5940fa0a1398f97ef02a98908357b71e"
],
0,
"c73dbcc4582e364b2c2974d67daa1ff1"
"c8ad11dbe08d4528b2f0bb795682dffc"
],
[
"Ex04e.find",
Expand All @@ -71,7 +71,7 @@
"fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
],
0,
"dc41e521e02fa0137d95329eb7fbe0c4"
"1cf7c4cd1988af44bf26a23a7cfa0243"
]
]
]
8 changes: 4 additions & 4 deletions doc/tutorial/code/exercises/Ex04f.fst.hints
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@
"projection_inverse_Prims.Cons_tl", "subterm_ordering_Prims.Cons"
],
0,
"726988d21fcd4f36ff4e87fc6782c790"
"8f8b16b05fe4024744fbc1bdd71a74f8"
],
[
"Ex04f.reverse",
Expand All @@ -29,7 +29,7 @@
"projection_inverse_Prims.Cons_tl", "subterm_ordering_Prims.Cons"
],
0,
"97da9420ee08246672626f18f300ae82"
"126fff165a3ad714764a3c8746bb7b63"
],
[
"Ex04f.append",
Expand All @@ -43,7 +43,7 @@
"fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
],
0,
"ddefc1ea0ddc7625cf1c71c407bd9e6b"
"5b2ccc32a1d5c86fa1bd382297552f34"
],
[
"Ex04f.reverse",
Expand All @@ -57,7 +57,7 @@
"fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
],
0,
"821ab704c704997749c35870fc251c16"
"685491b0e783e6e36b79a18e39feb5b1"
]
]
]
14 changes: 7 additions & 7 deletions doc/tutorial/code/exercises/Ex05a.fst.hints
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@
"fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
],
0,
"6b9262372eb3e636b4d0cb6396eed56b"
"90cffeea766a105ed82ca4f7dffa74fc"
],
[
"Ex05a.reverse",
Expand All @@ -27,7 +27,7 @@
"fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
],
0,
"67f6ee27bc0dc717483f28af4afe5033"
"064ae6d7b46262d86249593c3c5d0660"
],
[
"Ex05a.rev",
Expand All @@ -42,7 +42,7 @@
"subterm_ordering_Prims.Cons"
],
0,
"af29a57d7a7ee07fd428c2fbe1d94d53"
"d394db278d83c26f79a16e435796c0a4"
],
[
"Ex05a.append_assoc",
Expand All @@ -67,7 +67,7 @@
"subterm_ordering_Prims.Cons", "typing_Ex05a.append"
],
0,
"7de041ac85d0960c3a9beb2dbb7b1746"
"412d0b9100d057d10024d7ff35f4a585"
],
[
"Ex05a.append",
Expand All @@ -81,7 +81,7 @@
"fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
],
0,
"9967203601e2b0e6b7ad3f9e107f2174"
"8149301dcc4625e0aaafabc976882196"
],
[
"Ex05a.reverse",
Expand All @@ -95,7 +95,7 @@
"fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
],
0,
"899b2ca06d81faec2890ca253a44c598"
"d05e51a2eea94d2565731fe5cfc66367"
],
[
"Ex05a.rev",
Expand All @@ -110,7 +110,7 @@
"subterm_ordering_Prims.Cons"
],
0,
"327dec40075de9e5e8e0b4067d5b4f45"
"7acd14bea3069404b1c6eb5897521bb1"
]
]
]
Loading