Code

Leakage traces#431

Code

Open

OwenConoly wants to merge 91 commits intomit-plv:mastermit-plv/bedrock2:masterfrom OwenConoly:leakage_tracesOwenConoly/bedrock2:leakage_tracesCopy head branch name to clipboard

+7,636-1,178

Commits

Commits on Sep 30, 2024

• add LS.v

  OwenConoly

  committed
  23ef95f

• modify LS.v

  OwenConoly

  committed
  eb82e5e

• prettify MetricSemantics eval_expr

  OwenConoly

  committed
  c697ba1

• add MetricLeakageSemantics

  OwenConoly

  committed
  d921b46

• organize semantics-relation lemmas in MetricLeakageSemantics

  OwenConoly

  committed
  c2c9992

• remove unneeded direction of eval_expr equivalence

  OwenConoly

  committed
  309a4b6

• all the desired relations between semantics

  OwenConoly

  committed
  7ed12e9

• make build less noisy

  OwenConoly

  committed
  16cb728

• create LWP

  OwenConoly

  committed
  50f860c

• modify LeakageWeakestPrecondition.v

  OwenConoly

  committed
  29339e5

• add LWPP

  OwenConoly

  committed
  99d33fe

• modify LWPP.v

  OwenConoly

  committed
  a444868

• add LL.v

  OwenConoly

  committed
  61cb091

• edit LL.v

  OwenConoly

  committed
  b2002f6

• add LPL

  OwenConoly

  committed
  f2e3144

• first pass on editing LPL

  OwenConoly

  committed
  16fccea

• add kyber file. doesn't work, since straightline needs fixes

  OwenConoly

  committed
  8b30bfa

• make kyberslash work

  OwenConoly

  committed
  ba5b547

• remove garbage (Search commands, etc) from kyberslash proof

  OwenConoly

  committed
  13fba5a

• update FlatImp to use MetricLeakageSemantics

  OwenConoly

  committed
  c9c9c57

• add 'custom fixpoint' stuff. add comparison of Fix_eq and Fix_eq'.

  OwenConoly

  committed
  bdcc388

• add leakage function to DCEDef

  OwenConoly

  committed
  8db3172

• switch to using Fix instead of my_Fix.

  Show description for 6ab1564
  OwenConoly

  committed
  6ab1564

• switch to using Fix_eq' and get unstuck

  OwenConoly

  committed
  b0dbeb7

• start on DCE proof

  OwenConoly

  committed
  8b00511

• progress on DCE phase

  OwenConoly

  committed
  020ad0f

• add pick_sp stuff to DCE trace transformation function

  OwenConoly

  committed
  2838479

Commits on Oct 1, 2024

• finish updating DCE function

  OwenConoly

  committed
  b02a304

• had an idea about how to simplify function

  OwenConoly

  committed
  a486229

• DCE progress

  OwenConoly

  committed
  3a221fb

• up to loop case

  OwenConoly

  committed
  556d288

• get stuck in sequence (and while) case. IH is no good!

  Show description for 9fe2d00
  OwenConoly

  committed
  9fe2d00

Commits on Oct 2, 2024

• rewrite DCE function in CPS. need to decide how to prove fixpoint equation.

  OwenConoly

  committed
  d08e363

• new version of Fix with dependent types as well as arbitrary equivalence relations

  OwenConoly

  committed
  f5690fd

• all the variants of Fix_eq i could imagine wanting

  OwenConoly

  committed
  e142efe

Commits on Oct 26, 2024

• prove DCE leakage fixpoint equation

  OwenConoly

  committed
  24bcc75

• write DCE proof with leakage (it works now, since leakage function is in cps)

  OwenConoly

  committed
  ed7fa64

Commits on Oct 29, 2024

• start adapting spilling phase to leakage

  OwenConoly

  committed
  98f7015

• fix align_trace tactic and move it to LeakageSemantics

  OwenConoly

  committed
  2148f2c

• finish adapting spilling proof to leakage traces

  OwenConoly

  committed
  4de4f7e

• switch from mit-plv riscv-coq to my fork, and then to the leakage traces branch

  OwenConoly

  committed
  a9ad05f

• adapt FlattenExpr to leakage traces

  OwenConoly

  committed
  075038d

• add leakage traces to GoFlatToRiscv

  OwenConoly

  committed
  75ef583

• add leakage traces to ForeverSafe, RunInstruction

  OwenConoly

  committed
  877c92f

• add leakage to RiscvEventLoop

  Show description for 807f01c
  OwenConoly

  committed
  807f01c

• start on FlatToRiscvCommon

  OwenConoly

  committed
  5195e03

• add leakage transformation function for FlatToRiscv.

  Show description for 5c8665d
  OwenConoly

  committed
  5c8665d

Commits on Oct 30, 2024

• rewrite leakage functions in FlatToRiscvDef to return list LeakageEvent

  OwenConoly

  committed
  0b99a61

• add leakage traces to FlatToRiscvCommon

  OwenConoly

  committed
  376ec5a

• add leakage to FlatToRiscvLiterals

  OwenConoly

  committed
  8a01efb

• add leakage to load_save_regs_correct

  Show description for 10fd526
  OwenConoly

  committed
  10fd526

Commits on Nov 12, 2024

• start on Functions

  OwenConoly

  committed
  542434d

• finish compile_function_body_correct

  OwenConoly

  committed
  0682f92

• finish call case

  OwenConoly

  committed
  c5ed5ad

• up to stackalloc case...

  OwenConoly

  committed
  b50afb1

• up to while case

  OwenConoly

  committed
  55f4e95

• finish functions

  OwenConoly

  committed
  b75e11b

• leakage in UseImmediate

  OwenConoly

  committed
  5cbb5df

• leakage in regalloc

  OwenConoly

  committed
  5d18d3b

Commits on Nov 13, 2024

• add leakage to lower pipeline

  OwenConoly

  committed
  e4efffd

• some pipeline

  OwenConoly

  committed
  07dfe0e

• get to dce_correct in pipeline...

  OwenConoly

  committed
  5eff275

• composed_compiler_correct

  OwenConoly

  committed
  6235cd3

• compiler_correct

  OwenConoly

  committed
  2bc8edc

• memequal source level leakage prooof

  OwenConoly

  committed
  f2f175c

• hacky compiler_correct_wp

  OwenConoly

  committed
  4f8d83e

• MMIO compiler stuff

  OwenConoly

  committed
  5deac8a

• get to the point where I actually write the low-level spec of memequal

  OwenConoly

  committed
  01fdc8f

Commits on Nov 14, 2024

• prove memequal

  OwenConoly

  committed
  6652114

• make memequal basically axiom-free

  OwenConoly

  committed
  1cadb3d

Commits on Nov 15, 2024

• add ct.v

  OwenConoly

  committed
  6764d5f

Commits on Dec 17, 2024

• clean up most of pipeline.v

  OwenConoly

  committed
  23991bd

• get rid of WeakenCall in Pipeline; use func/prop ext instead

  OwenConoly

  committed
  dc436a3

• more cleaning up pipeline. up to spilling_correct

  OwenConoly

  committed
  a710ce7

• trying riscv_phase_correct

  OwenConoly

  committed
  76f2c60

Commits on Dec 19, 2024

• hooray Pipeline compiles now

  OwenConoly

  committed
  d99f342

• remove test_itauto (sam says it is not needed anymore)

  OwenConoly

  committed
  35556b3

• get rid of option_map lemmas

  OwenConoly

  committed
  4e8bb1d

• FE310 leakage comment

  Show description for 21d12fa
  

  OwenConoly

  and

  andres-erbsen

  committed
  21d12fa

• make some fixpoints local

  OwenConoly

  committed
  f49da82

• make ct.v use FE310CSemantics instead of BasicC32Semantics

  OwenConoly

  committed
  83a68f9

• revert BasicC32Semantics to have no leakage traces

  OwenConoly

  committed
  59c91fb

• start adapting examples using FE310 to work with leakage

  Show description for c1fbe27
  OwenConoly

  committed
  c1fbe27

• make leakage straightline work way better

  OwenConoly

  committed
  191b848

• fix straightline in a different way (still using letexists instead of eexists)

  OwenConoly

  committed
  dcc213f

Commits on Dec 20, 2024

• fixup leakage straightline.

  Show description for fbbf64f
  OwenConoly

  committed
  fbbf64f

• fnspec notations

  OwenConoly

  committed
  9250260

• leakage in LAN9250

  OwenConoly

  committed
  fbe8100

• add fnspec_ex! notations for specifying constant-time

  OwenConoly

  committed
  b606efd

• work on bedrock2Examples involving leakage (including using the

  Show description for d1295c2
  OwenConoly

  committed
  d1295c2

• make fnspec! exists notation more intuitive

  OwenConoly

  committed
  8b44f61