Verification fails, but succeeds with `--verify-function`

[jaylorch]

In the attached two .zip files generated by running with --record, the first run finds a verification failure in abort_after_failed_item_table_tentatively_write_item, namely a failure to satisfy a precondition of a lemma. But in the second run, using --verify-function abort_after_failed_item_table_tentatively_write_item, it reports "1 verified, 0 errors". 2024-09-18-11-56-53.zip 2024-09-18-11-58-15.zip

[jaylorch]

I've been informed that the --record didn't capture the important file libdeps_hack.rlib. Here's the release version: libdeps_hack.zip

And here's the debug version: libdeps_hack.zip

[jaylorch]

And here's the entirety of deps_hack/target/release: deps_hack_target_release.zip

[jaylorch]

Here are the SMT files generated: verify_function_kvdurabledurableimpl_v.smt2.zip verify_module_kvdurabledurableimpl_v.smt2.zip

[jaylorch]

If you want to build deps_hack yourself, you can use the kv_dev branch of https://github.com/microsoft/verified-storage

[yizhou7]

I am somewhat confused about the smt2 log output. For the module version of the query, line 58398--59621 seems to contain the query for abort_after_failed_item_table_tentatively_write_item.

;; Function-Def lib::kv::durable::durableimpl_v::DurableKvStore::abort_after_failed_item_table_tentatively_write_item
;; c:/Apps/verified-storage-windows/storage_node/src\kv\durable\durableimpl_v.rs:2500:9: 2504:10 (#0)

However, the corresponding check-sat at 59619 is not followed by get-model or more check-sat for debugging. In other words, that check-sat at 59619 seemed to have worked according to the smt2 log. I also ran Mariposa on that query and it turns out to be stable. Maybe I am misunderstanding something here?

[jaylorch]

Oh, I was apparently confused about where the errors were. Sorry about that!