Skip to content

Actions: vellvm/vellvm

All workflows

Actions

Loading...

Showing runs from all workflows
809 workflow runs
809 workflow runs
Event

Filter by event

Status

Filter by status

Branch
Actor

Filter by actor

Some notes about admits in model_E1E2_L2_orutt_strict.
Nix build for vellvm #507: Commit c0510bc pushed by Chobbes
July 11, 2023 13:49 24s new-raise-ub
July 11, 2023 13:49 24s
Proof of read_byte_correct with the new raise_ub.
Nix build for vellvm #506: Commit cf53589 pushed by Chobbes
July 10, 2023 13:45 23s new-raise-ub
July 10, 2023 13:45 23s
changed uvalue to N in UVALUE_ExtractByte
Nix build for vellvm #505: Commit ae218c2 pushed by Zdancewic
July 8, 2023 13:39 24s model-proof-test-updated
July 8, 2023 13:39 24s
Checkpoint... Progress on proofs of exec ∈ spec for memory model with
Nix build for vellvm #504: Commit 1a5d556 pushed by Chobbes
July 7, 2023 21:14 21s new-raise-ub
July 7, 2023 21:14 21s
merge
Nix build for vellvm #503: Commit 80e3301 pushed by Zdancewic
July 6, 2023 17:40 23s model-proof-test-updated
July 6, 2023 17:40 23s
QED serialize_sbytes_fin_inf
Nix build for vellvm #502: Commit 5bb5de9 pushed by Zdancewic
July 6, 2023 15:53 24s model-proof-test-updated
July 6, 2023 15:53 24s
Add a mempush_always_succeeds lemma. Prove UB case for MemPush...
Nix build for vellvm #501: Commit 0e7e3d6 pushed by Chobbes
July 6, 2023 15:41 22s model-proof-test
July 6, 2023 15:41 22s
Finish UBE / DebugE admits.
Nix build for vellvm #500: Commit c7e92c4 pushed by Chobbes
July 5, 2023 23:48 26s model-proof-test
July 5, 2023 23:48 26s
Big progress with oruttF's Vis case in
Nix build for vellvm #499: Commit da22e7f pushed by Chobbes
July 5, 2023 19:53 23s model-proof-test
July 5, 2023 19:53 23s
Work on vis case of model_E1E2_L3_orutt_strict.
Nix build for vellvm #498: Commit e9486b3 pushed by Chobbes
July 5, 2023 14:02 24s model-proof-test
July 5, 2023 14:02 24s
More cases proved on model_E1E2_L3_orutt_strict. Everything is
Nix build for vellvm #496: Commit 4d664df pushed by Chobbes
July 4, 2023 14:58 22s model-proof-test
July 4, 2023 14:58 22s
Some work on the extra model_E1E2_L3_orutt_strict admits.
Nix build for vellvm #495: Commit fa3bf96 pushed by Chobbes
July 4, 2023 00:49 25s model-proof-test
July 4, 2023 00:49 25s
QED uvalue_refine_strict_has_dtyp
Nix build for vellvm #494: Commit eaa6232 pushed by Zdancewic
July 3, 2023 17:00 22s model-proof-test-updated
July 3, 2023 17:00 22s
Convert OOME / DebugE / UBE to using print_msg.
Nix build for vellvm #493: Commit b954bbd pushed by Chobbes
July 3, 2023 16:47 21s model-proof-test
July 3, 2023 16:47 21s
typo
Nix build for vellvm #492: Commit bd3a8d6 pushed by Zdancewic
July 3, 2023 14:16 28s model-proof-test-updated
July 3, 2023 14:16 28s
Messing with proofs.
Nix build for vellvm #490: Commit f8803b5 pushed by Chobbes
June 30, 2023 21:02 26s model-proof-test
June 30, 2023 21:02 26s
Moving lemmas around. Map monad lemmas.
Nix build for vellvm #489: Commit ed5949a pushed by Chobbes
June 30, 2023 20:57 23s model-proof-test
June 30, 2023 20:57 23s
get_consecutive_ptrs_never_fails lemma. raise_error proof for store.
Nix build for vellvm #488: Commit 7d441fa pushed by Chobbes
June 29, 2023 14:45 24s model-proof-test
June 29, 2023 14:45 24s
Finishe load error case in model_E1E2_L3_orutt_strict.
Nix build for vellvm #486: Commit ee14219 pushed by Chobbes
June 28, 2023 16:18 24s model-proof-test
June 28, 2023 16:18 24s
fix DynamicValues.v proofs
Nix build for vellvm #484: Commit de69464 pushed by Zdancewic
June 28, 2023 10:06 21s model-proof-test-updated
June 28, 2023 10:06 21s
ProTip! You can narrow down the results and go further in time using created:<2023-06-28 or the other filters available.