Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Dm/traceconstraints #428

Merged
merged 8 commits into from
Aug 12, 2024
Merged

Dm/traceconstraints #428

merged 8 commits into from
Aug 12, 2024

Conversation

danmatichuk
Copy link
Collaborator

@danmatichuk danmatichuk commented Aug 5, 2024

support additional constraints when generating traces

  • add --add-trace-constraints flag that allows for generating additional traces with constraints for the final equivalence conditions
    • Defines a trace constraint datatype in Pate.TraceConstraint that is simply: expression, comparison, constant
  • add alternative what4 serializer that uses expression identifiers (based on what4 hashes/nonces) in lieu of serialized expressions
  • add deserialization infrastructure for expressions-containing types, using the expression environment from the identifier-based serializer

provides an additional interface for serializing expression-containing
types using abstract identifiers, producing a binding environment that
can be used during deserialization
* takes an ordered list of lists of triples: var-op-const
* identifiers are now somewhat more stable, as they
  are computed as an offset from some initial hash
* don't include trace footprints in tracetree by default
  - these are part of the toplevel output currently
  - can still be inspected via the "debug" tag
* support "negated" comparison ops (i.e. GE, GT, NEQ)
@danmatichuk danmatichuk marked this pull request as ready for review August 12, 2024 16:10
@danmatichuk danmatichuk merged commit 6ae487e into master Aug 12, 2024
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant