From 0c095c20b7825c036f7a2556c1c1ba631eca3a84 Mon Sep 17 00:00:00 2001 From: Owen Conoly Date: Fri, 10 Jan 2025 16:25:45 -0500 Subject: [PATCH] m --- compiler/src/compiler/Pipeline.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/compiler/src/compiler/Pipeline.v b/compiler/src/compiler/Pipeline.v index c890774d0..a725163b9 100644 --- a/compiler/src/compiler/Pipeline.v +++ b/compiler/src/compiler/Pipeline.v @@ -66,9 +66,9 @@ Section WithWordAndMem. Record Lang := { Program: Type; - Valid: Program -> Prop; - Leakage: Type; - Call(pick_sp: list Leakage -> word)(p: Program)(funcname: string) + Valid: Program -> Prop; + Leakage: Type; + Call(p: Program)(funcname: string)(pick_sp: list Leakage -> word) (k: list Leakage)(t: trace)(m: mem)(argvals: list word)(mc: MetricLog) (post: list Leakage -> trace -> mem -> list word -> MetricLog -> Prop): Prop; }.