Finish tulip basic resolve prophecy triples #548
jtassarottiAnnotations
15 errors and 5 warnings
|
build-vos (dev):
src/program_proof/tulip/invariance/linearize.v#L260
UNDEFINED EVARS:?X319==[Σ tulip_ghostG0 γ p ts tid future rds form Q m |- Union dbmap] (parameter Union of union) {?Union}
|
|
|
|
|
|
build-vos (dev):
src/program_proof/tulip/invariance/learn_commit.v#L23
UNDEFINED EVARS:?X67==[Σ tulip_ghostG0 γ p ts pwrs wrs histm |- tulip_ghostG ?Σ] (parameter tulip_ghostG0 of is_txn_committed) {?tulip_ghostG0}
|
|
build-vos (dev):
src/program_proof/tulip/invariance/learn_abort.v#L20
UNDEFINED EVARS:?X43==[Σ tulip_ghostG0 γ p ts keys |- tulip_ghostG ?Σ] (parameter tulip_ghostG0 of is_txn_aborted) {?tulip_ghostG0}
|
|
build (dev):
src/program_proof/tulip/invariance/preprepare.v#L6
In environment:
|
|
build (dev):
src/program_proof/tulip/invariance/prepare.v#L290
In environment:
|
|
build (dev):
src/program_proof/tulip/invariance/linearize.v#L260
UNDEFINED EVARS:?X47690==[Σ tulip_ghostG0 γ p ts tid future rds form Q m |- Union dbmap] (parameter Union of union) {?Union}
|
|
build (dev):
src/program_proof/tulip/invariance/learn_commit.v#L23
UNDEFINED EVARS:?X160==[Σ tulip_ghostG0 γ p ts pwrs wrs histm |- tulip_ghostG ?Σ] (parameter tulip_ghostG0 of is_txn_committed) {?tulip_ghostG0}
|
|
build (dev):
src/program_proof/tulip/invariance/learn_abort.v#L20
UNDEFINED EVARS:?X136==[Σ tulip_ghostG0 γ p ts keys |- tulip_ghostG ?Σ] (parameter tulip_ghostG0 of is_txn_aborted) {?tulip_ghostG0}
|
|
build (8.20):
src/program_proof/tulip/invariance/preprepare.v#L6
In environment:
|
|
build (8.20):
src/program_proof/tulip/invariance/prepare.v#L290
In environment:
|
|
build (8.20):
src/program_proof/tulip/invariance/linearize.v#L260
UNDEFINED EVARS:?X47769==[Σ tulip_ghostG0 γ p ts tid future rds form Q m |- Union dbmap] (parameter Union of union) {?Union}
|
|
build (8.20):
src/program_proof/tulip/invariance/learn_commit.v#L23
UNDEFINED EVARS:?X160==[Σ tulip_ghostG0 γ p ts pwrs wrs histm |- tulip_ghostG ?Σ@{γ:=γ; p:=p; ts:=ts; pwrs:=pwrs; wrs:=wrs; histm:=histm}] (parameter tulip_ghostG0 of is_txn_committed) {?tulip_ghostG0}
|
|
build (8.20):
src/program_proof/tulip/invariance/learn_abort.v#L20
UNDEFINED EVARS:?X136==[Σ tulip_ghostG0 γ p ts keys |- tulip_ghostG ?Σ@{γ:=γ; p:=p; ts:=ts; keys:=keys}] (parameter tulip_ghostG0 of is_txn_aborted) {?tulip_ghostG0}
|
|
python
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
|
check-goose
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
|
build-vos (dev)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
|
build (dev)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|
|
build (8.20)
ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636
|