Safety assert2 - #1170
Draft
lyonel2017 wants to merge 2 commits into
Draft
Conversation
lyonel2017
marked this pull request as draft
May 27, 2025 11:42
bgregoir
force-pushed
the
safety-assert2
branch
from
September 26, 2025 14:10
0c2384a to
4a1e756
Compare
bgregoir
force-pushed
the
safety-assert2
branch
from
November 15, 2025 07:39
824b2d0 to
ef25889
Compare
bgregoir
force-pushed
the
safety-assert2
branch
from
November 24, 2025 22:22
ef25889 to
b376ef8
Compare
Member
|
Why has the extraction for CT been changed in an incompatible way? |
bgregoir
force-pushed
the
safety-assert2
branch
3 times, most recently
from
December 12, 2025 07:00
e355928 to
12cc5a0
Compare
bgregoir
force-pushed
the
safety-assert2
branch
3 times, most recently
from
December 18, 2025 17:22
ed0ac68 to
06847d8
Compare
vbgl
force-pushed
the
safety-assert2
branch
2 times, most recently
from
January 21, 2026 05:42
c7c0da4 to
e0a472e
Compare
vbgl
force-pushed
the
safety-assert2
branch
3 times, most recently
from
January 27, 2026 15:19
425a075 to
47edd2c
Compare
vbgl
force-pushed
the
safety-assert2
branch
3 times, most recently
from
February 6, 2026 14:58
4855e17 to
8ae7062
Compare
vbgl
force-pushed
the
safety-assert2
branch
3 times, most recently
from
February 10, 2026 16:59
c1440d4 to
f55e78a
Compare
vbgl
force-pushed
the
safety-assert2
branch
2 times, most recently
from
February 17, 2026 14:24
0adec72 to
d23ace7
Compare
1 task
vbgl
force-pushed
the
safety-assert2
branch
5 times, most recently
from
March 4, 2026 10:59
857ec2e to
b6a8cee
Compare
Add Hoare rule for assert remove warning patch relational_logic, admit hoare_logic patch psem restore proofs proof of wint_word + remove_assert link remove_assert in compiler Add more proof for Hoare Logic Add ocaml part for bigop and assertions Add proof for hoare WIP Temp fix of a test Fix tests Fix tests extension for exprs, assertions extension for exprs, assertions (Ocaml) backward proof of wint_int (include safety), needs cleanup WIP safe semantics with catch finish wint_int_proof Take withcatch into account in relational_logic fix slh_lowering_proof safety_proof.v shared defs wint_int lemmas in safety_shared safety.v sc_op2 fix New EC model for safety and safety pass added to compiler safety proofs update moved lemma wint_int_proof safety_proof prog EC library proofs for safety lemmas all compile fix parser for tests do not split assert in two in wint_int remove admit in safety_proof.v Generating default function contracts fix Fix printer, add safety examples and wint_int spill fix EC Extraction fix encode some safety expressions using operators fix last merge remove axiom from safety_proof add extra tests in extra_vars_call to ensure freshness of introduced variables fix insert_copy_and_fix_length fix safety for get_global array add test fix constant-time check fix declassify fix printing use annotation for require and ensure fix printing of annotations improves printing of safety pre/post Safety Extraction to separate files and fix in leakage extraction fix syntax of safety test small cleanning in pretyping add option --output-proof to jasmin2ec remove assert false in linter fix VariableInitialisation remove assert false simplify parser use capitalize_ascii add tests for jasmin2ec --model safety remove assert false in latex printer remove assert false in latex printer small changes small cleanup restore proof remove partial-match in auto-spill SMT Exit Oarr_make automatically insert cast add proof of insert_cast Fix safety spec file import and safety eclib fix fix proof is_init - eclib eclib: simpler & more general JByte_array.init_arrP toEC: use init_arr fix typing in safety.v
…es = EXPR, ensures = EXPR }
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.