VST on Iris#755

Draft

mansky1 wants to merge 573 commits intomasterfrom

This pull request is big! We're only showing the most recent 250 commits

Commits on Mar 21, 2024

Commits on Mar 24, 2024

more progress on 32-bit examples
mansky1
committed

Commits on Mar 25, 2024

most simple 32-bit examples work
mansky1
committed

Commits on Mar 26, 2024

basic tests passing?
mansky1
committed

Commits on Mar 27, 2024

ported sha proofs
mansky1
committed

Commits on Mar 30, 2024

Commits on Mar 31, 2024

Commits on Apr 2, 2024

proved some pred equivalences as equalities; should help performance
mansky1
committed

Commits on Apr 7, 2024

Commits on Apr 8, 2024

Commits on Apr 11, 2024

fixes for newer Iris version
mansky1
committed

Commits on Apr 17, 2024

compat.v needs to be listed in FLOYD_FILES, otherwise compat.vo does not get installed
andrew-appel
committed

Commits on Apr 18, 2024

Adjust compatibility mode to support oracle polymorphism; see PORTING.md for more info
andrew-appel
committed

Commits on Apr 19, 2024

Commits on Apr 22, 2024

Commits on May 7, 2024

Commits on May 9, 2024

Judiciously suppress some warning messages
andrew-appel
committed

Commits on May 11, 2024

Commits on May 12, 2024

fix DrySafe proofs
mansky1
committed

Commits on May 13, 2024

Update ora submodule; carefully suppress warnings; fix a couple of broken proofs.
andrew-appel
committed

Commits on May 14, 2024

Commits on May 19, 2024

a bit more progress on lithium instance
mansky1
committed

Commits on May 21, 2024

progress on int ops
mansky1
committed

Commits on May 22, 2024

proved typing rules for int ops
mansky1
committed

Commits on Jun 5, 2024

Update ivst.md
mansky1
authored

Commits on Jun 18, 2024

Commits on Jun 19, 2024

Commits on Jun 23, 2024

initial work for atomic_bool
ducthann
committed

Commits on Jun 24, 2024

Commits on Jun 25, 2024

Commits on Jun 27, 2024

finished immovable.v
ducthann
committed

Commits on Jun 28, 2024

started on function type
mansky1
committed

Commits on Jul 7, 2024

Commits on Jul 9, 2024

more wp
mansky1
committed

Commits on Jul 12, 2024

add simpl_classes.v
mansky1
committed

Commits on Jul 13, 2024

Commits on Jul 18, 2024

Commits on Jul 23, 2024

Commits on Jul 24, 2024

Commits on Jul 26, 2024

finished porting globals.v
ducthann
committed

Commits on Jul 29, 2024

first attempt at stating adequacy
mansky1
committed

Commits on Jul 30, 2024

type_assgin mostly works

rinshankaihou
authored and
Ke Du
committed
wip interpreter.v

rinshankaihou
authored and
Ke Du
committed
interpreter.v works

madoka
authored and
Ke Du
committed
add typing/automation.v (wip)

madoka
authored and
Ke Du
committed
port proof_state.v for automation.v; still need to fix location_info
Ke Du
committed
make programs.v compile
Ke Du
committed
refactor lithium to have similar structure to RefinedC repo
Ke Du
committed
Merge pull request #784 from rinshankaihou/rvst
mansky1
authored

Commits on Jul 31, 2024

Commits on Aug 6, 2024

Commits on Aug 8, 2024

Commits on Aug 12, 2024

Commits on Aug 15, 2024

maybe-working sketch of adequacy for typed_function
mansky1
committed

Commits on Aug 19, 2024

trying to state typing rule for call
mansky1
committed

Commits on Aug 20, 2024

mostly-correct function type and call rule
mansky1
committed

Commits on Aug 21, 2024

made type_write_simple
Ke Du
committed
add type_set example
Ke Du
committed
Merge pull request #790 from rinshankaihou/rVST
mansky1
authored
tweaking type_set
mansky1
committed

Commits on Aug 22, 2024

add lithium support for goals like \box P \vdash <affine> P \star Q
Ke Du
committed

Commits on Aug 26, 2024

updating concurrent soundness infrastructure
mansky1
committed

Commits on Aug 29, 2024

Merge pull request #791 from rinshankaihou/rVST
mansky1
authored

Commits on Sep 16, 2024

outlined function call typing proof
mansky1
committed

Commits on Sep 18, 2024

add support for normalizing embed
Ke Du
committed
merge

rinshankaihou
authored and
Ke Du
committed
clean up code

rinshankaihou
authored and
Ke Du
committed
add typing rule for Evar

rinshankaihou
authored and
Ke Du
committed
fix type_write

rinshankaihou
authored and
Ke Du
committed
merge
Ke Du
committed
fix Sassgin example statement
Ke Du
committed
small fix
Ke Du
committed
tweaking function type
mansky1
committed
Merge pull request #796 from rinshankaihou/rVST
mansky1
authored
merge
mansky1
committed

Commits on Sep 23, 2024

fixed temps and lvars in typed_function
mansky1
committed

Commits on Oct 1, 2024

adding malloc_token share axioms
mansky1
committed
fix Sassign example

Ke Du
authored and
rinshankaihou
committed
add function example

Ke Du
authored and
rinshankaihou
committed
stuck on wp_return_some

Ke Du
authored and
rinshankaihou
committed
progress on funciton
rinshankaihou
committed
update example proof
rinshankaihou
committed
fix automation
rinshankaihou
committed
add frontend folder
rinshankaihou
committed
fix automation
rinshankaihou
committed
add frontend
rinshankaihou
committed
add prototype of frontend
rinshankaihou
committed
add clean command for refinedVST frontend examples in Makefile
rinshankaihou
committed

Commits on Oct 2, 2024

Merge pull request #797 from rinshankaihou/rVST
mansky1
authored

Commits on Oct 4, 2024

finished jsafe_perm_equiv lemma
ducthann
authored

Commits on Oct 31, 2024

Commits on Nov 1, 2024

Commits on Nov 5, 2024

started moving refinedVST to working core wp
mansky1
committed

Commits on Nov 19, 2024

fix type annotations on atomic_spec_post'
mansky1
authored

Commits on Dec 8, 2024

updated CompCert version
mansky1
committed

Commits on Dec 9, 2024

Commits on Jan 15, 2025

Commits on Jan 16, 2025

Commits on Jan 17, 2025

Commits on Jan 20, 2025

Commits on Jan 21, 2025

Commits on Jan 22, 2025

ported most types
mansky1
committed

Commits on Jan 23, 2025

updated refinedVST automation
mansky1
committed

Commits on Feb 10, 2025

Commits on Feb 27, 2025

Commits on Mar 27, 2025

WIP on semax_to_dry_machine.v
ducthann
authored

Commits on Apr 25, 2025

Commits on May 17, 2025

consistent type annotations for atomic notations
mansky1
committed

Commits on Jun 16, 2025

remove ora submodule; should install coq-vst-ora via opam instead
mansky1
committed

Commits on Aug 11, 2025

Update README.md
mansky1
authored

Commits on Aug 25, 2025